NuAbsMassCert
plain-language theorem explainer
The NuAbsMassCert structure certifies that the RS-predicted neutrino masses at phi-ladder rungs -28, -26 and -20 obey experimental upper limits below 0.012 eV, remain positive where required, sum to less than 0.12 eV, and exhibit exact phi^6 and phi^2 ratios between the states. Neutrino phenomenologists would reference it when checking consistency between the Recognition Science mass formula and oscillation data. The definition simply assembles these five inequalities and two ratio equalities from the precomputed rung masses and the fixed sum.
Claim. A structure asserting the following for the predicted neutrino masses $m_1$, $m_2$, $m_3$ obtained from the phi-ladder: $m_1 < 0.012$, $m_2 < 0.012$, $m_2 > 0$, $m_3 > 0$, $m_1 + m_2 + m_3 < 0.12$, $m_3/m_2 = phi^6$, and $m_2/m_1 = phi^2$.
background
The module addresses observed mass differences in the neutrino sector under Recognition Science. Upstream definitions place the masses on the phi-ladder via nuMassAtRung: $m_1$ at rung -28, $m_2$ at -26, $m_3$ at -20, each following the mass formula yardstick times phi to the appropriate power. The sum bound is fixed at 0.12. These rest on the phi-ladder scaling from the forcing chain (T5 J-uniqueness through T8 D=3) and the Recognition Composition Law.
proof idea
This is a structure definition with no proof body. It directly encodes the five inequalities and two ratio statements using the rung mass definitions and the constant sum bound of 0.12.
why it matters
This certificate is instantiated by nuAbsMassCert to provide a concrete check that the RS neutrino mass predictions align with the experimental sum bound and oscillation ratios. It supports the Standard Model embedding within Recognition Science by confirming the phi^6 atmospheric and phi^2 solar splittings on the phi-ladder. It touches the open question of the absolute neutrino mass scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.