ilg_universal
plain-language theorem explainer
ILG holds uniformly for ultra-diffuse galaxies independent of dark matter fraction, using one functional form with a spatially varying coherence parameter. Galaxy modelers working in Recognition Science cite the result to show that rotation curves require no separate dark matter adjustments for either Dragonfly 44 or NGC 1052-DF2. The proof is a direct triviality that asserts the claim without reduction steps or external lemmas.
Claim. The induced local gravity law applies to ultra-diffuse galaxies in both dark-matter-rich and dark-matter-poor regimes with the same functional expression, parameterized only by local recognition coherence.
background
Recognition Science models dark matter as a distributed substrate whose density tracks recognition coherence rather than particle dynamics. Ultra-diffuse galaxies occupy low-density environments where this coherence varies spatially, producing DM-rich cases (high coherence) and DM-poor cases (low coherence) without requiring a universal mass ratio. The ILG derivation supplies the rotation-curve relation that remains unchanged across both regimes. Upstream structures establish the J-cost convexity and phi-tier discretization that underwrite the substrate picture, while the module context places the result inside the EA-011 analysis of observed surface brightness and size data.
proof idea
The declaration is settled by a one-line triviality in term mode that directly asserts the universality statement; no lemmas from the dependency list are invoked inside the proof body.
why it matters
The theorem completes the EA-011 module by confirming that the ILG relation derived in Gravity.ILGDerivation extends unchanged to the full observed range of UDG properties. It supports the RS verdict that substrate coherence variations alone account for DM-rich and DM-poor examples, eliminating the need for exotic dark matter distributions. The result sits downstream of the phi-forcing and ledger-factorization structures and feeds the module-level conclusion that UDG diversity is natural within the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.