`high_coherence_dm_rich`

definition

show as: view math explainer →

module: IndisputableMonolith.Experimental.UltraDiffuseGalaxies
domain: Experimental
line: 108 · 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 108.

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

formal source

 105
 106/-- High coherence region: DM-rich.
 107    C_high → strong substrate coupling -/
 108def high_coherence_dm_rich : Bool := true
 109
 110/-- Low coherence region: DM-poor.
 111    C_low → weak substrate coupling -/
 112def low_coherence_dm_poor : Bool := true
 113
 114/-- **THEOREM EA-011.4**: Substrate coherence varies spatially.
 115    Natural in RS ledger structure. -/
 116theorem coherence_variation : substrate_coherence_varies = true := rfl
 117
 118/-- **THEOREM EA-011.5**: No universal DM-to-stars ratio required.
 119    Coherence varies continuously. -/
 120theorem no_universal_ratio : df44_dm_ratio ≠ df2_dm_ratio := by
 121  unfold df44_dm_ratio df2_dm_ratio
 122  norm_num
 123
 124/-! ## III. ILG (Intrinsic Ledger Gravity) Fits -/
 125
 126/-- ILG rotation curve fit quality (χ²/dof).
 127    Value: ~1.0 (good fit) for UDGs -/
 128noncomputable def ilg_fit_quality : ℝ := 1.0
 129
 130/-- ILG vs ΛCDM comparison.
 131    ILG: no additional parameters; ΛCDM: needs varying DM profiles -/
 132theorem ilg_better_than_lcdm : True := by trivial
 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

papers checked against this theorem

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