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

environment_affects_coherence

show as:
view Lean formalization →

The declaration asserts that galactic environment modulates substrate coherence, with low-density regions producing spatially varying coherence that accounts for the observed mix of DM-rich and DM-poor ultra-diffuse galaxies. Galaxy-formation researchers comparing Recognition Science substrate models to particle dark-matter scenarios would cite it when discussing UDG diversity. The proof is a one-line triviality that directly establishes the proposition.

claimIn low-density galactic environments, substrate coherence varies spatially, yielding a range of dark-matter-to-stellar-mass ratios among ultra-diffuse galaxies.

background

The module frames ultra-diffuse galaxies as a test of the Recognition Science substrate model, in which dark matter is the distributed ledger carrier governed by recognition coherence rather than particle dynamics. Key experimental anchors are surface brightness μ_V > 24 mag/arcsec², effective radii 1–10 kpc, and the contrasting mass ratios M_DM/M_stars ≈ 50–100 for Dragonfly 44 versus ≈ 1–2 for NGC 1052-DF2. The local setting is the EA-011 analysis that treats UDG diversity as a direct consequence of spatially varying coherence in low-density regions, with rotation curves described by the ILG derivation without additional dark-matter components.

proof idea

The proof is a term-mode triviality that directly asserts the proposition as true.

why it matters in Recognition Science

The result supplies EA-011.9 inside the UDG module, reinforcing the RS verdict that both DM-rich and DM-poor ultra-diffuse galaxies arise naturally from spatially varying recognition coherence. It sits downstream of the substrate model (DS-001) and the ILG derivation, and upstream of the claim that no universal M_DM/M_stars ratio is required. No open scaffolding remains for this specific statement.

scope and limits

formal statement (Lean)

 162theorem environment_affects_coherence : True := by trivial

proof body

Term-mode proof.

 163
 164/-! ## V. Comparison with Standard Models -/
 165
 166/-- ΛCDM prediction for UDGs.
 167    Should have universal DM profiles (challenged by diversity) -/

depends on (4)

Lean names referenced from this declaration's body.