df2_dm_ratio
plain-language theorem explainer
The definition assigns the value 1.5 to the dark-matter-to-stellar-mass ratio of NGC 1052-DF2. Galaxy-formation researchers and Recognition Science analysts cite the constant when contrasting DM-poor and DM-rich ultra-diffuse galaxies under the substrate-coherence model. The declaration is a direct real-number assignment with no further computation or lemmas.
Claim. Let $r_{DF2}$ denote the dark-matter-to-stellar-mass ratio for NGC 1052-DF2. Then $r_{DF2} = 1.5$.
background
The module treats dark matter as substrate distributed according to recognition coherence rather than particle dynamics. NGC 1052-DF2 supplies the DM-poor example with ratio near 1-2, set against the DM-rich case of Dragonfly 44 whose ratio lies near 50-100. The local setting states that UDG diversity follows from spatially varying substrate coherence and that ILG rotation curves fit both regimes without extra dark-matter components.
proof idea
The declaration is a direct definition that hard-codes the constant 1.5 drawn from the module's observational summary. No lemmas or tactics are invoked.
why it matters
The definition supplies the numerical input for the four downstream theorems that establish NGC 1052-DF2 is DM-poor, that no universal DM-to-stars ratio exists, that standard models are challenged by the observed spread, and that UDG diversity is real. It fills the concrete value slot required by the EA-011 substrate-model analysis of ultra-diffuse galaxies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.