theorem
proved
ilg_sufficient
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 136.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
133
134/-- **THEOREM EA-011.6**: ILG fits UDG rotation curves.
135 No additional dark matter needed beyond substrate. -/
136theorem ilg_sufficient : ilg_fit_quality < 2 := by
137 unfold ilg_fit_quality
138 norm_num
139
140/-- **THEOREM EA-011.7**: ILG applies to both DM-rich and DM-poor.
141 Same formula, different coherence parameter. -/
142theorem ilg_universal : True := by trivial
143
144/-! ## IV. Formation Environment -/
145
146/-- UDGs form in low-density environments.
147 Voids, outskirts of clusters -/
148def formation_in_low_density : Bool := true
149
150/-- Density contrast for UDG formation.
151 δρ/ρ < 0.1 compared to mean -/
152noncomputable def udg_density_contrast : ℝ := 0.05
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.