row_dm2_21_nufit
plain-language theorem explainer
The declaration certifies that the fractional-ladder prediction for the neutrino squared-mass splitting Δm²₂₁ lies strictly inside the NuFIT 5.2 1σ interval (7.21×10⁻⁵, 7.62×10⁻⁵) eV². Neutrino phenomenologists and Recognition Science modelers cite it when populating the neutrino mass scale scorecard. The proof is a one-line wrapper that directly invokes the upstream lemma establishing the identical numerical bound from the predicted masses.
Claim. The fractional-model prediction satisfies $7.21×10^{-5} < Δm^2_{21} < 7.62×10^{-5}$ (in eV²), where $Δm^2_{21}$ is computed as the squared difference between the fractional eV-scale masses assigned to the second and first neutrino states on the φ-ladder.
background
The NeutrinoMassScaleScoreCard module packages row-level consistency checks for the P2-ν phase. The definition dm2_21_frac_pred computes Δm²₂₁ := dm2(predicted_mass_eV_frac res_nu2, predicted_mass_eV_frac res_nu1), using the Recognition Science fractional rung masses. The upstream lemma dm2_21_frac_pred_in_nufit_1sigma states that this quantity lies inside a typical NuFIT 5.2 1σ band for normal ordering.
proof idea
The proof is a one-line wrapper that applies the lemma dm2_21_frac_pred_in_nufit_1sigma.
why it matters
This row supplies the Δm²₂₁ entry in the NeutrinoMassScaleScoreCardCert structure proved nonempty by neutrinoMassScaleScoreCardCert_holds. It thereby supplies the required consistency check for the P2-ν phase of the Recognition framework, linking φ-ladder rung assignments to experimental oscillation data within the stated 1σ window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.