nu_sum_bound_consistent
plain-language theorem explainer
The theorem shows that the sum of the three phi-ladder neutrino mass predictions lies strictly below the Planck cosmological upper limit of 0.12 eV. Cosmologists and model builders working in the Recognition Science Standard Model extension cite it when fixing absolute masses from oscillation data and large-scale structure constraints. The proof unfolds the rung-specific mass definitions, proves three elementary bounds on negative powers of phi together with their positivity, and closes the inequality by nlinarith.
Claim. Let $m_1$, $m_2$, $m_3$ be the predicted neutrino masses obtained from the yardstick at rung $-28$ scaled by the indicated negative powers of phi, and let $B$ be the Planck sum-mass bound. Then $m_1 + m_2 + m_3 < B$.
background
In the Recognition Science Standard Model module, neutrino masses are constructed via the seesaw mechanism with the right-handed scale fixed by the phi-ladder relation proved in seesaw_scale_phi_connection. The yardstick nuYardstick supplies the base mass at rung $-28$; the three generations are then placed at rungs $-28$, $-26$ and $-20$. The function sum_mass_bound is the numerical Planck limit expressed in the same units. Upstream lemmas supply the rung map from Compat.Constants and the discrete scale phi^k from Cosmology.LargeScaleStructureFromRS, which together embed all masses on the phi-ladder.
proof idea
The tactic proof begins by unfolding m_nu1_pred, m_nu2_pred, m_nu3_pred, nuMassAtRung, nuYardstick and sum_mass_bound. It then constructs three auxiliary facts (h20, h26, h28) showing that phi to the powers $-20$, $-26$ and $-28$ are each strictly less than 1, together with the three positivity statements pos20, pos26, pos28. The final step applies nlinarith to the resulting linear combination and obtains the strict inequality.
why it matters
nu_sum_bound_consistent is invoked directly inside nuAbsMassCert to supply the sum_bound field of the absolute-mass certificate. It thereby confirms that the phi-predicted seesaw masses remain compatible with the cosmological bound stated in the module comment on absolute mass intervals. The result supports the mass formula yardstick times phi to the appropriate rung offset and closes one consistency check required by the eight-tick octave assignment of fermion generations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.