circuitSeparation
plain-language theorem explainer
circuitSeparation assembles the CircuitSeparation structure by supplying its four fields from upstream lemmas on recognition time, moat width, decoder blindness, and capacity. Researchers reducing P versus NP inside Recognition Science cite this as the assembly step that makes the circuit ledger argument fully proved. The proof is a term-mode record construction that applies sat_recognition_time_bound, moat_width_unsat, no_sublinear_universal_decoder, and poly_circuit_poly_capacity directly to each field.
Claim. The structure CircuitSeparation holds: for every $n$ and SAT formula $f$ there exist steps $s$ and assignment $a$ with $sleq n$ and satJCost$(f,a)=0$; for every UNSAT formula every assignment has satJCost at least 1; no circuit querying fewer than $n$ inputs can decode balanced-parity encodings; polynomial-size circuits obey the Z-capacity bound.
background
The CircuitLedger module models Boolean circuits as feed-forward sub-ledgers lacking global J-cost coupling across the full Z^3 lattice; each gate sees only O(1) parents while the Recognition operator R̂ has global reach. CircuitSeparation encodes the claim that R̂ decides SAT in O(n) recognition steps while any circuit must read all n inputs to cross the defect moat of width at least 1 that separates satisfiable from unsatisfiable assignments. The module documentation states that stage 3 establishes the moat via RSatEncoding and stage 4 assembles the separation once capacity and blindness lemmas are available.
proof idea
The term proof constructs the CircuitSeparation record by direct field assignment. rhat_polytime is set to the output of sat_recognition_time_bound applied to the SAT hypothesis. moat_exists invokes moat_width_unsat. circuit_blind applies no_sublinear_universal_decoder. poly_circuit_bounded applies poly_circuit_poly_capacity. No further tactics or reductions occur.
why it matters
This theorem supplies the separation field to circuitLedgerCert, which populates PvsNPMasterCert in the P versus NP assembly. It completes the proved components of the circuit separation claim in the module (capacity bound and moat arguments) while leaving the spectral gap to TM simulation overhead as the explicit open gap. In the Recognition Science framework it supports the reduction of P versus NP to whether local circuits can simulate global J-cost gradient steps on the phi-lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.