From 79f08baa092ef8ee5bcda094e4eb102878d45a7d Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sun, 25 Oct 2026 00:42:40 +0000 Subject: [PATCH 1/2] refactor(Circuit): generalize FanIn input support bounds to weighted gate costs (#884) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Generalize Program.card_reachableInputs_le in Complexity.Computability.Circuit.FanIn to arbitrary per-operation weights w satisfying ∀ op, σ.Arity op ≤ 1 + w op, exposing Program.card_reachableInputs_le_cost and Program.card_biUnion_wireSupport_le_cost. Deduce Program.card_biUnion_wireSupport_le_cost_binaryCost in Complexity.Computability.Circuit.Boolean.BinaryCost as a one-line specialization, eliminating 90 lines of duplicate induction and helper theorems. Refs #884 (Item 7, F4) --- .../Circuit/Boolean/BinaryCost.lean | 95 +----------------- Complexity/Computability/Circuit/FanIn.lean | 98 ++++++++++++++----- 2 files changed, 77 insertions(+), 116 deletions(-) diff --git a/Complexity/Computability/Circuit/Boolean/BinaryCost.lean b/Complexity/Computability/Circuit/Boolean/BinaryCost.lean index 018483316b..103b93af47 100644 --- a/Complexity/Computability/Circuit/Boolean/BinaryCost.lean +++ b/Complexity/Computability/Circuit/Boolean/BinaryCost.lean @@ -7,6 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate +public import Complexity.Computability.Circuit.FanIn public import Complexity.Computability.Circuit.Simulation public import Complexity.Computability.Circuit.Support public import Cslib.Computability.Circuit.Boolean.Basic @@ -142,102 +143,12 @@ theorem Program.cost_binaryCost_le (p : Program Boolean.signature n g) : p.cost Boolean.binaryCost ≤ g := (p.cost_le_mul Boolean.binaryCost_le_one).trans_eq (one_mul g) -private theorem wire_castSucc_injective' : - Function.Injective (Wire.castSucc : Wire n g → Wire n (g + 1)) := by - intro a b h - cases a <;> cases b <;> simp_all [Wire.castSucc] - /-- In a De Morgan program, the number of inputs supporting a frontier of wires is at most the size of the frontier plus the number of binary (AND/OR) gates in the program. -/ theorem Program.card_biUnion_wireSupport_le_cost_binaryCost (p : Program signature n g) (frontier : Finset (Wire n g)) : - (frontier.biUnion p.wireSupport).card ≤ frontier.card + p.cost binaryCost := by - induction p with - | empty => - simp only [Program.cost_empty, Nat.add_zero] - have hsub : frontier.biUnion (Program.empty (σ := signature)).wireSupport ⊆ - Finset.univ.filter fun i : Fin n => Wire.input i ∈ frontier := by - intro i hi - rw [Finset.mem_biUnion] at hi - obtain ⟨w, hw, hi⟩ := hi - cases w with - | input j => - simp only [Program.wireSupport_input, Finset.mem_singleton] at hi - subst hi - exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, hw⟩ - | gate j => exact j.elim0 - refine (Finset.card_le_card hsub).trans ?_ - apply Finset.card_le_card_of_injOn Wire.input - · intro i hi - simpa using hi - · intro a _ b _ h - cases h - rfl - | @gate g p line ih => - let prior := Finset.univ.filter fun w : Wire n g => w.castSucc ∈ frontier - let lineInputs := Finset.univ.image line.wires - let opened := - if Wire.gate (Fin.last g) ∈ frontier then prior ∪ lineInputs else prior - have hsub : frontier.biUnion (p.gate line).wireSupport ⊆ opened.biUnion p.wireSupport := by - intro i hi - rw [Finset.mem_biUnion] at hi ⊢ - obtain ⟨w, hw, hi⟩ := hi - revert hw hi - induction w using Wire.lastCases with - | last => - intro hlast hi - rw [Program.wireSupport_gate_last] at hi - obtain ⟨arg, hi⟩ := Line.mem_inputSupport.mp hi - exact ⟨line.wires arg, by simp [opened, lineInputs, hlast], hi⟩ - | castSucc w => - intro hw hi - rw [Program.wireSupport_gate_castSucc] at hi - refine ⟨w, ?_, hi⟩ - by_cases hlast : Wire.gate (Fin.last g) ∈ frontier <;> - simp [opened, hlast, prior, hw] - have hline : lineInputs.card ≤ 1 + binaryCost line.op := by - calc lineInputs.card ≤ (Finset.univ : Finset (Fin (signature.Arity line.op))).card := - Finset.card_image_le - _ = signature.Arity line.op := by simp - _ ≤ 1 + binaryCost line.op := Boolean.arity_le_one_add_binaryCost line.op - have hopened : opened.card ≤ frontier.card + binaryCost line.op := by - by_cases hlast : Wire.gate (Fin.last g) ∈ frontier - · have hprior : prior.card ≤ (frontier.erase (Wire.gate (Fin.last g))).card := by - apply Finset.card_le_card_of_injOn Wire.castSucc - · intro w hw - change Wire.castSucc w ∈ frontier.erase (Wire.gate (Fin.last g)) - rw [Finset.mem_erase] - refine ⟨?_, by simpa [prior] using hw⟩ - cases w with - | input _ => simp - | gate _ => simp [Fin.castSucc_ne_last] - · exact wire_castSucc_injective'.injOn - have herase := Finset.card_erase_of_mem hlast - have hpos : 1 ≤ frontier.card := Finset.one_le_card.mpr ⟨_, hlast⟩ - have hopened_eq : opened = prior ∪ lineInputs := by simp [opened, hlast] - rw [hopened_eq] - calc (prior ∪ lineInputs).card ≤ prior.card + lineInputs.card := - Finset.card_union_le _ _ - _ ≤ (frontier.erase (Wire.gate (Fin.last g))).card + (1 + binaryCost line.op) := - Nat.add_le_add hprior hline - _ = frontier.card - 1 + (1 + binaryCost line.op) := by rw [herase] - _ = frontier.card + binaryCost line.op := by omega - · have hprior : prior.card ≤ frontier.card := by - apply Finset.card_le_card_of_injOn Wire.castSucc - · intro w hw - simpa [prior] using hw - · exact wire_castSucc_injective'.injOn - have hopened_eq : opened = prior := by simp [opened, hlast] - rw [hopened_eq] - omega - calc (frontier.biUnion (p.gate line).wireSupport).card - ≤ (opened.biUnion p.wireSupport).card := Finset.card_le_card hsub - _ ≤ opened.card + p.cost binaryCost := ih opened - _ ≤ frontier.card + binaryCost line.op + p.cost binaryCost := - Nat.add_le_add_right hopened _ - _ = frontier.card + (p.gate line).cost binaryCost := by - rw [Program.cost_gate] - omega + (frontier.biUnion p.wireSupport).card ≤ frontier.card + p.cost binaryCost := + p.card_biUnion_wireSupport_le_cost binaryCost arity_le_one_add_binaryCost frontier /-- A De Morgan circuit with `m` outputs has at most `m + c.program.cost binaryCost` supporting inputs, since only binary AND and OR gates increase the number of reachable inputs. -/ diff --git a/Complexity/Computability/Circuit/FanIn.lean b/Complexity/Computability/Circuit/FanIn.lean index 0db392b9ac..2ba244d0c0 100644 --- a/Complexity/Computability/Circuit/FanIn.lean +++ b/Complexity/Computability/Circuit/FanIn.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Computability.Circuit.Support public import Cslib.Computability.Circuit.Depth +public import Cslib.Computability.Circuit.Simulation public import Mathlib.Algebra.Order.BigOperators.Group.Finset /-! @@ -17,8 +18,17 @@ Unfolding a frontier through a bounded-fan-in program controls how many original inputs can reach the outputs. Essential inputs therefore give a lower bound on circuit size. +## Main definitions + +* `Cslib.Circuits.Program.reachableInputs`: the original circuit inputs reachable backwards from a + frontier of wires in a program. + ## Main results +* `Cslib.Circuits.Program.card_reachableInputs_le_cost`: reachable inputs are bounded by the + frontier size plus the program cost under any weight bounding arities by `1 + w op`. +* `Cslib.Circuits.Program.card_biUnion_wireSupport_le_cost`: supporting inputs are bounded by the + frontier size plus the program cost under any weight bounding arities by `1 + w op`. * `Cslib.Circuits.Circuit.card_inputSupport_le_size`: a circuit of fan-in `r` with `m` outputs has at most `m + (r - 1) size` supporting inputs. * `Cslib.Circuits.Circuit.essential_le_size`: the same bound for essential inputs of the computed @@ -33,7 +43,8 @@ namespace Cslib.Circuits variable {σ : Signature} {U V : Type*} {n m g : ℕ} -private def Program.reachableInputs : +/-- The original circuit inputs reachable backwards from a frontier of wires in a program. -/ +def Program.reachableInputs : ∀ {g : ℕ}, Program σ n g → Finset (Wire n g) → Finset (Fin n) | _, .empty, frontier => Finset.univ.filter fun input => Wire.input input ∈ frontier | _, @Program.gate _ _ g program line, frontier => @@ -45,7 +56,8 @@ private def Program.reachableInputs : prior program.reachableInputs opened -private theorem wire_castSucc_injective : +/-- Embedding a wire into a widened program by `Wire.castSucc` is injective. -/ +theorem Wire.castSucc_injective : Function.Injective (Wire.castSucc : Wire n g → Wire n (g + 1)) := by intro a b h cases a <;> cases b <;> simp_all [Wire.castSucc] @@ -65,7 +77,8 @@ private def Circuit.reachableInputs (c : Circuit σ n m) : Finset (Fin n) := c.program.reachableInputs c.frontier -private theorem Program.support_subset_reachableInputs +/-- Every input supporting a wire in the frontier is reachable from the frontier. -/ +theorem Program.support_subset_reachableInputs (program : Program σ n g) : ∀ frontier : Finset (Wire n g), frontier.biUnion program.wireSupport ⊆ @@ -118,16 +131,19 @@ private theorem Circuit.inputSupport_subset_reachableInputs obtain ⟨output, supported⟩ := present exact ⟨c.outputs output, ⟨output, rfl⟩, supported⟩ -private theorem Program.card_reachableInputs_le +/-- In any circuit program, the number of reachable inputs from a frontier of wires is bounded +by the size of the frontier plus the cost of the program, for any weight function that bounds gate +arities by `1 + w op`. -/ +theorem Program.card_reachableInputs_le_cost (program : Program σ n g) - (r : Nat) : - ∀ (_bounded : program.FanInAtMost r) (frontier : Finset (Wire n g)), - (program.reachableInputs frontier).card ≤ - frontier.card + (r - 1) * g := by + (w : σ.Op → ℕ) + (hw : ∀ op, σ.Arity op ≤ 1 + w op) + (frontier : Finset (Wire n g)) : + (program.reachableInputs frontier).card ≤ + frontier.card + program.cost w := by induction program with | empty => - intro _ frontier - simp only [Cslib.Circuits.Program.reachableInputs, Nat.mul_zero, Nat.add_zero] + simp only [Program.reachableInputs, Program.cost_empty, Nat.add_zero] apply Finset.card_le_card_of_injOn Wire.input · intro input present simpa using present @@ -135,8 +151,6 @@ private theorem Program.card_reachableInputs_le cases h rfl | @gate g program line ih => - intro bounded frontier - obtain ⟨programBounded, lineBounded⟩ := bounded let prior := Finset.univ.filter fun wire : Wire n g => wire.castSucc ∈ frontier let lineInputs := Finset.univ.image line.wires let opened := @@ -145,14 +159,14 @@ private theorem Program.card_reachableInputs_le apply Finset.card_le_card_of_injOn Wire.castSucc · intro wire present simpa [prior] using present - · exact wire_castSucc_injective.injOn - have lineBound : lineInputs.card ≤ r := by + · exact Wire.castSucc_injective.injOn + have lineBound : lineInputs.card ≤ 1 + w line.op := by calc lineInputs.card ≤ (Finset.univ : Finset (Fin (σ.Arity line.op))).card := Finset.card_image_le _ = σ.Arity line.op := by simp - _ ≤ r := lineBounded - have openedBound : opened.card ≤ frontier.card + (r - 1) := by + _ ≤ 1 + w line.op := hw line.op + have openedBound : opened.card ≤ frontier.card + w line.op := by by_cases lastSelected : Wire.gate (Fin.last g) ∈ frontier · have priorEraseBound : prior.card ≤ (frontier.erase (Wire.gate (Fin.last g))).card := by @@ -164,7 +178,7 @@ private theorem Program.card_reachableInputs_le cases wire with | input i => simp | gate j => simp [Fin.castSucc_ne_last] - · exact wire_castSucc_injective.injOn + · exact Wire.castSucc_injective.injOn have erased := Finset.card_erase_of_mem lastSelected have openedEq : opened = prior ∪ lineInputs := by simp [opened, lastSelected] @@ -172,10 +186,10 @@ private theorem Program.card_reachableInputs_le calc (prior ∪ lineInputs).card ≤ prior.card + lineInputs.card := Finset.card_union_le _ _ - _ ≤ (frontier.erase (Wire.gate (Fin.last g))).card + r := + _ ≤ (frontier.erase (Wire.gate (Fin.last g))).card + (1 + w line.op) := Nat.add_le_add priorEraseBound lineBound - _ = frontier.card - 1 + r := by rw [erased] - _ ≤ frontier.card + (r - 1) := by + _ = frontier.card - 1 + (1 + w line.op) := by rw [erased] + _ = frontier.card + w line.op := by have frontierPositive : 1 ≤ frontier.card := Finset.one_le_card.mpr ⟨_, lastSelected⟩ omega @@ -185,12 +199,48 @@ private theorem Program.card_reachableInputs_le omega change (program.reachableInputs opened).card ≤ _ calc - (program.reachableInputs opened).card ≤ opened.card + (r - 1) * g := - ih programBounded opened - _ ≤ frontier.card + (r - 1) * (g + 1) := by - rw [Nat.mul_succ] + (program.reachableInputs opened).card ≤ opened.card + program.cost w := + ih opened + _ ≤ frontier.card + w line.op + program.cost w := + Nat.add_le_add_right openedBound _ + _ = frontier.card + (program.gate line).cost w := by + rw [Program.cost_gate] omega +/-- The inputs supporting a frontier of wires in a program are bounded by the size of the frontier +plus the cost of the program, for any weight function that bounds gate arities by `1 + w op`. -/ +theorem Program.card_biUnion_wireSupport_le_cost + (program : Program σ n g) + (w : σ.Op → ℕ) + (hw : ∀ op, σ.Arity op ≤ 1 + w op) + (frontier : Finset (Wire n g)) : + (frontier.biUnion program.wireSupport).card ≤ + frontier.card + program.cost w := + (Finset.card_le_card (program.support_subset_reachableInputs frontier)).trans + (program.card_reachableInputs_le_cost w hw frontier) + +private theorem Program.cost_le_of_fanInAtMost (p : Program σ n g) {r : ℕ} (h : p.FanInAtMost r) : + p.cost (fun op => max (r - 1) (σ.Arity op - 1)) ≤ (r - 1) * g := by + induction p with + | empty => simp + | gate p line ih => + obtain ⟨hp, hline⟩ := h + rw [Program.cost_gate, Nat.mul_succ] + have hw : max (r - 1) (σ.Arity line.op - 1) = r - 1 := by omega + rw [hw] + exact Nat.add_le_add (ih hp) le_rfl + +private theorem Program.card_reachableInputs_le + (program : Program σ n g) + (r : Nat) : + ∀ (_bounded : program.FanInAtMost r) (frontier : Finset (Wire n g)), + (program.reachableInputs frontier).card ≤ + frontier.card + (r - 1) * g := by + intro bounded frontier + have hw : ∀ op, σ.Arity op ≤ 1 + max (r - 1) (σ.Arity op - 1) := fun op => by omega + exact (program.card_reachableInputs_le_cost _ hw frontier).trans + (Nat.add_le_add_left (program.cost_le_of_fanInAtMost bounded) _) + private theorem Circuit.card_reachableInputs_le_size (c : Circuit σ n m) (r : Nat) From 5008448bf583009deb7ca57c29e12659f6e07ffa Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sun, 25 Oct 2026 01:53:15 +0000 Subject: [PATCH 2/2] refactor(Circuit): privatize reachableInputs helpers, dedup wire_castSucc_injective'' --- .../Computability/Circuit/Boolean/BinaryCost.lean | 2 +- .../Computability/Circuit/Boolean/ReadOnce.lean | 10 +++------- Complexity/Computability/Circuit/FanIn.lean | 13 +++---------- 3 files changed, 7 insertions(+), 18 deletions(-) diff --git a/Complexity/Computability/Circuit/Boolean/BinaryCost.lean b/Complexity/Computability/Circuit/Boolean/BinaryCost.lean index 103b93af47..c12e30ebbc 100644 --- a/Complexity/Computability/Circuit/Boolean/BinaryCost.lean +++ b/Complexity/Computability/Circuit/Boolean/BinaryCost.lean @@ -7,7 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import Complexity.Computability.Circuit.FanIn +import Complexity.Computability.Circuit.FanIn public import Complexity.Computability.Circuit.Simulation public import Complexity.Computability.Circuit.Support public import Cslib.Computability.Circuit.Boolean.Basic diff --git a/Complexity/Computability/Circuit/Boolean/ReadOnce.lean b/Complexity/Computability/Circuit/Boolean/ReadOnce.lean index 09ad9e596c..af09b5d173 100644 --- a/Complexity/Computability/Circuit/Boolean/ReadOnce.lean +++ b/Complexity/Computability/Circuit/Boolean/ReadOnce.lean @@ -9,6 +9,7 @@ module public import Complexity.Computability.Circuit.Boolean.BinaryCost public import Complexity.Computability.Circuit.Monotone.Formula +import Complexity.Computability.Circuit.FanIn /-! # Positive and read-once Boolean formulas from tight binary-cost circuits @@ -673,11 +674,6 @@ end Boolean /-! ### Unfolding tight binary-cost De Morgan programs into formulas -/ -private theorem wire_castSucc_injective'' : - Function.Injective (Wire.castSucc : Wire n g → Wire n (g + 1)) := by - intro a b h - cases a <;> cases b <;> simp_all [Wire.castSucc] - @[simp] private theorem wire_lastCases_last {α : Sort*} (last : α) (castSucc : Wire n g → α) : Wire.lastCases (motive := fun _ => α) last castSucc (.gate (Fin.last g)) = last := by simp [Wire.lastCases] @@ -770,7 +766,7 @@ theorem Program.exists_litFormula_of_card_biUnion_wireSupport_ge (hn : 0 < n) | last => exact absurd rfl hne | castSucc w' => exact ⟨w', hw, rfl⟩ have hprior_card : prior.card = (frontier.erase (Wire.gate (Fin.last g))).card := by - rw [← hprior_image, Finset.card_image_of_injective _ wire_castSucc_injective''] + rw [← hprior_image, Finset.card_image_of_injective _ Wire.castSucc_injective] have hopened_le : opened.card ≤ frontier.card + binaryCost op := by by_cases hlast : Wire.gate (Fin.last g) ∈ frontier · have herase := Finset.card_erase_of_mem hlast @@ -838,7 +834,7 @@ theorem Program.exists_litFormula_of_card_biUnion_wireSupport_ge (hn : 0 < n) · have hsum_prior : ∑ w ∈ frontier.erase (Wire.gate (Fin.last g)), (F w).leafSize = ∑ w' ∈ prior, (F' w').leafSize := by - rw [← hprior_image, Finset.sum_image fun a _ b _ hab => wire_castSucc_injective'' hab] + rw [← hprior_image, Finset.sum_image fun a _ b _ hab => Wire.castSucc_injective hab] exact Finset.sum_congr rfl fun w' _ => by rw [show F w'.castSucc = F' w' from wire_lastCases_castSucc lastFormula F' w'] by_cases hlast : Wire.gate (Fin.last g) ∈ frontier diff --git a/Complexity/Computability/Circuit/FanIn.lean b/Complexity/Computability/Circuit/FanIn.lean index 2ba244d0c0..fe14fa49b7 100644 --- a/Complexity/Computability/Circuit/FanIn.lean +++ b/Complexity/Computability/Circuit/FanIn.lean @@ -18,15 +18,8 @@ Unfolding a frontier through a bounded-fan-in program controls how many original inputs can reach the outputs. Essential inputs therefore give a lower bound on circuit size. -## Main definitions - -* `Cslib.Circuits.Program.reachableInputs`: the original circuit inputs reachable backwards from a - frontier of wires in a program. - ## Main results -* `Cslib.Circuits.Program.card_reachableInputs_le_cost`: reachable inputs are bounded by the - frontier size plus the program cost under any weight bounding arities by `1 + w op`. * `Cslib.Circuits.Program.card_biUnion_wireSupport_le_cost`: supporting inputs are bounded by the frontier size plus the program cost under any weight bounding arities by `1 + w op`. * `Cslib.Circuits.Circuit.card_inputSupport_le_size`: a circuit of fan-in `r` with `m` outputs has @@ -44,7 +37,7 @@ namespace Cslib.Circuits variable {σ : Signature} {U V : Type*} {n m g : ℕ} /-- The original circuit inputs reachable backwards from a frontier of wires in a program. -/ -def Program.reachableInputs : +private def Program.reachableInputs : ∀ {g : ℕ}, Program σ n g → Finset (Wire n g) → Finset (Fin n) | _, .empty, frontier => Finset.univ.filter fun input => Wire.input input ∈ frontier | _, @Program.gate _ _ g program line, frontier => @@ -78,7 +71,7 @@ private def Circuit.reachableInputs (c : Circuit σ n m) : c.program.reachableInputs c.frontier /-- Every input supporting a wire in the frontier is reachable from the frontier. -/ -theorem Program.support_subset_reachableInputs +private theorem Program.support_subset_reachableInputs (program : Program σ n g) : ∀ frontier : Finset (Wire n g), frontier.biUnion program.wireSupport ⊆ @@ -134,7 +127,7 @@ private theorem Circuit.inputSupport_subset_reachableInputs /-- In any circuit program, the number of reachable inputs from a frontier of wires is bounded by the size of the frontier plus the cost of the program, for any weight function that bounds gate arities by `1 + w op`. -/ -theorem Program.card_reachableInputs_le_cost +private theorem Program.card_reachableInputs_le_cost (program : Program σ n g) (w : σ.Op → ℕ) (hw : ∀ op, σ.Arity op ≤ 1 + w op)