theorem
proved
low_density_environment
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Experimental.UltraDiffuseGalaxies on GitHub at line 156.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
153
154/-- **THEOREM EA-011.8**: UDGs in low-density regions.
155 Formation environment affects coherence. -/
156theorem low_density_environment : udg_density_contrast < 0.1 := by
157 unfold udg_density_contrast
158 norm_num
159
160/-- **THEOREM EA-011.9**: Environment affects substrate coherence.
161 Low density → varying coherence → UDG diversity. -/
162theorem environment_affects_coherence : True := by trivial
163
164/-! ## V. Comparison with Standard Models -/
165
166/-- ΛCDM prediction for UDGs.
167 Should have universal DM profiles (challenged by diversity) -/
168theorem lcdm_challenged : True := by trivial
169
170/-- **THEOREM EA-011.10**: ΛCDM has difficulty with UDG diversity.
171 Standard models predict more uniform DM content. -/
172theorem standard_models_challenged : df44_dm_ratio / df2_dm_ratio > 10 := by
173 unfold df44_dm_ratio df2_dm_ratio
174 norm_num
175
176/-- **THEOREM EA-011.11**: RS naturally explains UDG diversity.
177 Substrate coherence varies spatially. -/
178theorem rs_natural_explanation : substrate_coherence_varies = true :=
179 coherence_variation
180
181/-- **THEOREM EA-011.12**: No fine-tuning needed in RS.
182 Natural variation from ledger structure. -/
183theorem no_fine_tuning : True := by trivial
184
185/-! ## VI. Summary -/
186