theorem
proved
tactic proof
squared_mass_ratio_structural_phi7
show as:
view Lean formalization →
formal 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) -/