def definition def or abbrev

`Jcost_regularity_cert`

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

formal statement (Lean)

 203noncomputable def Jcost_regularity_cert :
 204    IndisputableMonolith.Foundation.ClosedFramework.RegularityCert Cost.Jcost where
 205  continuous := Jcost_continuous_pos

proof body

Definition body.

 206  strict_convex := Cost.Jcost_strictConvexOn_pos
 207  calibration := CPM.LawOfExistence.RS.Jcost_log_second_deriv_normalized
 208
 209end CostUniqueness
 210end IndisputableMonolith

depends on (6)

Lean names referenced from this declaration's body.

Jcost_strictConvexOn_pos in IndisputableMonolith.Cost.Convexity decl_use
Jcost_continuous_pos in IndisputableMonolith.CostUniqueness decl_use
Jcost_log_second_deriv_normalized in IndisputableMonolith.CPM.LawOfExistence decl_use
RegularityCert in IndisputableMonolith.Foundation.ClosedObservableFramework decl_use
calibration in IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use