m2_estimate
plain-language theorem explainer
The definition computes an estimate for the second neutrino mass eigenvalue m2 as 1000 times the square root of the solar mass-squared difference. Neutrino phenomenologists would cite it when mapping RS phi-ladder predictions onto oscillation data. It is a direct noncomputable definition with no lemmas or tactics.
Claim. Define $m_2^ est := 1000 sqrt(Δm²₂₁)$, where Δm²₂₁ denotes the solar neutrino mass-squared splitting fixed at 7.42 × 10^{-5} eV².
background
The module examines observed neutrino mass differences and their possible alignment with the golden ratio phi. Upstream, deltam21_sq supplies the experimental solar splitting Δm²₂₁ = 7.42 × 10^{-5} eV² as a fixed real constant, while the parallel definition in PMNSMatrix records the same value for cross-module consistency. The local setting centers on translating these inputs into mass estimates that can be compared against the phi-ladder.
proof idea
The definition is a one-line wrapper that applies the square root to deltam21_sq and multiplies the result by 1000. No lemmas are invoked; the expression relies only on the imported real arithmetic operations.
why it matters
This estimate is used by m3_m2_ratio and by the mass_ratio_phi4 theorem, which shows the atmospheric-to-solar ratio lies within 20% of phi^4. It therefore supplies the concrete mass scale needed to test whether neutrino masses follow the phi-ladder structure already established in the forcing chain (T6 phi fixed point). The construction closes the loop from experimental Δm² values to RS-native predictions without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.