circuitLedgerCert
plain-language theorem explainer
circuitLedgerCert packages the Z-capacity bound, defect moat width, blind decoder failure, separation structure, and open gap record into one CircuitLedgerCert for Boolean circuits as restricted sub-ledgers. Researchers reducing the P versus NP question inside Recognition Science cite it to consolidate the four-stage argument that poly-size circuits lack global J-cost reach. The definition is a direct record constructor that assigns each field to an existing theorem such as circuit_capacity_bound and moat_width_unsat.
Claim. The circuit ledger certificate is the record whose fields are: capacity bound stating that for every Boolean circuit on $n$ inputs, Z-capacity is at most twice the gate count; moat width stating that every assignment to an unsatisfiable CNF formula has J-cost at least 1; blind decoder stating that no decoder on a proper subset of the $n$ variables is universal; separation structure; and open gap record with spectral gap $1/2$, rhat convergence in $n$ steps, simulation cost $n/2$, and TM time lower bound $n(n/2)$.
background
The module treats Boolean circuits as feed-forward sub-ledgers inside the Recognition framework. A circuit of size S is a directed acyclic graph whose gates see only local parents, so its Z-complexity capacity is bounded by the number of bonds. CircuitLedgerCert bundles the four proved components that formalize this restriction: capacity bound, defect moat for UNSAT formulas, absence of a universal decoder on fewer than n variables, and the separation structure. The local setting is the reduction of P versus NP to whether such a circuit can simulate the global J-cost gradient used by R̂ to resolve SAT in linear recognition steps.
proof idea
The definition is a direct record constructor. It maps capacity_bound to the theorem circuit_capacity_bound (itself a one-line wrapper around circuit_bond_count_le), moat_width to moat_width_unsat (which applies unsat_cost_lower_bound), blind_decoder to adversarial_failure, separation to circuitSeparation, and open_gap to an explicit record whose four fields are filled by norm_num for the spectral gap 1/2 and by le_refl together with le_succ for the remaining arithmetic bounds.
why it matters
This definition collects the stage-1 through stage-3 results of the Circuit Ledger module and thereby supplies the consolidated certificate needed for the P versus NP reduction in Recognition Science. It feeds the open gap on spectral-gap to TM-step translation that remains after the capacity and moat arguments are in place. The construction directly supports the claim that a polynomial-size circuit has only polynomial Z-capacity and therefore cannot read the full n-bit information required to cross the defect moat.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.