pith. machine review for the scientific record. sign in
theorem proved term proof high

low_density_environment

show as:
view Lean formalization →

Ultra-diffuse galaxies form in regions where the density contrast falls below 0.1. Galaxy-formation researchers working in the Recognition Science substrate model cite this result to connect low-density environments to spatially varying coherence and the observed DM-rich versus DM-poor diversity. The proof is a one-line term reduction that unfolds the contrast definition and applies numerical normalization.

claimThe density contrast for ultra-diffuse galaxy formation satisfies $δρ/ρ < 0.1$.

background

The EA-011 module treats ultra-diffuse galaxies through the Recognition Science substrate model, in which dark matter is ledger coherence distributed across environments rather than particulate. The definition udg_density_contrast sets the contrast δρ/ρ to 0.05 relative to the cosmic mean. This rests on the Environment structure, which encodes an environment by its number of degrees of freedom, temperature, and interaction strength, together with the density scaling density(k) := φ^k from the phi-ladder.

proof idea

The term proof unfolds udg_density_contrast to its explicit value 0.05 and invokes norm_num to discharge the inequality 0.05 < 0.1.

why it matters in Recognition Science

The result supplies the low-density premise required by the EA-011 certificate, which concludes that UDG diversity follows directly from spatially varying substrate coherence. It completes the EA-011.8 step in the module and aligns with the Recognition Science claim that high-coherence regions produce DM-rich objects such as Dragonfly 44 while low-coherence regions produce DM-poor objects such as NGC 1052-DF2.

scope and limits

formal statement (Lean)

 156theorem low_density_environment : udg_density_contrast < 0.1 := by

proof body

Term-mode proof.

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.