pith. machine review for the scientific record. sign in
theorem proved tactic proof

alpha_gravity_pos

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  58theorem alpha_gravity_pos : 0 < alpha_gravity := by

proof body

Tactic-mode proof.

  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 -/

depends on (9)

Lean names referenced from this declaration's body.