circuit_bond_count_le
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.