normal_ordering
plain-language theorem explainer
Neutrino masses placed on the phi-ladder increase strictly with rung index, so the mass at rung k is less than the mass at rung k+1 for every natural number k. Modelers of neutrino spectra inside Recognition Science cite the result to lock in the predicted normal hierarchy against the three-flavor data. The proof unfolds the mass definition, inserts the golden-ratio square identity, records positivity of the power, rewrites the successor exponent, and finishes with linear arithmetic on phi greater than one.
Claim. For every natural number $k$, the neutrino mass at phi-ladder rung $k$ satisfies $m(k) < m(k+1)$.
background
Neutrino masses sit on the phi-ladder with ratios fixed by successive powers of the golden ratio, giving the three eigenstates the proportions phi^0 : phi^1 : phi^2. The module therefore asserts that Recognition Science predicts normal ordering for the three neutrino flavors. Upstream lemmas supply the key algebraic facts: phi squared equals phi plus one, and phi is strictly greater than one; both appear in Constants and are re-exported through PhiSupport.
proof idea
The term proof first unfolds neutrinoMass, then obtains the identity phi squared equals phi plus one. It records that phi to the k is positive, rewrites the successor power, and closes the inequality by linarith applied to one less than phi multiplied on the left by that positive term.
why it matters
The theorem supplies the normal_ordering field of the NeutrinoMassCert structure, which in turn certifies both the hierarchy and the constant phi ratio for any downstream mass calculation. It directly realizes the module claim that RS predicts normal ordering for the three flavors and thereby closes one link in the phi-ladder application to the neutrino sector. The result sits inside the broader forcing chain that derives D equals 3 and the eight-tick octave from the single functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.