udg_diversity_real
plain-language theorem explainer
The declaration asserts that Dragonfly 44 possesses a dark-matter-to-stellar-mass ratio above 10 while NGC 1052-DF2 possesses one below 5, confirming both dark-matter-rich and dark-matter-poor ultra-diffuse galaxies exist. Galaxy formation and modified-gravity researchers cite the result when confronting the observational spread in low-surface-brightness systems. The proof is a one-line term wrapper that unfolds the two ratio definitions and discharges the conjunction by numerical normalization.
Claim. Let $r_{44}$ denote the dark-matter-to-stellar-mass ratio of Dragonfly 44 and $r_2$ the ratio of NGC 1052-DF2. Then $r_{44} > 10$ and $r_2 < 5$.
background
Recognition Science treats dark matter as a distributed substrate whose local density tracks recognition coherence rather than particle orbits. The module supplies two concrete ratios drawn from observations: Dragonfly 44 at approximately 70 (range 50-100) and NGC 1052-DF2 at 1.5 (range 1-2). These values instantiate the claim that substrate coherence varies spatially, producing DM-rich UDGs in high-coherence patches and DM-poor UDGs in low-coherence patches without requiring a universal mass ratio.
proof idea
The term proof first unfolds the definitions of the two ratios, exposing the literals 70.0 and 1.5. Constructor splits the conjunction; norm_num then verifies each inequality by direct numerical comparison.
why it matters
The theorem anchors the EA-011 certificate, which states that ultra-diffuse galaxy diversity follows directly from the Recognition Science substrate model. It supplies the concrete observational content for the claim that no universal M_DM/M_* ratio is needed once coherence is allowed to vary. The result sits inside the experimental module that links ILG rotation curves to ledger-carrier dynamics and illustrates how the eight-tick substrate framework accommodates both Dragonfly 44 and NGC 1052-DF2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.