pith. sign in
def

formation_in_low_density

definition
show as:
module
IndisputableMonolith.Experimental.UltraDiffuseGalaxies
domain
Experimental
line
148 · github
papers citing
none yet

plain-language theorem explainer

Ultra-diffuse galaxies form in low-density environments such as voids and cluster outskirts. Researchers modeling galaxy formation under Recognition Science's substrate framework for dark matter would cite this definition when discussing spatial variation in recognition coherence. The implementation is a direct Boolean constant assignment with no computation or lemmas applied.

Claim. Ultra-diffuse galaxies form in low-density environments where the density contrast satisfies $δρ/ρ < 0.1$ relative to the mean cosmic density, specifically in voids and the outskirts of clusters.

background

The module EA-011 analyzes ultra-diffuse galaxies under Recognition Science, treating dark matter as substrate distributed by recognition coherence rather than particles. High-coherence regions produce DM-rich UDGs such as Dragonfly 44 while low-coherence regions produce DM-poor cases such as NGC 1052-DF2, with no universal mass ratio required. Rotation curves are described by the ILG derivation without additional dark-matter fits. The upstream result is the structure for from UniversalForcingSelfReference, which records structural properties required by orbit and step coherence axioms for meta-realization.

proof idea

This is a one-line definition that directly assigns the Boolean value true, accompanied by the inline comment on density contrast for UDG formation.

why it matters

The definition completes the formation step in the RS substrate model for UDGs, supporting the module verdict that both DM-rich and DM-poor examples arise naturally from spatially varying coherence. It sits alongside sibling definitions for surface brightness, size, and coherence variation, and connects to the ILG connection for rotation curves. No downstream uses are recorded, leaving it as a declarative anchor within the experimental analysis rather than a theorem feeding further derivations.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.