dm2_32_exp
plain-language theorem explainer
dm2_32_exp supplies the measured atmospheric neutrino mass-squared difference Δm²₃₂ = 2.453 × 10^{-3} eV². Neutrino mass modelers cite it when recovering the third neutrino mass from the deep ladder rung at R = -54 via square root. The definition is a direct numerical assignment with no reduction or lemmas applied.
Claim. The atmospheric neutrino mass-squared splitting is fixed at $Δm_{32}^2 = 2.453 × 10^{-3}$ in eV² units.
background
In the Recognition Science neutrino sector, neutrinos occupy the deep ladder at large negative integer rungs. The module places the atmospheric scale at rung R = -54, giving a structural mass near 0.056 eV that is compared against the observed value extracted from Δm²₃₂ ≈ 0.050 eV; a parallel solar scale sits at R = -58. All quantities follow a display convention that reuses the electron structural mass (dimensionless in RS-native units) as if expressed in MeV and converts by the factor 10^6 to reach eV; the module states explicitly that this is a reporting seam rather than a parameter-free derivation.
proof idea
The definition is a direct literal assignment of the constant 2.453e-3. No lemmas are invoked and no tactics are used.
why it matters
This constant anchors the neutrino mass approximations inside the T14 neutrino sector formalization. It is consumed by m3_approx to produce √(2.453 × 10^{-3}) ≈ 0.0495 eV and by the subsequent bounds lemma verifying 0.049 < m3_approx < 0.050. Within the framework it closes the comparison between the phi-ladder mass formula and the observed oscillation parameters, consistent with the eight-tick octave and D = 3 inherited from the unified forcing chain. It touches the open question of whether a fully RS-native calibration can replace the MeV-to-eV seam.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.