MassDisplayCalibration
MassDisplayCalibration packages the conversion factor from RS structural mass units to electron-volts for neutrino mass predictions. Neutrino sector derivations cite it to report absolute scales in eV after fixing the electron mass scale via the phi-ladder. The definition is a plain record with a positive real field and its positivity proof.
claimA structure consisting of a positive real number $c$ that converts one structural mass unit into electron-volts.
background
In the Neutrino Sector module, neutrino masses occupy the deep ladder with rungs near -54 and -58. The structural mass is defined upstream as lepton_yardstick times phi to the power of (electron_rung minus 8), a dimensionless RS-native quantity. The module states that quantities are reported in eV only after a display convention that reuses the electron structural mass as if measured in MeV and multiplies by 10^6. This is explicitly a reporting seam, not a parameter-free derivation of absolute scales; the preferred route for SI units runs through Constants.RSNativeUnits.ExternalCalibration.
proof idea
Defines the record directly with the field eV_per_structural_unit of type real and the field eV_per_structural_unit_pos asserting its positivity. No lemmas or tactics are invoked; it is a bare structure declaration.
why it matters in Recognition Science
This structure supplies the calibration parameter to downstream definitions including predicted_mass_eV_with, predicted_mass_eV_frac_with, dm2_21_frac_pred_with and dm2_31_frac_pred_with. It implements the explicit reporting seam required by T14 for the neutrino sector, allowing numerical comparison with observed Delta m squared values while leaving the absolute scale choice open. The module contrasts it with the RS-native pathway through ExternalCalibration, marking the boundary between display convention and first-principles derivation.
scope and limits
- Does not derive the numerical value of the conversion factor from first principles.
- Does not assign specific rungs to neutrino generations.
- Does not replace the RS-native SI calibration route.
- Does not constrain the phi-ladder spacing or residue differences.
Lean usage
def nu3_eV := predicted_mass_eV_with legacy_mass_display_calibration (-54)formal statement (Lean)
70structure MassDisplayCalibration where
71 eV_per_structural_unit : ℝ
72 eV_per_structural_unit_pos : 0 < eV_per_structural_unit
73
74/-- Legacy display convention: treat `electron_structural_mass` as MeV and convert to eV. -/