theorem proved term proof

`ngc1052df2_dm_poor`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

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.

ea011_certificate in IndisputableMonolith.Experimental.UltraDiffuseGalaxies decl_use

depends on (4)

Lean names referenced from this declaration's body.

Model in IndisputableMonolith.CPM.LawOfExistence decl_use
df2_dm_ratio in IndisputableMonolith.Experimental.UltraDiffuseGalaxies decl_use
Substrate in IndisputableMonolith.Relativity.ILG.Substrate decl_use
Substrate in IndisputableMonolith.Theology.SubstrateIndependentMonotheism decl_use