pith. machine review for the scientific record. sign in
def definition def or abbrev high

low_coherence_dm_poor

show as:
view Lean formalization →

Low coherence regions are defined as dark-matter poor with weak substrate coupling in the ultra-diffuse galaxy model. Galaxy formation analyses using Recognition Science substrate distribution cite this flag to separate NGC 1052-DF2-like cases from Dragonfly 44. The assignment follows directly from spatial variation in ledger coherence without further derivation.

claimIn low-coherence regions the dark-matter-to-stellar-mass ratio satisfies $M_{DM}/M_*sim 1-2$, corresponding to weak substrate coupling.

background

The module treats ultra-diffuse galaxies as systems with surface brightness above 24 mag/arcsec² whose dark matter content varies. Dark matter is identified with the substrate, a ledger carrier whose distribution follows recognition coherence rather than particle dynamics. Upstream the ILG Substrate structure supplies a normalized state and Hamiltonian inside the RS Hilbert space; the theology Substrate supplies phase, sigma charge and label. Low coherence therefore produces weak coupling and DM-poor galaxies.

proof idea

One-line definition that sets the Boolean flag to true, encoding the low-coherence DM-poor correspondence stated in the substrate model.

why it matters in Recognition Science

The definition supplies the EA-011.4 marker inside the ultra-diffuse galaxy analysis, asserting that substrate coherence varies spatially. It supports the RS claim that both DM-rich and DM-poor UDGs arise from the same ledger structure, with ILG rotation curves fitting either case without extra dark-matter components. The flag closes one concrete step in the module's verdict that UDG diversity is natural under Recognition Science.

scope and limits

formal statement (Lean)

 112def low_coherence_dm_poor : Bool := true

proof body

Definition body.

 113
 114/-- **THEOREM EA-011.4**: Substrate coherence varies spatially.
 115    Natural in RS ledger structure. -/

depends on (2)

Lean names referenced from this declaration's body.