predicted_mass_eV_frac_legacy
plain-language theorem explainer
The lemma equates the legacy fractional predicted mass in eV to the product of the electron structural mass, phi raised to the real value of the rung, and the MeV-to-eV conversion factor. Neutrino mass modelers cite it when converting rung-based phi-ladder predictions to observable eV scales for comparison with Delta m squared data. The term-mode proof reduces directly by unfolding the fractional mass definition and the legacy calibration constant.
Claim. For any rung $r$, the predicted mass satisfies $m(r) = m_e^struct · ϕ^{toReal(r)} · c_{MeV/eV}$, where $m_e^struct$ is the dimensionless electron structural mass and $c_{MeV/eV}$ is the legacy calibration factor converting structural units to eV.
background
In the Recognition Science neutrino sector, masses occupy the deep phi-ladder with rungs near -54 and -58. The mass formula scales the structural yardstick by phi to the rung power, after which a display convention reports the result in eV. The module treats electron_structural_mass as if measured in MeV before applying the conversion factor MeV_to_eV, which aliases legacy_mass_display_calibration.eV_per_structural_unit. This is explicitly a reporting seam rather than a first-principles SI derivation. Upstream, toReal transports the rung value to the real line for the exponentiation.
proof idea
The proof is a one-line simp tactic that unfolds predicted_mass_eV_frac, predicted_mass_eV_frac_with, and MeV_to_eV, reducing the statement to a definitional identity.
why it matters
This lemma supplies the conversion step used by the three downstream bound lemmas nu1_frac_pred_bounds, nu2_frac_pred_bounds, and nu3_frac_pred_bounds. It completes the legacy reporting path inside the T14 neutrino sector derivation, allowing direct numerical comparison of phi-ladder predictions against experimental atmospheric and solar mass-squared differences. The construction rests on the phi fixed point and the rung-based mass formula from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.