def
definition
ml_geometric
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Astrophysics.ObservabilityLimits on GitHub at line 115.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
112 simp
113
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