theorem proved term proof

`ml_geometric_is_phi`

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

formal statement (Lean)

 117theorem ml_geometric_is_phi : ml_geometric = φ := rfl

Term-mode proof.

 118
 119/-- The geometric M/L matches observations -/

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

three_strategies_agree in IndisputableMonolith.Astrophysics.MassToLight decl_use

Lean names referenced from this declaration's body.

ml_geometric in IndisputableMonolith.Astrophysics.ObservabilityLimits decl_use
L in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use