dm2_31_frac_pred
plain-language theorem explainer
dm2_31_frac_pred defines the predicted squared mass difference Δm²₃₁ between the third and first neutrino generations in the fractional rung model. Neutrino oscillation analysts and Recognition Science modelers cite it when testing the deep-ladder hypothesis against atmospheric data. The definition is a direct one-line application of the dm2 difference operator to the calibrated eV-scale mass predictions for those states.
Claim. $Δm²_{31} := dm2(m₃^{pred}, m₁^{pred})$ where the predicted masses are the fractional-rung outputs converted to eV units via the electron structural mass display convention.
background
The NeutrinoSector module derives neutrino masses on the deep phi-ladder, with m₃ at rung -54 and m₂ at rung -58, producing a residue spacing of 4 that is interpreted as quarter-ladder periodicity. The dm2 operator computes the squared difference of two such masses after the MeV-to-eV conversion that re-uses the electron structural mass as a reporting yardstick. Upstream results include the Calibration axiom from CostAxioms (“The second derivative at the origin (in log coordinates) equals 1”) and the rung selector from AnchorPolicy that maps sector and name to integer ladder position.
proof idea
This is a one-line definition that applies dm2 to the fractional predicted masses of the third and first neutrino states. No further tactics or lemmas are invoked inside the body.
why it matters
The definition supplies the numerical input for NeutrinoMassScaleScoreCardCert and for the lemma dm2_31_frac_pred_in_nufit_2sigma that places the value inside the NuFIT 5.2 2σ band. It completes the T14 neutrino-sector step of the Recognition Science chain by linking the phi-ladder mass formula to observed oscillation parameters while exposing the calibration seam between RS-native units and eV reporting. The module doc flags this seam as a display convention rather than a parameter-free absolute-scale derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.