deltam31_sq
plain-language theorem explainer
The definition supplies the observed atmospheric neutrino mass-squared splitting Δm₃₁² = 2.51 × 10^{-3} eV² as a fixed real number. Neutrino phenomenologists and Recognition Science builders cite it when forming mass ratios or testing φ-connections in the PMNS sector. It is introduced by direct numerical assignment with no computation or lemmas.
Claim. The atmospheric neutrino mass-squared difference is defined by Δm₃₁² := 2.51 × 10^{-3} eV².
background
The PMNSMatrix module develops the Pontecorvo-Maki-Nakagawa-Sakata mixing matrix from φ-quantized angles under Recognition Science. Neutrino flavor states mix with large angles (θ₁₂ ≈ 34°, θ₂₃ ≈ 45°, θ₁₃ ≈ 8.6°), and the module imports Constants to anchor numerical inputs for mass splittings and ratios. The local setting is SM-014, whose module doc targets derivation of PMNS angles from golden-ratio geometry with a cited PRD paper proposition.
proof idea
The declaration is a direct numerical assignment of the experimental value 2.51e-3. No lemmas or tactics are invoked; the definition serves as a constant input for downstream mass-ratio calculations.
why it matters
This constant is referenced by seven downstream declarations, including m3_estimate, massRatio, mass_ratio_phi4, and mass_ratio_phi7. The latter verifies that the atmospheric-to-solar mass ratio approximates φ^7 within a 15% band, supporting the RS claim that neutrino mass splittings connect to the phi-ladder. It fills the numerical anchor required by the module doc's paper proposition on neutrino mixing from golden-ratio geometry and touches the open question of exact φ-quantization for the neutrino sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.