nu2_abs_mass_upper
plain-language theorem explainer
The theorem shows that the Recognition Science predicted mass for the second neutrino eigenstate satisfies m_ν₂ < 0.012 eV. Neutrino phenomenologists cite this when matching the phi-ladder output to solar splitting data and cosmological sum bounds. The proof unfolds the rung definition, invokes the helper lemma that phi to a negative integer power is less than one, and finishes with nlinarith on positivity.
Claim. The predicted absolute mass of the second neutrino eigenstate satisfies $m_2 < 0.012$ eV, where the prediction is nuYardstick times phi to the power -26 and nuYardstick is the 0.0031 eV scale fitted to the solar mass-squared splitting.
background
Neutrino masses sit on the phi-ladder. nuYardstick is the base scale 0.0031 eV fitted once from the solar Δm²₂₁ floor. nuMassAtRung(r) scales this base by phi^r, so m_nu2_pred is defined as nuMassAtRung(-26). The module treats observed mass differences by converting squared splittings into absolute predictions via this self-similar scaling.
proof idea
Unfold m_nu2_pred, nuMassAtRung and nuYardstick to reduce the goal to 0.0031 * phi^{-26} < 0.012. Apply zpow_neg_lt_one to obtain phi^{-26} < 1, then close with nlinarith using the positivity of the power term.
why it matters
Supplies the upper bound for nu2_abs_mass_interval, which populates the nuAbsMassCert certificate. Realizes the RS mass formula yardstick * phi^r in the neutrino sector, consistent with the phi fixed point and eight-tick octave. Aligns with the module focus on converting observed splittings into absolute scales without invoking seesaw mechanisms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.