predicted_mass_eV
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not provide a parameter-free derivation of absolute eV values.
- Does not replace the RS-native calibration seam.
- Does not compute masses for rungs outside the deep ladder.
- Does not incorporate experimental uncertainties beyond the supplied bounds.
Lean usage
theorem use_site (r : ℤ) : predicted_mass_eV r = predicted_mass_eV_with legacy_mass_display_calibration r := by rflformal statement (Lean)
99noncomputable def predicted_mass_eV (rung : ℤ) : ℝ :=
proof body
Definition body.
100 predicted_mass_eV_with legacy_mass_display_calibration rung
101