rsatSeparation
plain-language theorem explainer
The rsatSeparation theorem assembles the RSATSeparation structure showing that satisfiable CNF formulas reach zero J-cost in at most n recognition steps while unsatisfiable ones maintain positive J-cost. Complexity researchers examining recognition operators would cite it when distinguishing R̂-time from standard Turing time. The proof proceeds by term construction that directly applies the recognition time bound, the adversarial failure lemma, and the cost lower bound.
Claim. The recognition separation theorem asserts: for every natural number $n$ and every CNF formula $f$ with $n$ variables, if $f$ is satisfiable then there exist steps at most $n$ and an assignment $a$ such that the J-cost of $f$ under $a$ is zero; moreover, for every $n$ and every subset $M$ of size less than $n$ there exist $b$, $R$, and $g$ such that $g$ disagrees with the encoded parity on the restriction to $M$; finally, every unsatisfiable $f$ has J-cost at least one under every assignment.
background
The module encodes SAT into the Recognition Science framework via the R̂ operator. J-cost measures recognition defect of a formula under an assignment; satisfiable formulas reach zero cost while unsatisfiable ones encounter a topological obstruction. The local setting is that R̂ supplies a non-natural polytime certifier separating recognition-time complexity from Turing time, as stated in the module documentation: 'This does NOT prove P ≠ NP for Turing machines. It establishes that the R̂ model separates the two complexity classes.'
proof idea
This is a term-mode proof constructing the RSATSeparation structure. The satisfiable polytime field is obtained directly from the recognition time bound theorem. The local certifier failure field is supplied by the adversarial failure result in BalancedParityHidden. The unsatisfiable obstruction field is taken from the cost lower bound theorem.
why it matters
This is the central theorem of the R̂ SAT Encoding module. It packages the constructive O(n) recognition bound for satisfiable instances together with the positive J-cost obstruction for unsatisfiable instances, exactly as described in the module documentation. In the Recognition Science framework it illustrates separation of recognition-time complexity from Turing computation without resolving classical P versus NP. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.