predicted_mass_eV_frac
plain-language theorem explainer
predicted_mass_eV_frac supplies the default eV-scale neutrino mass for any rational rung on the phi-ladder under the legacy calibration that treats the structural electron mass as 1 MeV. Neutrino mass scorecard constructions and delta-m-squared forecasts cite this definition to obtain the numerical predictions checked against NuFIT intervals. The implementation is a direct delegation to the parameterized form using the legacy display calibration.
Claim. For rung $r$ on the phi-ladder the predicted mass in eV equals $m_0 phi^r times 10^6$, where $m_0$ is the dimensionless structural mass and the factor $10^6$ implements the legacy MeV-to-eV conversion.
background
The NeutrinoSector module formalizes T14 predictions for neutrino masses on the deep phi-ladder. Neutrinos occupy even integer rungs near -50: rung -54 for the atmospheric scale m3 approximately 0.056 eV and rung -58 for the solar scale m2 approximately 0.0082 eV. The module notes that these are reporting quantities obtained after applying a display convention that reuses the electron structural mass as if measured in MeV. Rung is the type of possibly fractional rungs realized as rationals. legacy_mass_display_calibration sets the conversion factor to 10^6 eV per structural unit. This definition supplies the default instance of the parameterized predicted_mass_eV_frac_with.
proof idea
The definition is a one-line wrapper that invokes predicted_mass_eV_frac_with on the legacy_mass_display_calibration and the input rung.
why it matters
It populates the bounds in NeutrinoMassScaleScoreCardCert and the row theorems for nu1, nu2, nu3. The construction sits inside the T14 neutrino sector derivation, which places neutrino generations on the phi-ladder with spacing 4. The legacy seam is flagged as non-fundamental; the framework prefers the RS-native ExternalCalibration route for absolute scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.