predicted_mass_eV_frac_with
plain-language theorem explainer
This definition supplies the eV-scale mass for a rung on the phi-ladder under an explicit calibration seam. Neutrino mass calculations in the Recognition framework cite it when converting structural masses to observable scales for the deep ladder. The body is a direct product of the electron structural mass, phi raised to the transported rung, and the calibration conversion factor.
Claim. $m_ {eV}(c,r) = m_{struct} · ϕ^{toReal(r)} · c.eV_per_structural_unit$, where $m_{struct}$ is the electron structural mass, $ϕ$ the self-similar fixed point, $r$ the rung index, and $c$ the MassDisplayCalibration structure supplying the conversion factor.
background
The NeutrinoSector module places neutrinos on the deep ladder with even-integer rungs near -54 and -58. MassDisplayCalibration is the structure holding the positive real eV_per_structural_unit that converts the dimensionless structural mass (treated as MeV) into eV. electron_structural_mass equals lepton_yardstick times phi to the power (electron_rung minus octave_period). toReal transports the rung value to Mathlib reals for exponentiation. Rung assignments follow the RSBridge.Anchor mapping for fermions.
proof idea
This is a direct definition. It multiplies electron_structural_mass by (phi raised to toReal res) and by the eV_per_structural_unit field of the supplied calibration. The construction uses only field projection and the arithmetic already imported from Mathlib and the RS constants; no lemmas or tactics are applied.
why it matters
It supplies the mass expression invoked by dm2_21_frac_pred_with and dm2_31_frac_pred_with to obtain predicted squared-mass differences. The definition fills the T14 neutrino-sector hypothesis, linking the deep-ladder rungs to the phi-ladder forced by T5 J-uniqueness and T6 self-similar fixed point, with the eight-tick octave fixing the base shift of 8. The calibration seam permits numerical comparison to observed Delta m squared values while remaining separate from RS-native unit derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.