`udg_surface_brightness`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Experimental.UltraDiffuseGalaxies on GitHub at line 76.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

radius IndisputableMonolith.Complexity.CellularAutomata

formal source

  73
  74/-- Typical UDG surface brightness (mag/arcsec²).
  75    Value: μ_V > 24 -/
  76noncomputable def udg_surface_brightness : ℝ := 25.0
  77
  78/-- UDG effective radius (kpc).
  79    Value: r_e ~ 1-10 kpc -/
  80noncomputable def udg_size : ℝ := 5.0
  81
  82/-- **THEOREM EA-011.1**: UDG diversity is real.
  83    Both DM-rich and DM-poor examples exist. -/
  84theorem udg_diversity_real : df44_dm_ratio > 10 ∧ df2_dm_ratio < 5 := by
  85  unfold df44_dm_ratio df2_dm_ratio
  86  constructor <;> norm_num
  87
  88/-- **THEOREM EA-011.2**: Dragonfly 44 is DM-rich.
  89    M_DM/M_stars ~ 70 >> 1. -/
  90theorem dragonfly44_dm_rich : df44_dm_ratio > 50 := by
  91  unfold df44_dm_ratio
  92  norm_num
  93
  94/-- **THEOREM EA-011.3**: NGC 1052-DF2 is DM-poor.
  95    M_DM/M_stars ~ 1.5 ≈ 1. -/
  96theorem ngc1052df2_dm_poor : df2_dm_ratio < 3 := by
  97  unfold df2_dm_ratio
  98  norm_num
  99
 100/-! ## II. RS Substrate Model -/
 101
 102/-- Recognition coherence varies spatially.
 103    C(x) = C_0 × f(φ, environment) -/
 104def substrate_coherence_varies : Bool := true
 105
 106/-- High coherence region: DM-rich.

papers checked against this theorem

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