phi_10_bounds

formal source

  96  linarith
  97
  98/-- φ¹⁰ > 100. -/
  99theorem phi_10_bounds : phi_power 10 > 100 := by
 100  unfold phi_power
 101  have h : phi > 1.6 := phi_gt_1_6
 102  have h10 : phi ^ 10 > 1.6 ^ 10 := pow_lt_pow_left h (by norm_num) (by norm_num)
 103  have : (1.6 : ℝ) ^ 10 > 100 := by norm_num
 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]