nu_rung_gap_ratio
plain-language theorem explainer
The theorem establishes that the ratio of predicted third to second neutrino masses equals phi to the sixth power. Neutrino phenomenology researchers in the Recognition Science mass ladder would cite this when matching the phi-based rung assignments to oscillation data. The proof is a direct algebraic simplification obtained by unfolding the mass definitions and canceling common factors via field simplification after non-zero checks.
Claim. The ratio of the predicted third-generation neutrino mass to the second-generation neutrino mass satisfies $m_3 / m_2 = phi^6$, where each mass is the yardstick scaled by the appropriate power of phi at its rung adjusted by the gap function for the species.
background
In Recognition Science, fermion masses sit on the phi-ladder via yardstick times phi to the power (rung minus 8 plus gap(Z)), with rung an integer level per species and gap(Z) the logarithmic residue ln(1 + Z/phi)/ln(phi). The module addresses observed mass differences for neutrinos. Upstream results supply rung as the integer 1 for certain fermions, gap as the product of closure and Fibonacci factors (claimed equal to 45), and the anchor gap function F(Z) as the closed-form residue at the anchor scale.
proof idea
The proof unfolds the definitions of the two predicted masses, which invoke the nuMassAtRung predicate. It then proves phi and the neutrino yardstick are nonzero via positivity lemmas, followed by a single field_simp application that cancels the common factors to obtain the exact power of phi.
why it matters
This supplies the exact rung-gap ratio required by the downstream absolute mass certification. It completes the neutrino sector of the phi-ladder mass formula, aligning with the T5 J-uniqueness and T6 self-similar fixed point while producing a ratio close to observed oscillation data. The result advances the claim that neutrino masses follow directly from the Recognition Science constants without extra parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.