IndisputableMonolith.Physics.NeutrinoSector
IndisputableMonolith/Physics/NeutrinoSector.lean · 759 lines · 53 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Constants
3import IndisputableMonolith.Constants.ExternalAnchors
4import IndisputableMonolith.Constants.RSNativeUnits
5import IndisputableMonolith.Physics.ElectronMass
6import IndisputableMonolith.Physics.ElectronMass.Necessity
7import IndisputableMonolith.Numerics.Interval.PhiBounds
8import IndisputableMonolith.Support.RungFractions
9
10/-!
11# T14: The Neutrino Sector
12
13This module formalizes the derivation of the neutrino mass scale.
14
15## The Hypothesis
16
17Neutrinos occupy the **Deep Ladder**: integer rungs far below the electron ($R_e = 2$).
18Specifically, they appear to occupy even integers in the -50 range.
19
201. **Mass 3 ($m_3$)**: The atmospheric scale corresponds to $R = -54$.
21 $$ m_3 \approx m_{struct} \cdot \phi^{-54} \approx 0.056 \text{ eV} $$
22 Observed (from $\Delta m^2_{32}$): $\approx 0.050$ eV.
23
242. **Mass 2 ($m_2$)**: The solar scale corresponds to $R = -58$.
25 $$ m_2 \approx m_{struct} \cdot \phi^{-58} \approx 0.0082 \text{ eV} $$
26 Observed (from $\Delta m^2_{21}$): $\approx 0.0086$ eV.
27
28## Interpretation
29
30The residue difference between generations is $\Delta_{32} = 4$.
31This suggests a spacing of 4 rungs, consistent with a quarter-ladder structure
32where the "period" might be integers of 4.
33
34## Unit / calibration note (important)
35
36The quantities in this file are reported in **eV** only after making a *display convention*
37about the charged‑lepton mass scale. Concretely, we reuse `ElectronMass.electron_structural_mass`
38(a dimensionless RS-native quantity) as if it were measured in **MeV**, and then apply
39`MeV_to_eV = 1e6` as a unit conversion.
40
41This is a **calibration/reporting seam**, not a parameter-free derivation of absolute eV scales.
42For a fully explicit SI/eV reporting seam, prefer the RS-native calibration pathway:
43`Constants.RSNativeUnits.ExternalCalibration` and `Measurement.RSNative.Calibration.*`.
44
45-/
46
47namespace IndisputableMonolith
48namespace Physics
49namespace NeutrinoSector
50
51open Real Constants ElectronMass
52open IndisputableMonolith.Support.RungFractions
53
54/-! ## Experimental Values (PDG 2022) -/
55
56/-- Mass squared differences (eV^2). -/
57def dm2_21_exp : ℝ := 7.53e-5
58def dm2_32_exp : ℝ := 2.453e-3
59
60/-- Approximate masses assuming m1 ~ 0. -/
61noncomputable def m2_approx : ℝ := Real.sqrt dm2_21_exp
62noncomputable def m3_approx : ℝ := Real.sqrt dm2_32_exp
63
64/-! ## The Deep Ladder -/
65
66def rung_nu3 : ℤ := -54
67def rung_nu2 : ℤ := -58
68
69/-- Explicit reporting seam for converting the RS structural mass scale to eV. -/
70structure MassDisplayCalibration where
71 eV_per_structural_unit : ℝ
72 eV_per_structural_unit_pos : 0 < eV_per_structural_unit
73
74/-- Legacy display convention: treat `electron_structural_mass` as MeV and convert to eV. -/
75def legacy_mass_display_calibration : MassDisplayCalibration where
76 eV_per_structural_unit := 1e6
77 eV_per_structural_unit_pos := by norm_num
78
79/-- SI-backed display seam from an RS external calibration object.
80 This maps coherence quanta to eV through Joules and the elementary charge. -/
81noncomputable def mass_display_calibration_of_external
82 (cal : Constants.RSNativeUnits.ExternalCalibration) : MassDisplayCalibration where
83 eV_per_structural_unit := cal.joules_per_coh / Constants.ExternalAnchors.e_SI
84 eV_per_structural_unit_pos := by
85 have hcal : 0 < cal.joules_per_coh := cal.joules_pos
86 have he : 0 < Constants.ExternalAnchors.e_SI := by
87 norm_num [Constants.ExternalAnchors.e_SI]
88 exact div_pos hcal he
89
90/-- Backwards-compatible alias for old code paths. -/
91def MeV_to_eV : ℝ := legacy_mass_display_calibration.eV_per_structural_unit
92
93/-- Predicted Mass (eV). -/
94noncomputable def predicted_mass_eV_with
95 (cal : MassDisplayCalibration) (rung : ℤ) : ℝ :=
96 electron_structural_mass * (phi ^ rung) * cal.eV_per_structural_unit
97
98/-- Default predicted mass in eV (legacy convention). -/
99noncomputable def predicted_mass_eV (rung : ℤ) : ℝ :=
100 predicted_mass_eV_with legacy_mass_display_calibration rung
101
102lemma predicted_mass_eV_legacy (rung : ℤ) :
103 predicted_mass_eV rung = electron_structural_mass * (phi ^ rung) * MeV_to_eV := by
104 simp [predicted_mass_eV, predicted_mass_eV_with, MeV_to_eV]
105
106/-!
107## Quarter/half-ladder upgrade (Gap 6 / declared convention seam)
108
109The integer-rung deep ladder above implies a *squared-mass* hierarchy ratio
110approximately \( \phi^8 \) (because \(r_3 - r_2 = 4\)).
111
112However, the experimentally inferred ratio \(Δm^2_{31}/Δm^2_{21}\) is closer to
113\(\phi^7\) than \(\phi^8\).
114
115In a pure φ-power law with \(m_i \propto \phi^{r_i}\) and negligible \(m_1\),
116we have:
117\[
118 \frac{Δm^2_{31}}{Δm^2_{21}} \approx \frac{m_3^2}{m_2^2} = \phi^{2(r_3-r_2)}.
119\]
120So landing on \(\phi^7\) corresponds to **\(r_3-r_2 = 7/2\)**, which requires
121half/quarter rungs.
122
123This section introduces a minimal fractional-rung representation using `ℚ`
124(`Support.RungFractions`) and records a **canonical, parameter-free** choice:
125
126- a fixed **phase offset** of \(-2/8 = -1/4\) (two ticks out of the 8‑tick cycle),
127- a fixed **generation spacing** of \((8-1)/2 = 7/2\).
128
129We keep the integer-rung model above for backwards compatibility and as a
130baseline scaffold. The fractional model is the *target* going forward; numeric
131quarter-step φ-power bounds for these exponents are proved in
132`IndisputableMonolith/Numerics/Interval/PhiBounds.lean` (no numeric axioms).
133-/
134
135/-! ### Canonical fractional rungs (quarter resolution) -/
136
137/-- Neutrino phase offset: \(-2/8\) of an octave = \(-1/4\) rung. -/
138def nu_phase_offset : Rung := (-(2 : ℚ)) / 8
139
140/-- Neutrino spacing for the solar-to-atmospheric gap: \((8-1)/2 = 7/2\) rungs. -/
141def nu_spacing : Rung := ((8 : ℚ) - 1) / 2
142
143lemma nu_phase_offset_eq : nu_phase_offset = (-1 : ℚ) / 4 := by
144 unfold nu_phase_offset
145 norm_num
146
147lemma nu_spacing_eq : nu_spacing = (7 : ℚ) / 2 := by
148 unfold nu_spacing
149 norm_num
150
151/-- Upgraded atmospheric rung: integer base (-54) plus the fixed quarter offset (-1/4). -/
152def res_nu3 : Rung := ofInt rung_nu3 + nu_phase_offset
153
154/-- Upgraded solar rung: enforce \(r_3-r_2 = 7/2\) (→ φ⁷ in squared-mass ratio). -/
155def res_nu2 : Rung := res_nu3 - nu_spacing
156
157/-- Canonical lightest rung spacing: one quarter of the 8‑tick cycle (8/4 = 2 rungs). -/
158def nu1_spacing : Rung := (8 : ℚ) / 4
159
160lemma nu1_spacing_eq : nu1_spacing = (2 : ℚ) := by
161 unfold nu1_spacing
162 norm_num
163
164/-- Upgraded lightest rung: place ν1 two rungs below ν2 (parameter-free 8‑tick quarter). -/
165def res_nu1 : Rung := res_nu2 - nu1_spacing
166
167lemma res_nu3_simp : res_nu3 = (-217 : ℚ) / 4 := by
168 unfold res_nu3
169 -- rung_nu3 = -54, offset = -1/4
170 simp [rung_nu3, nu_phase_offset_eq]
171 norm_num
172
173lemma res_nu2_simp : res_nu2 = (-231 : ℚ) / 4 := by
174 unfold res_nu2
175 -- res_nu3 = -217/4, spacing = 7/2 = 14/4
176 simp [res_nu3_simp, nu_spacing_eq]
177 norm_num
178
179lemma res_nu1_simp : res_nu1 = (-239 : ℚ) / 4 := by
180 unfold res_nu1
181 -- res_nu2 = -231/4, nu1_spacing = 2 = 8/4
182 simp [res_nu2_simp, nu1_spacing_eq]
183 norm_num
184
185theorem rung_gap_21_is_two : res_nu2 - res_nu1 = (2 : ℚ) := by
186 unfold res_nu1
187 simp [nu1_spacing_eq]
188
189/-- Predicted mass in eV for a fractional rung (reporting seam: treat `m_struct` as MeV). -/
190noncomputable def predicted_mass_eV_frac_with
191 (cal : MassDisplayCalibration) (res : Rung) : ℝ :=
192 electron_structural_mass * (phi ^ (toReal res)) * cal.eV_per_structural_unit
193
194/-- Default fractional-rung prediction in eV (legacy convention). -/
195noncomputable def predicted_mass_eV_frac (res : Rung) : ℝ :=
196 predicted_mass_eV_frac_with legacy_mass_display_calibration res
197
198lemma predicted_mass_eV_frac_legacy (res : Rung) :
199 predicted_mass_eV_frac res = electron_structural_mass * (phi ^ (toReal res)) * MeV_to_eV := by
200 simp [predicted_mass_eV_frac, predicted_mass_eV_frac_with, MeV_to_eV]
201
202/-! ### What it takes to land on φ⁷ (symbolic) -/
203
204/-- The upgraded rung gap is exactly \(7/2\), hence the squared-mass ratio is \(φ^7\) in the pure law. -/
205theorem rung_gap_is_seven_halves : res_nu3 - res_nu2 = (7 : ℚ) / 2 := by
206 unfold res_nu2
207 simp [nu_spacing_eq]
208
209/-! ### Rigorous interval bounds for the fractional rungs
210
211We now have **proven** bounds for the required fractional φ-powers in
212`Numerics/Interval/PhiBounds.lean`:
213
214- `phi_neg2174_gt/lt` for \(φ^{-217/4}\)
215- `phi_neg2314_gt/lt` for \(φ^{-231/4}\)
216
217This lets us bound the *fractional* neutrino masses without any numeric axioms.
218
219Note: using the canonical ν1 placement (`nu1_spacing = 2`) we can also bound the derived
220mass-squared splittings in the fractional model (`dm2_21_frac_pred_in_nufit_1sigma`,
221`dm2_31_frac_pred_in_nufit_2sigma`).
222-/
223
224lemma nu3_frac_pred_bounds :
225 (0.04985 : ℝ) < predicted_mass_eV_frac res_nu3 ∧ predicted_mass_eV_frac res_nu3 < (0.04993 : ℝ) := by
226 -- unfold the reporting seam
227 simp only [predicted_mass_eV_frac_legacy, MeV_to_eV, legacy_mass_display_calibration]
228 have h_sm := ElectronMass.Necessity.structural_mass_bounds
229 have h_pow_lo := IndisputableMonolith.Numerics.phi_neg2174_gt
230 have h_pow_hi := IndisputableMonolith.Numerics.phi_neg2174_lt
231 have h_phi_eq : phi = Real.goldenRatio := rfl
232 rw [h_phi_eq]
233 -- rewrite exponent (toReal res_nu3) = (-217/4 : ℝ)
234 have hexp : (toReal res_nu3 : ℝ) = (((-217 : ℚ) / 4 : ℚ) : ℝ) := by
235 simp [toReal, res_nu3_simp]
236 rw [hexp]
237 have hpos_sm : (0 : ℝ) < electron_structural_mass := by linarith [h_sm.1]
238 have hpos_pow : (0 : ℝ) < Real.goldenRatio ^ (((-217 : ℚ) / 4 : ℚ) : ℝ) := by
239 have : (0 : ℝ) < Real.goldenRatio := by simpa using Real.goldenRatio_pos
240 exact Real.rpow_pos_of_pos this _
241 constructor
242 · -- lower bound: 0.04985 < 10856 * 4.593e-12 * 1e6 < m_struct * φ^(-217/4) * 1e6
243 calc (0.04985 : ℝ)
244 < (10856 : ℝ) * (4.593e-12 : ℝ) * (1e6 : ℝ) := by norm_num
245 _ < electron_structural_mass * (4.593e-12 : ℝ) * (1e6 : ℝ) := by nlinarith [h_sm.1]
246 _ < electron_structural_mass * (Real.goldenRatio ^ (((-217 : ℚ) / 4 : ℚ) : ℝ)) * (1e6 : ℝ) := by
247 nlinarith [h_pow_lo, hpos_sm]
248 · -- upper bound: m_struct * φ^(-217/4) * 1e6 < 10858 * 4.598e-12 * 1e6 < 0.04993
249 calc electron_structural_mass * (Real.goldenRatio ^ (((-217 : ℚ) / 4 : ℚ) : ℝ)) * (1e6 : ℝ)
250 < (10858 : ℝ) * (Real.goldenRatio ^ (((-217 : ℚ) / 4 : ℚ) : ℝ)) * (1e6 : ℝ) := by
251 nlinarith [h_sm.2, hpos_pow]
252 _ < (10858 : ℝ) * (4.598e-12 : ℝ) * (1e6 : ℝ) := by
253 nlinarith [h_pow_hi]
254 _ < (0.04993 : ℝ) := by norm_num
255
256lemma nu2_frac_pred_bounds :
257 (0.00924 : ℝ) < predicted_mass_eV_frac res_nu2 ∧ predicted_mass_eV_frac res_nu2 < (0.00928 : ℝ) := by
258 simp only [predicted_mass_eV_frac_legacy, MeV_to_eV, legacy_mass_display_calibration]
259 have h_sm := ElectronMass.Necessity.structural_mass_bounds
260 have h_pow_lo := IndisputableMonolith.Numerics.phi_neg2314_gt
261 have h_pow_hi := IndisputableMonolith.Numerics.phi_neg2314_lt
262 have h_phi_eq : phi = Real.goldenRatio := rfl
263 rw [h_phi_eq]
264 have hexp : (toReal res_nu2 : ℝ) = (((-231 : ℚ) / 4 : ℚ) : ℝ) := by
265 simp [toReal, res_nu2_simp]
266 rw [hexp]
267 have hpos_sm : (0 : ℝ) < electron_structural_mass := by linarith [h_sm.1]
268 have hpos_pow : (0 : ℝ) < Real.goldenRatio ^ (((-231 : ℚ) / 4 : ℚ) : ℝ) := by
269 have : (0 : ℝ) < Real.goldenRatio := by simpa using Real.goldenRatio_pos
270 exact Real.rpow_pos_of_pos this _
271 constructor
272 · calc (0.00924 : ℝ)
273 < (10856 : ℝ) * (8.514e-13 : ℝ) * (1e6 : ℝ) := by norm_num
274 _ < electron_structural_mass * (8.514e-13 : ℝ) * (1e6 : ℝ) := by nlinarith [h_sm.1]
275 _ < electron_structural_mass * (Real.goldenRatio ^ (((-231 : ℚ) / 4 : ℚ) : ℝ)) * (1e6 : ℝ) := by
276 nlinarith [h_pow_lo, hpos_sm]
277 · calc electron_structural_mass * (Real.goldenRatio ^ (((-231 : ℚ) / 4 : ℚ) : ℝ)) * (1e6 : ℝ)
278 < (10858 : ℝ) * (Real.goldenRatio ^ (((-231 : ℚ) / 4 : ℚ) : ℝ)) * (1e6 : ℝ) := by
279 nlinarith [h_sm.2, hpos_pow]
280 _ < (10858 : ℝ) * (8.538e-13 : ℝ) * (1e6 : ℝ) := by
281 nlinarith [h_pow_hi]
282 _ < (0.00928 : ℝ) := by norm_num
283
284lemma nu1_frac_pred_bounds :
285 (0.00352 : ℝ) < predicted_mass_eV_frac res_nu1 ∧ predicted_mass_eV_frac res_nu1 < (0.00355 : ℝ) := by
286 -- Unfold the reporting seam.
287 simp only [predicted_mass_eV_frac_legacy, MeV_to_eV, legacy_mass_display_calibration]
288 have h_sm := ElectronMass.Necessity.structural_mass_bounds
289 have h_phi_eq : phi = Real.goldenRatio := rfl
290 rw [h_phi_eq]
291 -- Split: φ^(r1) = φ^(r2) * φ^(-2).
292 have hposφ : (0 : ℝ) < Real.goldenRatio := by simpa using Real.goldenRatio_pos
293 have hexp : (toReal res_nu1 : ℝ) = (toReal res_nu2 : ℝ) + (-2 : ℝ) := by
294 simp [res_nu1, nu1_spacing_eq, toReal, sub_eq_add_neg]
295 have hsplit :
296 Real.goldenRatio ^ (toReal res_nu1 : ℝ)
297 = Real.goldenRatio ^ (res_nu2 : ℝ) * Real.goldenRatio ^ (-2 : ℝ) := by
298 calc
299 Real.goldenRatio ^ (toReal res_nu1 : ℝ)
300 = Real.goldenRatio ^ ((toReal res_nu2 : ℝ) + (-2 : ℝ)) := by
301 exact congrArg (fun t : ℝ => Real.goldenRatio ^ t) hexp
302 _ = Real.goldenRatio ^ (res_nu2 : ℝ) * Real.goldenRatio ^ (-2 : ℝ) := by
303 simpa using (Real.rpow_add hposφ (toReal res_nu2 : ℝ) (-2 : ℝ))
304
305 -- Bounds for φ^(r2) = φ^(-231/4)
306 have h_r2 : (res_nu2 : ℝ) = (((-231 : ℚ) / 4 : ℚ) : ℝ) := by
307 simpa using congrArg (fun q : ℚ => (q : ℝ)) res_nu2_simp
308 have h_pow_r2_lo : (8.514e-13 : ℝ) < Real.goldenRatio ^ (res_nu2 : ℝ) := by
309 simpa [h_r2] using IndisputableMonolith.Numerics.phi_neg2314_gt
310 have h_pow_r2_hi : Real.goldenRatio ^ (res_nu2 : ℝ) < (8.538e-13 : ℝ) := by
311 simpa [h_r2] using IndisputableMonolith.Numerics.phi_neg2314_lt
312
313 -- Bounds for φ^(-2) (as rpow, derived from the proved zpow bounds).
314 have hz2 : Real.goldenRatio ^ (-2 : ℝ) = Real.goldenRatio ^ (-2 : ℤ) := by
315 rw [← Real.rpow_intCast]
316 norm_cast
317 have h_pow_neg2_lo : (0.3818 : ℝ) < Real.goldenRatio ^ (-2 : ℝ) := by
318 simpa [hz2] using IndisputableMonolith.Numerics.phi_neg2_gt
319 have h_pow_neg2_hi : Real.goldenRatio ^ (-2 : ℝ) < (0.382 : ℝ) := by
320 simpa [hz2] using IndisputableMonolith.Numerics.phi_neg2_lt
321
322 have hpos_sm : (0 : ℝ) < electron_structural_mass := by linarith [h_sm.1]
323 have hpos_r2 : (0 : ℝ) < Real.goldenRatio ^ (res_nu2 : ℝ) := by linarith [h_pow_r2_lo]
324 have hpos_neg2 : (0 : ℝ) < Real.goldenRatio ^ (-2 : ℝ) := by linarith [h_pow_neg2_lo]
325
326 -- Combine product bounds for φ^(r1).
327 have hphi_r1_lo :
328 (8.514e-13 : ℝ) * (0.3818 : ℝ) < Real.goldenRatio ^ (res_nu2 : ℝ) * Real.goldenRatio ^ (-2 : ℝ) := by
329 have hpos_c : (0 : ℝ) < (0.3818 : ℝ) := by norm_num
330 have h1 :
331 (8.514e-13 : ℝ) * (0.3818 : ℝ) < (Real.goldenRatio ^ (res_nu2 : ℝ)) * (0.3818 : ℝ) :=
332 mul_lt_mul_of_pos_right h_pow_r2_lo hpos_c
333 have h2 :
334 (Real.goldenRatio ^ (res_nu2 : ℝ)) * (0.3818 : ℝ)
335 < (Real.goldenRatio ^ (res_nu2 : ℝ)) * (Real.goldenRatio ^ (-2 : ℝ)) :=
336 mul_lt_mul_of_pos_left h_pow_neg2_lo hpos_r2
337 exact lt_trans h1 h2
338
339 have hphi_r1_hi :
340 Real.goldenRatio ^ (res_nu2 : ℝ) * Real.goldenRatio ^ (-2 : ℝ)
341 < (8.538e-13 : ℝ) * (0.382 : ℝ) := by
342 have hpos_b : (0 : ℝ) < Real.goldenRatio ^ (-2 : ℝ) := hpos_neg2
343 have h1 :
344 Real.goldenRatio ^ (res_nu2 : ℝ) * Real.goldenRatio ^ (-2 : ℝ)
345 < (8.538e-13 : ℝ) * Real.goldenRatio ^ (-2 : ℝ) :=
346 mul_lt_mul_of_pos_right h_pow_r2_hi hpos_b
347 have hpos_a : (0 : ℝ) < (8.538e-13 : ℝ) := by norm_num
348 have h2 :
349 (8.538e-13 : ℝ) * Real.goldenRatio ^ (-2 : ℝ) < (8.538e-13 : ℝ) * (0.382 : ℝ) :=
350 mul_lt_mul_of_pos_left h_pow_neg2_hi hpos_a
351 exact lt_trans h1 h2
352
353 -- Now bound the full mass (include `electron_structural_mass` and `1e6`).
354 rw [hsplit]
355 constructor
356 · -- lower
357 calc (0.00352 : ℝ)
358 < (10856 : ℝ) * ((8.514e-13 : ℝ) * (0.3818 : ℝ)) * (1e6 : ℝ) := by norm_num
359 _ < electron_structural_mass * ((8.514e-13 : ℝ) * (0.3818 : ℝ)) * (1e6 : ℝ) := by
360 have hpos_const : (0 : ℝ) < ((8.514e-13 : ℝ) * (0.3818 : ℝ)) * (1e6 : ℝ) := by norm_num
361 have h := mul_lt_mul_of_pos_right h_sm.1 hpos_const
362 simpa [mul_assoc, mul_left_comm, mul_comm] using h
363 _ < electron_structural_mass * (Real.goldenRatio ^ (res_nu2 : ℝ) * Real.goldenRatio ^ (-2 : ℝ)) * (1e6 : ℝ) := by
364 -- scale `hphi_r1_lo` by `electron_structural_mass` and `1e6` (both positive)
365 have hpos_1e6 : (0 : ℝ) < (1e6 : ℝ) := by norm_num
366 have h1 : electron_structural_mass * ((8.514e-13 : ℝ) * (0.3818 : ℝ))
367 < electron_structural_mass * (Real.goldenRatio ^ (res_nu2 : ℝ) * Real.goldenRatio ^ (-2 : ℝ)) :=
368 mul_lt_mul_of_pos_left hphi_r1_lo hpos_sm
369 have h2 := mul_lt_mul_of_pos_right h1 hpos_1e6
370 simpa [mul_assoc, mul_left_comm, mul_comm] using h2
371 · -- upper
372 calc electron_structural_mass * (Real.goldenRatio ^ (res_nu2 : ℝ) * Real.goldenRatio ^ (-2 : ℝ)) * (1e6 : ℝ)
373 < (10858 : ℝ) * (Real.goldenRatio ^ (res_nu2 : ℝ) * Real.goldenRatio ^ (-2 : ℝ)) * (1e6 : ℝ) := by
374 have hpos_prod : (0 : ℝ) < (Real.goldenRatio ^ (res_nu2 : ℝ) * Real.goldenRatio ^ (-2 : ℝ)) * (1e6 : ℝ) := by
375 have hpos_1e6 : (0 : ℝ) < (1e6 : ℝ) := by norm_num
376 have hpos_ab : (0 : ℝ) < Real.goldenRatio ^ (res_nu2 : ℝ) * Real.goldenRatio ^ (-2 : ℝ) :=
377 mul_pos hpos_r2 hpos_neg2
378 exact mul_pos hpos_ab hpos_1e6
379 have h := mul_lt_mul_of_pos_right h_sm.2 hpos_prod
380 simpa [mul_assoc, mul_left_comm, mul_comm] using h
381 _ < (10858 : ℝ) * ((8.538e-13 : ℝ) * (0.382 : ℝ)) * (1e6 : ℝ) := by
382 have hpos_1e6 : (0 : ℝ) < (1e6 : ℝ) := by norm_num
383 have hpos_10858 : (0 : ℝ) < (10858 : ℝ) := by norm_num
384 have h1 : (10858 : ℝ) * (Real.goldenRatio ^ (res_nu2 : ℝ) * Real.goldenRatio ^ (-2 : ℝ))
385 < (10858 : ℝ) * ((8.538e-13 : ℝ) * (0.382 : ℝ)) :=
386 mul_lt_mul_of_pos_left hphi_r1_hi hpos_10858
387 have h2 := mul_lt_mul_of_pos_right h1 hpos_1e6
388 simpa [mul_assoc, mul_left_comm, mul_comm] using h2
389 _ < (0.00355 : ℝ) := by norm_num
390
391/-- Predicted mass-squared splitting \(Δm^2 = m_{\text{hi}}^2 - m_{\text{lo}}^2\). -/
392noncomputable def dm2 (m_hi m_lo : ℝ) : ℝ := m_hi ^ (2 : ℕ) - m_lo ^ (2 : ℕ)
393
394noncomputable def dm2_21_frac_pred : ℝ :=
395 dm2 (predicted_mass_eV_frac res_nu2) (predicted_mass_eV_frac res_nu1)
396
397noncomputable def dm2_31_frac_pred : ℝ :=
398 dm2 (predicted_mass_eV_frac res_nu3) (predicted_mass_eV_frac res_nu1)
399
400/-- Calibration-parameterized Δm²21 prediction (fractional rung model). -/
401noncomputable def dm2_21_frac_pred_with (cal : MassDisplayCalibration) : ℝ :=
402 dm2 (predicted_mass_eV_frac_with cal res_nu2) (predicted_mass_eV_frac_with cal res_nu1)
403
404/-- Calibration-parameterized Δm²31 prediction (fractional rung model). -/
405noncomputable def dm2_31_frac_pred_with (cal : MassDisplayCalibration) : ℝ :=
406 dm2 (predicted_mass_eV_frac_with cal res_nu3) (predicted_mass_eV_frac_with cal res_nu1)
407
408lemma dm2_21_frac_pred_with_legacy :
409 dm2_21_frac_pred_with legacy_mass_display_calibration = dm2_21_frac_pred := by
410 simp [dm2_21_frac_pred_with, dm2_21_frac_pred, predicted_mass_eV_frac]
411
412lemma dm2_31_frac_pred_with_legacy :
413 dm2_31_frac_pred_with legacy_mass_display_calibration = dm2_31_frac_pred := by
414 simp [dm2_31_frac_pred_with, dm2_31_frac_pred, predicted_mass_eV_frac]
415
416/-- Fractional model Δm²21 is consistent with a typical NuFIT 5.2 1σ band (normal ordering). -/
417lemma dm2_21_frac_pred_in_nufit_1sigma :
418 (7.21e-5 : ℝ) < dm2_21_frac_pred ∧ dm2_21_frac_pred < (7.62e-5 : ℝ) := by
419 -- abbreviate
420 let m2 : ℝ := predicted_mass_eV_frac res_nu2
421 let m1 : ℝ := predicted_mass_eV_frac res_nu1
422 have hm2 := nu2_frac_pred_bounds
423 have hm1 := nu1_frac_pred_bounds
424 have hm2_lo : (0.00924 : ℝ) < m2 := by simpa [m2] using hm2.1
425 have hm2_hi : m2 < (0.00928 : ℝ) := by simpa [m2] using hm2.2
426 have hm1_lo : (0.00352 : ℝ) < m1 := by simpa [m1] using hm1.1
427 have hm1_hi : m1 < (0.00355 : ℝ) := by simpa [m1] using hm1.2
428 have hm2_pos : (0 : ℝ) < m2 := lt_trans (by norm_num) hm2_lo
429 have hm1_pos : (0 : ℝ) < m1 := lt_trans (by norm_num) hm1_lo
430
431 -- square bounds
432 have hm2_sq_lo : (0.00924 : ℝ) ^ (2 : ℕ) < m2 ^ (2 : ℕ) := by
433 have habs : |(0.00924 : ℝ)| < |m2| := by
434 simpa [abs_of_pos (by norm_num : (0 : ℝ) < (0.00924 : ℝ)), abs_of_pos hm2_pos] using hm2_lo
435 exact (sq_lt_sq).2 habs
436 have hm2_sq_hi : m2 ^ (2 : ℕ) < (0.00928 : ℝ) ^ (2 : ℕ) := by
437 have habs : |m2| < |(0.00928 : ℝ)| := by
438 have hpos : (0 : ℝ) < (0.00928 : ℝ) := by norm_num
439 simpa [abs_of_pos hm2_pos, abs_of_pos hpos] using hm2_hi
440 exact (sq_lt_sq).2 habs
441 have hm1_sq_lo : (0.00352 : ℝ) ^ (2 : ℕ) < m1 ^ (2 : ℕ) := by
442 have habs : |(0.00352 : ℝ)| < |m1| := by
443 simpa [abs_of_pos (by norm_num : (0 : ℝ) < (0.00352 : ℝ)), abs_of_pos hm1_pos] using hm1_lo
444 exact (sq_lt_sq).2 habs
445 have hm1_sq_hi : m1 ^ (2 : ℕ) < (0.00355 : ℝ) ^ (2 : ℕ) := by
446 have habs : |m1| < |(0.00355 : ℝ)| := by
447 have hpos : (0 : ℝ) < (0.00355 : ℝ) := by norm_num
448 simpa [abs_of_pos hm1_pos, abs_of_pos hpos] using hm1_hi
449 exact (sq_lt_sq).2 habs
450
451 -- unfold the target expression
452 have hdm : dm2_21_frac_pred = (m2 ^ (2 : ℕ)) - (m1 ^ (2 : ℕ)) := by
453 simp [dm2_21_frac_pred, dm2, m2, m1]
454 rw [hdm]
455 constructor
456 · -- lower bound
457 have hnum : (7.21e-5 : ℝ) < (0.00924 : ℝ) ^ (2 : ℕ) - (0.00355 : ℝ) ^ (2 : ℕ) := by
458 norm_num
459 have hstep1 :
460 (0.00924 : ℝ) ^ (2 : ℕ) - (0.00355 : ℝ) ^ (2 : ℕ)
461 < (m2 ^ (2 : ℕ)) - (0.00355 : ℝ) ^ (2 : ℕ) :=
462 sub_lt_sub_right hm2_sq_lo _
463 have hstep2 :
464 (m2 ^ (2 : ℕ)) - (0.00355 : ℝ) ^ (2 : ℕ) < (m2 ^ (2 : ℕ)) - (m1 ^ (2 : ℕ)) := by
465 -- since m1^2 < 0.00355^2, subtracting m1^2 is larger
466 have : -(0.00355 : ℝ) ^ (2 : ℕ) < -(m1 ^ (2 : ℕ)) := by
467 exact neg_lt_neg hm1_sq_hi
468 simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using (add_lt_add_left this (m2 ^ (2 : ℕ)))
469 exact lt_trans hnum (lt_trans hstep1 hstep2)
470 · -- upper bound
471 have hnum : (0.00928 : ℝ) ^ (2 : ℕ) - (0.00352 : ℝ) ^ (2 : ℕ) < (7.62e-5 : ℝ) := by
472 norm_num
473 have hstep1 :
474 (m2 ^ (2 : ℕ)) - (m1 ^ (2 : ℕ))
475 < (0.00928 : ℝ) ^ (2 : ℕ) - (m1 ^ (2 : ℕ)) :=
476 sub_lt_sub_right hm2_sq_hi _
477 have hstep2 :
478 (0.00928 : ℝ) ^ (2 : ℕ) - (m1 ^ (2 : ℕ)) < (0.00928 : ℝ) ^ (2 : ℕ) - (0.00352 : ℝ) ^ (2 : ℕ) := by
479 -- since 0.00352^2 < m1^2, subtracting 0.00352^2 is larger (so this is a strict upper bound)
480 have : -(m1 ^ (2 : ℕ)) < -((0.00352 : ℝ) ^ (2 : ℕ)) := by
481 exact neg_lt_neg hm1_sq_lo
482 simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using (add_lt_add_left this ((0.00928 : ℝ) ^ (2 : ℕ)))
483 exact lt_trans (lt_trans hstep1 hstep2) hnum
484
485/-- Legacy-calibrated parameterized form preserves the proved Δm²21 interval bound. -/
486lemma dm2_21_frac_pred_with_legacy_in_nufit_1sigma :
487 (7.21e-5 : ℝ) < dm2_21_frac_pred_with legacy_mass_display_calibration ∧
488 dm2_21_frac_pred_with legacy_mass_display_calibration < (7.62e-5 : ℝ) := by
489 simpa [dm2_21_frac_pred_with_legacy] using dm2_21_frac_pred_in_nufit_1sigma
490
491/-- Fractional model Δm²31 is within a typical NuFIT 5.2 2σ band (normal ordering). -/
492lemma dm2_31_frac_pred_in_nufit_2sigma :
493 (2.455e-3 : ℝ) < dm2_31_frac_pred ∧ dm2_31_frac_pred < (2.567e-3 : ℝ) := by
494 let m3 : ℝ := predicted_mass_eV_frac res_nu3
495 let m1 : ℝ := predicted_mass_eV_frac res_nu1
496 have hm3 := nu3_frac_pred_bounds
497 have hm1 := nu1_frac_pred_bounds
498 have hm3_lo : (0.04985 : ℝ) < m3 := by simpa [m3] using hm3.1
499 have hm3_hi : m3 < (0.04993 : ℝ) := by simpa [m3] using hm3.2
500 have hm1_lo : (0.00352 : ℝ) < m1 := by simpa [m1] using hm1.1
501 have hm1_hi : m1 < (0.00355 : ℝ) := by simpa [m1] using hm1.2
502 have hm3_pos : (0 : ℝ) < m3 := lt_trans (by norm_num) hm3_lo
503 have hm1_pos : (0 : ℝ) < m1 := lt_trans (by norm_num) hm1_lo
504
505 have hm3_sq_lo : (0.04985 : ℝ) ^ (2 : ℕ) < m3 ^ (2 : ℕ) := by
506 have habs : |(0.04985 : ℝ)| < |m3| := by
507 simpa [abs_of_pos (by norm_num : (0 : ℝ) < (0.04985 : ℝ)), abs_of_pos hm3_pos] using hm3_lo
508 exact (sq_lt_sq).2 habs
509 have hm3_sq_hi : m3 ^ (2 : ℕ) < (0.04993 : ℝ) ^ (2 : ℕ) := by
510 have habs : |m3| < |(0.04993 : ℝ)| := by
511 have hpos : (0 : ℝ) < (0.04993 : ℝ) := by norm_num
512 simpa [abs_of_pos hm3_pos, abs_of_pos hpos] using hm3_hi
513 exact (sq_lt_sq).2 habs
514 have hm1_sq_lo : (0.00352 : ℝ) ^ (2 : ℕ) < m1 ^ (2 : ℕ) := by
515 have habs : |(0.00352 : ℝ)| < |m1| := by
516 simpa [abs_of_pos (by norm_num : (0 : ℝ) < (0.00352 : ℝ)), abs_of_pos hm1_pos] using hm1_lo
517 exact (sq_lt_sq).2 habs
518 have hm1_sq_hi : m1 ^ (2 : ℕ) < (0.00355 : ℝ) ^ (2 : ℕ) := by
519 have habs : |m1| < |(0.00355 : ℝ)| := by
520 have hpos : (0 : ℝ) < (0.00355 : ℝ) := by norm_num
521 simpa [abs_of_pos hm1_pos, abs_of_pos hpos] using hm1_hi
522 exact (sq_lt_sq).2 habs
523
524 have hdm : dm2_31_frac_pred = (m3 ^ (2 : ℕ)) - (m1 ^ (2 : ℕ)) := by
525 simp [dm2_31_frac_pred, dm2, m3, m1]
526 rw [hdm]
527 constructor
528 · -- lower
529 have hnum : (2.455e-3 : ℝ) < (0.04985 : ℝ) ^ (2 : ℕ) - (0.00355 : ℝ) ^ (2 : ℕ) := by
530 norm_num
531 have hstep1 :
532 (0.04985 : ℝ) ^ (2 : ℕ) - (0.00355 : ℝ) ^ (2 : ℕ)
533 < (m3 ^ (2 : ℕ)) - (0.00355 : ℝ) ^ (2 : ℕ) :=
534 sub_lt_sub_right hm3_sq_lo _
535 have hstep2 :
536 (m3 ^ (2 : ℕ)) - (0.00355 : ℝ) ^ (2 : ℕ) < (m3 ^ (2 : ℕ)) - (m1 ^ (2 : ℕ)) := by
537 have : -(0.00355 : ℝ) ^ (2 : ℕ) < -(m1 ^ (2 : ℕ)) := by
538 exact neg_lt_neg hm1_sq_hi
539 simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using (add_lt_add_left this (m3 ^ (2 : ℕ)))
540 exact lt_trans hnum (lt_trans hstep1 hstep2)
541 · -- upper
542 have hnum : (0.04993 : ℝ) ^ (2 : ℕ) - (0.00352 : ℝ) ^ (2 : ℕ) < (2.567e-3 : ℝ) := by
543 norm_num
544 have hstep1 :
545 (m3 ^ (2 : ℕ)) - (m1 ^ (2 : ℕ))
546 < (0.04993 : ℝ) ^ (2 : ℕ) - (m1 ^ (2 : ℕ)) :=
547 sub_lt_sub_right hm3_sq_hi _
548 have hstep2 :
549 (0.04993 : ℝ) ^ (2 : ℕ) - (m1 ^ (2 : ℕ)) < (0.04993 : ℝ) ^ (2 : ℕ) - (0.00352 : ℝ) ^ (2 : ℕ) := by
550 have : -(m1 ^ (2 : ℕ)) < -((0.00352 : ℝ) ^ (2 : ℕ)) := by
551 exact neg_lt_neg hm1_sq_lo
552 simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using (add_lt_add_left this ((0.04993 : ℝ) ^ (2 : ℕ)))
553 exact lt_trans (lt_trans hstep1 hstep2) hnum
554
555/-- Legacy-calibrated parameterized form preserves the proved Δm²31 interval bound. -/
556lemma dm2_31_frac_pred_with_legacy_in_nufit_2sigma :
557 (2.455e-3 : ℝ) < dm2_31_frac_pred_with legacy_mass_display_calibration ∧
558 dm2_31_frac_pred_with legacy_mass_display_calibration < (2.567e-3 : ℝ) := by
559 simpa [dm2_31_frac_pred_with_legacy] using dm2_31_frac_pred_in_nufit_2sigma
560
561/-! ### Exact structural ratio: why Δr = 7/2 ⇒ φ⁷ (no numerics)
562
563Ignoring the common prefactor `electron_structural_mass * MeV_to_eV`, the *pure* ladder law
564is `m ∝ φ^r`. For `m1 ≈ 0`, the Δm² ratio is approximately:
565\[
566 \frac{Δm^2_{31}}{Δm^2_{21}} \approx \frac{m_3^2}{m_2^2} = φ^{2(r_3-r_2)}.
567\]
568
569Since we enforce `r_3 - r_2 = 7/2`, the structural prediction is **exactly φ⁷**.
570-/
571
572theorem squared_mass_ratio_structural_phi7 :
573 (Real.goldenRatio ^ (toReal res_nu3)) ^ (2 : ℕ) / (Real.goldenRatio ^ (toReal res_nu2)) ^ (2 : ℕ)
574 = Real.goldenRatio ^ (7 : ℝ) := by
575 have hg0 : (0 : ℝ) ≤ Real.goldenRatio := le_of_lt (by simpa using Real.goldenRatio_pos)
576 have hgpos : (0 : ℝ) < Real.goldenRatio := by simpa using Real.goldenRatio_pos
577 -- Convert the rung gap from ℚ to ℝ.
578 have hgapQ : res_nu3 - res_nu2 = (7 : ℚ) / 2 := rung_gap_is_seven_halves
579 have hgapR : (res_nu3 : ℝ) - (res_nu2 : ℝ) = (7 : ℝ) / 2 := by
580 simpa using congrArg (fun q : ℚ => (q : ℝ)) hgapQ
581 -- Use rpow_sub to rewrite the ratio as a single rpow, then square via rpow_mul.
582 have hsub : (Real.goldenRatio ^ (res_nu3 : ℝ)) / (Real.goldenRatio ^ (res_nu2 : ℝ))
583 = Real.goldenRatio ^ ((res_nu3 : ℝ) - (res_nu2 : ℝ)) := by
584 -- `rpow_sub` gives the reverse direction; take `.symm`.
585 simpa using (Real.rpow_sub hgpos (res_nu3 : ℝ) (res_nu2 : ℝ)).symm
586 have hmul : (Real.goldenRatio ^ ((res_nu3 : ℝ) - (res_nu2 : ℝ))) ^ (2 : ℝ)
587 = Real.goldenRatio ^ (7 : ℝ) := by
588 -- rpow_mul reduces squaring to multiplying the exponent by 2.
589 calc
590 (Real.goldenRatio ^ ((res_nu3 : ℝ) - (res_nu2 : ℝ))) ^ (2 : ℝ)
591 = Real.goldenRatio ^ (((res_nu3 : ℝ) - (res_nu2 : ℝ)) * (2 : ℝ)) := by
592 -- rpow_mul: x^(y*z) = (x^y)^z
593 simpa using (Real.rpow_mul hg0 ((res_nu3 : ℝ) - (res_nu2 : ℝ)) (2 : ℝ)).symm
594 _ = Real.goldenRatio ^ (7 : ℝ) := by
595 -- substitute the gap (7/2) and simplify
596 simp [hgapR]
597 -- Now rewrite the goal. We bridge between Nat power and rpow at exponent 2 using `rpow_natCast`.
598 calc
599 (Real.goldenRatio ^ (toReal res_nu3)) ^ (2 : ℕ) / (Real.goldenRatio ^ (toReal res_nu2)) ^ (2 : ℕ)
600 = ((Real.goldenRatio ^ (res_nu3 : ℝ)) / (Real.goldenRatio ^ (res_nu2 : ℝ))) ^ (2 : ℕ) := by
601 -- (a^2)/(b^2) = (a/b)^2 for Nat powers
602 -- also normalize `toReal` away
603 simp [toReal, div_pow]
604 _ = (Real.goldenRatio ^ ((res_nu3 : ℝ) - (res_nu2 : ℝ))) ^ (2 : ℕ) := by
605 simpa [hsub]
606 _ = (Real.goldenRatio ^ ((res_nu3 : ℝ) - (res_nu2 : ℝ))) ^ (2 : ℝ) := by
607 -- convert Nat power back to rpow for the final exponent arithmetic
608 symm
609 simpa using (Real.rpow_natCast (Real.goldenRatio ^ ((res_nu3 : ℝ) - (res_nu2 : ℝ))) 2)
610 _ = Real.goldenRatio ^ (7 : ℝ) := by
611 simpa using hmul
612
613
614/-! ## Verification -/
615
616/-- PROVEN: Bounds on the predicted m3 mass.
617
618 Numerically: predicted_mass_eV (-54) ≈ 0.0563 eV
619 m3_approx = sqrt(2.453e-3) ≈ 0.0495 eV
620 |pred - exp| ≈ 0.0068 < 0.01
621
622 Proof: Uses structural_mass ∈ (10856, 10858) and φ^(-54) ∈ (5.181e-12, 5.185e-12) -/
623lemma nu3_pred_bounds : (0.055 : ℝ) < predicted_mass_eV rung_nu3 ∧ predicted_mass_eV rung_nu3 < (0.058 : ℝ) := by
624 simp only [predicted_mass_eV_legacy, rung_nu3, MeV_to_eV, legacy_mass_display_calibration]
625 have h_sm := ElectronMass.Necessity.structural_mass_bounds
626 have h_phi54_gt := IndisputableMonolith.Numerics.phi_neg54_gt
627 have h_phi54_lt := IndisputableMonolith.Numerics.phi_neg54_lt
628 have h_phi_eq : phi = Real.goldenRatio := rfl
629 rw [h_phi_eq]
630 have hpos_sm : (0 : ℝ) < electron_structural_mass := by
631 have h := h_sm.1
632 linarith
633 have hpos_phi : (0 : ℝ) < Real.goldenRatio ^ (-54 : ℤ) := by
634 have h := h_phi54_gt
635 linarith
636 constructor
637 · -- 0.055 < structural_mass * φ^(-54) * 1e6
638 -- Lower bound: 10856 * 5.181e-12 * 1e6 = 0.05626... > 0.055
639 calc (0.055 : ℝ) < (10856 : ℝ) * (5.181e-12 : ℝ) * (1e6 : ℝ) := by norm_num
640 _ < electron_structural_mass * (5.181e-12 : ℝ) * (1e6 : ℝ) := by nlinarith [h_sm.1]
641 _ < electron_structural_mass * Real.goldenRatio ^ (-54 : ℤ) * (1e6 : ℝ) := by nlinarith [h_phi54_gt, hpos_sm]
642 · -- structural_mass * φ^(-54) * 1e6 < 0.058
643 -- Upper bound: 10858 * 5.185e-12 * 1e6 = 0.05629... < 0.058
644 calc electron_structural_mass * Real.goldenRatio ^ (-54 : ℤ) * (1e6 : ℝ)
645 < (10858 : ℝ) * Real.goldenRatio ^ (-54 : ℤ) * (1e6 : ℝ) := by nlinarith [h_sm.2, hpos_phi]
646 _ < (10858 : ℝ) * (5.185e-12 : ℝ) * (1e6 : ℝ) := by nlinarith [h_phi54_lt]
647 _ < (0.058 : ℝ) := by norm_num
648
649/-- PROVEN: Bounds on m3_approx = sqrt(2.453e-3) ≈ 0.0495 eV
650 Proof: 0.049² = 0.002401 < 0.002453 < 0.0025 = 0.050² -/
651lemma m3_approx_bounds : (0.049 : ℝ) < m3_approx ∧ m3_approx < (0.050 : ℝ) := by
652 simp only [m3_approx, dm2_32_exp]
653 constructor
654 · -- 0.049 < sqrt(0.002453)
655 -- Equivalent to: 0.049² < 0.002453 (since both positive)
656 have h1 : (0.049 : ℝ)^2 < 0.002453 := by norm_num
657 have h_pos : (0 : ℝ) < 0.002453 := by norm_num
658 have h_sqrt_pos : 0 < Real.sqrt 0.002453 := Real.sqrt_pos.mpr h_pos
659 have h_049_pos : (0 : ℝ) ≤ 0.049 := by norm_num
660 rw [← Real.sqrt_sq h_049_pos]
661 exact Real.sqrt_lt_sqrt (sq_nonneg _) h1
662 · -- sqrt(0.002453) < 0.050
663 -- Equivalent to: 0.002453 < 0.050² (since both positive)
664 have h1 : (0.002453 : ℝ) < 0.050^2 := by norm_num
665 have h_pos : (0 : ℝ) ≤ 0.002453 := by norm_num
666 have h_050_pos : (0 : ℝ) < 0.050 := by norm_num
667 rw [← Real.sqrt_sq (le_of_lt h_050_pos)]
668 exact Real.sqrt_lt_sqrt h_pos h1
669
670/-- m3 matches the -54 rung to within tolerance (< 0.01 eV).
671
672 Proof: From nu3_pred_bounds and m3_approx_bounds,
673 |0.056 - 0.050| ≈ 0.006 < 0.01 ✓ -/
674theorem nu3_match : abs (predicted_mass_eV rung_nu3 - m3_approx) < 0.01 := by
675 have h_pred := nu3_pred_bounds
676 have h_m3 := m3_approx_bounds
677 -- pred ∈ (0.055, 0.058), m3 ∈ (0.049, 0.050)
678 -- Worst case: |0.058 - 0.049| = 0.009 < 0.01 ✓
679 rw [abs_lt]
680 constructor <;> linarith [h_pred.1, h_pred.2, h_m3.1, h_m3.2]
681
682/-- PROVEN: Bounds on the predicted m2 mass.
683
684 Numerically: predicted_mass_eV (-58) ≈ 0.00821 eV
685 m2_approx = sqrt(7.53e-5) ≈ 0.00868 eV
686 |pred - exp| ≈ 0.00047 < 0.001
687
688 Proof: Uses structural_mass ∈ (10856, 10858) and φ^(-58) ∈ (7.55e-13, 7.57e-13) -/
689lemma nu2_pred_bounds : (0.0081 : ℝ) < predicted_mass_eV rung_nu2 ∧ predicted_mass_eV rung_nu2 < (0.0083 : ℝ) := by
690 simp only [predicted_mass_eV_legacy, rung_nu2, MeV_to_eV, legacy_mass_display_calibration]
691 have h_sm := ElectronMass.Necessity.structural_mass_bounds
692 have h_phi58_gt := IndisputableMonolith.Numerics.phi_neg58_gt
693 have h_phi58_lt := IndisputableMonolith.Numerics.phi_neg58_lt
694 have h_phi_eq : phi = Real.goldenRatio := rfl
695 rw [h_phi_eq]
696 have hpos_sm : (0 : ℝ) < electron_structural_mass := by
697 have h := h_sm.1
698 linarith
699 have hpos_phi : (0 : ℝ) < Real.goldenRatio ^ (-58 : ℤ) := by
700 have h := h_phi58_gt
701 linarith
702 constructor
703 · -- 0.0081 < structural_mass * φ^(-58) * 1e6
704 -- Lower bound: 10856 * 7.55e-13 * 1e6 = 0.00819... > 0.0081
705 calc (0.0081 : ℝ) < (10856 : ℝ) * (7.55e-13 : ℝ) * (1e6 : ℝ) := by norm_num
706 _ < electron_structural_mass * (7.55e-13 : ℝ) * (1e6 : ℝ) := by nlinarith [h_sm.1]
707 _ < electron_structural_mass * Real.goldenRatio ^ (-58 : ℤ) * (1e6 : ℝ) := by nlinarith [h_phi58_gt, hpos_sm]
708 · -- structural_mass * φ^(-58) * 1e6 < 0.0083
709 -- Upper bound: 10858 * 7.57e-13 * 1e6 = 0.00821... < 0.0083
710 calc electron_structural_mass * Real.goldenRatio ^ (-58 : ℤ) * (1e6 : ℝ)
711 < (10858 : ℝ) * Real.goldenRatio ^ (-58 : ℤ) * (1e6 : ℝ) := by nlinarith [h_sm.2, hpos_phi]
712 _ < (10858 : ℝ) * (7.57e-13 : ℝ) * (1e6 : ℝ) := by nlinarith [h_phi58_lt]
713 _ < (0.0083 : ℝ) := by norm_num
714
715/-- PROVEN: Bounds on m2_approx = sqrt(7.53e-5) ≈ 0.00868 eV
716 Proof: 0.0086² = 7.396e-5 < 7.53e-5 < 7.744e-5 = 0.0088² -/
717lemma m2_approx_bounds : (0.0086 : ℝ) < m2_approx ∧ m2_approx < (0.0088 : ℝ) := by
718 simp only [m2_approx, dm2_21_exp]
719 constructor
720 · -- 0.0086 < sqrt(7.53e-5)
721 have h1 : (0.0086 : ℝ)^2 < 7.53e-5 := by norm_num
722 have h_pos : (0 : ℝ) < 7.53e-5 := by norm_num
723 have h_sqrt_pos : 0 < Real.sqrt (7.53e-5) := Real.sqrt_pos.mpr h_pos
724 have h_086_pos : (0 : ℝ) ≤ 0.0086 := by norm_num
725 rw [← Real.sqrt_sq h_086_pos]
726 exact Real.sqrt_lt_sqrt (sq_nonneg _) h1
727 · -- sqrt(7.53e-5) < 0.0088
728 have h1 : (7.53e-5 : ℝ) < 0.0088^2 := by norm_num
729 have h_pos : (0 : ℝ) ≤ 7.53e-5 := by norm_num
730 have h_088_pos : (0 : ℝ) < 0.0088 := by norm_num
731 rw [← Real.sqrt_sq (le_of_lt h_088_pos)]
732 exact Real.sqrt_lt_sqrt h_pos h1
733
734/-- m2 matches the -58 rung to within tolerance (< 0.001 eV).
735
736 Proof: From nu2_pred_bounds and m2_approx_bounds,
737 |0.0082 - 0.0087| ≈ 0.0005 < 0.001 ✓ -/
738theorem nu2_match : abs (predicted_mass_eV rung_nu2 - m2_approx) < 0.001 := by
739 have h_pred := nu2_pred_bounds
740 have h_m2 := m2_approx_bounds
741 -- pred ∈ (0.0081, 0.0083), m2 ∈ (0.0086, 0.0088)
742 -- Worst case: |0.0081 - 0.0088| = 0.0007 < 0.001 ✓
743 rw [abs_lt]
744 constructor <;> linarith [h_pred.1, h_pred.2, h_m2.1, h_m2.2]
745
746/-- **CERTIFICATE: Neutrino Deep Ladder**
747 Packages the proofs for atmospheric (m3) and solar (m2) neutrino mass matches. -/
748structure NeutrinoMassCert where
749 m3_match : abs (predicted_mass_eV rung_nu3 - m3_approx) < 0.01
750 m2_match : abs (predicted_mass_eV rung_nu2 - m2_approx) < 0.001
751
752theorem neutrino_mass_verified : NeutrinoMassCert where
753 m3_match := nu3_match
754 m2_match := nu2_match
755
756end NeutrinoSector
757end Physics
758end IndisputableMonolith
759