poly_circuit_poly_capacity
plain-language theorem explainer
A Boolean circuit on n inputs whose gate count is bounded by a polynomial in n has Z-complexity capacity likewise bounded by a polynomial in n. Researchers studying the Recognition Science reduction of P versus NP cite this corollary when bounding the representational power of feed-forward sub-ledgers. The proof obtains the gate-count polynomial and scales the existing capacity bound by a constant factor of two via linear arithmetic and ring normalization.
Claim. Let $c$ be a Boolean circuit on $n$ input variables whose total number of gates is at most $k n^d$ for natural numbers $k$ and $d$. Then there exist natural numbers $k'$ and $d'$ such that the Z-complexity capacity of $c$ is at most $k' n^{d'}$.
background
In the Circuit Ledger module, Boolean circuits are formalized as restricted sub-ledgers: feed-forward structures with local determinism and no global J-cost coupling across the full Z³ lattice. Each gate interacts only with its immediate parents, limiting the circuit's reach compared to the global ledger used by R̂. CircuitZCapacity is defined as the circuit bond count, representing the number of independent topological invariants the bond graph can represent. The upstream theorem on circuit capacity bound establishes that this capacity is at most twice the gate count for any Boolean circuit. This corollary extends that bound to the polynomial regime, showing that if gate count is polynomial in n then so is Z-capacity. It sits within the broader argument that polynomial circuits cannot sense the defect moat separating SAT from UNSAT instances.
proof idea
The proof is a short tactic script. It destructures the existential hypothesis on the gate-count polynomial to obtain k and d together with the inequality. It then applies the circuit capacity bound lemma to replace the Z-capacity with a term at most twice the gate count. The remaining steps use linarith to absorb the constant 2 into the polynomial coefficient and ring to normalize the expression into the desired form.
why it matters
This theorem supplies the polynomial bound on Z-capacity required by the circuit separation theorem, which assembles the full separation structure for the P versus NP question in Recognition Science. It completes Stage 4 of the module's argument: a poly-size circuit has poly-bounded Z-capacity, yet the defect moat requires full n-bit information to cross. The result therefore sharpens the open gap concerning the exponential depth overhead needed for a circuit to simulate global recognition steps. It directly supports the claim that restricted sub-ledgers cannot replicate the O(n) recognition time of the full ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.