IndisputableMonolith.Numerics.Interval.PhiBounds
IndisputableMonolith/Numerics/Interval/PhiBounds.lean · 995 lines · 98 declarations
show as:
view math explainer →
1import IndisputableMonolith.Numerics.Interval.Basic
2import Mathlib.NumberTheory.Real.GoldenRatio
3import Mathlib.Analysis.SpecialFunctions.Pow.Real
4
5/-!
6# Rigorous Bounds on the Golden Ratio
7
8This module provides rigorous bounds on φ = (1 + √5)/2 using algebraic properties.
9
10## Strategy
11
12We use the fact that:
13- 2.236² = 4.999696 < 5 < 5.001956 = 2.237²
14- Therefore 2.236 < √5 < 2.237
15- Therefore (1 + 2.236)/2 < φ < (1 + 2.237)/2
16- i.e., 1.618 < φ < 1.6185
17
18For tighter bounds, we use more decimal places.
19-/
20
21namespace IndisputableMonolith.Numerics
22
23open Real
24
25/-- 2.236² < 5 -/
26theorem sq_2236_lt_5 : (2.236 : ℝ)^2 < 5 := by norm_num
27
28/-- 5 < 2.237² -/
29theorem five_lt_sq_2237 : (5 : ℝ) < (2.237 : ℝ)^2 := by norm_num
30
31/-- 2.236 < √5 -/
32theorem sqrt5_gt_2236 : (2.236 : ℝ) < sqrt 5 := by
33 rw [← sqrt_sq (by norm_num : (0 : ℝ) ≤ 2.236)]
34 exact sqrt_lt_sqrt (by norm_num) sq_2236_lt_5
35
36/-- √5 < 2.237 -/
37theorem sqrt5_lt_2237 : sqrt 5 < (2.237 : ℝ) := by
38 rw [← sqrt_sq (by norm_num : (0 : ℝ) ≤ 2.237)]
39 exact sqrt_lt_sqrt (by norm_num : (0 : ℝ) ≤ 5) five_lt_sq_2237
40
41/-- 1.618 < φ -/
42theorem phi_gt_1618 : (1.618 : ℝ) < goldenRatio := by
43 unfold goldenRatio
44 have h : (2.236 : ℝ) < sqrt 5 := sqrt5_gt_2236
45 linarith
46
47/-- φ < 1.6185 -/
48theorem phi_lt_16185 : goldenRatio < (1.6185 : ℝ) := by
49 unfold goldenRatio
50 have h : sqrt 5 < (2.237 : ℝ) := sqrt5_lt_2237
51 linarith
52
53-- For tighter bounds, we need more precision
54
55/-- 2.2360679² < 5 -/
56theorem sq_22360679_lt_5 : (2.2360679 : ℝ)^2 < 5 := by norm_num
57
58/-- 5 < 2.2360680² -/
59theorem five_lt_sq_22360680 : (5 : ℝ) < (2.2360680 : ℝ)^2 := by norm_num
60
61/-- 2.2360679 < √5 -/
62theorem sqrt5_gt_22360679 : (2.2360679 : ℝ) < sqrt 5 := by
63 rw [← sqrt_sq (by norm_num : (0 : ℝ) ≤ 2.2360679)]
64 exact sqrt_lt_sqrt (by norm_num) sq_22360679_lt_5
65
66/-- √5 < 2.2360680 -/
67theorem sqrt5_lt_22360680 : sqrt 5 < (2.2360680 : ℝ) := by
68 rw [← sqrt_sq (by norm_num : (0 : ℝ) ≤ 2.2360680)]
69 exact sqrt_lt_sqrt (by norm_num : (0 : ℝ) ≤ 5) five_lt_sq_22360680
70
71/-- 1.61803395 < φ -/
72theorem phi_gt_161803395 : (1.61803395 : ℝ) < goldenRatio := by
73 unfold goldenRatio
74 have h : (2.2360679 : ℝ) < sqrt 5 := sqrt5_gt_22360679
75 linarith
76
77/-- φ < 1.6180340 -/
78theorem phi_lt_16180340 : goldenRatio < (1.6180340 : ℝ) := by
79 unfold goldenRatio
80 have h : sqrt 5 < (2.2360680 : ℝ) := sqrt5_lt_22360680
81 linarith
82
83/-- Convenience: a bundled “tight enough” φ bound.
84
85This replaces the legacy `Numerics/Interval.lean` `phi_tight_bounds` lemma and is the
86canonical bound used across the codebase going forward. -/
87theorem phi_tight_bounds : (1.61803395 : ℝ) < goldenRatio ∧ goldenRatio < (1.6180340 : ℝ) :=
88 ⟨phi_gt_161803395, phi_lt_16180340⟩
89
90/-- Interval containing φ with tight bounds -/
91def phiIntervalTight : Interval where
92 lo := 161803395 / 100000000 -- 1.61803395
93 hi := 16180340 / 10000000 -- 1.6180340
94 valid := by norm_num
95
96/-- φ is contained in phiIntervalTight - PROVEN -/
97theorem phi_in_phiIntervalTight : phiIntervalTight.contains goldenRatio := by
98 simp only [Interval.contains, phiIntervalTight]
99 constructor
100 · have h := phi_gt_161803395
101 have h1 : ((161803395 / 100000000 : ℚ) : ℝ) < goldenRatio := by
102 calc ((161803395 / 100000000 : ℚ) : ℝ) = (1.61803395 : ℝ) := by norm_num
103 _ < goldenRatio := h
104 exact le_of_lt h1
105 · have h := phi_lt_16180340
106 have h1 : goldenRatio < ((16180340 / 10000000 : ℚ) : ℝ) := by
107 calc goldenRatio < (1.6180340 : ℝ) := h
108 _ = ((16180340 / 10000000 : ℚ) : ℝ) := by norm_num
109 exact le_of_lt h1
110
111/-! ## Quarter-root bounds (needed for quarter/half-ladder rungs) -/
112
113/-- A certified lower rational bound for \(φ^{1/4}\). -/
114noncomputable def phi_quarter_lo : ℝ := 1.12783847
115
116/-- A certified upper rational bound for \(φ^{1/4}\). -/
117noncomputable def phi_quarter_hi : ℝ := 1.12783849
118
119lemma phi_quarter_lo_pow4_lt_phi_lo : phi_quarter_lo ^ (4 : ℕ) < (1.61803395 : ℝ) := by
120 simp [phi_quarter_lo]
121 norm_num
122
123lemma phi_hi_lt_phi_quarter_hi_pow4 : (1.6180340 : ℝ) < phi_quarter_hi ^ (4 : ℕ) := by
124 simp [phi_quarter_hi]
125 norm_num
126
127/-- Lower bound: `phi_quarter_lo < φ^(1/4)` (proved via monotonicity of `x ↦ x^4`). -/
128theorem phi_quarter_gt : phi_quarter_lo < goldenRatio ^ (1/4 : ℝ) := by
129 have hx : (0 : ℝ) ≤ phi_quarter_lo := by simp [phi_quarter_lo]; norm_num
130 have hy : (0 : ℝ) ≤ goldenRatio ^ (1/4 : ℝ) := by
131 exact Real.rpow_nonneg (le_of_lt (by simpa using Real.goldenRatio_pos)) _
132 have hz : (0 : ℝ) < (4 : ℝ) := by norm_num
133 -- Normalize `1/4` to `4⁻¹` to match simp-normal form in `rpow_mul`.
134 have hright : (goldenRatio ^ (4⁻¹ : ℝ)) ^ (4 : ℝ) = goldenRatio := by
135 have hg0 : (0 : ℝ) ≤ goldenRatio := le_of_lt (by simpa using Real.goldenRatio_pos)
136 calc (goldenRatio ^ (4⁻¹ : ℝ)) ^ (4 : ℝ)
137 = goldenRatio ^ ((4⁻¹ : ℝ) * (4 : ℝ)) := by
138 simpa using (Real.rpow_mul hg0 (4⁻¹ : ℝ) (4 : ℝ)).symm
139 _ = goldenRatio ^ (1 : ℝ) := by norm_num
140 _ = goldenRatio := by simp
141 have hleft : phi_quarter_lo ^ (4 : ℝ) = phi_quarter_lo ^ (4 : ℕ) := by
142 simpa using (Real.rpow_natCast phi_quarter_lo 4)
143 have hq : phi_quarter_lo ^ (4 : ℝ) < goldenRatio := by
144 have h1 : phi_quarter_lo ^ (4 : ℕ) < (1.61803395 : ℝ) := phi_quarter_lo_pow4_lt_phi_lo
145 have h2 : (1.61803395 : ℝ) < goldenRatio := phi_gt_161803395
146 have h1' : phi_quarter_lo ^ (4 : ℝ) < (1.61803395 : ℝ) := by simpa [hleft] using h1
147 exact lt_trans h1' h2
148 have hpow : phi_quarter_lo ^ (4 : ℝ) < (goldenRatio ^ (4⁻¹ : ℝ)) ^ (4 : ℝ) := by
149 simpa [hright] using hq
150 have hlt : phi_quarter_lo < goldenRatio ^ (4⁻¹ : ℝ) :=
151 (Real.rpow_lt_rpow_iff hx (by
152 exact Real.rpow_nonneg (le_of_lt (by simpa using Real.goldenRatio_pos)) _) hz).1 hpow
153 -- `simp` normalizes `(1/4 : ℝ)` to `4⁻¹`, so this closes.
154 simpa using hlt
155
156/-- Upper bound: `φ^(1/4) < phi_quarter_hi` (proved via monotonicity of `x ↦ x^4`). -/
157theorem phi_quarter_lt : goldenRatio ^ (1/4 : ℝ) < phi_quarter_hi := by
158 -- Work in the simp-normal form `4⁻¹` (Lean normalizes `1/4` to `4⁻¹`).
159 have hx : (0 : ℝ) ≤ goldenRatio ^ (4⁻¹ : ℝ) := by
160 exact Real.rpow_nonneg (le_of_lt (by simpa using Real.goldenRatio_pos)) _
161 have hy : (0 : ℝ) ≤ phi_quarter_hi := by simp [phi_quarter_hi]; norm_num
162 have hz : (0 : ℝ) < (4 : ℝ) := by norm_num
163 have hright : (goldenRatio ^ (4⁻¹ : ℝ)) ^ (4 : ℝ) = goldenRatio := by
164 have hg0 : (0 : ℝ) ≤ goldenRatio := le_of_lt (by simpa using Real.goldenRatio_pos)
165 calc (goldenRatio ^ (4⁻¹ : ℝ)) ^ (4 : ℝ)
166 = goldenRatio ^ ((4⁻¹ : ℝ) * (4 : ℝ)) := by
167 simpa using (Real.rpow_mul hg0 (4⁻¹ : ℝ) (4 : ℝ)).symm
168 _ = goldenRatio ^ (1 : ℝ) := by norm_num
169 _ = goldenRatio := by simp
170 have hleft : phi_quarter_hi ^ (4 : ℝ) = phi_quarter_hi ^ (4 : ℕ) := by
171 simpa using (Real.rpow_natCast phi_quarter_hi 4)
172 have hq : goldenRatio < phi_quarter_hi ^ (4 : ℝ) := by
173 have h1 : goldenRatio < (1.6180340 : ℝ) := phi_lt_16180340
174 have h2 : (1.6180340 : ℝ) < phi_quarter_hi ^ (4 : ℕ) := phi_hi_lt_phi_quarter_hi_pow4
175 have h2' : (1.6180340 : ℝ) < phi_quarter_hi ^ (4 : ℝ) := by simpa [hleft] using h2
176 exact lt_trans h1 h2'
177 have hpow : (goldenRatio ^ (4⁻¹ : ℝ)) ^ (4 : ℝ) < phi_quarter_hi ^ (4 : ℝ) := by
178 simpa [hright] using hq
179 have hlt : goldenRatio ^ (4⁻¹ : ℝ) < phi_quarter_hi :=
180 (Real.rpow_lt_rpow_iff hx hy hz).1 hpow
181 -- convert back to the displayed exponent `1/4`
182 simpa using hlt
183
184/-- Consolidated quarter-root bounds. -/
185theorem phi_quarter_bounds : phi_quarter_lo < goldenRatio ^ (1/4 : ℝ) ∧ goldenRatio ^ (1/4 : ℝ) < phi_quarter_hi :=
186 ⟨phi_quarter_gt, phi_quarter_lt⟩
187
188/-- Bounds for \(φ^{-1/4}\) derived from the quarter-root bounds by inversion. -/
189theorem phi_neg_quarter_bounds :
190 (1 / phi_quarter_hi) < goldenRatio ^ (-(1/4 : ℝ)) ∧ goldenRatio ^ (-(1/4 : ℝ)) < (1 / phi_quarter_lo) := by
191 have hq := phi_quarter_bounds
192 have hg0 : (0 : ℝ) ≤ goldenRatio := le_of_lt (by simpa using Real.goldenRatio_pos)
193 have hpos : (0 : ℝ) < goldenRatio ^ (4⁻¹ : ℝ) := by
194 have : (0 : ℝ) < goldenRatio := by simpa using Real.goldenRatio_pos
195 exact Real.rpow_pos_of_pos this _
196 have hneg : goldenRatio ^ (-(4⁻¹ : ℝ)) = (goldenRatio ^ (4⁻¹ : ℝ))⁻¹ := by
197 simpa using (Real.rpow_neg hg0 (4⁻¹ : ℝ))
198 have hlo : phi_quarter_lo < goldenRatio ^ (4⁻¹ : ℝ) := by
199 simpa using hq.1
200 have hhi : goldenRatio ^ (4⁻¹ : ℝ) < phi_quarter_hi := by
201 simpa using hq.2
202 have h_lower : (1 / phi_quarter_hi) < 1 / (goldenRatio ^ (4⁻¹ : ℝ)) :=
203 one_div_lt_one_div_of_lt hpos hhi
204 have h_upper : (1 / (goldenRatio ^ (4⁻¹ : ℝ))) < (1 / phi_quarter_lo) :=
205 one_div_lt_one_div_of_lt (by
206 have : (0 : ℝ) < phi_quarter_lo := by simp [phi_quarter_lo]; norm_num
207 exact this) hlo
208 -- `simp` normalizes `-(1/4)` to `-(4⁻¹)`
209 constructor
210 · simpa [hneg, one_div] using h_lower
211 · simpa [hneg, one_div] using h_upper
212
213/-! ## Powers of φ using the recurrence φ² = φ + 1 -/
214
215/-- φ² = φ + 1, so 2.618 < φ² < 2.619 -/
216theorem phi_sq_gt : (2.618 : ℝ) < goldenRatio ^ 2 := by
217 have h := phi_gt_1618
218 have h2 : goldenRatio ^ 2 = goldenRatio + 1 := goldenRatio_sq
219 linarith
220
221theorem phi_sq_lt : goldenRatio ^ 2 < (2.619 : ℝ) := by
222 have h := phi_lt_16185
223 have h2 : goldenRatio ^ 2 = goldenRatio + 1 := goldenRatio_sq
224 linarith
225
226/-! ## φ^(-2) bounds (for quark masses) -/
227
228/-- φ^(-2) > 0.3818 (using φ² < 2.619) -/
229theorem phi_neg2_gt : (0.3818 : ℝ) < goldenRatio ^ (-2 : ℤ) := by
230 have h := phi_sq_lt -- φ² < 2.619
231 have hpos : (0 : ℝ) < goldenRatio ^ 2 := by positivity
232 have heq : goldenRatio ^ (-2 : ℤ) = (goldenRatio ^ 2)⁻¹ :=
233 zpow_neg_coe_of_pos goldenRatio (by norm_num : 0 < 2)
234 rw [heq]
235 have h1 : (0.3818 : ℝ) < 1 / (2.619 : ℝ) := by norm_num
236 have h2 : 1 / (2.619 : ℝ) < 1 / goldenRatio ^ 2 :=
237 one_div_lt_one_div_of_lt hpos h
238 have h3 : 1 / goldenRatio ^ 2 = (goldenRatio ^ 2)⁻¹ := one_div _
239 linarith
240
241/-- φ^(-2) < 0.382 (using φ² > 2.618) -/
242theorem phi_neg2_lt : goldenRatio ^ (-2 : ℤ) < (0.382 : ℝ) := by
243 have h := phi_sq_gt -- 2.618 < φ²
244 have hpos_bound : (0 : ℝ) < 2.618 := by norm_num
245 have heq : goldenRatio ^ (-2 : ℤ) = (goldenRatio ^ 2)⁻¹ :=
246 zpow_neg_coe_of_pos goldenRatio (by norm_num : 0 < 2)
247 rw [heq]
248 have h1 : (goldenRatio ^ 2)⁻¹ < (2.618 : ℝ)⁻¹ :=
249 inv_strictAnti₀ hpos_bound h
250 have h2 : (2.618 : ℝ)⁻¹ < (0.382 : ℝ) := by norm_num
251 linarith
252
253/-! ## Negative powers of φ (using φ⁻¹ = φ - 1) -/
254
255/-- φ⁻¹ = φ - 1 ≈ 0.618 -/
256theorem phi_inv_eq : goldenRatio⁻¹ = goldenRatio - 1 := by
257 -- φ⁻¹ = -ψ = -(1 - √5)/2 = (√5 - 1)/2 = (1 + √5)/2 - 1 = φ - 1
258 rw [inv_goldenRatio]
259 unfold goldenRatio goldenConj
260 ring
261
262theorem phi_inv_gt : (0.618 : ℝ) < goldenRatio⁻¹ := by
263 rw [phi_inv_eq]
264 have h := phi_gt_1618
265 linarith
266
267theorem phi_inv_lt : goldenRatio⁻¹ < (0.6186 : ℝ) := by
268 rw [phi_inv_eq]
269 have h := phi_lt_16185
270 linarith
271
272/-- Interval containing φ⁻¹ - PROVEN -/
273def phi_inv_interval_proven : Interval where
274 lo := 618 / 1000
275 hi := 6186 / 10000
276 valid := by norm_num
277
278theorem phi_inv_in_interval_proven : phi_inv_interval_proven.contains goldenRatio⁻¹ := by
279 simp only [Interval.contains, phi_inv_interval_proven]
280 constructor
281 · have h := phi_inv_gt
282 exact le_of_lt (by calc ((618 / 1000 : ℚ) : ℝ) = (0.618 : ℝ) := by norm_num
283 _ < goldenRatio⁻¹ := h)
284 · have h := phi_inv_lt
285 exact le_of_lt (by calc goldenRatio⁻¹ < (0.6186 : ℝ) := h
286 _ = ((6186 / 10000 : ℚ) : ℝ) := by norm_num)
287
288/-! ## Higher powers using Fibonacci recurrence φ^(n+2) = φ^(n+1) + φ^n -/
289
290/-- φ³ = φ² + φ = (φ + 1) + φ = 2φ + 1 -/
291theorem phi_cubed_eq : goldenRatio ^ 3 = 2 * goldenRatio + 1 := by
292 have h : goldenRatio ^ 2 = goldenRatio + 1 := goldenRatio_sq
293 calc goldenRatio ^ 3 = goldenRatio ^ 2 * goldenRatio := by ring
294 _ = (goldenRatio + 1) * goldenRatio := by rw [h]
295 _ = goldenRatio ^ 2 + goldenRatio := by ring
296 _ = (goldenRatio + 1) + goldenRatio := by rw [h]
297 _ = 2 * goldenRatio + 1 := by ring
298
299theorem phi_cubed_gt : (4.236 : ℝ) < goldenRatio ^ 3 := by
300 rw [phi_cubed_eq]
301 have h := phi_gt_1618
302 linarith
303
304theorem phi_cubed_lt : goldenRatio ^ 3 < (4.237 : ℝ) := by
305 rw [phi_cubed_eq]
306 have h := phi_lt_16185
307 linarith
308
309/-- φ⁴ = φ³ + φ² = (2φ + 1) + (φ + 1) = 3φ + 2 -/
310theorem phi_pow4_eq : goldenRatio ^ 4 = 3 * goldenRatio + 2 := by
311 have h2 : goldenRatio ^ 2 = goldenRatio + 1 := goldenRatio_sq
312 have h3 : goldenRatio ^ 3 = 2 * goldenRatio + 1 := phi_cubed_eq
313 calc goldenRatio ^ 4 = goldenRatio ^ 3 * goldenRatio := by ring
314 _ = (2 * goldenRatio + 1) * goldenRatio := by rw [h3]
315 _ = 2 * goldenRatio ^ 2 + goldenRatio := by ring
316 _ = 2 * (goldenRatio + 1) + goldenRatio := by rw [h2]
317 _ = 3 * goldenRatio + 2 := by ring
318
319theorem phi_pow4_gt : (6.854 : ℝ) < goldenRatio ^ 4 := by
320 rw [phi_pow4_eq]
321 have h := phi_gt_1618
322 linarith
323
324theorem phi_pow4_lt : goldenRatio ^ 4 < (6.856 : ℝ) := by
325 rw [phi_pow4_eq]
326 have h := phi_lt_16185
327 linarith
328
329/-- φ⁵ = φ⁴ + φ³ = (3φ + 2) + (2φ + 1) = 5φ + 3 -/
330theorem phi_pow5_eq : goldenRatio ^ 5 = 5 * goldenRatio + 3 := by
331 have h3 : goldenRatio ^ 3 = 2 * goldenRatio + 1 := phi_cubed_eq
332 have h4 : goldenRatio ^ 4 = 3 * goldenRatio + 2 := phi_pow4_eq
333 calc goldenRatio ^ 5 = goldenRatio ^ 4 * goldenRatio := by ring
334 _ = (3 * goldenRatio + 2) * goldenRatio := by rw [h4]
335 _ = 3 * goldenRatio ^ 2 + 2 * goldenRatio := by ring
336 _ = 3 * (goldenRatio + 1) + 2 * goldenRatio := by rw [goldenRatio_sq]
337 _ = 5 * goldenRatio + 3 := by ring
338
339theorem phi_pow5_gt : (11.09 : ℝ) < goldenRatio ^ 5 := by
340 rw [phi_pow5_eq]
341 have h := phi_gt_1618
342 linarith
343
344theorem phi_pow5_lt : goldenRatio ^ 5 < (11.1 : ℝ) := by
345 rw [phi_pow5_eq]
346 have h := phi_lt_16185
347 linarith
348
349/-- φ⁶ = 8φ + 5 -/
350theorem phi_pow6_eq : goldenRatio ^ 6 = 8 * goldenRatio + 5 := by
351 have h2 : goldenRatio ^ 2 = goldenRatio + 1 := goldenRatio_sq
352 have h4 : goldenRatio ^ 4 = 3 * goldenRatio + 2 := phi_pow4_eq
353 calc goldenRatio ^ 6 = goldenRatio ^ 4 * goldenRatio ^ 2 := by ring
354 _ = (3 * goldenRatio + 2) * (goldenRatio + 1) := by rw [h4, h2]
355 _ = 3 * goldenRatio ^ 2 + 5 * goldenRatio + 2 := by ring
356 _ = 3 * (goldenRatio + 1) + 5 * goldenRatio + 2 := by rw [h2]
357 _ = 8 * goldenRatio + 5 := by ring
358
359/-- φ⁷ = 13φ + 8 -/
360theorem phi_pow7_eq : goldenRatio ^ 7 = 13 * goldenRatio + 8 := by
361 have h2 : goldenRatio ^ 2 = goldenRatio + 1 := goldenRatio_sq
362 have h5 : goldenRatio ^ 5 = 5 * goldenRatio + 3 := phi_pow5_eq
363 calc goldenRatio ^ 7 = goldenRatio ^ 5 * goldenRatio ^ 2 := by ring
364 _ = (5 * goldenRatio + 3) * (goldenRatio + 1) := by rw [h5, h2]
365 _ = 5 * goldenRatio ^ 2 + 8 * goldenRatio + 3 := by ring
366 _ = 5 * (goldenRatio + 1) + 8 * goldenRatio + 3 := by rw [h2]
367 _ = 13 * goldenRatio + 8 := by ring
368
369/-- φ⁸ = F₈·φ + F₇ = 21φ + 13 (where F_n is Fibonacci) -/
370theorem phi_pow8_eq : goldenRatio ^ 8 = 21 * goldenRatio + 13 := by
371 -- φ⁶ = 8φ + 5, φ⁷ = 13φ + 8, φ⁸ = 21φ + 13
372 have h2 : goldenRatio ^ 2 = goldenRatio + 1 := goldenRatio_sq
373 have h4 : goldenRatio ^ 4 = 3 * goldenRatio + 2 := phi_pow4_eq
374 calc goldenRatio ^ 8 = goldenRatio ^ 4 * goldenRatio ^ 4 := by ring
375 _ = (3 * goldenRatio + 2) * (3 * goldenRatio + 2) := by rw [h4]
376 _ = 9 * goldenRatio ^ 2 + 12 * goldenRatio + 4 := by ring
377 _ = 9 * (goldenRatio + 1) + 12 * goldenRatio + 4 := by rw [h2]
378 _ = 21 * goldenRatio + 13 := by ring
379
380theorem phi_pow8_gt : (46.97 : ℝ) < goldenRatio ^ 8 := by
381 rw [phi_pow8_eq]
382 have h := phi_gt_1618
383 linarith
384
385theorem phi_pow8_lt : goldenRatio ^ 8 < (46.99 : ℝ) := by
386 rw [phi_pow8_eq]
387 have h := phi_lt_16185
388 linarith
389
390/-- Interval containing φ⁸ - PROVEN -/
391def phi_pow8_interval_proven : Interval where
392 lo := 4697 / 100
393 hi := 4699 / 100
394 valid := by norm_num
395
396theorem phi_pow8_in_interval_proven : phi_pow8_interval_proven.contains (goldenRatio ^ 8) := by
397 simp only [Interval.contains, phi_pow8_interval_proven]
398 constructor
399 · have h := phi_pow8_gt
400 exact le_of_lt (by calc ((4697 / 100 : ℚ) : ℝ) = (46.97 : ℝ) := by norm_num
401 _ < goldenRatio ^ 8 := h)
402 · have h := phi_pow8_lt
403 exact le_of_lt (by calc goldenRatio ^ 8 < (46.99 : ℝ) := h
404 _ = ((4699 / 100 : ℚ) : ℝ) := by norm_num)
405
406/-! ## Negative powers using (φ⁻¹)^n -/
407
408/-- (φ⁻¹)² bounds -/
409theorem phi_inv2_gt : (0.381 : ℝ) < goldenRatio⁻¹ ^ 2 := by
410 have h := phi_inv_gt
411 have hpos : 0 < goldenRatio⁻¹ := inv_pos.mpr goldenRatio_pos
412 nlinarith [sq_nonneg goldenRatio⁻¹]
413
414theorem phi_inv2_lt : goldenRatio⁻¹ ^ 2 < (0.383 : ℝ) := by
415 have h := phi_inv_lt
416 have hpos : 0 < goldenRatio⁻¹ := inv_pos.mpr goldenRatio_pos
417 nlinarith [sq_nonneg goldenRatio⁻¹]
418
419/-- (φ⁻¹)³ bounds -/
420theorem phi_inv3_gt : (0.2359 : ℝ) < goldenRatio⁻¹ ^ 3 := by
421 have h1 := phi_inv_gt
422 have h2 := phi_inv2_gt
423 have hpos : 0 < goldenRatio⁻¹ := inv_pos.mpr goldenRatio_pos
424 have hpos2 : 0 < goldenRatio⁻¹ ^ 2 := sq_pos_of_pos hpos
425 nlinarith [sq_nonneg goldenRatio⁻¹]
426
427theorem phi_inv3_lt : goldenRatio⁻¹ ^ 3 < (0.237 : ℝ) := by
428 have h1 := phi_inv_lt
429 have h2 := phi_inv2_lt
430 have hpos : 0 < goldenRatio⁻¹ := inv_pos.mpr goldenRatio_pos
431 nlinarith [sq_nonneg goldenRatio⁻¹]
432
433/-- Interval containing (φ⁻¹)³ - PROVEN -/
434def phi_inv3_interval_proven : Interval where
435 lo := 2359 / 10000
436 hi := 237 / 1000
437 valid := by norm_num
438
439theorem phi_inv3_in_interval_proven : phi_inv3_interval_proven.contains (goldenRatio⁻¹ ^ 3) := by
440 simp only [Interval.contains, phi_inv3_interval_proven]
441 constructor
442 · have h := phi_inv3_gt
443 exact le_of_lt (by calc ((2359 / 10000 : ℚ) : ℝ) = (0.2359 : ℝ) := by norm_num
444 _ < goldenRatio⁻¹ ^ 3 := h)
445 · have h := phi_inv3_lt
446 exact le_of_lt (by calc goldenRatio⁻¹ ^ 3 < (0.237 : ℝ) := h
447 _ = ((237 / 1000 : ℚ) : ℝ) := by norm_num)
448
449/-! ## Direct bounds for φ^(-3) (zpow form)
450
451Some physics modules use `phi ^ (-3 : ℤ)` directly (rather than `(phi⁻¹)^3`), so we provide
452an explicit, proven envelope in zpow form.
453
454This replaces the legacy `Numerics/Interval.lean` theorem `phi_inv3_zpow_bounds`. -/
455
456theorem phi_inv3_zpow_bounds :
457 (0.2360 : ℝ) < goldenRatio ^ (-3 : ℤ) ∧ goldenRatio ^ (-3 : ℤ) < (0.2361 : ℝ) := by
458 -- Rewrite φ^(-3) as the inverse of φ^3 and use φ^3 = 2φ + 1.
459 have h3 : goldenRatio ^ (3 : ℕ) = 2 * goldenRatio + 1 := phi_cubed_eq
460 have hz : goldenRatio ^ (-3 : ℤ) = (goldenRatio ^ (3 : ℕ))⁻¹ := by
461 simpa using (zpow_neg_coe_of_pos goldenRatio (by norm_num : 0 < (3 : ℕ)))
462 have hz' : goldenRatio ^ (-3 : ℤ) = (2 * goldenRatio + 1)⁻¹ := by
463 rw [hz, h3]
464
465 -- Bounds on 2φ + 1 from the bundled φ bounds.
466 have hlo : (4.2360679 : ℝ) < 2 * goldenRatio + 1 := by
467 have hφ := phi_tight_bounds.1
468 linarith
469 have hhi : 2 * goldenRatio + 1 < (4.2360680 : ℝ) := by
470 have hφ := phi_tight_bounds.2
471 linarith
472 have hpos : (0 : ℝ) < 2 * goldenRatio + 1 := lt_trans (by norm_num) hlo
473
474 -- Invert the inequalities.
475 have h_lower : (1 / (4.2360680 : ℝ)) < (2 * goldenRatio + 1)⁻¹ := by
476 have := one_div_lt_one_div_of_lt hpos hhi
477 simpa [one_div] using this
478 have h_upper : (2 * goldenRatio + 1)⁻¹ < (1 / (4.2360679 : ℝ)) := by
479 have hpos_lo : (0 : ℝ) < (4.2360679 : ℝ) := by norm_num
480 have := one_div_lt_one_div_of_lt hpos_lo hlo
481 simpa [one_div] using this
482
483 constructor
484 · have hnum : (0.2360 : ℝ) < 1 / (4.2360680 : ℝ) := by norm_num
485 have : (0.2360 : ℝ) < (2 * goldenRatio + 1)⁻¹ := lt_trans hnum h_lower
486 simpa [hz'] using this
487 · have hnum : (1 / (4.2360679 : ℝ)) < (0.2361 : ℝ) := by norm_num
488 have : (2 * goldenRatio + 1)⁻¹ < (0.2361 : ℝ) := lt_trans h_upper hnum
489 simpa [hz'] using this
490
491/-- (φ⁻¹)⁵ bounds - using 0.381 * 0.2359 ≈ 0.0899 -/
492theorem phi_inv5_gt : (0.089 : ℝ) < goldenRatio⁻¹ ^ 5 := by
493 have h2 := phi_inv2_gt
494 have h3 := phi_inv3_gt
495 have hpos : 0 < goldenRatio⁻¹ := inv_pos.mpr goldenRatio_pos
496 have hpos2 : 0 < goldenRatio⁻¹ ^ 2 := sq_pos_of_pos hpos
497 have hpos3 : 0 < goldenRatio⁻¹ ^ 3 := pow_pos hpos 3
498 have h : goldenRatio⁻¹ ^ 5 = goldenRatio⁻¹ ^ 2 * goldenRatio⁻¹ ^ 3 := by ring
499 nlinarith
500
501theorem phi_inv5_lt : goldenRatio⁻¹ ^ 5 < (0.091 : ℝ) := by
502 have h2 := phi_inv2_lt
503 have h3 := phi_inv3_lt
504 have hpos : 0 < goldenRatio⁻¹ := inv_pos.mpr goldenRatio_pos
505 have hpos2 : 0 < goldenRatio⁻¹ ^ 2 := sq_pos_of_pos hpos
506 have hpos3 : 0 < goldenRatio⁻¹ ^ 3 := pow_pos hpos 3
507 have h : goldenRatio⁻¹ ^ 5 = goldenRatio⁻¹ ^ 2 * goldenRatio⁻¹ ^ 3 := by ring
508 nlinarith
509
510/-- Interval containing (φ⁻¹)⁵ - PROVEN -/
511def phi_inv5_interval_proven : Interval where
512 lo := 89 / 1000
513 hi := 91 / 1000
514 valid := by norm_num
515
516theorem phi_inv5_in_interval_proven : phi_inv5_interval_proven.contains (goldenRatio⁻¹ ^ 5) := by
517 simp only [Interval.contains, phi_inv5_interval_proven]
518 constructor
519 · have h := phi_inv5_gt
520 exact le_of_lt (by calc ((89 / 1000 : ℚ) : ℝ) = (0.089 : ℝ) := by norm_num
521 _ < goldenRatio⁻¹ ^ 5 := h)
522 · have h := phi_inv5_lt
523 exact le_of_lt (by calc goldenRatio⁻¹ ^ 5 < (0.091 : ℝ) := h
524 _ = ((91 / 1000 : ℚ) : ℝ) := by norm_num)
525
526/-! ## Higher powers for φ^16 -/
527
528/-- φ^16 = F₁₆·φ + F₁₅ = 987φ + 610 -/
529theorem phi_pow16_eq : goldenRatio ^ 16 = 987 * goldenRatio + 610 := by
530 have h2 : goldenRatio ^ 2 = goldenRatio + 1 := goldenRatio_sq
531 have h8 : goldenRatio ^ 8 = 21 * goldenRatio + 13 := phi_pow8_eq
532 calc goldenRatio ^ 16 = goldenRatio ^ 8 * goldenRatio ^ 8 := by ring
533 _ = (21 * goldenRatio + 13) * (21 * goldenRatio + 13) := by rw [h8]
534 _ = 441 * goldenRatio ^ 2 + 546 * goldenRatio + 169 := by ring
535 _ = 441 * (goldenRatio + 1) + 546 * goldenRatio + 169 := by rw [h2]
536 _ = 987 * goldenRatio + 610 := by ring
537
538theorem phi_pow16_gt : (2206.9 : ℝ) < goldenRatio ^ 16 := by
539 rw [phi_pow16_eq]
540 have h := phi_gt_1618
541 linarith
542
543theorem phi_pow16_lt : goldenRatio ^ 16 < (2207.5 : ℝ) := by
544 rw [phi_pow16_eq]
545 have h := phi_lt_16185
546 linarith
547
548/-- φ^51 = F₅₁·φ + F₅₀ = 20365011074·φ + 12586269025 -/
549theorem phi_pow51_eq : goldenRatio ^ 51 = 20365011074 * goldenRatio + 12586269025 := by
550 have h :=
551 (Real.goldenRatio_mul_fib_succ_add_fib 50 :
552 goldenRatio * (Nat.fib 51 : ℝ) + Nat.fib 50 = goldenRatio ^ 51)
553 have fib51 : (Nat.fib 51 : ℝ) = 20365011074 := by norm_num
554 have fib50 : (Nat.fib 50 : ℝ) = 12586269025 := by norm_num
555 simpa [fib51, fib50, mul_comm, mul_left_comm, add_comm, add_left_comm, add_assoc] using h.symm
556
557theorem phi_pow51_gt : (45537548334 : ℝ) < goldenRatio ^ 51 := by
558 rw [phi_pow51_eq]
559 have hphi := phi_gt_161803395
560 linarith
561
562theorem phi_pow51_lt : goldenRatio ^ 51 < (45537549354 : ℝ) := by
563 rw [phi_pow51_eq]
564 have h := phi_lt_16180340
565 linarith
566
567def phi_pow51_interval_proven : Interval where
568 lo := 45537548334
569 hi := 45537549354
570 valid := by norm_num
571
572theorem phi_pow51_in_interval_proven :
573 phi_pow51_interval_proven.contains (goldenRatio ^ 51) := by
574 simp [Interval.contains, phi_pow51_interval_proven, phi_pow51_gt, phi_pow51_lt, le_of_lt]
575
576/-! ## φ^54 bounds (for neutrino mass predictions) -/
577
578/-- φ^54 = φ^51 × φ^3 -/
579theorem phi_pow54_eq : goldenRatio ^ 54 = goldenRatio ^ 51 * goldenRatio ^ 3 := by
580 ring_nf
581
582/-- φ^54 > 192894126000 (using φ^51 > 45536856942 and φ^3 > 4.236) -/
583theorem phi_pow54_gt : (192894126000 : ℝ) < goldenRatio ^ 54 := by
584 rw [phi_pow54_eq]
585 have h51 := phi_pow51_gt -- 45536856942 < φ^51
586 have h3 := phi_cubed_gt -- 4.236 < φ^3
587 have hpos51 : (0 : ℝ) < goldenRatio ^ 51 := by positivity
588 have hpos3 : (0 : ℝ) < goldenRatio ^ 3 := by positivity
589 -- 45536856942 * 4.236 = 192894126006.312 > 192894126000
590 calc (192894126000 : ℝ) < (45536856942 : ℝ) * (4.236 : ℝ) := by norm_num
591 _ < goldenRatio ^ 51 * (4.236 : ℝ) := by nlinarith
592 _ < goldenRatio ^ 51 * goldenRatio ^ 3 := by nlinarith
593
594/-- φ^54 < 192983018016 (using φ^51 < 45547089449 and φ^3 < 4.237) -/
595theorem phi_pow54_lt : goldenRatio ^ 54 < (192983018016 : ℝ) := by
596 rw [phi_pow54_eq]
597 have h51 := phi_pow51_lt -- φ^51 < 45547089449
598 have h3 := phi_cubed_lt -- φ^3 < 4.237
599 have hpos51 : (0 : ℝ) < goldenRatio ^ 51 := by positivity
600 have hpos3 : (0 : ℝ) < goldenRatio ^ 3 := by positivity
601 -- 45547089449 * 4.237 = 192983018015.413 < 192983018016
602 calc goldenRatio ^ 51 * goldenRatio ^ 3 < (45547089449 : ℝ) * goldenRatio ^ 3 := by nlinarith
603 _ < (45547089449 : ℝ) * (4.237 : ℝ) := by nlinarith
604 _ < (192983018016 : ℝ) := by norm_num
605
606/-! ## φ^(-54) bounds (for neutrino mass predictions) -/
607
608/-- φ^(-54) > 5.181e-12 (using φ^54 < 192983018016) -/
609theorem phi_neg54_gt : (5.181e-12 : ℝ) < goldenRatio ^ (-54 : ℤ) := by
610 have h := phi_pow54_lt -- φ^54 < 192983018016
611 have hpos : (0 : ℝ) < goldenRatio ^ 54 := by positivity
612 have heq : goldenRatio ^ (-54 : ℤ) = (goldenRatio ^ 54)⁻¹ :=
613 zpow_neg_coe_of_pos goldenRatio (by norm_num : 0 < 54)
614 rw [heq]
615 -- 1/192983018016 > 5.181e-12
616 have h1 : (5.181e-12 : ℝ) < 1 / (192983018016 : ℝ) := by norm_num
617 have h2 : 1 / (192983018016 : ℝ) < 1 / goldenRatio ^ 54 :=
618 one_div_lt_one_div_of_lt hpos h
619 have h3 : 1 / goldenRatio ^ 54 = (goldenRatio ^ 54)⁻¹ := one_div _
620 linarith
621
622/-- φ^(-54) < 5.185e-12 (using φ^54 > 192894126000) -/
623theorem phi_neg54_lt : goldenRatio ^ (-54 : ℤ) < (5.185e-12 : ℝ) := by
624 have h := phi_pow54_gt -- 192894126000 < φ^54
625 have hpos_bound : (0 : ℝ) < 192894126000 := by norm_num
626 have heq : goldenRatio ^ (-54 : ℤ) = (goldenRatio ^ 54)⁻¹ :=
627 zpow_neg_coe_of_pos goldenRatio (by norm_num : 0 < 54)
628 rw [heq]
629 -- 1/192894126000 < 5.185e-12
630 have h1 : (goldenRatio ^ 54)⁻¹ < (192894126000 : ℝ)⁻¹ :=
631 inv_strictAnti₀ hpos_bound h
632 have h2 : (192894126000 : ℝ)⁻¹ < (5.185e-12 : ℝ) := by norm_num
633 linarith
634
635/-! ## φ^58 bounds (for neutrino mass predictions) -/
636
637/-- φ^58 = φ^54 × φ^4 -/
638theorem phi_pow58_eq : goldenRatio ^ 58 = goldenRatio ^ 54 * goldenRatio ^ 4 := by
639 ring_nf
640
641/-- φ^58 > 1.3219e12 (using φ^54 > 192894126000 and φ^4 > 6.854) -/
642theorem phi_pow58_gt : (1.3219e12 : ℝ) < goldenRatio ^ 58 := by
643 rw [phi_pow58_eq]
644 have h54 := phi_pow54_gt -- 192894126000 < φ^54
645 have h4 := phi_pow4_gt -- 6.854 < φ^4
646 have hpos54 : (0 : ℝ) < goldenRatio ^ 54 := by positivity
647 have hpos4 : (0 : ℝ) < goldenRatio ^ 4 := by positivity
648 -- 192894126000 * 6.854 = 1321900000000.0
649 calc (1.3219e12 : ℝ) ≤ (192894126000 : ℝ) * (6.854 : ℝ) := by norm_num
650 _ < goldenRatio ^ 54 * (6.854 : ℝ) := by nlinarith
651 _ < goldenRatio ^ 54 * goldenRatio ^ 4 := by nlinarith
652
653/-- φ^58 < 1.324e12 (using φ^54 < 192983018016 and φ^4 < 6.86) -/
654theorem phi_pow58_lt : goldenRatio ^ 58 < (1.324e12 : ℝ) := by
655 rw [phi_pow58_eq]
656 have h54 := phi_pow54_lt -- φ^54 < 192983018016
657 have h4 := phi_pow4_lt -- φ^4 < 6.86
658 have hpos54 : (0 : ℝ) < goldenRatio ^ 54 := by positivity
659 have hpos4 : (0 : ℝ) < goldenRatio ^ 4 := by positivity
660 calc goldenRatio ^ 54 * goldenRatio ^ 4 < (192983018016 : ℝ) * goldenRatio ^ 4 := by nlinarith
661 _ < (192983018016 : ℝ) * (6.86 : ℝ) := by nlinarith
662 _ < (1.324e12 : ℝ) := by norm_num
663
664/-! ## φ^(-58) bounds (for neutrino mass predictions) -/
665
666/-- φ^(-58) > 7.55e-13 (using φ^58 < 1.324e12) -/
667theorem phi_neg58_gt : (7.55e-13 : ℝ) < goldenRatio ^ (-58 : ℤ) := by
668 have h := phi_pow58_lt -- φ^58 < 1.324e12
669 have hpos : (0 : ℝ) < goldenRatio ^ 58 := by positivity
670 have heq : goldenRatio ^ (-58 : ℤ) = (goldenRatio ^ 58)⁻¹ :=
671 zpow_neg_coe_of_pos goldenRatio (by norm_num : 0 < 58)
672 rw [heq]
673 have h1 : (7.55e-13 : ℝ) < 1 / (1.324e12 : ℝ) := by norm_num
674 have h2 : 1 / (1.324e12 : ℝ) < 1 / goldenRatio ^ 58 :=
675 one_div_lt_one_div_of_lt hpos h
676 have h3 : 1 / goldenRatio ^ 58 = (goldenRatio ^ 58)⁻¹ := one_div _
677 linarith
678
679/-- φ^(-58) < 7.57e-13 (using φ^58 > 1.3219e12) -/
680theorem phi_neg58_lt : goldenRatio ^ (-58 : ℤ) < (7.57e-13 : ℝ) := by
681 have h := phi_pow58_gt -- 1.3219e12 < φ^58
682 have hpos_bound : (0 : ℝ) < 1.3219e12 := by norm_num
683 have heq : goldenRatio ^ (-58 : ℤ) = (goldenRatio ^ 58)⁻¹ :=
684 zpow_neg_coe_of_pos goldenRatio (by norm_num : 0 < 58)
685 rw [heq]
686 have h1 : (goldenRatio ^ 58)⁻¹ < (1.3219e12 : ℝ)⁻¹ :=
687 inv_strictAnti₀ hpos_bound h
688 have h2 : (1.3219e12 : ℝ)⁻¹ < (7.57e-13 : ℝ) := by norm_num
689 linarith
690
691/-! ## Quarter-step derived bounds (φ^(-217/4), φ^(-231/4))
692
693These are the first interval-style lemmas needed to support **quarter/half-ladder**
694neutrino rungs without numeric axioms.
695
696Strategy:
697- use proven integer-power bounds (e.g. `phi_neg54_gt/lt`, `phi_neg58_gt/lt`)
698- use proven quarter-root bounds (`phi_quarter_bounds`, `phi_neg_quarter_bounds`)
699- combine via `Real.rpow_add` and monotone multiplication
700-/
701
702private lemma qhi_pos : (0 : ℝ) < phi_quarter_hi := by
703 simp [phi_quarter_hi]; norm_num
704
705private lemma qlo_pos : (0 : ℝ) < phi_quarter_lo := by
706 simp [phi_quarter_lo]; norm_num
707
708/-- Lower bound for \(φ^{-217/4} = φ^{-54}·φ^{-1/4}\). -/
709theorem phi_neg2174_gt : (4.593e-12 : ℝ) < goldenRatio ^ (((-217 : ℚ) / 4 : ℚ) : ℝ) := by
710 -- Split exponent: -217/4 = -54 - 1/4 (in simp-normal form: -54 + -(4⁻¹))
711 have hexp : (((-217 : ℚ) / 4 : ℚ) : ℝ) = (-54 : ℝ) + (-(4⁻¹ : ℝ)) := by
712 norm_num
713 have hposφ : (0 : ℝ) < goldenRatio := by simpa using Real.goldenRatio_pos
714 have hsplit :
715 goldenRatio ^ (((-217 : ℚ) / 4 : ℚ) : ℝ)
716 = goldenRatio ^ (-54 : ℝ) * goldenRatio ^ (-(4⁻¹ : ℝ)) := by
717 simpa [hexp] using (Real.rpow_add hposφ (-54 : ℝ) (-(4⁻¹ : ℝ)))
718 -- Convert φ^(-54:ℝ) to zpow for reuse of existing bounds.
719 have hz54 : goldenRatio ^ (-54 : ℝ) = goldenRatio ^ (-54 : ℤ) := by
720 rw [← Real.rpow_intCast]
721 norm_cast
722 have h54_lo : (5.181e-12 : ℝ) < goldenRatio ^ (-54 : ℝ) := by
723 simpa [hz54] using phi_neg54_gt
724 have hq := phi_neg_quarter_bounds
725 have hq_lo : (1 / phi_quarter_hi) < goldenRatio ^ (-(4⁻¹ : ℝ)) := by
726 -- `simp` normalizes `-(1/4)` to `-(4⁻¹)`
727 simpa using hq.1
728 have hq_pos : (0 : ℝ) < (1 / phi_quarter_hi) := by
729 exact one_div_pos.2 qhi_pos
730 have hφ54_pos : (0 : ℝ) < goldenRatio ^ (-54 : ℝ) := by
731 linarith [h54_lo]
732 -- Numeric: 4.593e-12 < 5.181e-12 * (1/phi_quarter_hi)
733 have hnum : (4.593e-12 : ℝ) < (5.181e-12 : ℝ) * (1 / phi_quarter_hi) := by
734 simp [phi_quarter_hi]
735 norm_num
736 -- Propagate bounds to the product.
737 have hstep1 : (5.181e-12 : ℝ) * (1 / phi_quarter_hi) < (goldenRatio ^ (-54 : ℝ)) * (1 / phi_quarter_hi) :=
738 mul_lt_mul_of_pos_right h54_lo hq_pos
739 have hstep2 : (goldenRatio ^ (-54 : ℝ)) * (1 / phi_quarter_hi) < (goldenRatio ^ (-54 : ℝ)) * (goldenRatio ^ (-(4⁻¹ : ℝ))) :=
740 mul_lt_mul_of_pos_left hq_lo hφ54_pos
741 -- Finish.
742 rw [hsplit]
743 exact lt_trans hnum (lt_trans hstep1 hstep2)
744
745/-- Upper bound for \(φ^{-217/4} = φ^{-54}·φ^{-1/4}\). -/
746theorem phi_neg2174_lt : goldenRatio ^ (((-217 : ℚ) / 4 : ℚ) : ℝ) < (4.598e-12 : ℝ) := by
747 have hexp : (((-217 : ℚ) / 4 : ℚ) : ℝ) = (-54 : ℝ) + (-(4⁻¹ : ℝ)) := by
748 norm_num
749 have hposφ : (0 : ℝ) < goldenRatio := by simpa using Real.goldenRatio_pos
750 have hsplit :
751 goldenRatio ^ (((-217 : ℚ) / 4 : ℚ) : ℝ)
752 = goldenRatio ^ (-54 : ℝ) * goldenRatio ^ (-(4⁻¹ : ℝ)) := by
753 simpa [hexp] using (Real.rpow_add hposφ (-54 : ℝ) (-(4⁻¹ : ℝ)))
754 have hz54 : goldenRatio ^ (-54 : ℝ) = goldenRatio ^ (-54 : ℤ) := by
755 rw [← Real.rpow_intCast]
756 norm_cast
757 have h54_hi : goldenRatio ^ (-54 : ℝ) < (5.185e-12 : ℝ) := by
758 simpa [hz54] using phi_neg54_lt
759 have hq := phi_neg_quarter_bounds
760 have hq_hi : goldenRatio ^ (-(4⁻¹ : ℝ)) < (1 / phi_quarter_lo) := by
761 simpa using hq.2
762 have hφq_pos : (0 : ℝ) < goldenRatio ^ (-(4⁻¹ : ℝ)) := by
763 have : (0 : ℝ) < goldenRatio := by simpa using Real.goldenRatio_pos
764 exact Real.rpow_pos_of_pos this _
765 -- bound product
766 have hstep1 : (goldenRatio ^ (-54 : ℝ)) * (goldenRatio ^ (-(4⁻¹ : ℝ))) < (5.185e-12 : ℝ) * (goldenRatio ^ (-(4⁻¹ : ℝ))) :=
767 mul_lt_mul_of_pos_right h54_hi hφq_pos
768 have hstep2 : (5.185e-12 : ℝ) * (goldenRatio ^ (-(4⁻¹ : ℝ))) < (5.185e-12 : ℝ) * (1 / phi_quarter_lo) :=
769 mul_lt_mul_of_pos_left hq_hi (by norm_num : (0 : ℝ) < (5.185e-12 : ℝ))
770 have hnum : (5.185e-12 : ℝ) * (1 / phi_quarter_lo) < (4.598e-12 : ℝ) := by
771 simp [phi_quarter_lo]
772 norm_num
773 rw [hsplit]
774 exact lt_trans (lt_trans hstep1 hstep2) hnum
775
776/-- Lower bound for \(φ^{-231/4} = φ^{-58}·φ^{1/4}\). -/
777theorem phi_neg2314_gt : (8.514e-13 : ℝ) < goldenRatio ^ (((-231 : ℚ) / 4 : ℚ) : ℝ) := by
778 have hexp : (((-231 : ℚ) / 4 : ℚ) : ℝ) = (-58 : ℝ) + (4⁻¹ : ℝ) := by
779 norm_num
780 have hposφ : (0 : ℝ) < goldenRatio := by simpa using Real.goldenRatio_pos
781 have hsplit :
782 goldenRatio ^ (((-231 : ℚ) / 4 : ℚ) : ℝ)
783 = goldenRatio ^ (-58 : ℝ) * goldenRatio ^ (4⁻¹ : ℝ) := by
784 simpa [hexp] using (Real.rpow_add hposφ (-58 : ℝ) (4⁻¹ : ℝ))
785 have hz58 : goldenRatio ^ (-58 : ℝ) = goldenRatio ^ (-58 : ℤ) := by
786 rw [← Real.rpow_intCast]
787 norm_cast
788 have h58_lo : (7.55e-13 : ℝ) < goldenRatio ^ (-58 : ℝ) := by
789 simpa [hz58] using phi_neg58_gt
790 have hq := phi_quarter_bounds
791 have hq_lo : phi_quarter_lo < goldenRatio ^ (4⁻¹ : ℝ) := by
792 simpa using hq.1
793 have hq_pos : (0 : ℝ) < phi_quarter_lo := qlo_pos
794 have hφ58_pos : (0 : ℝ) < goldenRatio ^ (-58 : ℝ) := by
795 linarith [h58_lo]
796 -- 7.55e-13 * 1.12783847 = 8.5151804485e-13 > 8.514e-13
797 have hnum : (8.514e-13 : ℝ) < (7.55e-13 : ℝ) * phi_quarter_lo := by
798 simp [phi_quarter_lo]
799 norm_num
800 have hstep1 : (7.55e-13 : ℝ) * phi_quarter_lo < (goldenRatio ^ (-58 : ℝ)) * phi_quarter_lo :=
801 mul_lt_mul_of_pos_right h58_lo hq_pos
802 have hstep2 : (goldenRatio ^ (-58 : ℝ)) * phi_quarter_lo < (goldenRatio ^ (-58 : ℝ)) * (goldenRatio ^ (4⁻¹ : ℝ)) :=
803 mul_lt_mul_of_pos_left hq_lo hφ58_pos
804 rw [hsplit]
805 exact lt_trans hnum (lt_trans hstep1 hstep2)
806
807/-- Upper bound for \(φ^{-231/4} = φ^{-58}·φ^{1/4}\). -/
808theorem phi_neg2314_lt : goldenRatio ^ (((-231 : ℚ) / 4 : ℚ) : ℝ) < (8.538e-13 : ℝ) := by
809 have hexp : (((-231 : ℚ) / 4 : ℚ) : ℝ) = (-58 : ℝ) + (4⁻¹ : ℝ) := by
810 norm_num
811 have hposφ : (0 : ℝ) < goldenRatio := by simpa using Real.goldenRatio_pos
812 have hsplit :
813 goldenRatio ^ (((-231 : ℚ) / 4 : ℚ) : ℝ)
814 = goldenRatio ^ (-58 : ℝ) * goldenRatio ^ (4⁻¹ : ℝ) := by
815 simpa [hexp] using (Real.rpow_add hposφ (-58 : ℝ) (4⁻¹ : ℝ))
816 have hz58 : goldenRatio ^ (-58 : ℝ) = goldenRatio ^ (-58 : ℤ) := by
817 rw [← Real.rpow_intCast]
818 norm_cast
819 have h58_hi : goldenRatio ^ (-58 : ℝ) < (7.57e-13 : ℝ) := by
820 simpa [hz58] using phi_neg58_lt
821 have hq := phi_quarter_bounds
822 have hq_hi : goldenRatio ^ (4⁻¹ : ℝ) < phi_quarter_hi := by
823 simpa using hq.2
824 have hφq_pos : (0 : ℝ) < goldenRatio ^ (4⁻¹ : ℝ) := by
825 have : (0 : ℝ) < goldenRatio := by simpa using Real.goldenRatio_pos
826 exact Real.rpow_pos_of_pos this _
827 have hstep1 : (goldenRatio ^ (-58 : ℝ)) * (goldenRatio ^ (4⁻¹ : ℝ)) < (7.57e-13 : ℝ) * (goldenRatio ^ (4⁻¹ : ℝ)) :=
828 mul_lt_mul_of_pos_right h58_hi hφq_pos
829 have hstep2 : (7.57e-13 : ℝ) * (goldenRatio ^ (4⁻¹ : ℝ)) < (7.57e-13 : ℝ) * phi_quarter_hi :=
830 mul_lt_mul_of_pos_left hq_hi (by norm_num : (0 : ℝ) < (7.57e-13 : ℝ))
831 have hnum : (7.57e-13 : ℝ) * phi_quarter_hi < (8.538e-13 : ℝ) := by
832 simp [phi_quarter_hi]
833 norm_num
834 rw [hsplit]
835 exact lt_trans (lt_trans hstep1 hstep2) hnum
836
837/-! ## φ⁶ bounds (mass verification) -/
838
839theorem phi_pow6_gt : (17.944 : ℝ) < goldenRatio ^ 6 := by
840 rw [phi_pow6_eq]; linarith [phi_gt_1618]
841
842theorem phi_pow6_lt : goldenRatio ^ 6 < (17.948 : ℝ) := by
843 rw [phi_pow6_eq]; linarith [phi_lt_16185]
844
845/-! ## φ^32 bounds (proton mass verification)
846
847φ^32 = (φ^16)². -/
848
849theorem phi_pow32_gt : (4870400 : ℝ) < goldenRatio ^ 32 := by
850 have heq : goldenRatio ^ 32 = goldenRatio ^ 16 * goldenRatio ^ 16 := by ring_nf
851 rw [heq]
852 have h16 := phi_pow16_gt
853 have hpos : (0 : ℝ) < goldenRatio ^ 16 := by positivity
854 calc (4870400 : ℝ) < (2206.9 : ℝ) * (2206.9 : ℝ) := by norm_num
855 _ < goldenRatio ^ 16 * (2206.9 : ℝ) := by nlinarith
856 _ < goldenRatio ^ 16 * goldenRatio ^ 16 := by nlinarith
857
858theorem phi_pow32_lt : goldenRatio ^ 32 < (4873100 : ℝ) := by
859 have heq : goldenRatio ^ 32 = goldenRatio ^ 16 * goldenRatio ^ 16 := by ring_nf
860 rw [heq]
861 have h16 := phi_pow16_lt
862 have hpos : (0 : ℝ) < goldenRatio ^ 16 := by positivity
863 calc goldenRatio ^ 16 * goldenRatio ^ 16
864 < (2207.5 : ℝ) * goldenRatio ^ 16 := by nlinarith
865 _ < (2207.5 : ℝ) * (2207.5 : ℝ) := by nlinarith
866 _ < (4873100 : ℝ) := by norm_num
867
868/-! ## φ^43 bounds (proton mass verification)
869
870φ^43 = φ^32 × φ^8 × φ^3. -/
871
872theorem phi_pow43_gt : (969030000 : ℝ) < goldenRatio ^ 43 := by
873 have heq : goldenRatio ^ 43 = goldenRatio ^ 32 * goldenRatio ^ 8 * goldenRatio ^ 3 := by ring_nf
874 rw [heq]
875 have h32 := phi_pow32_gt
876 have h8 := phi_pow8_gt
877 have h3 := phi_cubed_gt
878 have hpos32 : (0 : ℝ) < goldenRatio ^ 32 := by positivity
879 have hpos32x8 : (0 : ℝ) < goldenRatio ^ 32 * goldenRatio ^ 8 := by positivity
880 have h40 : (4870400 : ℝ) * (46.97 : ℝ) < goldenRatio ^ 32 * goldenRatio ^ 8 :=
881 mul_lt_mul h32 (le_of_lt h8) (by norm_num) (le_of_lt hpos32)
882 have h43 : (4870400 : ℝ) * (46.97 : ℝ) * (4.236 : ℝ) <
883 goldenRatio ^ 32 * goldenRatio ^ 8 * goldenRatio ^ 3 :=
884 mul_lt_mul h40 (le_of_lt h3) (by norm_num) (le_of_lt hpos32x8)
885 have hnum : (969030000 : ℝ) < (4870400 : ℝ) * (46.97 : ℝ) * (4.236 : ℝ) := by norm_num
886 linarith
887
888theorem phi_pow43_lt : goldenRatio ^ 43 < (970320000 : ℝ) := by
889 have heq : goldenRatio ^ 43 = goldenRatio ^ 32 * goldenRatio ^ 8 * goldenRatio ^ 3 := by ring_nf
890 rw [heq]
891 have h32 := phi_pow32_lt
892 have h8 := phi_pow8_lt
893 have h3 := phi_cubed_lt
894 have hpos8 : (0 : ℝ) < goldenRatio ^ 8 := by positivity
895 have hpos3 : (0 : ℝ) < goldenRatio ^ 3 := by positivity
896 have h40 : goldenRatio ^ 32 * goldenRatio ^ 8 < (4873100 : ℝ) * (46.99 : ℝ) :=
897 mul_lt_mul h32 (le_of_lt h8) hpos8 (by norm_num)
898 have h43 : goldenRatio ^ 32 * goldenRatio ^ 8 * goldenRatio ^ 3 <
899 (4873100 : ℝ) * (46.99 : ℝ) * (4.237 : ℝ) :=
900 mul_lt_mul h40 (le_of_lt h3) hpos3 (by norm_num)
901 have hnum : (4873100 : ℝ) * (46.99 : ℝ) * (4.237 : ℝ) < (970320000 : ℝ) := by norm_num
902 linarith
903
904/-! ## φ^59 bounds (electron mass verification)
905
906φ^59 = φ^51 × φ^8. We compose existing bounds on each factor. -/
907
908theorem phi_pow59_gt : (2138898000000 : ℝ) < goldenRatio ^ 59 := by
909 have heq : goldenRatio ^ 59 = goldenRatio ^ 51 * goldenRatio ^ 8 := by ring_nf
910 rw [heq]
911 have h51 := phi_pow51_gt
912 have h8 := phi_pow8_gt
913 have hpos51 : (0 : ℝ) < goldenRatio ^ 51 := by positivity
914 calc (2138898000000 : ℝ) < (45537548334 : ℝ) * (46.97 : ℝ) := by norm_num
915 _ < goldenRatio ^ 51 * (46.97 : ℝ) := by nlinarith
916 _ < goldenRatio ^ 51 * goldenRatio ^ 8 := by nlinarith
917
918theorem phi_pow59_lt : goldenRatio ^ 59 < (2139810000000 : ℝ) := by
919 have heq : goldenRatio ^ 59 = goldenRatio ^ 51 * goldenRatio ^ 8 := by ring_nf
920 rw [heq]
921 have h51 := phi_pow51_lt
922 have h8 := phi_pow8_lt
923 have hpos8 : (0 : ℝ) < goldenRatio ^ 8 := by positivity
924 calc goldenRatio ^ 51 * goldenRatio ^ 8
925 < (45537549354 : ℝ) * goldenRatio ^ 8 := by nlinarith
926 _ < (45537549354 : ℝ) * (46.99 : ℝ) := by nlinarith
927 _ < (2139810000000 : ℝ) := by norm_num
928
929/-! ## φ^70 bounds (muon mass verification)
930
931φ^70 = φ^54 × φ^16. -/
932
933theorem phi_pow70_gt : (425698000000000 : ℝ) < goldenRatio ^ 70 := by
934 have heq : goldenRatio ^ 70 = goldenRatio ^ 54 * goldenRatio ^ 16 := by ring_nf
935 rw [heq]
936 have h54 := phi_pow54_gt
937 have h16 := phi_pow16_gt
938 have hpos54 : (0 : ℝ) < goldenRatio ^ 54 := by positivity
939 calc (425698000000000 : ℝ)
940 < (192894126000 : ℝ) * (2206.9 : ℝ) := by norm_num
941 _ < goldenRatio ^ 54 * (2206.9 : ℝ) := by nlinarith
942 _ < goldenRatio ^ 54 * goldenRatio ^ 16 := by nlinarith
943
944theorem phi_pow70_lt : goldenRatio ^ 70 < (426011000000000 : ℝ) := by
945 have heq : goldenRatio ^ 70 = goldenRatio ^ 54 * goldenRatio ^ 16 := by ring_nf
946 rw [heq]
947 have h54 := phi_pow54_lt
948 have h16 := phi_pow16_lt
949 have hpos16 : (0 : ℝ) < goldenRatio ^ 16 := by positivity
950 calc goldenRatio ^ 54 * goldenRatio ^ 16
951 < (192983018016 : ℝ) * goldenRatio ^ 16 := by nlinarith
952 _ < (192983018016 : ℝ) * (2207.5 : ℝ) := by nlinarith
953 _ < (426011000000000 : ℝ) := by norm_num
954
955/-! ## φ^76 bounds (tau mass verification)
956
957φ^76 = φ^70 × φ^6. -/
958
959theorem phi_pow76_gt : (7638724000000000 : ℝ) < goldenRatio ^ 76 := by
960 have heq : goldenRatio ^ 76 = goldenRatio ^ 70 * goldenRatio ^ 6 := by ring_nf
961 rw [heq]
962 have h70 := phi_pow70_gt
963 have h6 := phi_pow6_gt
964 have hpos70 : (0 : ℝ) < goldenRatio ^ 70 := by positivity
965 calc (7638724000000000 : ℝ)
966 < (425698000000000 : ℝ) * (17.944 : ℝ) := by norm_num
967 _ < goldenRatio ^ 70 * (17.944 : ℝ) := by nlinarith
968 _ < goldenRatio ^ 70 * goldenRatio ^ 6 := by nlinarith
969
970theorem phi_pow76_lt : goldenRatio ^ 76 < (7646046000000000 : ℝ) := by
971 have heq : goldenRatio ^ 76 = goldenRatio ^ 70 * goldenRatio ^ 6 := by ring_nf
972 rw [heq]
973 have h70 := phi_pow70_lt
974 have h6 := phi_pow6_lt
975 have hpos6 : (0 : ℝ) < goldenRatio ^ 6 := by positivity
976 calc goldenRatio ^ 70 * goldenRatio ^ 6
977 < (426011000000000 : ℝ) * goldenRatio ^ 6 := by nlinarith
978 _ < (426011000000000 : ℝ) * (17.948 : ℝ) := by nlinarith
979 _ < (7646046000000000 : ℝ) := by norm_num
980
981/-! ## φ − 1 bounds (preparation for log φ analysis) -/
982
983lemma phi_sub_one_pos : 0 < goldenRatio - 1 := by
984 have h := phi_gt_1618
985 linarith
986
987lemma phi_sub_one_lt_one : goldenRatio - 1 < 1 := by
988 have h := Real.goldenRatio_lt_two
989 linarith
990
991lemma phi_sub_one_mem_Icc : goldenRatio - 1 ∈ Set.Icc (0 : ℝ) 1 := by
992 exact ⟨le_of_lt phi_sub_one_pos, le_of_lt phi_sub_one_lt_one⟩
993
994end IndisputableMonolith.Numerics
995