rhat_is_non_natural
plain-language theorem explainer
No proper subset of variables admits a local function that recovers satisfiability status for every satisfiable CNF formula. Researchers comparing recognition-time complexity to Turing computation cite the result to separate the R̂ model from local certification. The argument selects an excluded variable j, builds a single-clause formula on j, and produces two assignments that agree on the subset yet disagree on satisfaction, forcing any candidate g to output contradictory values on identical input.
Claim. No subset $M$ of the $n$ variables with $|M|<n$ admits a map $g$ from assignments on $M$ such that, for every satisfiable CNF formula $f$, $g(R|_M)$ equals the double negation of the satisfaction indicator of $f$ under any full assignment $R$.
background
The module encodes SAT instances inside the Recognition Science operator R̂ so that satisfiable formulas reach zero J-cost in linear recognition steps while unsatisfiable ones encounter a topological obstruction. CNFFormula n is a list of clauses together with a variable count fixed at n; each clause is a short list of signed literals. BalancedParityHidden.restrict projects any full assignment Fin n → Bool onto the coordinates in M, returning a function on the subtype {i // i ∈ M}. The upstream definition of restrict supplies the projection used to formalize locality.
proof idea
Assume such an M with card < n exists. Cardinality supplies j ∉ M. Form the single-literal clause on j and the corresponding one-clause formula φ, which is satisfiable by the constant-true assignment. The hypothesis yields g for this φ. The all-false assignment R₁ and the assignment R₂ that sets only j true have identical restrictions to M. Yet φ evaluates to false on R₁ and true on R₂, so the two calls to g on the same restricted input return false and true, a contradiction.
why it matters
The theorem supplies the non-natural component inside TuringBridge.turingBridgeCert and the companion rhat_is_non_natural definition. It completes the lower-bound half of the R̂ Separation Theorem stated in the module documentation, showing that global evaluation of the J-cost landscape cannot be replaced by any proper local projection. In the broader framework the result aligns with T5 J-uniqueness and the requirement that the eight-tick octave operate on the full lattice rather than a strict subset.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.