phi_pow_51_in_interval

formal source

 124  hi := 45537549354
 125  valid := by norm_num
 126
 127theorem phi_pow_51_in_interval :
 128    phi_pow_51_interval.contains (((1 + Real.sqrt 5) / 2) ^ (51 : ℝ)) := by
 129  simp only [Interval.contains, phi_pow_51_interval]
 130  -- (1 + √5)/2 = goldenRatio
 131  have h_phi : (1 + Real.sqrt 5) / 2 = goldenRatio := rfl
 132  -- Convert real power to natural power: x^(51 : ℝ) = x^51
 133  have h_eq : ((1 + Real.sqrt 5) / 2) ^ (51 : ℝ) = goldenRatio ^ (51 : ℕ) := by
 134    conv_lhs => rw [h_phi]
 135    exact Real.rpow_natCast goldenRatio 51
 136  rw [h_eq]
 137  have h := phi_pow51_in_interval_proven
 138  simp only [Interval.contains, phi_pow51_interval_proven] at h
 139  exact h
 140
 141/-- φ^8 interval ≈ 46.979 - PROVEN -/
 142def phi_pow_8_interval : Interval where
 143  lo := 4697 / 100  -- Matches phi_pow8_interval_proven
 144  hi := 4699 / 100
 145  valid := by norm_num
 146
 147theorem phi_pow_8_in_interval : phi_pow_8_interval.contains (((1 + Real.sqrt 5) / 2) ^ (8 : ℝ)) := by
 148  simp only [Interval.contains, phi_pow_8_interval]
 149  rw [← phi_eq_formula]
 150  have h : goldenRatio ^ (8 : ℝ) = goldenRatio ^ 8 := by
 151    have : (8 : ℝ) = (8 : ℕ) := by norm_num
 152    rw [this, Real.rpow_natCast]
 153  rw [h]
 154  have hcontains := phi_pow8_in_interval_proven
 155  simp only [Interval.contains, phi_pow8_interval_proven] at hcontains
 156  exact hcontains
 157