`clay_bridge_theorem`

proved

show as: view math explainer →

module: IndisputableMonolith.Complexity.ComputationBridge
domain: Complexity
line: 233 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Complexity.ComputationBridge on GitHub at line 233.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 230    to_clay RC = RC.Tc
 231
 232/-- The bridge theorem: connecting to Clay's formulation -/
 233theorem clay_bridge_theorem :
 234  ∃ (CB : ClayBridge),
 235    -- Our resolution is invisible to Clay's framework
 236    (∀ RC : RecognitionComplete,
 237      CB.to_clay RC = RC.Tc) ∧
 238    -- Clay's P vs NP conflates two different questions
 239    (∃ RC, RC.Tc.1 < RC.Tr.1) := by
 240  -- Construct the bridge
 241  let CB : ClayBridge := {
 242    to_clay := fun RC => RC.Tc
 243    projection := fun _ => rfl
 244    ill_posed := fun RC _ => rfl
 245  }
 246  use CB
 247  constructor
 248  · intro RC; rfl
 249  · -- Witness: SAT complexity
 250    -- Provide a simple RC with Tc 1 < Tr 1
 251    let RC : RecognitionComplete := {
 252      Tc := fun _ => 0
 253      Tr := fun n => n
 254      Tc_subpoly := by
 255        use 1, (1/3 : ℝ)
 256        constructor <;> norm_num
 257        intro n hn
 258        -- 0 ≤ c * n^k * log n
 259        have : 0 ≤ (1 : ℝ) * (n : ℝ)^(1/3 : ℝ) * Real.log n := by
 260          have hlog : 0 ≤ Real.log (n : ℝ) := by
 261            cases n with
 262            | zero => simp
 263            | succ n' =>

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.