circuit_bond_count_le
The theorem establishes that the total bond count in any Boolean circuit is at most twice the gate count. Researchers bounding Z-complexity capacity for feed-forward circuits in Recognition Science cite this to limit polynomial-size circuits to polynomial topological invariants. The proof unfolds the bond sum, applies a per-gate parent-length inequality via Finset.sum_le_sum, simplifies the constant sum on the right, and closes with linarith.
claimFor a Boolean circuit $c$ over $n$ variables, let $B(c)$ be the total number of parent-child bonds (sum of parent-list lengths over all gates) and $G(c)$ the gate count. Then $B(c) ≤ 2 · G(c)$.
background
The Circuit Ledger module treats Boolean circuits as restricted sub-ledgers: feed-forward, locally deterministic structures lacking global J-cost coupling across the Z³ lattice. BooleanCircuit is the structure with gate_count, a Fin-indexed map to gates in topological order, input-variable constraints, and an output-gate existence condition. CircuitBondCount is the definition that sums (c.gates i).parents.length over Fin gate_count, counting all wires in the bond graph.
proof idea
Tactic-mode proof. Unfold CircuitBondCount to expose the sum of parent lengths. Establish the inequality via Finset.sum_le_sum applied to the arity_le property of each gate. Simplify the right-hand side (sum of 2 over gate_count indices) to exactly 2 * gate_count using simp on sum_const, smul_eq_mul, and mul_comm. Conclude by linarith.
why it matters in Recognition Science
This feeds the circuit_capacity_bound theorem, which concludes CircuitZCapacity c ≤ 2 * c.gate_count and notes that poly-size circuits therefore have only poly-bounded Z-capacity. It completes Stage 2 of the module's argument that separates local circuit reach from the full ledger's global J-cost resolution of SAT. In the Recognition Science setting it supplies the bond-count step needed for the defect-moat separation structure and the open question of exponential depth overhead for moat-crossing verification.
scope and limits
- Does not bound circuit depth or evaluation time.
- Does not incorporate global J-cost coupling from the full ledger.
- Does not address satisfiability or defect-moat crossing.
- Does not supply lower bounds on bond counts.
Lean usage
theorem circuit_capacity_bound {n : ℕ} (c : BooleanCircuit n) : CircuitZCapacity c ≤ 2 * c.gate_count := circuit_bond_count_le cformal statement (Lean)
140theorem circuit_bond_count_le {n : ℕ} (c : BooleanCircuit n) :
141 CircuitBondCount c ≤ 2 * c.gate_count := by
proof body
Tactic-mode proof.
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. -/