no_universal_ratio
plain-language theorem explainer
The theorem establishes that the dark-matter-to-stellar-mass ratio for Dragonfly 44 differs from the ratio for NGC 1052-DF2. Galaxy formation researchers would cite it when rejecting any fixed universal ratio across ultra-diffuse galaxies. The proof is a one-line wrapper that unfolds the two constant definitions and reduces the inequality by numerical normalization.
Claim. The Dragonfly 44 dark-matter-to-stellar-mass ratio is unequal to the NGC 1052-DF2 dark-matter-to-stellar-mass ratio.
background
In the EA-011 module, ultra-diffuse galaxies are analyzed under the Recognition Science substrate model in which dark matter is the ledger carrier whose distribution follows local recognition coherence rather than particle dynamics. The sibling definitions supply the concrete ratios: Dragonfly 44 at 70.0 and NGC 1052-DF2 at 1.5. The module setting states that both DM-rich and DM-poor UDGs arise naturally once coherence is allowed to vary spatially, removing any requirement for a single M_DM/M_* value.
proof idea
The proof is a one-line wrapper that unfolds df44_dm_ratio and df2_dm_ratio then applies norm_num to obtain the numerical inequality directly.
why it matters
This theorem supplies the explicit inequality required by the ea011_certificate, which records that UDG diversity is explained by the RS substrate model. It fills the EA-011.5 slot in the module's key theorems list and aligns with the broader claim that substrate coherence varies continuously, consistent with the Recognition Science treatment of dark matter as ledger carrier rather than fixed-ratio particles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.