MeV_to_eV
plain-language theorem explainer
This definition supplies the legacy unit conversion factor of 10^6 that turns structural masses into electronvolts for neutrino predictions. Neutrino-sector lemmas cite it to report masses on the phi-ladder in eV for direct comparison with oscillation data. It is realized as a one-line alias to the eV_per_structural_unit field of the legacy calibration record.
Claim. Define the conversion constant $10^6$ as the number of electronvolts per structural mass unit under the legacy display convention that treats the electron structural mass as if expressed in MeV.
background
The NeutrinoSector module places neutrinos on the deep phi-ladder at even negative rungs near -50. Mass 3 sits at rung -54 and mass 2 at rung -58; after calibration these yield predicted values near 0.056 eV and 0.0082 eV respectively. The module document states that all reported eV quantities rely on a display seam: the electron structural mass is reused as a MeV-scale number and then multiplied by the present factor to reach eV. Upstream, Mass is the abbreviation for the reals in RSNativeUnits, while legacy_mass_display_calibration is the record that hard-codes eV_per_structural_unit to 1e6.
proof idea
One-line definition that aliases the eV_per_structural_unit field of the legacy_mass_display_calibration record.
why it matters
The definition supplies the reporting seam required by every legacy-calibrated neutrino bound (nu3_pred_bounds, nu2_pred_bounds, nu1_frac_pred_bounds, dm2_31_frac_pred_with_legacy_in_nufit_2sigma). It implements the explicit calibration note in the T14 Neutrino Sector hypothesis, allowing the phi-ladder mass formula to be compared with experimental Δm² intervals while the RS-native ExternalCalibration pathway remains available for future work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.