low_density_environment
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.