ml_geometric_is_phi

formal source

 114/-- The M/L ratio from geometric constraints -/
 115noncomputable def ml_geometric : ℝ := φ
 116
 117theorem ml_geometric_is_phi : ml_geometric = φ := rfl
 118
 119/-- The geometric M/L matches observations -/
 120theorem ml_geometric_bounds : 1 < ml_geometric ∧ ml_geometric < 2 := by
 121  unfold ml_geometric φ
 122  constructor
 123  · exact Constants.one_lt_phi
 124  · exact Constants.phi_lt_two
 125
 126/-! ## Information-Theoretic Derivation -/
 127
 128/-- Information content of mass vs light.
 129
 130The ledger tracks:
 131- Mass events: I_mass = n_mass × J_bit information
 132- Light events: I_light = n_light × J_bit information
 133
 134Conservation: I_mass + I_light = I_total
 135
 136At equilibrium, the ratio n_mass/n_light = φ because φ is the
 137unique fixed point of the J-cost recursion. -/
 138theorem information_balance_gives_phi :
 139    ∃ (ratio : ℝ), ratio = φ ∧ ratio ^ 2 = ratio + 1 := by
 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