predicted_mass_eV_with
plain-language theorem explainer
This definition supplies the predicted neutrino mass in eV for any integer rung on the phi-ladder once a MassDisplayCalibration is supplied. Neutrino mass modelers in the Recognition Science program cite it to convert the structural mass scale into laboratory units for the deep-ladder states at rungs near -54 and -58. The body is a direct algebraic product of the electron structural mass, phi raised to the rung, and the calibration factor.
Claim. Let $m_0$ be the electron structural mass and let $c$ be the positive real factor $eV_per_structural_unit$ from a MassDisplayCalibration record. The predicted mass in eV at rung $r$ is then $m_0 · ϕ^r · c$.
background
The NeutrinoSector module develops T14, placing neutrinos on the deep ladder at large negative even rungs (R = -54 for the atmospheric scale, R = -58 for the solar scale). The structural mass itself is defined upstream as lepton_yardstick · ϕ^(electron_rung - octave_period), where octave_period is the eight-tick period 8. MassDisplayCalibration is the explicit reporting seam that converts this dimensionless RS quantity into eV; its legacy instance treats the structural mass as if measured in MeV and multiplies by 10^6.
proof idea
One-line wrapper that multiplies the upstream electron_structural_mass by ϕ^rung and the calibration field eV_per_structural_unit.
why it matters
It is the common implementation used by both predicted_mass_eV (legacy convention) and predicted_mass_eV_legacy. The definition closes the calibration seam required by the module doc for T14, allowing the phi-ladder mass formula to be reported in eV while keeping the underlying RS-native derivation parameter-free. It touches the open question of whether a fully SI-native calibration (via RSNativeUnits.ExternalCalibration) will eventually replace the legacy MeV-to-eV seam.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.