rsatSeparation
The rsatSeparation theorem shows that the Recognition Science operator R̂ separates SAT complexity classes in its model: satisfiable formulas reach zero J-cost in at most n recognition steps, unsatisfiable formulas carry a positive J-cost lower bound, and no local certifier succeeds on all instances with fewer than n variables. Researchers comparing non-Turing recognition models to standard complexity would cite the result. The proof is a direct term-mode record construction that assembles the three fields from the time-bound, adversarial-fail,
claimFor the recognition operator $R̂$, every satisfiable $n$-variable CNF formula $f$ admits steps $s$ with $s ≤ n$ and assignment $a$ such that satJCost$(f,a)=0$. No local certifier on a proper subset of $n$ variables decides all formulas correctly. For every unsatisfiable $f$, satJCost$(f,a) ≥ 1$ holds for all assignments $a$.
background
The RSATSeparation structure encodes the separation claim for SAT under R̂. Its sat_polytime field requires that satisfiable formulas reach zero J-cost (defined via satJCost) in ≤ n steps. The local_certifier_fails field uses adversarial constructions from BalancedParityHidden to show no local certifier works. The unsat_obstruction field asserts a positive lower bound on J-cost for unsatisfiable formulas. This sits in the Complexity.RSatEncoding module, which encodes SAT instances into the Recognition Science ledger. The module imports LedgerForcing and BalancedParityHidden to handle the recognition steps and adversarial cases. Upstream, sat_recognition_time_bound proves the O(n) bound for satisfiable cases by reaching zero via sat_reaches_zero, while unsat_cost_lower_bound shows the minimum cost is at least 1 for unsatisfiable formulas.
proof idea
The proof is a term-mode construction of the RSATSeparation record. It defines sat_polytime by unpacking the steps and assignment from sat_recognition_time_bound. For local_certifier_fails it invokes BalancedParityHidden.adversarial_failure with the constant-true function to produce the counterexample b, R, and g. The unsat_obstruction field is obtained directly by applying unsat_cost_lower_bound.
why it matters in Recognition Science
This theorem completes the constructive and obstruction directions of the R̂ SAT encoding, showing that recognition time for SAT is linear while Turing-style local certification fails. It supports the module's core claim that R̂ separates recognition-time complexity from Turing computation time, without proving P ≠ NP. The result touches the natural-proof barrier hypothesis mentioned in the module documentation.
scope and limits
- Does not establish P ≠ NP for standard Turing machines.
- Does not supply an explicit Turing-machine algorithm.
- Applies only inside the R̂ recognition ledger model.
- Assumes the SAT-to-ledger encoding preserves satisfiability.
- Does not address the full natural-proof barrier.
formal statement (Lean)
261theorem rsatSeparation : RSATSeparation where
262 sat_polytime := fun n f h =>
proof body
Term-mode proof.
263 let ⟨steps, a, hle, ha⟩ := sat_recognition_time_bound f h
264 ⟨steps, hle, a, ha⟩
265 local_certifier_fails := fun n M hcard =>
266 let ⟨b, R, g_eq⟩ := BalancedParityHidden.adversarial_failure M (fun _ => true)
267 ⟨b, R, fun _ => true, g_eq⟩
268 unsat_obstruction := fun n f h => unsat_cost_lower_bound f h
269
270end RSatEncoding
271end Complexity
272end IndisputableMonolith