SeparationClaim
plain-language theorem explainer
SeparationClaim packages the assertion that R-hat resolves every SAT instance through some ResolutionTime, the proposition that Turing simulation of this global J-cost minimization incurs superpolynomial overhead, and the implication that such overhead yields P ≠ NP. Complexity theorists examining RS-to-Turing bridges would cite it as the structural container for the remaining P vs NP gap. It is introduced as a bare structure definition with no computational content or proof obligations.
Claim. A structure asserting that for every SAT instance $S$ (with $n$ variables and $m$ clauses) there exists a resolution time $t$ such that $t$ records $S$, that the proposition 'simulation overhead of R-hat by Turing machines is superpolynomial' holds, and that this proposition implies P ≠ NP.
background
The module addresses the remaining gap between RS-native R-hat minimization of J-cost on a Z³ lattice and classical Turing-machine complexity classes. SATInstance is the structure recording a SAT problem with positive numbers of variables and clauses; each clause contributes a local J-cost term so that total J-cost vanishes exactly when the instance is satisfiable. ResolutionTime records the number of octaves required for R-hat to drive defect below a threshold on that landscape. The module document states that encoding and non-naturality (Razborov-Rudich) steps are already established; the Turing-simulation step remains open.
proof idea
This is a structure definition that packages three fields: a universal quantifier over SATInstance, an opaque Prop for the overhead claim, and a trivial implication arrow to True. No lemmas are applied; the declaration simply records the intended separation claim.
why it matters
It supplies the formal container for the open Turing-bridge step referenced in PvsNP_SelfContained_Final.tex and biggest-questions.md §XIII Q3. The parent claim is that R-hat's global operation on the full lattice cannot be simulated in polynomial time by a local Turing machine; if the overhead proposition is later shown to hold, the structure directly yields P ≠ NP. It touches the open question of convergence rate and spectral gap from the Theory-Engineering Bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.