nuAbsMassCert
plain-language theorem explainer
nuAbsMassCert bundles the component bounds and positivity statements on the three predicted neutrino masses together with their exact phi-power rung ratios into one certificate record. A neutrino phenomenologist matching Recognition Science ladder predictions against oscillation data and the cosmological sum bound would cite this certificate. The construction is a direct record literal that populates each field from an already-proven upstream theorem.
Claim. Let $m_1$, $m_2$, $m_3$ be the predicted absolute neutrino masses on the phi-ladder. The certificate asserts $m_1 < 0.012$, $m_2 < 0.012$, $m_2 > 0$, $m_3 > 0$, $m_1 + m_2 + m_3$ below the cosmological sum bound, $m_3/m_2 = phi^6$, and $m_2/m_1 = phi^2$.
background
In the NeutrinoMassHierarchy module the absolute masses are obtained from nuMassAtRung applied at fixed rungs, using the common nuYardstick factor and powers of phi. The module opens with observed mass differences, framing the task of matching predicted rung ratios to solar and atmospheric oscillation data. Upstream theorems establish each piece separately: nu1_abs_mass_upper reduces $m_1 < 0.012$ to a phi^{-28} bound via zpow_neg_lt_one and nlinarith; nu2_abs_mass_pos and nu2_abs_mass_upper do the same for the middle state at exponent -26; nu3_abs_mass_positive confirms positivity at its rung; nu_rung_gap_ratio and nu_solar_rung_ratio cancel the yardstick to obtain the exact phi^6 and phi^2 ratios.
proof idea
The definition is a record constructor that directly assigns the seven fields to the corresponding upstream theorems: nu1_upper to nu1_abs_mass_upper, nu2_upper to nu2_abs_mass_upper, nu2_pos to nu2_abs_mass_pos, nu3_positive to nu3_abs_mass_positive, sum_bound to nu_sum_bound_consistent, rung_gap_ratio to nu_rung_gap_ratio, and solar_gap_ratio to nu_solar_rung_ratio.
why it matters
The certificate supplies the concrete numerical interface for the phi-ladder mass formula applied to neutrinos, collecting all bounds and ratios required for comparison with experiment. It sits at the top of the NeutrinoMassHierarchy module and encodes the self-similar rung spacing forced by the Recognition Science phi fixed point and eight-tick octave. No downstream uses are recorded yet, leaving open the question of how the certificate will be invoked in a larger consistency proof with the full Standard Model sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.