nu3_frac_pred_bounds
plain-language theorem explainer
The lemma establishes that the fractional phi-ladder prediction for the third neutrino mass satisfies 0.04985 < m_struct * phi^(-217/4) * 10^6 < 0.04993 in eV. Neutrino mass modelers working inside the Recognition Science framework cite it to anchor the atmospheric scale without floating-point axioms. The proof unfolds the legacy calibration, pulls in structural mass bounds and the two pre-proven phi-power inequalities, rewrites the rung exponent, and closes both sides of the interval with calc chains and nlinarith.
Claim. Let $m_{struct}$ be the structural electron mass and $phi$ the golden ratio. The fractional rung prediction for the third neutrino satisfies $0.04985 < m_{struct} · phi^{-217/4} · 10^6 < 0.04993$.
background
The NeutrinoSector module places the third neutrino on the deep phi-ladder at the fractional rung whose real value is -217/4. The structural mass is defined as $m_{struct} = Y · phi^{r_e-8}$ (ElectronMass.Defs.electron_structural_mass) and carries the tight interval 10856 < m_struct < 10858 from ElectronMass.Necessity.structural_mass_bounds. The power bounds 4.593e-12 < phi^{-217/4} < 4.598e-12 are supplied by Numerics.Interval.PhiBounds.phi_neg2174_gt and phi_neg2174_lt. The legacy_mass_display_calibration treats m_struct as MeV and multiplies the product by 10^6 to report in eV; toReal transports the rung residue into Mathlib reals.
proof idea
The tactic proof first simplifies predicted_mass_eV_frac via legacy_mass_display_calibration and MeV_to_eV. It obtains structural_mass_bounds together with the two phi_neg2174 inequalities, sets phi equal to goldenRatio, and rewrites toReal res_nu3 to -217/4. Positivity facts are established by linarith and rpow_pos_of_pos. Two calc blocks then sandwich the product: the lower block steps from the numerical constant through m_struct and the lower phi power; the upper block steps from the product through the upper structural bound, the upper phi power, and the target constant, all closed by nlinarith and norm_num.
why it matters
The lemma supplies the nu3 interval for row_nu3_frac in NeutrinoMassScaleScoreCard and the m3 value required by dm2_31_frac_pred_in_nufit_2sigma. It completes the rigorous fractional-rung bound inside the T14 neutrino-sector derivation, showing that the phi-ladder placement at exponent -217/4 lands inside the observed atmospheric scale once the legacy calibration is applied. The argument rests on the pre-established phi-power and structural-mass intervals rather than external numerics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.