nu1_abs_mass_upper
plain-language theorem explainer
The theorem establishes that the RS-predicted absolute mass of the lightest neutrino satisfies m_ν1 < 0.012 eV. Cosmologists and neutrino physicists comparing phi-ladder predictions to the cosmological sum bound would cite this result. The proof unfolds the mass definition to expose a negative power of phi, invokes a dedicated positivity lemma for that power, and closes via linear arithmetic.
Claim. The RS-predicted mass of the lightest neutrino on the phi-ladder satisfies $m_1 = y_0 · ϕ^{-28} < 0.012$, where $y_0$ denotes the neutrino yardstick scale.
background
The NeutrinoMassHierarchy module derives absolute neutrino masses from the phi-ladder after the observed squared-mass differences. The yardstick supplies the base mass unit; rung -28 is assigned to ν₁, so the predicted mass is the yardstick times ϕ to the power -28. This places the value below one-tenth of the cosmological sum bound of 0.12 eV.
proof idea
The tactic proof unfolds m_nu1_pred, nuMassAtRung and nuYardstick to reach the expression yardstick · ϕ^{-28}. It applies the lemma zpow_neg_lt_one at exponent 28 to obtain ϕ^{-28} < 1, then invokes nlinarith together with the positivity of ϕ to a negative power.
why it matters
The result populates the nu1_upper field inside nuAbsMassCert, which collects certified absolute-mass bounds for all three neutrinos. It supports the RS claim that neutrino masses occupy the phi-ladder below the cosmological sum limit and aligns with the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.