theorem proved term proof

`Jcost_is_normalized`

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

formal statement (Lean)

 149theorem Jcost_is_normalized : FunctionalEquation.IsNormalized Jcost :=

Term-mode proof.

 150  Jcost_unit0
 151
 152/-- `Jcost` satisfies the Recognition Composition Law. -/

Lean names referenced from this declaration's body.

Jcost_unit0 in IndisputableMonolith.Cost decl_use
IsNormalized in IndisputableMonolith.Cost.FunctionalEquation decl_use
Jcost_unit0 in IndisputableMonolith.Cost.JcostCore decl_use
Composition in IndisputableMonolith.Foundation.CostAxioms decl_use
IsNormalized in IndisputableMonolith.Foundation.DAlembert.Inevitability decl_use