rsPrediction
plain-language theorem explainer
RS neutrino mass prediction selects the normal hierarchy for the three neutrino mass eigenstates. Neutrino oscillation experiments would cite this assignment when testing against measured mass-squared splittings. The definition directly instantiates the normal branch using rung assignments on the phi ladder with yardstick phi to the minus five.
Claim. The Recognition Science neutrino mass prediction is the normal ordering $m_1 < m_2 < m_3$, with rung assignments -28, -26, -20 on the phi-ladder (yardstick $m_0 = phi^{-5}$).
background
The module addresses observed mass differences. Neutrino masses sit on the phi-ladder shifted by the seesaw offset from the Majorana scale, with yardstick $m_0 = phi^{-5}$ in RS-native units. Normal hierarchy assigns nu1 to rung -28 (lightest), nu2 to -26 (solar splitting), nu3 to -20 (atmospheric splitting). Upstream results supply rung as a natural number and scale as phi to the power k.
proof idea
One-line definition that directly returns the Normal constructor of the mass ordering inductive type.
why it matters
This definition supplies the concrete rung assignments for neutrinos in the phi-ladder framework, enabling mass predictions that match oscillation data via rung gaps of 6 and 4. It fills the rung assignment step for the standard model neutrino sector and connects to the mass formula using phi powers. No downstream uses are listed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.