m_nu1_pred
plain-language theorem explainer
The definition sets the predicted mass of the lightest neutrino to the Recognition Science yardstick scaled by phi to the power negative twenty-eight. Neutrino phenomenologists comparing RS predictions to oscillation splittings and the Planck sum bound less than 0.12 eV would cite this value. It is realized as a direct one-line application of the rung-based mass function at rung index negative twenty-eight.
Claim. The predicted mass of the lightest neutrino satisfies $m_1 = y_0 · ϕ^{-28}$, where $y_0$ is the Recognition Science neutrino yardstick and ϕ is the golden-ratio fixed point of the self-similar forcing chain.
background
Recognition Science places fermion masses on a phi-ladder whose rungs are integer powers of the golden ratio ϕ. The module treats observed neutrino mass-squared differences from solar and atmospheric oscillations. The upstream theorem from PrimitiveDistinction extracts four structural conditions plus three definitional facts from seven independent axioms; these conditions license the phi-ladder construction. The sibling definition nuMassAtRung supplies the general scaling $y_0 · ϕ^r$ for any integer rung r.
proof idea
This is a one-line definition that applies the nuMassAtRung function at rung index negative twenty-eight.
why it matters
The value feeds the absolute-mass upper-bound theorem and the NuAbsMassCert structure that certify consistency with the cosmological sum bound. It instantiates the RS mass formula at the rung required for the lightest neutrino, linking to the eight-tick octave and the derivation of three spatial dimensions in the forcing chain T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.