 111    gate structure and input wiring. We model this as a bundled function field
 112    rather than implementing gate-by-gate evaluation (which would require
 113    enriching BooleanCircuit with explicit input wiring). -/
 114structure BooleanCircuitWithEval (n : ℕ) extends BooleanCircuit n where
 115  /-- The function computed by this circuit -/
 116  eval : Assignment n → Bool
 117
 118/-- A circuit with evaluation *decides* a formula if its eval matches
 119    satisfiability on every assignment. -/
 120def CircuitWithEvalDecides {n : ℕ} (c : BooleanCircuitWithEval n) (f : CNFFormula n) : Prop :=
 121  ∀ a : Assignment n, c.eval a = (f.satisfiedBy a)
 122
 123/-- For backward compatibility: CircuitEval and CircuitDecides use an
 124    existential model — a circuit "decides" a formula if there EXISTS an
 125    evaluation function consistent with the gate structure that matches
 126    satisfiability. This is the correct abstract model: it says "the
 127    circuit's structure is rich enough to compute satisfiability." -/
 128def CircuitDecides {n : ℕ} (c : BooleanCircuit n) (f : CNFFormula n) : Prop :=
 129  ∃ eval : Assignment n → Bool,
 130    (∀ a : Assignment n, eval a = (f.satisfiedBy a))
 131
 132/-! ## Part 2: Circuit Z-Complexity Capacity -/
 133
 134/-- The **bond count** of a circuit is the total number of wires (parent→child edges).
 135    Each gate contributes at most 2 wires (arity_le). -/
 136def CircuitBondCount {n : ℕ} (c : BooleanCircuit n) : ℕ :=
 137  Finset.univ.sum (fun i => (c.gates i).parents.length)
 138
 139/-- Bond count is bounded by 2 × gate_count (each gate has ≤ 2 parents). -/
 140theorem circuit_bond_count_le {n : ℕ} (c : BooleanCircuit n) :
 141    CircuitBondCount c ≤ 2 * c.gate_count := by
 142  unfold CircuitBondCount
 143  have hle : Finset.univ.sum (fun i => (c.gates i).parents.length) ≤
 144             Finset.univ.sum (fun _ : Fin c.gate_count => 2) :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.