dm2_21_exp
plain-language theorem explainer
The declaration supplies the experimental solar neutrino mass-squared splitting as the constant 7.53 × 10^{-5} eV². Neutrino oscillation studies cite this value when matching Recognition Science ladder predictions against solar data. The definition consists of a direct numerical assignment with no further computation or hypotheses.
Claim. $Δm^2_{21} = 7.53 × 10^{-5} eV^2$
background
The NeutrinoSector module places neutrinos on the deep phi-ladder at even rungs near -50. Mass 2 occupies rung -58, so the structural mass formula yields m₂ ≈ m_struct · ϕ^{-58} ≈ 0.0082 eV after the module's calibration step. The definition records the measured solar splitting Δm²₂₁ in eV² units obtained by treating the electron structural mass as a MeV-scale quantity and multiplying by 10^6.
proof idea
One-line definition that directly assigns the numerical value 7.53e-5.
why it matters
It supplies the input constant for the downstream definitions m2_approx = sqrt(Δm²₂₁) and the lemma m2_approx_bounds that verifies the interval (0.0086, 0.0088) eV. The declaration anchors the T14 neutrino-sector formalization, connecting the phi-ladder mass formula to laboratory solar-neutrino data and exposing the reporting seam between RS-native units and eV scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.