def scaffolding sorry stub

`functionalConvexity_status`

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

formal statement (Lean)

 313def functionalConvexity_status : String :=

proof body

Body contains sorry. Scaffold only; not proved.

 314  "Action.FunctionalConvexity: actionJ_convex_on_interp, geodesic_minimizes_unconditional (0 sorry, 0 axiom)"
 315
 316end Action
 317end IndisputableMonolith

depends on (3)

Lean names referenced from this declaration's body.

actionJ_convex_on_interp in IndisputableMonolith.Action.FunctionalConvexity decl_use
geodesic_minimizes_unconditional in IndisputableMonolith.Action.FunctionalConvexity decl_use
Action in IndisputableMonolith.Constants.RSNativeUnits decl_use