nu2_match
plain-language theorem explainer
The solar neutrino mass scale matches the phi-ladder prediction at rung -58 to within 0.001 eV. Physicists deriving neutrino masses from the unified forcing chain cite this to confirm the deep-ladder assignment for the solar scale. The proof obtains explicit numerical bounds on the predicted mass and the experimental approximation then applies linear arithmetic to verify the absolute difference lies below tolerance.
Claim. Let $m_2$ be the solar neutrino mass scale given by the square root of the experimental $Δm_{21}^2$. Let $m_{pred}$ be the predicted mass in eV at rung -58 obtained from the structural mass scaled by $φ^{-58}$ under the legacy calibration. Then $|m_{pred} - m_2| < 0.001$.
background
The Neutrino Sector module places neutrinos on the deep phi-ladder with the solar scale at rung -58. The predicted mass converts the dimensionless structural mass (treated as MeV) to eV via a factor of 10^6. The approximate $m_2$ is the square root of the experimental $Δm_{21}^2 ≈ 7.53×10^{-5}$ eV². Upstream lemmas establish the predicted mass lies in (0.0081, 0.0083) eV and the approximate mass lies in (0.0086, 0.0088) eV using structural-mass bounds and explicit $φ^{-58}$ interval bounds.
proof idea
The term proof first invokes the pre-proven interval lemmas for the predicted mass at rung -58 and for the square-root approximation of $Δm_{21}^2$. It rewrites the absolute-value goal into a pair of strict inequalities and discharges both with linear arithmetic on the four endpoint values, confirming the worst-case gap of 0.0007 is below 0.001.
why it matters
This supplies the solar-scale component of the NeutrinoMassCert theorem that packages verified matches for both atmospheric and solar neutrinos. It completes the T14 neutrino-sector derivation inside the Recognition Science framework, confirming the phi-ladder mass formula at deep negative rungs consistent with the forcing chain and RCL. It touches the open calibration question of reporting absolute eV scales without legacy conventions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.