leastAction_status
plain-language theorem explainer
Human-readable status tag asserting that the least-action verification certificate is complete: five theorems, zero sorry, zero axioms. Dashboard and audit consumers cite it as a one-line health check for the Action namespace. The body is a fixed string literal, not a mathematical proof.
Claim. A fixed status message reporting that the principle-of-least-action certificate is verified: five bundled theorems, with no unfinished proofs and no extra axioms.
background
The surrounding module is the master verification certificate for the principle of least action. It aggregates the central results of the Action namespace into one checkable package: convexity of the J-action, local-min implies global-min, uniqueness of the constant ground state for the cost-rate Euler–Lagrange equation, Newton’s second law from the standard Lagrangian, and energy conservation.
Upstream, the unconditional least-action theorem states that if a geodesic path does not decrease the action toward any fixed-endpoint competitor along even one positive straight-line interpolation step, then it globally minimizes the action. The certificate structure packages those five assertions into a single verified predicate. The J-cost functional and its convexity are the analytic engine behind the claim that least action is a theorem of the d’Alembert functional equation.
proof idea
No mathematical argument. The definition is a one-line string constant that hard-codes the audit summary for the least-action certificate and names the upstream unconditional least-action theorem as the headline item. There is no tactic proof, no term construction, and no discharge of the certificate predicate.
why it matters
This string is the human-facing badge for Paper A’s headline: least action as a theorem via convexity of the J-cost, not an independent postulate. It sits in the Verification layer so external readers and CI can see, at a glance, that the five Action theorems (convexity, local-to-global minimality, cost-rate EL uniqueness, Newton from EL, energy conservation) are claimed complete. It does not feed further theorems (no downstream uses). Framework-wise it advertises closure of the Action package that supports the recognition forcing story, but the string itself is scaffolding until a real certificate instance and a proof of the verified predicate replace the hard-coded report.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.