theorem proved term proof

`rhoCriticalMin_eq`

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

formal statement (Lean)

  86theorem rhoCriticalMin_eq : rhoCriticalMin = phi⁻¹ ^ 2 :=

Term-mode proof.

  87  RecognitionBandGeometry.rhoBandLower_eq
  88
  89/-- The fixed control band used by the runtime. -/

Lean names referenced from this declaration's body.

band in IndisputableMonolith.Foundation.PreLogicalCost decl_use
rhoCriticalMin in IndisputableMonolith.Unification.CriticalRecognitionLoading decl_use
rhoBandLower_eq in IndisputableMonolith.Unification.RecognitionBandGeometry decl_use