row_sqmass_ratio_phi7
plain-language theorem explainer
row_sqmass_ratio_phi7 delivers the exact identity (phi^{toReal res_nu3})^2 / (phi^{toReal res_nu2})^2 = phi^7 for the upgraded neutrino rungs. Neutrino modelers inside the Recognition Science ladder cite it to fix the atmospheric-to-solar squared-mass splitting at phi^7 without adjustable parameters. The proof is a one-line wrapper that invokes the upstream structural theorem squared_mass_ratio_structural_phi7.
Claim. $ (phi^{r_3})^2 / (phi^{r_2})^2 = phi^7 $, where $r_3 =$ res_nu3 and $r_2 =$ res_nu2 are the atmospheric and solar rungs satisfying $r_3 - r_2 = 7/2$.
background
In the P2-ν phase the neutrino mass scale is placed on the phi-ladder using fractional rungs. res_nu3 places the atmospheric neutrino at an integer base plus quarter-cycle offset; res_nu2 places the solar neutrino at res_nu3 minus nu_spacing, enforcing the 7/2 gap. The toReal conversion from RungFractions turns each rational rung into a real exponent for Real.goldenRatio powers. squared_mass_ratio_structural_phi7 proves the resulting ratio identity by algebraic reduction of the exponent difference.
proof idea
The proof is a one-line wrapper that applies squared_mass_ratio_structural_phi7. That lemma converts the rung gap 7/2 into an exponent difference of exactly 7 using the algebraic properties of Real.goldenRatio and the toReal transport.
why it matters
This equality supplies the structural phi^7 ratio required by neutrinoMassScaleScoreCardCert_holds to certify the scorecard rows. It realizes the module-level prediction that m_3^2/m_2^2 equals phi^7 under the res_nu3 - res_nu2 = 7/2 model. The result closes one link between the eight-tick octave, the phi fixed point, and observable neutrino splittings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.