theorem
proved
term proof
information_balance_gives_phi
show as:
view Lean formalization →
formal statement (Lean)
138theorem information_balance_gives_phi :
139 ∃ (ratio : ℝ), ratio = φ ∧ ratio ^ 2 = ratio + 1 := by
proof body
Term-mode proof.
140 use φ
141 constructor
142 · rfl
143 · unfold φ
144 exact PhiSupport.phi_squared
145
146/-- The IMF (Initial Mass Function) slope follows from J-minimization.
147
148The Salpeter IMF has slope α ≈ 2.35.
149This is related to φ^2 ≈ 2.618 within the expected variation.
150
151The IMF shape is derived, not fitted. -/