IndisputableMonolith.RSBridge.GapProperties
IndisputableMonolith/RSBridge/GapProperties.lean · 457 lines · 20 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Constants
3import IndisputableMonolith.RSBridge.Anchor
4
5/-!
6# Properties of the display / structural residue `gap(Z)`
7
8This file provides **Lean-checked** properties of the Recognition/structural residue
9
10 `gap(Z) = log(1 + Z/φ) / log φ`
11
12used throughout the mass framework (a.k.a. `𝓕(Z)` in the papers).
13
14These properties are important because `gap` is the proposed **zero-parameter**
15Recognition-side residue `f^{Rec}`. Unlike the Standard-Model RG residue (which requires
16external kernels), `gap` is definitional and we can verify its algebraic/analytic behavior
17directly in Lean.
18-/
19
20namespace IndisputableMonolith
21namespace RSBridge
22
23open IndisputableMonolith.Constants
24
25noncomputable section
26
27/-! ## Basic identities -/
28
29@[simp] theorem gap_zero : gap (0 : ℤ) = 0 := by
30 simp [gap]
31
32/-!
33`gap` can be rewritten as a shifted log-base-φ:
34
35 `gap(Z) = log_φ(φ + Z) - 1`
36
37for any `Z` with `0 < φ + Z` (in practice all `Z ≥ 0` used in the mass bands).
38-/
39theorem gap_eq_log_phi_add_sub_one {Z : ℤ} (hZ : 0 < (phi + (Z : ℝ))) :
40 gap Z = (Real.log (phi + (Z : ℝ)) / Real.log phi) - 1 := by
41 have hφpos : 0 < phi := phi_pos
42 have hφne : (phi : ℝ) ≠ 0 := ne_of_gt hφpos
43 have hlogφ : Real.log phi ≠ 0 := by
44 have : (1 : ℝ) < phi := one_lt_phi
45 exact ne_of_gt (Real.log_pos this)
46 -- log(1 + Z/φ) = log((φ+Z)/φ) = log(φ+Z) - log(φ)
47 have h1 : (1 + (Z : ℝ) / phi) = (phi + (Z : ℝ)) / phi := by
48 field_simp [hφne]
49 have hpos1 : 0 < (1 + (Z : ℝ) / phi) := by
50 -- since (φ+Z)/φ > 0
51 have : 0 < (phi + (Z : ℝ)) / phi := by
52 exact div_pos hZ hφpos
53 simpa [h1] using this
54 calc
55 gap Z
56 = Real.log (1 + (Z : ℝ) / phi) / Real.log phi := by rfl
57 _ = (Real.log ((phi + (Z : ℝ)) / phi)) / Real.log phi := by simp [h1]
58 _ = (Real.log (phi + (Z : ℝ)) - Real.log phi) / Real.log phi := by
59 simp [Real.log_div, hZ.ne', hφne]
60 _ = (Real.log (phi + (Z : ℝ)) / Real.log phi) - 1 := by
61 field_simp [hlogφ]
62
63/-! ## Monotonicity (verification property) -/
64
65theorem gap_strictMono_on_nonneg :
66 StrictMono fun n : ℕ => gap (n : ℤ) := by
67 intro a b hab
68 -- Convert to reals for monotonicity of log.
69 have hφpos : 0 < phi := phi_pos
70 have hlogφpos : 0 < Real.log phi := Real.log_pos one_lt_phi
71 have ha : 0 < (1 + ((a : ℤ) : ℝ) / phi) := by
72 have : (0 : ℝ) ≤ ((a : ℤ) : ℝ) / phi := by
73 have : (0 : ℝ) ≤ ((a : ℤ) : ℝ) := by exact_mod_cast (Nat.zero_le a)
74 exact div_nonneg this (le_of_lt hφpos)
75 linarith
76 have hlt : (1 + ((a : ℤ) : ℝ) / phi) < (1 + ((b : ℤ) : ℝ) / phi) := by
77 have hab' : ((a : ℤ) : ℝ) < ((b : ℤ) : ℝ) := by exact_mod_cast hab
78 have : ((a : ℤ) : ℝ) / phi < ((b : ℤ) : ℝ) / phi :=
79 (div_lt_div_of_pos_right hab' hφpos)
80 linarith
81 have hlog : Real.log (1 + ((a : ℤ) : ℝ) / phi) < Real.log (1 + ((b : ℤ) : ℝ) / phi) :=
82 Real.log_lt_log ha hlt
83 -- divide by positive log(phi)
84 have := (div_lt_div_of_pos_right hlog hlogφpos)
85 simpa [gap] using this
86
87/-! ## Band ordering (structural sanity checks) -/
88
89theorem gap_24_lt_gap_276 : gap (24 : ℤ) < gap (276 : ℤ) := by
90 have hmono := gap_strictMono_on_nonneg
91 -- 24 < 276 in ℕ
92 have : (24 : ℕ) < (276 : ℕ) := by decide
93 simpa using hmono this
94
95theorem gap_276_lt_gap_1332 : gap (276 : ℤ) < gap (1332 : ℤ) := by
96 have hmono := gap_strictMono_on_nonneg
97 have : (276 : ℕ) < (1332 : ℕ) := by decide
98 simpa using hmono this
99
100/-! ## Concavity / diminishing increments -/
101
102/-- Real-extension of the display function on `ℝ` (used for concavity statements). -/
103noncomputable def gapR (x : ℝ) : ℝ :=
104 Real.log (1 + x / phi) / Real.log phi
105
106@[simp] theorem gapR_nat (n : ℕ) : gapR (n : ℝ) = gap (n : ℤ) := by
107 simp [gapR, gap]
108
109/-- `gapR` is strictly concave on `[0,∞)`. -/
110theorem strictConcaveOn_gapR_Ici : StrictConcaveOn ℝ (Set.Ici (0 : ℝ)) gapR := by
111 -- Reduce to strict concavity of `Real.log` on `(0,∞)` and use an injective affine reparametrization.
112 let g : ℝ → ℝ := Real.log
113 have hlog : StrictConcaveOn ℝ (Set.Ioi (0 : ℝ)) g := strictConcaveOn_log_Ioi
114
115 have hφpos : 0 < phi := phi_pos
116 have hφne : (phi : ℝ) ≠ 0 := ne_of_gt hφpos
117 have hlogφpos : 0 < Real.log phi := Real.log_pos one_lt_phi
118 have hlogφne : Real.log phi ≠ 0 := ne_of_gt hlogφpos
119
120 -- affine map h(x) = 1 + x/phi
121 let hlin : ℝ →ₗ[ℝ] ℝ := (LinearMap.id : ℝ →ₗ[ℝ] ℝ).smulRight (1 / phi)
122 let h : ℝ →ᵃ[ℝ] ℝ :=
123 AffineMap.mk (toFun := fun x => 1 + x / phi) (linear := hlin) (map_vadd' := by
124 intro p v
125 -- v +ᵥ p = v + p in ℝ-torsor
126 simp [hlin, add_div, hφne]
127 ring)
128
129 -- helper: h maps Ici 0 into Ioi 0
130 have h_img0 : ∀ {x : ℝ}, x ∈ Set.Ici (0 : ℝ) → h x ∈ Set.Ioi (0 : ℝ) := by
131 intro x hx
132 have hx0 : 0 ≤ x := hx
133 have hx_div : 0 ≤ x / phi := div_nonneg hx0 (le_of_lt hφpos)
134 have : (0 : ℝ) < 1 + x / phi := by linarith
135 simpa [h] using this
136
137 -- injectivity of h on Ici 0
138 have h_inj : Set.InjOn h (Set.Ici (0 : ℝ)) := by
139 intro x hx y hy hxy
140 have hEq : (1 + x / phi) = (1 + y / phi) := by simpa [h] using hxy
141 have hDiv : x / phi = y / phi := by
142 have h' := congrArg (fun t => t - 1) hEq
143 simpa using h'
144 have hm : (x / phi) * phi = (y / phi) * phi := congrArg (fun t => t * phi) hDiv
145 simpa [div_eq_mul_inv, hφne, mul_assoc] using hm
146
147 -- strict concavity of log ∘ h on Ici 0
148 have h_log_comp : StrictConcaveOn ℝ (Set.Ici (0 : ℝ)) (g ∘ h) := by
149 refine ⟨convex_Ici (0 : ℝ), ?_⟩
150 intro x hx y hy hxy a b ha hb hab
151 have hx' : h x ∈ Set.Ioi (0 : ℝ) := h_img0 hx
152 have hy' : h y ∈ Set.Ioi (0 : ℝ) := h_img0 hy
153 have hxy' : h x ≠ h y := by
154 intro hEq
155 exact hxy (h_inj hx hy hEq)
156 have hh : a * h x + b * h y = h (a * x + b * y) := by
157 simpa [smul_eq_mul] using (Convex.combo_affine_apply (f := h) hab).symm
158 -- Apply strict concavity of log and rewrite via hh
159 have h0 := hlog.2 hx' hy' hxy' ha hb hab
160 -- `h0` is about `log (a • h x + b • h y)`; rewrite that argument via `hh`.
161 simpa [Function.comp, smul_eq_mul, hh] using h0
162
163 -- scale by positive constant: gapR = (1/log φ) * (log ∘ h)
164 refine ⟨h_log_comp.1, ?_⟩
165 intro x hx y hy hxy a b ha hb hab
166 have hc : 0 < (1 / Real.log phi) := one_div_pos.2 hlogφpos
167 have hbase := h_log_comp.2 hx hy hxy ha hb hab
168 -- rewrite `gapR` as a constant multiple of `log (h x)`
169 have hdef : ∀ t : ℝ, gapR t = (1 / Real.log phi) * g (h t) := by
170 intro t
171 simp [gapR, g, h, div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]
172 -- multiply strict inequality by positive constant and distribute
173 have hmul : (1 / Real.log phi) * (a * (g (h x)) + b * (g (h y))) <
174 (1 / Real.log phi) * (g (h (a • x + b • y))) := by
175 -- `smul` on ℝ is multiplication; `hbase` is already in that form
176 have := mul_lt_mul_of_pos_left hbase hc
177 -- rewrite scalar multiplications
178 simpa [smul_eq_mul, mul_add, add_mul, mul_assoc, mul_left_comm, mul_comm] using this
179 -- convert back to gapR and finish
180 -- LHS: a*gapR x + b*gapR y ; RHS: gapR(a•x + b•y)
181 have : a * gapR x + b * gapR y < gapR (a • x + b • y) := by
182 -- rewrite all gapR occurrences using hdef, then use hmul
183 simpa [hdef, smul_eq_mul, mul_add, add_mul, mul_assoc, mul_left_comm, mul_comm] using hmul
184 simpa [StrictConcaveOn, smul_eq_mul] using this
185
186/-!
187Diminishing increments: for `n ≥ 0`, the discrete first differences decrease.
188
189This is the discrete shadow of strict concavity:
190\[
191 \Fgap(n+2)-\Fgap(n+1) < \Fgap(n+1)-\Fgap(n).
192\]
193-/
194theorem gap_diminishing_increments (n : ℕ) :
195 gap ((n + 2 : ℕ) : ℤ) - gap ((n + 1 : ℕ) : ℤ) <
196 gap ((n + 1 : ℕ) : ℤ) - gap (n : ℤ) := by
197 -- Use slope inequality for strict concave functions on ℝ with x=n, y=n+1, z=n+2.
198 have hsc := strictConcaveOn_gapR_Ici
199 have hx : (n : ℝ) ∈ Set.Ici (0 : ℝ) := by
200 simpa [Set.mem_Ici] using (show (0 : ℝ) ≤ (n : ℝ) from by exact_mod_cast (Nat.zero_le n))
201 have hy : ((n + 1 : ℕ) : ℝ) ∈ Set.Ici (0 : ℝ) := by
202 simpa [Set.mem_Ici] using (show (0 : ℝ) ≤ ((n + 1 : ℕ) : ℝ) from by exact_mod_cast (Nat.zero_le (n + 1)))
203 have hz : ((n + 2 : ℕ) : ℝ) ∈ Set.Ici (0 : ℝ) := by
204 simpa [Set.mem_Ici] using (show (0 : ℝ) ≤ ((n + 2 : ℕ) : ℝ) from by exact_mod_cast (Nat.zero_le (n + 2)))
205 have hxy : (n : ℝ) < ((n + 1 : ℕ) : ℝ) := by
206 exact_mod_cast (Nat.lt_succ_self n)
207 have hyz : ((n + 1 : ℕ) : ℝ) < ((n + 2 : ℕ) : ℝ) := by
208 exact_mod_cast (Nat.lt_succ_self (n + 1))
209 have hslope :
210 (gapR ((n + 2 : ℕ) : ℝ) - gapR ((n + 1 : ℕ) : ℝ)) /
211 (((n + 2 : ℕ) : ℝ) - ((n + 1 : ℕ) : ℝ)) <
212 (gapR ((n + 1 : ℕ) : ℝ) - gapR (n : ℝ)) /
213 (((n + 1 : ℕ) : ℝ) - (n : ℝ)) :=
214 StrictConcaveOn.slope_anti_adjacent hsc (hx := hx) (hz := hz) hxy hyz
215 -- simplify denominators (both are 1), noting simp may rewrite `((n+1:ℕ):ℝ)` as `↑n + 1`
216 have hslope' : gapR ((n + 2 : ℕ) : ℝ) - gapR ((n + 1 : ℕ) : ℝ) <
217 gapR ((n + 1 : ℕ) : ℝ) - gapR (n : ℝ) := by
218 -- First simplify the denominators to explicit numerals, then discharge them with `norm_num`.
219 have hs' :
220 (gapR (↑n + 2) - gapR (↑n + 1)) / ((2 : ℝ) - 1) <
221 (gapR (↑n + 1) - gapR (n : ℝ)) / ((1 : ℝ) - 0) := by
222 -- `simp` rewrites casts like `((n+1:ℕ):ℝ)` into `↑n + 1`.
223 -- It also rewrites the differences of successive naturals into numerals.
224 simpa [Nat.cast_add, Nat.cast_ofNat, add_assoc, add_left_comm, add_comm] using hslope
225 have hdenL : ((2 : ℝ) - 1) = (1 : ℝ) := by norm_num
226 have hdenR : ((1 : ℝ) - 0) = (1 : ℝ) := by norm_num
227 -- remove the divisions by 1
228 simpa [hdenL, hdenR, div_one] using hs'
229 -- rewrite back from `gapR` on naturals to `gap` on integers.
230 -- We do this with explicit `simp` so the rewriting doesn't get stuck on expressions like `↑n + k`.
231 have hfinal :
232 gap ((n + 2 : ℕ) : ℤ) - gap ((n + 1 : ℕ) : ℤ) <
233 gap ((n + 1 : ℕ) : ℤ) - gap (n : ℤ) := by
234 -- `simp` likes to rewrite `((n+k:ℕ):ℝ)` into `↑n + k`, which prevents `gapR_nat` from firing.
235 -- So we rewrite *back* to the `(n+k : ℕ)` cast form first, then apply `gapR_nat`.
236 have hslope_cast :
237 gapR (↑n + 2) - gapR (↑n + 1) < gapR (↑n + 1) - gapR (n : ℝ) := by
238 -- avoid `simp` here (it can loop on casts); use `rw` with explicit cast equalities.
239 have h1 : ((n + 1 : ℕ) : ℝ) = (↑n + 1 : ℝ) := by norm_num
240 have h2 : ((n + 2 : ℕ) : ℝ) = (↑n + 2 : ℝ) := by norm_num
241 have h := hslope'
242 -- rewrite nat-casts into `↑n + k`
243 rw [h1, h2] at h
244 exact h
245
246 have hcast1 : (↑n + 1 : ℝ) = ((n + 1 : ℕ) : ℝ) := by norm_num
247 have hcast2 : (↑n + 2 : ℝ) = ((n + 2 : ℕ) : ℝ) := by norm_num
248
249 -- rewrite the inequality into the nat-cast form
250 have hslope_nat :
251 gapR ((n + 2 : ℕ) : ℝ) - gapR ((n + 1 : ℕ) : ℝ) <
252 gapR ((n + 1 : ℕ) : ℝ) - gapR (n : ℝ) := by
253 have h := hslope_cast
254 -- rewrite `↑n + k` back into `((n+k):ℕ):ℝ`
255 rw [hcast1, hcast2] at h
256 exact h
257
258 -- finally, apply `gapR_nat` on the three natural arguments (using `rw` to avoid cast rewriting).
259 have h := hslope_nat
260 rw [gapR_nat (n + 2), gapR_nat (n + 1), gapR_nat n] at h
261 simpa using h
262 exact hfinal
263
264theorem gap_second_difference_neg (n : ℕ) :
265 gap ((n + 2 : ℕ) : ℤ) + gap (n : ℤ) < 2 * gap ((n + 1 : ℕ) : ℤ) := by
266 have h := gap_diminishing_increments (n := n)
267 -- rearrange: g(n+2) - g(n+1) < g(n+1) - g(n) ↔ g(n+2) + g(n) < 2 g(n+1)
268 linarith
269
270end
271
272/-! ## Numerical interval bounds for canonical bands
273
274The following theorems establish verified numerical bounds for the `gap` function
275at the canonical Z-values (24, 276, 1332) used in the three fermion mass bands.
276
277These are structured as certified intervals matching the style in
278`Physics/ElectronMass/Necessity.lean`.
279-/
280
281section IntervalBounds
282
283/-! ### Foundational bounds on φ and log(φ)
284
285These numerical bounds are used to certify interval arithmetic for gap values.
286The bounds on φ come from √5 computation; bounds on log(φ) are represented as hypotheses
287as they require Taylor polynomial evaluation (see Physics/ElectronMass/Necessity.lean
288for the full proof machinery).
289-/
290
291/-- φ is bounded: φ ∈ (1.618033, 1.618034) -/
292lemma phi_bounds : (1.618033 : ℝ) < phi ∧ phi < (1.618034 : ℝ) := by
293 -- φ = (1 + √5)/2
294 -- We need: 2.236066 < √5 < 2.236068
295 have sqrt5_lower : (2.236066 : ℝ) < Real.sqrt 5 := by
296 have h : (2.236066 : ℝ)^2 < 5 := by norm_num
297 have h_pos : (0 : ℝ) ≤ 2.236066 := by norm_num
298 rw [← Real.sqrt_sq h_pos]
299 exact Real.sqrt_lt_sqrt (by norm_num) h
300 have sqrt5_upper : Real.sqrt 5 < (2.236068 : ℝ) := by
301 have h : (5 : ℝ) < (2.236068)^2 := by norm_num
302 have h_pos : (0 : ℝ) ≤ 2.236068 := by norm_num
303 rw [← Real.sqrt_sq h_pos]
304 exact Real.sqrt_lt_sqrt (by positivity) h
305 constructor
306 · -- Lower bound
307 have h : (1.618033 : ℝ) < (1 + Real.sqrt 5) / 2 := by
308 have : (1 : ℝ) + 2.236066 < 1 + Real.sqrt 5 := by linarith
309 linarith
310 simp only [phi]
311 exact h
312 · -- Upper bound
313 have h : (1 + Real.sqrt 5) / 2 < (1.618034 : ℝ) := by
314 have : (1 : ℝ) + Real.sqrt 5 < 1 + 2.236068 := by linarith
315 linarith
316 simp only [phi]
317 exact h
318
319/-- Hypothesis: log(1.618033) > 0.481211 (verified externally via Taylor expansion) -/
320def log_lower_bound_phi_hypothesis : Prop := (0.481211 : ℝ) < Real.log (1.618033 : ℝ)
321
322/-- Hypothesis: log(1.618034) < 0.481213 (verified externally via Taylor expansion) -/
323def log_upper_bound_phi_hypothesis : Prop := Real.log (1.618034 : ℝ) < (0.481213 : ℝ)
324
325/-- log(φ) is bounded: log(φ) ∈ (0.481211, 0.481213) -/
326lemma log_phi_bounds (h_low : log_lower_bound_phi_hypothesis) (h_high : log_upper_bound_phi_hypothesis) :
327 (0.481211 : ℝ) < Real.log phi ∧ Real.log phi < (0.481213 : ℝ) := by
328 have hphi := phi_bounds
329 have h_low' : (0.481211 : ℝ) < Real.log (1.618033 : ℝ) := by
330 simpa [log_lower_bound_phi_hypothesis] using h_low
331 have h_high' : Real.log (1.618034 : ℝ) < (0.481213 : ℝ) := by
332 simpa [log_upper_bound_phi_hypothesis] using h_high
333 constructor
334 · -- Lower bound: log(φ) > log(1.618033) > 0.481211
335 have h_mono : Real.log (1.618033 : ℝ) < Real.log phi := by
336 apply Real.log_lt_log (by norm_num) hphi.1
337 exact lt_trans h_low' h_mono
338 · -- Upper bound: log(φ) < log(1.618034) < 0.481213
339 have h_mono : Real.log phi < Real.log (1.618034 : ℝ) := by
340 apply Real.log_lt_log (by linarith [hphi.1]) hphi.2
341 exact lt_trans h_mono h_high'
342
343/-! ### Auxiliary numerical log bounds -/
344
345/-- Hypothesis for numerical lower bound: log(1 + 24/1.618034) > 2.7613 -/
346def log_15p83_lower_hypothesis : Prop := (2.7613 : ℝ) < Real.log (1 + 24 / (1.618034 : ℝ))
347
348/-- Hypothesis for numerical upper bound: log(1 + 24/1.618033) < 2.7615 -/
349def log_15p83_upper_hypothesis : Prop := Real.log (1 + 24 / (1.618033 : ℝ)) < (2.7615 : ℝ)
350
351/-- Hypothesis for numerical lower bound: log(1 + 276/1.618034) > 5.1442 -/
352def log_171p6_lower_hypothesis : Prop := (5.1442 : ℝ) < Real.log (1 + 276 / (1.618034 : ℝ))
353
354/-- Hypothesis for numerical upper bound: log(1 + 276/1.618033) < 5.1444 -/
355def log_171p6_upper_hypothesis : Prop := Real.log (1 + 276 / (1.618033 : ℝ)) < (5.1444 : ℝ)
356
357/-- Bounds on gap(24). -/
358lemma gap_24_bounds
359 (h_low_phi : log_lower_bound_phi_hypothesis)
360 (h_high_phi : log_upper_bound_phi_hypothesis)
361 (h_low_24 : log_15p83_lower_hypothesis)
362 (h_high_24 : log_15p83_upper_hypothesis) :
363 (5.737 : ℝ) < gap 24 ∧ gap 24 < (5.74 : ℝ) := by
364 simp only [gap]
365 have hphi := phi_bounds
366 have hlogphi := log_phi_bounds h_low_phi h_high_phi
367 have h_phi_pos : 0 < phi := phi_pos
368 have h_log_pos : 0 < Real.log phi := Real.log_pos (by linarith [hphi.1])
369 -- Bounds on 1 + 24/φ
370 have h_arg_lower : 1 + 24 / (1.618034 : ℝ) < 1 + 24 / phi := by
371 have hdiv : (24 : ℝ) / (1.618034 : ℝ) < 24 / phi := by
372 have hpos : (0 : ℝ) < (24 : ℝ) := by norm_num
373 exact div_lt_div_of_pos_left hpos h_phi_pos hphi.2
374 linarith
375 have h_arg_upper : 1 + 24 / phi < 1 + 24 / (1.618033 : ℝ) := by
376 have hdiv : (24 : ℝ) / phi < 24 / (1.618033 : ℝ) := by
377 have hpos : (0 : ℝ) < (24 : ℝ) := by norm_num
378 exact div_lt_div_of_pos_left hpos (by norm_num : (0 : ℝ) < (1.618033 : ℝ)) hphi.1
379 linarith
380 -- Bounds on log(1 + 24/φ) using monotonicity
381 have h_log_lower : Real.log (1 + 24 / (1.618034 : ℝ)) < Real.log (1 + 24 / phi) := by
382 apply Real.log_lt_log (by norm_num) h_arg_lower
383 have h_log_upper : Real.log (1 + 24 / phi) < Real.log (1 + 24 / (1.618033 : ℝ)) := by
384 have h_pos : 0 < 1 + 24 / phi := by positivity
385 apply Real.log_lt_log h_pos h_arg_upper
386 -- Combine with numerical bounds
387 have h_num_lower : (2.7613 : ℝ) < Real.log (1 + 24 / phi) :=
388 lt_trans h_low_24 h_log_lower
389 have h_num_upper : Real.log (1 + 24 / phi) < (2.7615 : ℝ) :=
390 lt_trans h_log_upper h_high_24
391 constructor
392 · -- Lower bound: gap > 5.737
393 have h_chain : 5.737 * Real.log phi < Real.log (1 + 24 / phi) := by
394 have h1 : 5.737 * Real.log phi < 5.737 * 0.481213 := by nlinarith [hlogphi.2]
395 have h2 : (5.737 : ℝ) * 0.481213 < 2.7613 := by norm_num
396 linarith
397 exact (lt_div_iff₀ h_log_pos).mpr h_chain
398 · -- Upper bound: gap < 5.74
399 have h_chain : Real.log (1 + 24 / phi) < 5.74 * Real.log phi := by
400 have h1 : 5.74 * 0.481211 < 5.74 * Real.log phi := by nlinarith [hlogphi.1]
401 have h2 : (2.7615 : ℝ) < 5.74 * 0.481211 := by norm_num
402 linarith
403 exact (div_lt_iff₀ h_log_pos).mpr h_chain
404
405/-- Bounds on gap(276). -/
406lemma gap_276_bounds
407 (h_low_phi : log_lower_bound_phi_hypothesis)
408 (h_high_phi : log_upper_bound_phi_hypothesis)
409 (h_low_276 : log_171p6_lower_hypothesis)
410 (h_high_276 : log_171p6_upper_hypothesis) :
411 (10.689 : ℝ) < gap 276 ∧ gap 276 < (10.691 : ℝ) := by
412 simp only [gap]
413 have hphi := phi_bounds
414 have hlogphi := log_phi_bounds h_low_phi h_high_phi
415 have h_phi_pos : 0 < phi := phi_pos
416 have h_log_pos : 0 < Real.log phi := Real.log_pos (by linarith [hphi.1])
417 -- Bounds on 1 + 276/φ
418 have h_arg_lower : 1 + 276 / (1.618034 : ℝ) < 1 + 276 / phi := by
419 have hdiv : (276 : ℝ) / (1.618034 : ℝ) < 276 / phi := by
420 have hpos : (0 : ℝ) < (276 : ℝ) := by norm_num
421 exact div_lt_div_of_pos_left hpos h_phi_pos hphi.2
422 linarith
423 have h_arg_upper : 1 + 276 / phi < 1 + 276 / (1.618033 : ℝ) := by
424 have hdiv : (276 : ℝ) / phi < 276 / (1.618033 : ℝ) := by
425 have hpos : (0 : ℝ) < (276 : ℝ) := by norm_num
426 exact div_lt_div_of_pos_left hpos (by norm_num : (0 : ℝ) < (1.618033 : ℝ)) hphi.1
427 linarith
428 -- Bounds on log(1 + 276/φ) using monotonicity
429 have h_log_lower : Real.log (1 + 276 / (1.618034 : ℝ)) < Real.log (1 + 276 / phi) := by
430 apply Real.log_lt_log (by norm_num) h_arg_lower
431 have h_log_upper : Real.log (1 + 276 / phi) < Real.log (1 + 276 / (1.618033 : ℝ)) := by
432 have h_pos : 0 < 1 + 276 / phi := by positivity
433 apply Real.log_lt_log h_pos h_arg_upper
434 -- Combine with numerical bounds
435 have h_num_lower : (5.1442 : ℝ) < Real.log (1 + 276 / phi) :=
436 lt_trans h_low_276 h_log_lower
437 have h_num_upper : Real.log (1 + 276 / phi) < (5.1444 : ℝ) :=
438 lt_trans h_log_upper h_high_276
439 constructor
440 · -- Lower bound: gap > 10.689
441 have h_chain : 10.689 * Real.log phi < Real.log (1 + 276 / phi) := by
442 have h1 : 10.689 * Real.log phi < 10.689 * 0.481213 := by nlinarith [hlogphi.2]
443 have h2 : (10.689 : ℝ) * 0.481213 < 5.1442 := by norm_num
444 linarith
445 exact (lt_div_iff₀ h_log_pos).mpr h_chain
446 · -- Upper bound: gap < 10.691
447 have h_chain : Real.log (1 + 276 / phi) < 10.691 * Real.log phi := by
448 have h1 : 10.691 * 0.481211 < 10.691 * Real.log phi := by nlinarith [hlogphi.1]
449 have h2 : (5.1444 : ℝ) < 10.691 * 0.481211 := by norm_num
450 linarith
451 exact (div_lt_iff₀ h_log_pos).mpr h_chain
452
453end IntervalBounds
454
455end RSBridge
456end IndisputableMonolith
457