CircuitLedgerCert
plain-language theorem explainer
CircuitLedgerCert bundles the Z-capacity bound for Boolean circuits, the defect moat for unsatisfiable formulas, the blind decoder limitation, the separation structure, and the open spectral Turing hypothesis. Researchers examining the Recognition Science reduction of the P versus NP gap to J-cost gradients would cite this collection when contrasting local circuit reach against global recognition steps. The declaration is a structure definition that assembles these components directly from prior module results.
Claim. A certificate consists of: capacity bound, that every Boolean circuit of size $S$ on $n$ variables has Z-complexity capacity at most $2S$; moat width, that every unsatisfiable CNF formula on $n$ variables has satJCost at least 1 for every assignment; blind decoder, that no function on a proper subset of the $n$ input bits can recover every hidden bit; separation, the full circuit separation structure; and open gap, the spectral Turing bridge hypothesis.
background
In the Circuit Ledger module the P versus NP question in Recognition Science is recast as whether a feed-forward Boolean circuit can simulate the global J-cost gradient used by the recognition operator R̂ to resolve SAT instances in linear steps. Boolean circuits are defined as structures with a gate count and a list of gates in topological order, each gate being input, and, or, or output, with inputs referencing variables from 0 to n-1. This makes them restricted sub-ledgers lacking the full Z³ lattice coupling present in the global ledger.
proof idea
The declaration is a structure definition. It directly incorporates the capacity bound proved via circuit_capacity_bound, the moat width from the RSatEncoding result moat_width_unsat, the blind decoder from adversarial_failure in BalancedParityHidden, the separation structure from circuitSeparation, and the open gap hypothesis. No additional tactics are required beyond field assignment.
why it matters
This structure is instantiated in circuitLedgerCert and supplies the separation component to conditional_separation, which then derives the conditional Omega(n squared) Turing machine time bound against the O(n) recognition steps of R̂. It completes the proved portion of the circuit separation claim in the module's four-stage analysis of the P versus NP gap. The open gap component points to the remaining spectral-to-TM overhead argument needed for an unconditional separation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.