Recognized formatting cleanup task for mathematical text We prove that the principle of least action is a theorem of d'Alembert's classical functional equation. Starting from the cost functional J(x) = ½(x + x⁻¹) − 1, the unique continuous solution of d'Alembert's equation in calibrated form, we construct the J-action S[γ] = ∫ₐᵇ J(γ(t)) dt on the space of admissible paths. The convexity of J on (0, ∞) propagates to convexity of S on the convex hull of any two admissible paths in the path space. From this single fact follows the unconditional principle of least action: any admissible path that does not strictly decrease the action toward a competitor (along even one positive interpolation step) globally minimizes the action against that competitor. The Euler-Lagrange equation, Newton's second law, the Hamiltonian formalism, and Noether's theorem all follow as corollaries. The entire derivation is formalized in Lean 4 with zero sorry declarations and zero user-declared axioms beyond Mathlib. The single bridge axiom of the d'Alembert classification (Aczél's C⁰ → C∞ smoothness theorem) is inherited from the upstream uniqueness paper and consumed only in the continuity-only formulation.