module module

`IndisputableMonolith.Experimental.UltraDiffuseGalaxies`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Gravity.ILGDerivation module_import

declarations in this module (25)

def df44_dm_ratio L68
def df2_dm_ratio L72
def udg_surface_brightness L76
def udg_size L80
theorem udg_diversity_real L84
theorem dragonfly44_dm_rich L90
theorem ngc1052df2_dm_poor L96
def substrate_coherence_varies L104
def high_coherence_dm_rich L108
def low_coherence_dm_poor L112
theorem coherence_variation L116
theorem no_universal_ratio L120
def ilg_fit_quality L128
theorem ilg_better_than_lcdm L132
theorem ilg_sufficient L136
theorem ilg_universal L142
def formation_in_low_density L148
def udg_density_contrast L152
theorem low_density_environment L156
theorem environment_affects_coherence L162
theorem lcdm_challenged L168
theorem standard_models_challenged L172
theorem rs_natural_explanation L178
theorem no_fine_tuning L183
def ea011_certificate L207