theorem
proved
alpha_gravity_eq_two_alphaLock
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Gravity.GravityParameters on GitHub at line 51.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
48 α_gravity = 2 · alphaLock = 1 - 1/φ ≈ 0.382 -/
49def alpha_gravity : ℝ := 1 - 1 / phi
50
51theorem alpha_gravity_eq_two_alphaLock : alpha_gravity = 2 * alphaLock := by
52 unfold alpha_gravity alphaLock
53 ring
54
55/-- Paper fitted value: 0.389 ± 0.015
56 RS prediction: 1 - 1/φ ≈ 0.382
57 Match: 1.8% -/
58theorem alpha_gravity_pos : 0 < alpha_gravity := by
59 unfold alpha_gravity
60 have h := one_lt_phi -- 1 < φ
61 have hphi_pos := phi_pos
62 have : 1 / phi < 1 := by
63 rw [div_lt_one hphi_pos]
64 exact h
65 linarith
66
67/-! ## 2. Υ★ (Mass-to-Light Ratio) — DERIVED
68
69The stellar mass-to-light ratio is φ.
70This is proven in `Astrophysics/MassToLight.lean`. -/
71
72/-- The RS-derived stellar mass-to-light ratio.
73 Υ★ = φ ≈ 1.618 -/
74def upsilon_star : ℝ := phi
75
76theorem upsilon_star_eq_phi : upsilon_star = phi := rfl
77
78theorem upsilon_star_bounds : 1.5 < upsilon_star ∧ upsilon_star < 1.62 := by
79 unfold upsilon_star
80 exact ⟨phi_gt_onePointFive, phi_lt_onePointSixTwo⟩
81