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

ngc1052df2_dm_poor

show as:
view Lean formalization →

NGC 1052-DF2 has a dark matter to stellar mass ratio of 1.5, satisfying the bound below 3. Galaxy formation researchers and modified-gravity modelers cite this when contrasting DM-poor and DM-rich ultra-diffuse systems. The proof is a one-line wrapper that unfolds the constant definition of the ratio and applies numerical normalization.

claimThe dark matter to stellar mass ratio for NGC 1052-DF2 satisfies $M_{DM}/M_* < 3$.

background

Recognition Science treats dark matter as substrate ledger carrier whose distribution follows spatially varying recognition coherence rather than particle dynamics. The module sets experimental anchors for ultra-diffuse galaxies: surface brightness above 24 mag/arcsec², sizes 1-10 kpc, and contrasting ratios (Dragonfly 44 near 70, NGC 1052-DF2 near 1-2). The sibling definition df2_dm_ratio fixes the value at 1.5, while upstream Substrate structures from ILG and SubstrateIndependentMonotheism supply the phase and sigma-charge ledger that carries coherence.

proof idea

One-line wrapper that unfolds df2_dm_ratio to the constant 1.5 and invokes norm_num to discharge the inequality.

why it matters in Recognition Science

The result supplies one concrete case inside the EA-011 certificate, which certifies that UDG diversity follows from spatially varying substrate coherence with no universal mass ratio required. It aligns with the ILG derivation that rotation curves are recovered by modified gravity alone and closes the DM-poor branch of the experimental verification.

scope and limits

formal statement (Lean)

  96theorem ngc1052df2_dm_poor : df2_dm_ratio < 3 := by

proof body

Term-mode proof.

  97  unfold df2_dm_ratio
  98  norm_num
  99
 100/-! ## II. RS Substrate Model -/
 101
 102/-- Recognition coherence varies spatially.
 103    C(x) = C_0 × f(φ, environment) -/

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.