theorem proved term proof

`J_nonneg`

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

formal statement (Lean)

  75theorem J_nonneg (x : ℝ) (hx : 0 < x) : 0 ≤ J x :=

Term-mode proof.

  76  Jcost_nonneg hx
  77
  78/-- **Defect characterization**: J(x) = (x − 1)²/(2x) for x ≠ 0. -/

Lean names referenced from this declaration's body.

Jcost_nonneg in IndisputableMonolith.Cost decl_use
Jcost_nonneg in IndisputableMonolith.Cost.JcostCore decl_use
Defect in IndisputableMonolith.CPM.LNALBridge decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
Jcost_nonneg in IndisputableMonolith.Gravity.CoherenceCollapse decl_use
Jcost_nonneg in IndisputableMonolith.Gravity.EnergyProcessingBridge decl_use
Jcost_nonneg in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use