`alpha_gravity`

definition

show as: view math explainer →

module: IndisputableMonolith.Gravity.GravityParameters
domain: Gravity
line: 49 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Gravity.GravityParameters on GitHub at line 49.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  46
  47/-- The RS-derived dynamical-time exponent.
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.