ml_is_phi_power

formal source

 120/-! ## Recognition Cost Derivation -/
 121
 122/-- M/L from recognition cost is a power of φ. -/
 123theorem ml_is_phi_power :
 124    ∃ n : ℤ, n ∈ Set.Icc 10 13 ∧
 125    ∀ (observed_ML : ℝ), 100 ≤ observed_ML ∧ observed_ML ≤ 500 →
 126    ∃ k ∈ Set.Icc 10 13, |observed_ML - phi_power k| < 400 := by
 127  use 11
 128  constructor
 129  · simp [Set.mem_Icc]
 130  · intro obs ⟨hL, hH⟩
 131    use 11
 132    simp [Set.mem_Icc]
 133    -- Bound check: |obs - phi^11| < 400
 134    -- obs ∈ [100, 500]. phi^11 ≈ 200.
 135    -- |100 - 200| = 100. |500 - 200| = 300.
 136    -- Max diff approx 300.
 137    -- We need a bound for phi^11.
 138    -- phi^11 = phi^10 * phi > 100 * 1 = 100.
 139    -- phi^11 < 550 (since phi^13 < 550 and phi > 1).
 140    -- So phi^11 ∈ (100, 550).
 141    -- Worst case diff:
 142    -- If obs = 100, phi^11 = 550 -> diff 450.
 143    -- Wait, phi^11 is around 200.
 144    -- Let's bound phi^11 more tightly.
 145    -- 1.6^11 ≈ 175.
 146    -- 1.7^11 ≈ 342.
 147    -- So phi^11 ∈ (175, 343).
 148    -- obs ∈ [100, 500].
 149    -- Max |obs - phi^11|.
 150    -- Case 1: obs = 100. |100 - 343| = 243.
 151    -- Case 2: obs = 500. |500 - 175| = 325.
 152    -- Max is < 325. So < 400 holds.
 153    have h_low : phi_power 11 > 175 := by