predicted_mass_eV_legacy
plain-language theorem explainer
The lemma equates the legacy neutrino mass prediction in eV for integer rung r to electron structural mass scaled by phi^r and multiplied by the MeV-to-eV conversion factor. Neutrino mass modelers in the Recognition Science framework cite it when converting deep-ladder rung predictions to observable scales. The proof is a direct simplification that unfolds the definitions of predicted_mass_eV, predicted_mass_eV_with, and the legacy conversion constant.
Claim. For any integer rung $r$, the predicted neutrino mass in eV satisfies $m(r) = m_e^{struct} · ϕ^r · k$, where $k$ is the legacy conversion from structural units to eV.
background
The module formalizes the neutrino mass scale on the deep phi-ladder, with neutrinos at even integer rungs far below the electron rung $R_e=2$ (specifically near -54 and -58). The mass formula follows the Recognition Science yardstick scaled by phi to the rung power, with electron_structural_mass serving as the reference scale. Quantities are reported in eV via a display convention that treats the structural mass as if measured in MeV before applying the factor $k = 10^6$. Upstream results include the octave definition (one octave equals 8 ticks) and the rung concept from Constants, which anchor the phi-power hierarchy.
proof idea
The proof is a one-line term-mode wrapper that applies simp to unfold predicted_mass_eV, predicted_mass_eV_with, and MeV_to_eV. No additional lemmas or tactics are required beyond the definitional reductions.
why it matters
This lemma supplies the backwards-compatible expression used by the downstream bounds nu2_pred_bounds and nu3_pred_bounds, which numerically match experimental Delta m^2 scales to within 0.001 eV. It fills the T14 neutrino sector hypothesis, linking the deep-ladder mass formula (T5 J-uniqueness and T6 phi fixed point) to observable eV values while preserving the integer-rung scaffold before the quarter-ladder upgrade. The legacy calibration seam is explicitly noted as non-derivational.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.