MassOrdering
plain-language theorem explainer
The declaration introduces an inductive type that classifies neutrino mass hierarchies into normal or inverted orderings based on observed squared mass splittings. Physicists assigning rung values on the phi-ladder for RS neutrino mass predictions cite it to select the hierarchy in downstream constants. The definition consists of a direct inductive declaration with two constructors and carries no proof obligations.
Claim. The type of neutrino mass orderings consisting of the case normal ordering where $m_1 < m_2 < m_3$ and the case inverted ordering where $m_3 < m_1 < m_2$.
background
The module treats neutrino masses through the phi-ladder structure of Recognition Science, importing constants and phi-interval bounds to constrain predictions from observed squared mass differences. This inductive type provides the classification needed to label the three neutrino masses consistently with experimental data on the splittings. No upstream lemmas are required; the definition stands alone as a carrier for hierarchy choice in rung assignments.
proof idea
The declaration is a direct inductive definition that introduces two nullary constructors. No lemmas are applied, no tactics are used, and the body contains no reduction steps or proof terms.
why it matters
The type is referenced by the rsPrediction definition that fixes the normal ordering for RS neutrino rung assignments on the phi-ladder. This choice feeds the mass formula using yardstick times phi to a rung offset and aligns with the forcing chain that yields three spatial dimensions. It leaves open the question of whether the RS framework can derive the hierarchy preference rather than stipulate it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.