CircuitBondCount

formal source

 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.
 159
 160    The significance: a polynomial-size circuit (S = poly(n)) has
 161    Z-capacity at most 2·poly(n) = poly(n). -/
 162theorem circuit_capacity_bound {n : ℕ} (c : BooleanCircuit n) :
 163    CircuitZCapacity c ≤ 2 * c.gate_count :=
 164  circuit_bond_count_le c
 165
 166/-- Corollary: a poly-size circuit has poly-bounded Z-capacity. -/