CircuitDecides

formal source

 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
 151    invariants the circuit's bond graph can represent.
 152    In RS, Z-complexity is the topological charge of the bond graph.
 153    For a circuit, it is bounded by the bond count. -/
 154def CircuitZCapacity {n : ℕ} (c : BooleanCircuit n) : ℕ :=
 155  CircuitBondCount c
 156
 157/-- **THEOREM (Circuit Capacity Bound).**
 158    A Boolean circuit of size S has Z-complexity capacity at most 2S.