pith. machine review for the scientific record. sign in
def definition def or abbrev

ea011_certificate

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

formal statement (Lean)

 207def ea011_certificate : String :=

proof body

Definition body.

 208  "═══════════════════════════════════════════════════════════\n" ++
 209  "  EA-011: ULTRA-DIFFUSE GALAXIES — STATUS: EXPLAINED\n" ++
 210  "═══════════════════════════════════════════════════════════\n" ++
 211  "✓ udg_diversity_real:               Both DM-rich and DM-poor\n" ++
 212  "✓ dragonfly44_dm_rich:              M_DM/M_* ~ 70\n" ++
 213  "✓ ngc1052df2_dm_poor:                 M_DM/M_* ~ 1.5\n" ++
 214  "✓ coherence_variation:                  Substrate varies spatially\n" ++
 215  "✓ no_universal_ratio:                   No required M_DM/M_*\n" ++
 216  "✓ ilg_sufficient:                         Fits rotation curves\n" ++
 217  "✓ low_density_environment:                  Formation in voids\n" ++
 218  "✓ standard_models_challenged:               ΛCDM difficulty\n" ++
 219  "✓ rs_natural_explanation:                     Substrate model\n" ++
 220  "VERDICT: Explained by RS substrate model.\n" ++
 221  "  Spatial coherence variation → UDG diversity.\n"
 222
 223#eval ea011_certificate
 224
 225end UltraDiffuseGalaxies
 226end Experimental
 227end IndisputableMonolith

depends on (16)

Lean names referenced from this declaration's body.