poly_circuit_poly_capacity
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish that polynomial circuits can decide SAT instances.
- Does not quantify the circuit depth required to approach the defect moat.
- Does not address Turing machine simulation overhead from spectral gap considerations.
- Does not prove lower bounds on circuit size for specific formula families.
formal statement (Lean)
167theorem poly_circuit_poly_capacity {n : ℕ} (c : BooleanCircuit n)
168 (h_poly : ∃ (k d : ℕ), c.gate_count ≤ k * n ^ d) :
169 ∃ (k d : ℕ), CircuitZCapacity c ≤ k * n ^ d := by
proof body
Tactic-mode proof.
170 obtain ⟨k, d, hk⟩ := h_poly
171 exact ⟨2 * k, d, by
172 calc CircuitZCapacity c ≤ 2 * c.gate_count := circuit_capacity_bound c
173 _ ≤ 2 * (k * n ^ d) := by linarith
174 _ = 2 * k * n ^ d := by ring⟩
175
176/-! ## Part 3: The Defect Moat -/
177
178/-- The **Defect Moat** for a formula f: 0 if SAT, 1 if UNSAT. -/