clay_bridge_theorem

proof body

Tactic-mode proof.

 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' =>
 264              have : (1 : ℝ) ≤ (n.succ : ℝ) := by exact_mod_cast Nat.succ_le_succ (Nat.zero_le _)
 265              simpa using Real.log_nonneg_iff.mpr this
 266          have hrpow : 0 ≤ (n : ℝ)^(1/3 : ℝ) := by
 267            have : 0 ≤ (n : ℝ) := by exact_mod_cast Nat.zero_le _
 268            exact Real.rpow_nonneg_of_nonneg this _
 269          simpa [mul_comm, mul_left_comm, mul_assoc] using mul_nonneg (by norm_num) (mul_nonneg hrpow hlog)
 270        simpa using this
 271      Tr_linear := by
 272        use (1 : ℝ)
 273        constructor; norm_num
 274        intro n hn; simpa
 275    }
 276    exact ⟨RC, by decide⟩
 277
 278/-- Connection to existing ledger infrastructure -/