m_nu2_pred
plain-language theorem explainer
The definition sets the predicted second neutrino mass to the rung -26 case of the mass-at-rung function. Neutrino phenomenologists working inside Recognition Science cite it when converting solar oscillation splittings into absolute mass intervals. It is a direct substitution of the integer rung into the yardstick times phi to the power r expression.
Claim. $m_2 = y_0 · ϕ^{-26}$ where $y_0$ is the neutrino yardstick scale and $ϕ$ is the golden-ratio fixed point of the self-similar map.
background
The module organizes neutrino mass predictions around observed squared-mass differences by placing each species on an integer rung of the phi-ladder. The supporting definition nuMassAtRung(r) returns the product of the fixed yardstick and phi raised to rung r. The upstream from theorem extracts four structural conditions plus three definitional facts from seven independent axioms, supplying the justification for assigning the solar floor to rung -26.
proof idea
One-line definition that applies nuMassAtRung to the concrete argument -26.
why it matters
The definition supplies the concrete value used by nu2_abs_mass_interval, nu2_abs_mass_pos, nu2_abs_mass_upper, NuAbsMassCert, nu_rung_gap_ratio and nu_solar_rung_ratio. It realizes the T6 phi fixed-point and T7 eight-tick octave predictions for the neutrino sector, placing the solar and atmospheric splittings on the same phi-ladder that yields D = 3 and the alpha band. No open scaffolding remains at this site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.