legacy_mass_display_calibration
plain-language theorem explainer
Legacy mass display calibration supplies the conversion factor of 10^6 that turns the RS structural mass (treated as MeV) into eV units for neutrino predictions. Workers on the T14 neutrino sector cite this definition to align phi-ladder masses at rungs near -54 and -58 with observed Delta m squared intervals. The construction is a direct structure instance whose positivity constraint is discharged by a single norm_num tactic.
Claim. The legacy mass display calibration is the mass display calibration structure instance with conversion factor eV per structural unit set to $10^6$.
background
MassDisplayCalibration is the structure supplying an explicit reporting seam that converts the RS structural mass scale to eV; it consists of a positive real eV_per_structural_unit together with a positivity proof. The NeutrinoSector module applies the legacy instance by treating electron_structural_mass as if measured in MeV and multiplying by 10^6, as stated in the module note: 'This is a calibration/reporting seam, not a parameter-free derivation of absolute eV scales.' Upstream results include the SingleAnchor calibration definition that produces ExternalCalibration objects and the PrimitiveDistinction axioms that ground the structural mass scale.
proof idea
The definition directly constructs the MassDisplayCalibration structure by assigning the literal 1e6 to eV_per_structural_unit. The required positivity field is discharged by the norm_num tactic.
why it matters
This definition supplies the legacy seam used by downstream lemmas such as dm2_21_frac_pred_with_legacy and dm2_31_frac_pred_with_legacy_in_nufit_2sigma to recover the predicted fractional Delta m squared bounds. It implements the reporting convention described for the T14 neutrino sector on the deep phi-ladder. The construction touches the open distinction between this legacy path and the preferred RS-native ExternalCalibration route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.