predicted_mass_eV
plain-language theorem explainer
The definition supplies the default predicted neutrino mass in eV for any integer rung on the phi-ladder under the legacy display convention. Neutrino physicists citing Recognition Science predictions for atmospheric and solar scales would reference this for quick numerical checks. It is realized as a one-line wrapper delegating to the general predicted_mass_eV_with function with the legacy calibration object.
Claim. For integer rung $r$, the predicted mass is $m(r) = m_{struct} · ϕ^r · 10^6$ eV, where $m_{struct}$ denotes the dimensionless structural mass of the electron and the factor implements the legacy MeV-to-eV conversion.
background
In the Recognition Science framework, neutrino masses are obtained by descending the phi-ladder from the structural electron mass. The rung parameter selects the exponent in $ϕ^r$, with negative values placing neutrinos on the deep ladder (rungs near -54 and -58 for the atmospheric and solar scales, per the module documentation on T14). The legacy_mass_display_calibration treats the structural mass as if expressed in MeV and multiplies by 10^6 to report in eV; this is a reporting seam rather than a fundamental derivation. Upstream, predicted_mass_eV_with supplies the general form electron_structural_mass * (phi ^ rung) * cal.eV_per_structural_unit, while rung functions from RSBridge.Anchor and AnchorPolicy supply the integer labels for each fermion species.
proof idea
This definition is a one-line wrapper that applies predicted_mass_eV_with to the legacy_mass_display_calibration object and the supplied rung.
why it matters
It serves as the default entry point for neutrino mass calculations in the legacy convention, feeding directly into NeutrinoMassCert, nu2_match, nu3_match, and the associated bounds lemmas. The module realizes T14 by placing neutrinos on the deep ladder with rung spacings of 4, consistent with the quarter-ladder structure. It touches the open question of absolute scale calibration versus the RS-native pathway in Constants.RSNativeUnits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.