massSplitRatio_eq
plain-language theorem explainer
The theorem establishes that the neutrino mass-squared splitting ratio equals the golden ratio plus one. Cosmologists enumerating phi-ladder hierarchies cite this identity to certify the five-state count. The proof is a one-line wrapper that unfolds the ratio definition and invokes the standard phi-squared identity.
Claim. The adjacent neutrino mass-squared splitting ratio equals $phi + 1$.
background
The module treats three neutrino masses ordered on the phi-ladder with adjacent mass-squared splittings whose ratio is defined as phi squared. The phi square equation lemma states that phi squared equals phi plus one, the defining algebraic identity of the golden ratio. The local setting is the structural count of three masses plus two hierarchy orientations, totaling five states that match configDim D.
proof idea
One-line wrapper that unfolds the massSplitRatio definition and applies the phi square equation identity from the constants module.
why it matters
This supplies the split ratio field inside the neutrinoHierarchyCert definition, which records the five-state enumeration. It closes the phi-ladder step required by the cosmology module and connects to the forced phi fixed point in the recognition chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.