squared_mass_ratio_structural_phi7
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the rung assignments for nu2 and nu3.
- Does not propagate experimental uncertainties on Delta m squared.
- Does not incorporate neutrino mixing angles or CP phases.
- Does not replace the legacy eV calibration with full RS-native units.
Lean usage
theorem row_sqmass_ratio_phi7 : (Real.goldenRatio ^ (toReal res_nu3)) ^ (2 : ℕ) / (Real.goldenRatio ^ (toReal res_nu2)) ^ (2 : ℕ) = Real.goldenRatio ^ (7 : ℝ) := squared_mass_ratio_structural_phi7formal statement (Lean)
572theorem squared_mass_ratio_structural_phi7 :
573 (Real.goldenRatio ^ (toReal res_nu3)) ^ (2 : ℕ) / (Real.goldenRatio ^ (toReal res_nu2)) ^ (2 : ℕ)
574 = Real.goldenRatio ^ (7 : ℝ) := by
proof body
Tactic-mode proof.
575 have hg0 : (0 : ℝ) ≤ Real.goldenRatio := le_of_lt (by simpa using Real.goldenRatio_pos)
576 have hgpos : (0 : ℝ) < Real.goldenRatio := by simpa using Real.goldenRatio_pos
577 -- Convert the rung gap from ℚ to ℝ.
578 have hgapQ : res_nu3 - res_nu2 = (7 : ℚ) / 2 := rung_gap_is_seven_halves
579 have hgapR : (res_nu3 : ℝ) - (res_nu2 : ℝ) = (7 : ℝ) / 2 := by
580 simpa using congrArg (fun q : ℚ => (q : ℝ)) hgapQ
581 -- Use rpow_sub to rewrite the ratio as a single rpow, then square via rpow_mul.
582 have hsub : (Real.goldenRatio ^ (res_nu3 : ℝ)) / (Real.goldenRatio ^ (res_nu2 : ℝ))
583 = Real.goldenRatio ^ ((res_nu3 : ℝ) - (res_nu2 : ℝ)) := by
584 -- `rpow_sub` gives the reverse direction; take `.symm`.
585 simpa using (Real.rpow_sub hgpos (res_nu3 : ℝ) (res_nu2 : ℝ)).symm
586 have hmul : (Real.goldenRatio ^ ((res_nu3 : ℝ) - (res_nu2 : ℝ))) ^ (2 : ℝ)
587 = Real.goldenRatio ^ (7 : ℝ) := by
588 -- rpow_mul reduces squaring to multiplying the exponent by 2.
589 calc
590 (Real.goldenRatio ^ ((res_nu3 : ℝ) - (res_nu2 : ℝ))) ^ (2 : ℝ)
591 = Real.goldenRatio ^ (((res_nu3 : ℝ) - (res_nu2 : ℝ)) * (2 : ℝ)) := by
592 -- rpow_mul: x^(y*z) = (x^y)^z
593 simpa using (Real.rpow_mul hg0 ((res_nu3 : ℝ) - (res_nu2 : ℝ)) (2 : ℝ)).symm
594 _ = Real.goldenRatio ^ (7 : ℝ) := by
595 -- substitute the gap (7/2) and simplify
596 simp [hgapR]
597 -- Now rewrite the goal. We bridge between Nat power and rpow at exponent 2 using `rpow_natCast`.
598 calc
599 (Real.goldenRatio ^ (toReal res_nu3)) ^ (2 : ℕ) / (Real.goldenRatio ^ (toReal res_nu2)) ^ (2 : ℕ)
600 = ((Real.goldenRatio ^ (res_nu3 : ℝ)) / (Real.goldenRatio ^ (res_nu2 : ℝ))) ^ (2 : ℕ) := by
601 -- (a^2)/(b^2) = (a/b)^2 for Nat powers
602 -- also normalize `toReal` away
603 simp [toReal, div_pow]
604 _ = (Real.goldenRatio ^ ((res_nu3 : ℝ) - (res_nu2 : ℝ))) ^ (2 : ℕ) := by
605 simpa [hsub]
606 _ = (Real.goldenRatio ^ ((res_nu3 : ℝ) - (res_nu2 : ℝ))) ^ (2 : ℝ) := by
607 -- convert Nat power back to rpow for the final exponent arithmetic
608 symm
609 simpa using (Real.rpow_natCast (Real.goldenRatio ^ ((res_nu3 : ℝ) - (res_nu2 : ℝ))) 2)
610 _ = Real.goldenRatio ^ (7 : ℝ) := by
611 simpa using hmul
612
613
614/-! ## Verification -/
615
616/-- PROVEN: Bounds on the predicted m3 mass.
617
618 Numerically: predicted_mass_eV (-54) ≈ 0.0563 eV
619 m3_approx = sqrt(2.453e-3) ≈ 0.0495 eV
620 |pred - exp| ≈ 0.0068 < 0.01
621
622 Proof: Uses structural_mass ∈ (10856, 10858) and φ^(-54) ∈ (5.181e-12, 5.185e-12) -/