m_nu3_pred
plain-language theorem explainer
The definition supplies the predicted absolute mass for the third neutrino as the Recognition Science phi-ladder value at rung -20. Neutrino hierarchy certificates and ratio theorems cite it to bound sums and confirm positivity. It is a direct one-line instantiation of the general nuMassAtRung function with no further reduction.
Claim. $m_3^pred = nuYardstick * phi^{-20}$, where nuYardstick is the neutrino base scale and phi is the golden ratio fixed point.
background
The module treats observed neutrino mass differences inside the Recognition Science Standard Model extension. Masses are assigned on the phi-ladder by scaling a yardstick by integer powers of phi at chosen rungs; rung -20 is selected here for the atmospheric floor of the heaviest state. Upstream rung and gap definitions appear in Constants and Gap45.Derivation, where gap is the product of closure and Fibonacci factors and equals 45. The nuYardstick itself is fixed by the neutrino-specific anchor policy.
proof idea
One-line definition that applies nuMassAtRung directly at the integer argument -20. The body expands to nuYardstick multiplied by phi to the power -20; no lemmas, tactics, or reductions are invoked.
why it matters
It supplies the concrete value required by nu3_abs_mass_positive, NuAbsMassCert, nu_rung_gap_ratio, and nu_sum_bound_consistent. The ratio theorem then shows m3/m2 equals phi^6, aligning with observed atmospheric splitting. This realizes the mass-ladder prediction step for neutrinos and connects to the phi fixed point and eight-tick octave structure in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.