massSplitRatio
plain-language theorem explainer
The adjacent mass-squared splitting ratio for neutrinos on the phi-ladder is defined as the square of the golden ratio constant phi. Cosmologists enumerating neutrino mass states would cite this when building the five-state hierarchy certificate. It is a direct one-line definition with no computational steps.
Claim. The adjacent mass-squared splitting ratio is defined by $r = phi^2$, where $phi$ denotes the golden ratio fixed point.
background
The phi-ladder places successive masses at integer powers of the golden ratio phi, the self-similar fixed point forced by the Recognition Composition Law. In this module three neutrino masses m1 < m2 < m3 sit on the ladder; the ratio of adjacent mass-squared splittings is required to equal phi squared. The module states that this choice plus the two hierarchy scenarios yields exactly five configurations, matching configDim D.
proof idea
This is a one-line definition that directly assigns the value phi squared in the reals.
why it matters
The definition supplies the splitting ratio required by NeutrinoHierarchyCert to certify five states, positive ratio, and equality to phi plus one. It implements the phi-ladder step inside the cosmology module and connects to the T6 fixed-point construction. No open scaffolding remains in the file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.