squared_mass_ratio_structural_phi7
plain-language theorem explainer
The theorem shows that the squared structural mass ratio for neutrino generations 3 and 2 equals exactly phi to the 7 when their phi-ladder rung difference is 7/2. Neutrino mass modelers in the Recognition Science framework cite it to obtain the exact Delta m squared ratio prediction from the ladder law. The tactic proof reduces the expression by substituting the gap lemma, applying rpow_sub and rpow_mul, then normalizing Nat powers via div_pow and rpow_natCast.
Claim. Let $r_3$ and $r_2$ be the phi-ladder rungs for the third and second neutrino generations. If $r_3 - r_2 = 7/2$, then $ (phi^{r_3})^2 / (phi^{r_2})^2 = phi^7 $, where $phi$ denotes the golden ratio.
background
The NeutrinoSector module places neutrinos on the deep phi-ladder with rungs near -54 for the atmospheric scale and -58 for the solar scale. Structural masses follow the ladder law: yardstick times phi to the adjusted rung, after the legacy conversion MeV_to_eV that reuses the electron structural mass as a display unit. The module enforces a rung gap of 7/2 between nu3 and nu2 to produce the exact squared-mass ratio without numerics.
proof idea
The tactic proof begins by establishing positivity of the golden ratio. It calls the rung gap lemma to obtain res_nu3 minus res_nu2 equals 7/2 in rationals and converts the equality to reals. It rewrites the ratio of powers via rpow_sub, reduces the square via rpow_mul to an exponent of 7, then normalizes the original Nat powers with div_pow and rpow_natCast before substituting the reduced form.
why it matters
This supplies the exact phi^7 factor for the squared mass ratio under the T14 neutrino hypothesis. It is invoked directly by row_sqmass_ratio_phi7 in NeutrinoMassScaleScoreCard to populate the structural entry. In the framework it realizes the phi-ladder mass formula for Delta m squared ratios, confirming that the enforced 7/2 gap yields the observed scale separation as a direct consequence of the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.