CircuitWithEvalDecides

formal source

 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) :=
 145    Finset.sum_le_sum (fun i _ => (c.gates i).arity_le)
 146  have heq : Finset.univ.sum (fun _ : Fin c.gate_count => 2) = 2 * c.gate_count := by
 147    simp [Finset.sum_const, smul_eq_mul, mul_comm]
 148  linarith
 149
 150/-- **Z-Complexity capacity** of a circuit: how many independent topological