CircuitSeparation
plain-language theorem explainer
CircuitSeparation bundles four properties separating recognition-based SAT resolution from circuit-based decision. It asserts linear-time zero-cost recognition for satisfiable formulas, a unit-width defect moat for unsatisfiable ones, blindness of sublinear circuits to that moat, and polynomial Z-capacity for polynomial circuits. Complexity theorists examining the RS dissolution of P versus NP cite this structure when building the master certificate. The definition assembles four independently proved components without additional obligations.
Claim. A structure asserting that for every $n$ and satisfiable CNF formula $f$ on $n$ variables there exist steps $s$ and assignment $a$ with $s$ at most $n$ and J-cost of $f$ under $a$ equal to zero; for unsatisfiable $f$ every assignment has J-cost at least 1; no decoder on a proper subset of the $n$ variables can correctly identify the hidden bit for all masks; and every polynomial-size Boolean circuit over $n$ variables has Z-capacity bounded by a polynomial in $n$.
background
In the Circuit Ledger module Boolean circuits are modeled as feed-forward sub-ledgers with local determinism and no global J-cost coupling across the Z³ lattice. CircuitZCapacity is defined as the bond count of the circuit graph and bounded above by twice the gate count. The module sets up the P versus NP question in Recognition Science by contrasting the global reach of the recognition operator R̂ with the bounded depth of circuits. Upstream results from BalancedParityHidden supply the encoder and restrict functions used to formalize the blindness property while RSatEncoding provides the defect moat for unsatisfiable formulas.
proof idea
The structure is introduced directly as a bundle of four fields. Each field is populated by a prior lemma: rhat_polytime from sat_recognition_time_bound, moat_exists from moat_width_unsat, circuit_blind from no_sublinear_universal_decoder, and poly_circuit_bounded from the capacity bound theorem. No tactics are required beyond the structural definition.
why it matters
This definition supplies the separation structure required by the circuitSeparation theorem and the PvsNPMasterCert in the P versus NP assembly. It encodes the core claim that recognition resolves SAT in O(n) steps while any circuit must read all n inputs to cross the defect moat. The open gap noted in the module is the formal link from Z-capacity less than n to exponential depth overhead which would complete the Turing simulation argument. It sits within the broader Recognition Science program of deriving complexity bounds from the J-cost functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.