circuit_capacity_bound
plain-language theorem explainer
A Boolean circuit with S gates has Z-complexity capacity at most 2S. Researchers studying the P versus NP gap in Recognition Science cite the bound to show that polynomial-size circuits retain only polynomial Z-capacity. The proof is a one-line wrapper that applies the bond-count lemma once capacity is identified with bond count.
Claim. Let $c$ be a Boolean circuit over $n$ input variables with gate count $S$. Then the Z-complexity capacity satisfies $C_Z(c) ≤ 2S$, where $C_Z(c)$ equals the total number of parent bonds in the circuit's gate graph.
background
The Circuit Ledger module treats Boolean circuits as restricted sub-ledgers: feed-forward, acyclic graphs in which each gate sees only its immediate parents and lacks global J-cost coupling across the full Z³ lattice. BooleanCircuit n packages the gate list, input-variable map, and output existence into a single structure whose size is the gate count S.
proof idea
CircuitZCapacity is defined to be exactly CircuitBondCount. The proof is therefore a one-line wrapper that invokes the upstream lemma circuit_bond_count_le, which establishes the bond count is at most twice the gate count by summing the per-gate parent-length bound of 2.
why it matters
The result populates the capacity_bound field of CircuitLedgerCert and supplies the key step in poly_circuit_poly_capacity. It completes Stage 2 of the module argument that any polynomial-size circuit remains polynomially bounded in Z-capacity, contrasting with the global reach of the R̂ ledger; the remaining open gap is the depth overhead needed to cross the defect moat.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.