nu2_pred_bounds
plain-language theorem explainer
The lemma places the predicted solar neutrino mass at the -58 rung between 0.0081 and 0.0083 eV after applying the legacy MeV-to-eV display conversion to the structural mass. Modelers working on the Recognition Science neutrino sector cite it to confirm the rung assignment before comparing against sqrt of the observed dm2_21. The proof unfolds the calibration definitions, pulls the structural-mass interval and the phi^{-58} interval, then uses two calc blocks with nlinarith to sandwich the product.
Claim. $0.0081 < m_2 < 0.0083$ where $m_2 = m_ {struct} · ϕ^{-58} · 10^6$, $m_{struct}$ is the electron structural mass, and the factor $10^6$ implements the legacy display convention that treats the structural mass as if measured in MeV.
background
The NeutrinoSector module derives neutrino masses on the deep phi-ladder below the electron rung. Mass 2 occupies rung -58 and is obtained by scaling the electron structural mass by ϕ^{-58}. The structural mass itself is defined as lepton_yardstick · ϕ^{electron_rung - 8} and equals 2^{-22} · ϕ^{51} after the forced relations; its interval (10856, 10858) is supplied by the upstream structural_mass_bounds theorem. The legacy_mass_display_calibration treats this dimensionless quantity as MeV and multiplies by 10^6 to report in eV.
proof idea
The tactic proof begins with simp that unfolds predicted_mass_eV, rung_nu2, MeV_to_eV and the legacy calibration. It obtains structural_mass_bounds, phi_neg58_gt and phi_neg58_lt, rewrites ϕ to Real.goldenRatio, and proves positivity of both factors. Two separate calc blocks then apply nlinarith: the lower bound inserts the structural-mass lower edge and the phi^{-58} lower edge; the upper bound inserts the structural-mass upper edge and the phi^{-58} upper edge, finally closing with norm_num.
why it matters
This bound feeds directly into m2_approx_bounds and the nu2_match theorem that verifies |predicted - observed| < 0.001 eV. It completes the rung assignment step inside the T14 neutrino-sector derivation, where the phi-ladder with period-4 spacing separates the atmospheric scale at -54 from the solar scale at -58. The result relies on the eight-tick octave and the phi self-similarity already established in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.