theorem proved term proof

`ilg_sufficient`

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

formal statement (Lean)

 136theorem ilg_sufficient : ilg_fit_quality < 2 := by

proof body

Term-mode proof.

 137  unfold ilg_fit_quality
 138  norm_num
 139
 140/-- **THEOREM EA-011.7**: ILG applies to both DM-rich and DM-poor.
 141    Same formula, different coherence parameter. -/

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 (2)

Lean names referenced from this declaration's body.

ilg_fit_quality in IndisputableMonolith.Experimental.UltraDiffuseGalaxies decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use