nuMassSum_eq_Y_times_factor
plain-language theorem explainer
The neutrino mass sum equals the yardstick Y multiplied by the fixed factor phi to the minus eight plus phi cubed plus phi to the eleven. Cosmologists applying the Planck sum bound would cite this linearity to convert the total-mass limit into an upper bound on Y. The proof is a direct term-mode expansion that unfolds the sum and mass definitions then closes by matrix simplification and ring.
Claim. Let $m_i(Y) = Y · ϕ^{r_i - 8}$ where the rung indices are $r = [0, 11, 19]$. Then $∑_i m_i(Y) = Y · (ϕ^{-8} + ϕ^3 + ϕ^{11})$.
background
The neutrino yardstick module treats the neutrino sector as the last unfixed mass parameter. Each neutrino mass is defined by the product of the yardstick Y and a power of phi fixed by the rung assignment, with rungs set to 0, 11 and 19 and gap correction zero. The sumFactor is the explicit sum of the three powers ϕ^{-8} + ϕ^3 + ϕ^{11} that arise after subtracting the baseline rung offset of 8. This construction inherits the general yardstick definition from the Anchor module: yardstick(s) = 2^{B_pow s} · E_coh · ϕ^{r0 s}. The module records the cosmological constraint Σm_i < 0.12 eV and notes that the neutrino yardstick remains the final free parameter.
proof idea
The proof unfolds nuMassSum, nuMass, sumFactor and nu_rungs, applies simp on the matrix constructors for the Fin 3 vector, then closes the resulting polynomial identity by ring.
why it matters
This equality supplies the linear relation required by the downstream yardstick_upper_bound theorem, which rewrites the cosmological inequality nuMassSum Y < 0.12 into the explicit bound Y < 0.12 / sumFactor. It thereby anchors the neutrino sector inside the Recognition Science mass-ladder construction and the phi-ladder with eight-tick octave structure. The module doc-comment identifies the result as one of the theorem constraints that must be satisfied before the unique determination of Y can be attempted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.