rhat_is_non_natural
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.
claimNo 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 in Recognition Science
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.
scope and limits
- Does not prove P ≠ NP inside the standard Turing-machine model.
- Does not construct or exhibit any explicit local certifier.
- Applies only to the CNF encoding used inside the R̂ J-cost.
- Does not treat unsatisfiable formulas or their cost lower bounds.
formal statement (Lean)
178theorem rhat_is_non_natural (n : ℕ) :
179 ¬ ∃ (M : Finset (Fin n)),
180 (M.card < n) ∧
181 ∀ (f : CNFFormula n) (_ : f.isSAT),
182 ∃ g : ({i // i ∈ M} → Bool) → Bool,
183 ∀ R : Fin n → Bool,
184 g (BalancedParityHidden.restrict R M) = (f.clauses.any
185 (fun c => c.satisfiedBy (fun i => R i))).not.not := by
proof body
Tactic-mode proof.
186 intro ⟨M, hcard, hforall⟩
187 -- Since |M| < n, there exists j ∉ M
188 have ⟨j, hj⟩ : ∃ j : Fin n, j ∉ M := by
189 by_contra hall; push_neg at hall
190 have hsub : Finset.univ ⊆ M := fun x _ => hall x
191 exact absurd (Finset.card_le_card hsub) (by simp [Finset.card_fin]; omega)
192 -- Construct a single-clause formula depending only on variable j
193 let clause_j : Clause n := ⟨[(j, true)], by simp⟩
194 let φ : CNFFormula n := ⟨[clause_j], n, rfl⟩
195 -- φ is SAT: the all-true assignment satisfies it
196 have hsat : φ.isSAT := by
197 refine ⟨fun _ => true, ?_⟩
198 simp only [CNFFormula.satisfiedBy, φ, List.all_cons, List.all_nil, Bool.and_true,
199 Clause.satisfiedBy, clause_j, List.any_cons, List.any_nil, Bool.or_false,
200 Literal.satisfiedBy, ite_true]
201 obtain ⟨g, hg⟩ := hforall φ hsat
202 -- Two assignments: R₁ all-false, R₂ flips j to true
203 let R₁ : Fin n → Bool := fun _ => false
204 let R₂ : Fin n → Bool := fun i => i == j
205 -- restrict R₁ M = restrict R₂ M (since j ∉ M, the only difference is invisible)
206 have hrestr : BalancedParityHidden.restrict R₁ M = BalancedParityHidden.restrict R₂ M := by
207 funext ⟨i, hi⟩
208 simp only [BalancedParityHidden.restrict, R₁, R₂]
209 have hne : i ≠ j := fun heq => absurd (heq ▸ hi) hj
210 simp [beq_eq_false_iff_ne.mpr hne]
211 -- g gives the same output for both (same restricted input)
212 have hg1 := hg R₁; have hg2 := hg R₂
213 rw [hrestr] at hg1
214 -- The formula evaluates to R j on any assignment R
215 -- Evaluate on R₁: clause_j.satisfiedBy R₁ = Literal.satisfiedBy (j,true) R₁ = R₁ j = false
216 have hv1 : Literal.satisfiedBy (j, true) (fun i => R₁ i) = false := by
217 simp [Literal.satisfiedBy, R₁]
218 have hc1 : Clause.satisfiedBy clause_j (fun i => R₁ i) = false := by
219 simp [Clause.satisfiedBy, clause_j, List.any_cons, List.any_nil, hv1]
220 have hf1 : (φ.clauses.any fun c => c.satisfiedBy fun i => R₁ i) = false := by
221 simp [φ, List.any_cons, List.any_nil, hc1]
222 -- Evaluate on R₂: clause_j.satisfiedBy R₂ = Literal.satisfiedBy (j,true) R₂ = R₂ j = true
223 have hv2 : Literal.satisfiedBy (j, true) (fun i => R₂ i) = true := by
224 simp [Literal.satisfiedBy, R₂]
225 have hc2 : Clause.satisfiedBy clause_j (fun i => R₂ i) = true := by
226 simp [Clause.satisfiedBy, clause_j, List.any_cons, List.any_nil, hv2]
227 have hf2 : (φ.clauses.any fun c => c.satisfiedBy fun i => R₂ i) = true := by
228 simp [φ, List.any_cons, List.any_nil, hc2]
229 -- Now hg1 : g(restrict R₂ M) = !!false = false
230 -- and hg2 : g(restrict R₂ M) = !!true = true
231 rw [hf1, Bool.not_false, Bool.not_true] at hg1
232 rw [hf2, Bool.not_true, Bool.not_false] at hg2
233 -- hg1 : g(...) = false, hg2 : g(...) = true → contradiction
234 rw [hg1] at hg2
235 exact absurd hg2 (by decide)
236
237/-! ## Part 4: The R̂ Separation Theorem -/
238
239/-- **R̂ SEPARATION THEOREM**: The recognition-time complexity of SAT under R̂
240 differs from the Turing computation time.
241
242 Constructive direction (R̂ polytime): SAT has O(n) recognition time (sat_recognition_time_bound)
243 Lower bound (Turing exponential): Any local certifier fails (rhat_is_non_natural)
244
245 This is NOT a proof of P ≠ NP for Turing machines. It establishes that
246 the R̂ model of computation separates the classes in a different way. -/