nu3_pred_bounds
plain-language theorem explainer
The lemma establishes that the RS-predicted m3 mass at rung -54 lies in (0.055 eV, 0.058 eV) under the legacy display convention. Neutrino-sector modelers cite it to confirm the deep-ladder assignment against atmospheric oscillation data. The proof rewrites the prediction via legacy calibration, pulls interval bounds on structural mass and on phi^(-54), then chains the inequalities with nlinarith and norm_num.
Claim. $0.055 < m_3^pred < 0.058$ where $m_3^pred = m_{struct} · ϕ^{-54} · 10^6$ (in eV) and $m_{struct}$ is the electron structural mass.
background
The Neutrino Sector module assigns neutrinos to deep negative rungs on the phi-ladder, with the atmospheric scale m3 placed at rung -54. The electron structural mass is the dimensionless quantity lepton_yardstick · phi^(electron_rung - octave_period) and is known to lie in (10856, 10858) by the upstream structural_mass_bounds theorem. The legacy_mass_display_calibration treats this structural mass as if measured in MeV and multiplies by 10^6 to obtain an eV-scale display value; predicted_mass_eV applies this convention at the supplied rung.
proof idea
The tactic proof first simplifies via predicted_mass_eV_legacy, rung_nu3, MeV_to_eV and legacy_mass_display_calibration. It imports structural_mass_bounds, phi_neg54_gt and phi_neg54_lt, equates phi to Real.goldenRatio, and proves positivity of both factors. The lower bound is obtained by norm_num comparison to the product 10856 · 5.181e-12 · 1e6 followed by two nlinarith replacements; the upper bound proceeds symmetrically by replacing the structural mass from above and the phi power from below, ending with norm_num.
why it matters
The result supplies the predicted interval that is compared to m3_approx = sqrt(Δm²_32) inside the downstream nu3_match theorem, which verifies |pred - approx| < 0.01. It completes the numerical check for the -54 rung assignment in the T14 neutrino-sector derivation. The argument rests on the phi-ladder and eight-tick octave from the forcing chain but inherits the legacy calibration seam rather than a full RS-native unit conversion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.