dm2_31_frac_pred_with
plain-language theorem explainer
The definition supplies a calibration-dependent expression for the predicted atmospheric neutrino mass-squared splitting Δm²₃₁ in the fractional rung model. Neutrino physicists comparing Recognition Science structural predictions to oscillation data would cite it when adopting a custom MassDisplayCalibration. It is realized as a direct composition of the dm2 splitting with the eV-scale masses for the res_nu3 and res_nu1 rungs.
Claim. For a MassDisplayCalibration $cal$, the predicted splitting is defined by $Δm^2_{31}(cal) := m_3(cal)^2 - m_1(cal)^2$, where $m_3(cal)$ and $m_1(cal)$ are the eV masses obtained from the fractional rung model applied to the atmospheric rung res_nu3 and the lightest rung res_nu1 respectively.
background
The NeutrinoSector module develops the T14 hypothesis that neutrinos occupy deep phi-ladder rungs far below the electron, with m3 at rung -54 and m2 at rung -58. The residue difference of 4 between generations is interpreted as a quarter-ladder spacing. The MassDisplayCalibration structure supplies an explicit reporting seam consisting of a positive real factor eV_per_structural_unit that converts the dimensionless RS structural mass (treated as MeV under the legacy convention) into eV units.
proof idea
One-line wrapper that applies dm2 to the pair of predicted masses obtained from predicted_mass_eV_frac_with applied to res_nu3 and res_nu1 under the supplied calibration.
why it matters
This definition anchors the parameterized predictions inside the T14 neutrino sector formalization and is invoked by the legacy calibration lemma dm2_31_frac_pred_with_legacy together with the NuFIT 2σ interval check dm2_31_frac_pred_with_legacy_in_nufit_2sigma. It implements the deep-ladder hypothesis with rung spacings tied to the eight-tick octave and phi-ladder structure of the Recognition framework, enabling direct comparison to experimental Δm² intervals. The construction leaves open a fully parameter-free SI calibration route via RSNativeUnits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.