theorem
proved
alpha_gravity_pos
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Gravity.GravityParameters on GitHub at line 58.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
82/-- Upsilon-star bounds imply positivity of the stellar mass-to-light ratio. -/
83theorem upsilon_star_bounds_implies_pos (h : 1.5 < upsilon_star ∧ upsilon_star < 1.62) :
84 0 < upsilon_star := by
85 linarith [h.1]
86
87/-! ## 3. C_ξ (Morphology Coupling) — HAS RS BASIS
88