massRatio
plain-language theorem explainer
The declaration defines the ratio of atmospheric to solar neutrino mass-squared differences as a real number. Researchers comparing experimental neutrino hierarchies to golden-ratio scaling predictions in Recognition Science would cite this quantity. It arises from a direct division of the two fixed experimental constants deltam31_sq and deltam21_sq.
Claim. Let $r = 2.51e-3 / 7.42e-5$, where $2.51e-3$ is the atmospheric neutrino mass-squared difference in eV$^2$ and $7.42e-5$ is the solar difference in eV$^2$.
background
The module records observed neutrino mass differences. deltam21_sq is the solar neutrino mass-squared difference fixed at 7.42e-5 eV$^2$. deltam31_sq is the atmospheric difference fixed at 2.51e-3 eV$^2$. Upstream, GaugeBosonMassesFromRS defines an analogous massRatio as 6/(3 + phi) while ThreeGenerations defines massRatio as phi itself, establishing the template for generational scaling. The PMNSMatrix module records the same squared differences and notes that their ratio approximates 34, near phi^7.
proof idea
This is a one-line definition that computes the quotient of deltam31_sq by deltam21_sq.
why it matters
This definition supplies the numerical ratio used in downstream certificates such as GaugeBosonMassCert and WZBosonRatioScoreCard, as well as the phi^7 comparison in mass_ratio_phi7. It quantifies the neutrino mass hierarchy for comparison against the phi-ladder in the Recognition Science framework. It touches the open question of why the observed ratio deviates from exact phi^7 by a factor of about three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.