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

dragonfly44_dm_rich

show as:
view Lean formalization →

Dragonfly 44 exhibits a dark matter to stellar mass ratio exceeding 50, matching observational estimates near 70 for this ultra-diffuse galaxy. Researchers examining galaxy diversity under substrate-based gravity models cite the result when contrasting DM-rich and DM-poor systems without invoking universal particle distributions. The verification reduces to unfolding the constant definition of the ratio and confirming the inequality by numerical normalization.

claimThe dark matter to stellar mass ratio for Dragonfly 44 satisfies $M_{DM}/M_* > 50$.

background

Recognition Science models dark matter as a distributed substrate whose density tracks local recognition coherence rather than as collisionless particles. The module EA-011 introduces df44_dm_ratio as the constant 70.0 to encode the observed ratio for Dragonfly 44, placed alongside the contrasting NGC 1052-DF2 case. This sits inside the substrate-coherence framework that predicts spatial variation in ledger carrier density, with high-coherence patches yielding DM-rich UDGs and low-coherence patches yielding DM-poor ones. Upstream results supply the ratio definition itself together with collision-free ledger properties and mechanism-design structures that keep the substrate description free of additional axioms.

proof idea

The proof is a one-line wrapper that unfolds df44_dm_ratio to the literal value 70.0 and applies norm_num to discharge the numerical comparison.

why it matters in Recognition Science

The theorem supplies one of the two concrete observational anchors inside the EA-011 certificate, which certifies that UDG diversity is explained by spatially varying substrate coherence. It thereby closes the experimental loop for the claim that no universal M_DM/M_* ratio is required, consistent with the recognition composition law and the eight-tick periodicity of the forcing chain. The parent certificate aggregates this result with its DM-poor counterpart to produce the overall status string.

scope and limits

formal statement (Lean)

  90theorem dragonfly44_dm_rich : df44_dm_ratio > 50 := by

proof body

Term-mode proof.

  91  unfold df44_dm_ratio
  92  norm_num
  93
  94/-- **THEOREM EA-011.3**: NGC 1052-DF2 is DM-poor.
  95    M_DM/M_stars ~ 1.5 ≈ 1. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.