RSATSeparation
RSATSeparation bundles three properties showing that the recognition operator R̂ solves satisfiable SAT instances in linear steps to zero J-cost while unsatisfiable instances retain a positive J-cost lower bound from topological obstruction. Complexity researchers examining alternative computation models cite this to distinguish recognition time from Turing time. The structure definition is populated downstream by a theorem that applies the constructive recognition bound and an adversarial failure lemma from the balanced parity construction.
claimA structure containing three assertions: (1) for every natural number $n$ and every $k$-CNF formula $f$ on $n$ variables, if $f$ is satisfiable then there exist steps at most $n$ and a Boolean assignment $a$ such that the J-cost of $f$ under $a$ equals zero; (2) for every $n$ and every subset $M$ of the $n$ indices with $|M|<n$, there exist a bit $b$, a mask $R$, and a function $g$ on the restricted domain such that $g$ applied to the restricted encoded word differs from $b$; (3) for every $n$ and every unsatisfiable $k$-CNF formula $f$, every assignment $a$ yields J-cost of $f$ under $a$ at least 1.
background
In this module a $k$-CNF formula on $n$ variables is a list of clauses, and an assignment is a Boolean function from the $n$ indices to truth values. The J-cost function measures recognition cost of an assignment on the formula, built from the J-uniqueness map $J(x)=(x+x^{-1})/2-1$ of the forcing chain. The balanced parity hidden encoder maps a bit $b$ and mask $R$ to a word, with restriction to index subsets used to exhibit adversarial failures. The module setting states that the recognition operator R̂ supplies a non-natural polytime certifier for SAT, separating recognition-time complexity from Turing computation time.
proof idea
This is a structure definition with no proof body. Its three fields are instantiated downstream in the rsatSeparation theorem by applying the constructive recognition-time bound lemma to the satisfiable case and the adversarial failure result from the balanced parity hidden encoder to the local-certifier claim.
why it matters in Recognition Science
This structure is the central claim of the R̂ SAT encoding and is used directly by the rsatSeparation theorem. It fills the separation between recognition-time complexity and Turing time described in the module documentation, without claiming a resolution of P versus NP. Within the Recognition Science framework it shows how J-cost landscapes and topological obstructions appear in complexity problems, consistent with the recognition composition law and the phi-ladder cost structure.
scope and limits
- Does not prove P ≠ NP for Turing machines.
- Does not supply an explicit Turing algorithm for SAT.
- Does not resolve the natural proof barrier in classical complexity.
- Applies only inside the R̂ recognition operator.
- Does not construct solutions for concrete SAT instances.
formal statement (Lean)
247structure RSATSeparation where
248 /-- SAT is solvable in O(n) recognition steps for satisfiable instances -/
249 sat_polytime : ∀ n : ℕ, ∀ f : CNFFormula n, f.isSAT →
250 ∃ steps : ℕ, steps ≤ n ∧ ∃ a : Assignment n, satJCost f a = 0
251 /-- No local certifier works for all formulas (adversarial failure) -/
252 local_certifier_fails : ∀ n : ℕ, ∀ M : Finset (Fin n),
253 M.card < n →
254 ∃ b : Bool, ∃ R : Fin n → Bool,
255 ∃ g : ({i // i ∈ M} → Bool) → Bool,
256 g (BalancedParityHidden.restrict (BalancedParityHidden.enc b R) M) ≠ b
257 /-- UNSAT instances have a persistent topological obstruction -/
258 unsat_obstruction : ∀ n : ℕ, ∀ f : CNFFormula n, f.isUNSAT →
259 ∀ a : Assignment n, satJCost f a ≥ 1
260