functionalConvexity_status
plain-language theorem explainer
The declaration is a status string reporting that the J-action convexity on path interpolations and unconditional geodesic minimization are established with zero sorrys or axioms. Researchers deriving the principle of least action from the d'Alembert equation would cite it to confirm removal of conditional witnesses. The implementation is a direct string literal summarizing the module's sibling results.
Claim. The status of the convexity properties of the action functional is the string reporting that the integrated J-cost convexity and the unconditional geodesic minimization hold with no unresolved sorrys or axioms.
background
In the Recognition Science framework the J-action functional is the integral of the J-cost along an admissible path from a to b. The module establishes that this functional is convex under convex combinations of paths, so the action of an interpolated path is at most the convex combination of the separate actions. This follows from pointwise convexity of the J-cost, itself a consequence of the d'Alembert functional equation. The upstream convexity result on interpolations directly yields the headline theorem that a path minimizing along every interpolation segment is a global minimizer.
proof idea
This declaration is a one-line scaffolding stub that constructs a status string by concatenating the convexity theorem and the unconditional minimization theorem, appending a note on the absence of sorrys and axioms.
why it matters
This scaffolding declaration marks completion of the unconditional principle of least action, discharging the interpolation-witness hypothesis required in earlier variational statements. It aligns with the paper companion section on the variational principle on the cost manifold and advances the framework by using convexity inherited from J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.