`ilg_universal`

proved

show as: view math explainer →

module: IndisputableMonolith.Experimental.UltraDiffuseGalaxies
domain: Experimental
line: 142 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Experimental.UltraDiffuseGalaxies on GitHub at line 142.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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.
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.