RSATSeparation
plain-language theorem explainer
The RSATSeparation structure packages three properties for SAT under the R̂ operator: satisfiable k-CNF formulas reach zero J-cost in at most n recognition steps, every proper local subset admits an adversarial mask that defeats certification, and unsatisfiable formulas carry positive J-cost on every assignment. Researchers comparing recognition-time complexity to Turing time would cite the structure when discussing non-natural polytime certifiers. It is a bare structure definition that collects the three assertions with no additional proof.
Claim. The structure asserts: for every $n$ and every $k$-CNF formula $f$ on $n$ variables, if $f$ is satisfiable then there exist steps $s$ with $s ≤ n$ and an assignment $a$ such that the J-cost of $f$ under $a$ equals zero; for every $n$ and every proper subset $M$ of size less than $n$, there exist a bit $b$, mask $R$, and local function $g$ such that $g$ applied to the restricted hidden encoding of $b$ and $R$ differs from $b$; and for every unsatisfiable $f$, every assignment yields J-cost at least 1.
background
CNFFormula(n) is a structure holding a list of clauses together with a var_count field fixed to n. Assignment(n) is the type Fin n → Bool. satJCost measures the J-cost of an encoded SAT instance under a given assignment. The module sets the local setting as the R̂ model of computation, where satisfiable instances admit O(n) recognition steps to zero cost while unsatisfiable instances retain a topological obstruction measured by positive Betti-1. Upstream BalancedParityHidden.enc encodes a hidden bit b with mask R, and restrict projects that encoding onto a queried index set M.
proof idea
The declaration is a structure definition whose three fields are stated directly as quantified propositions; no tactics or lemmas are applied inside the body.
why it matters
The structure is instantiated by the downstream theorem rsatSeparation, which supplies the sat_polytime field from sat_recognition_time_bound and the local_certifier_fails field from BalancedParityHidden.adversarial_failure. It records the separation between recognition-time complexity and Turing time inside the R̂ model, as described in the module claim that R̂ supplies a non-natural polytime certifier. The declaration does not address the classical P versus NP question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.