phi_13_bounds

formal source

 104  exact gt_of_gt_of_gt h10 this
 105
 106/-- φ¹³ < 550. -/
 107theorem phi_13_bounds : phi_power 13 < 550 := by
 108  unfold phi_power
 109  have h : phi < 1.62 := by
 110    unfold phi
 111    norm_num
 112    have : Real.sqrt 5 < 2.24 := by
 113      rw [← Real.sqrt_sq (by norm_num : (0:ℝ)≤2.24)]
 114      apply Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
 115    linarith
 116  have h13 : phi ^ 13 < 1.62 ^ 13 := pow_lt_pow_left h (by norm_num) (by norm_num)
 117  have : (1.62 : ℝ) ^ 13 < 550 := by norm_num
 118  exact lt_trans h13 this
 119
 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.