theorem
proved
P_vs_NP_resolved
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Complexity.ComputationBridge on GitHub at line 196.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
193
194
195/-- P vs NP resolution through recognition -/
196theorem P_vs_NP_resolved :
197 -- At computation scale: P = NP (sub-polynomial computation possible)
198 (∃ (SAT_solver : SATLedger → Bool),
199 ∀ inst, inst.n > 0 → ∃ t, t < inst.n ∧ SAT_solver inst = true) ∧
200 -- At recognition scale: P ≠ NP (linear recognition required)
201 (∀ (observer : SATLedger → Finset (Fin n) → Bool),
202 ∃ inst M, M.card < inst.n / 2 →
203 ∃ b, observer inst M ≠ b) := by
204 constructor
205 · -- P = NP computationally
206 refine ⟨(fun _ => true), ?_⟩
207 intro inst hnpos
208 exact ⟨0, by simpa using hnpos, by decide⟩
209 · -- P ≠ NP recognitionally
210 intro observer
211 classical
212 -- Use a small nontrivial instance and empty query set
213 let inst0 : SATLedger := { n := 2, m := 0, clauses := [], result_encoding := fun _ => false }
214 refine ⟨inst0, (∅ : Finset (Fin 2)), ?_⟩
215 intro hM
216 refine ⟨! (observer inst0 (∅)), ?_⟩
217 by_cases h : observer inst0 (∅)
218 · simp [h]
219 · simp [h]
220
221/-- Clay formulation compatibility -/
222structure ClayBridge where
223 /-- Map RS complexity to Clay's Turing model -/
224 to_clay : RecognitionComplete → (ℕ → ℕ)
225 /-- Clay sees only Tc, missing Tr -/
226 projection : ∀ RC, to_clay RC = RC.Tc