demoRecognitionScenario

formal source

 110  eventual_gap : ∀ ⦃n : ℕ⦄, 100 ≤ n → (rc.Tc n : ℝ) < n ∧ (rc.Tr n : ℝ) ≥ n
 111
 112/-- Concrete scenario used by downstream demos: Tc = 0 and Tr = id. -/
 113noncomputable def demoRecognitionScenario : RecognitionScenario :=
 114  let rc : RecognitionComplete := {
 115    Tc := fun _ => 0
 116    Tr := fun n => n
 117    Tc_subpoly := by
 118      use 1, (1 / 3 : ℝ)
 119      constructor <;> norm_num
 120      intro n hn
 121      have hlog : 0 ≤ Real.log (n : ℝ) := by
 122        cases n with
 123        | zero => simp
 124        | succ n' =>
 125          have : (1 : ℝ) ≤ (Nat.succ n' : ℝ) := by exact_mod_cast Nat.succ_le_succ (Nat.zero_le _)
 126          simpa using Real.log_nonneg_iff.mpr this
 127      have hrpow : 0 ≤ (n : ℝ)^(1/3 : ℝ) :=
 128        Real.rpow_nonneg_of_nonneg (show 0 ≤ (n : ℝ) by exact_mod_cast Nat.zero_le _) _
 129      simpa [mul_comm, mul_left_comm, mul_assoc] using mul_nonneg (by norm_num) (mul_nonneg hrpow hlog)
 130    Tr_linear := by
 131      use (1 : ℝ)
 132      constructor <;> norm_num
 133      intro n _; simp }
 134  {
 135    rc
 136    sat_bound := by
 137      intro inst
 138      constructor
 139      · have : 0 ≤ (inst.n : ℝ)^(1/3 : ℝ) * Real.log (inst.n : ℝ) := by
 140          have hlog : 0 ≤ Real.log (inst.n : ℝ) := by
 141            cases inst.n with
 142            | zero => simp
 143            | succ n' =>