CircuitSeparation
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not prove that Z-capacity less than n forces exponential circuit size.
- Does not address the spectral gap to Turing machine step count translation.
- Does not claim a resolution of P versus NP, only the separation structure.
- Does not cover quantum circuits or other non-Boolean models.
Lean usage
example : CircuitSeparation := circuitSeparationformal statement (Lean)
239structure CircuitSeparation where
240 /-- PROVED: R̂ reaches zero cost in ≤ n steps for SAT formulas -/
241 rhat_polytime : ∀ n : ℕ, ∀ f : CNFFormula n, f.isSAT →
242 ∃ (steps : ℕ) (a : Assignment n),
243 steps ≤ n ∧ satJCost f a = 0
244 /-- PROVED: UNSAT formulas have a defect moat of width ≥ 1 -/
245 moat_exists : ∀ n : ℕ, ∀ f : CNFFormula n, f.isUNSAT →
246 ∀ a : Assignment n, satJCost f a ≥ 1
247 /-- PROVED: no fixed-view decoder over fewer than n variables can
248 universally certify the moat -/
249 circuit_blind : ∀ n : ℕ, ∀ M : Finset (Fin n), M.card < n →
250 ∀ decoder : ({i // i ∈ M} → Bool) → Bool,
251 ¬ ∀ (b : Bool) (R : Fin n → Bool),
252 decoder (restrict (enc b R) M) = b
253 /-- PROVED: poly-size circuits have poly-bounded Z-capacity -/
254 poly_circuit_bounded : ∀ n : ℕ, ∀ c : BooleanCircuit n,
255 (∃ k d : ℕ, c.gate_count ≤ k * n ^ d) →
256 ∃ k d : ℕ, CircuitZCapacity c ≤ k * n ^ d
257
258/-- **THEOREM**: The circuit separation structure is instantiable with
259 all proved components. -/