standardLagrangian
plain-language theorem explainer
The declaration defines the standard Lagrangian L(q, q̇) = (m/2) q̇² - V(q) for a particle of mass m in potential V. Researchers recovering classical mechanics from the small-strain limit of the J-cost functional would cite it as the explicit bridge to kinetic-energy action. It is supplied by a direct definition that matches the quadratic Taylor expansion of J(1 + ε) without additional lemmas.
Claim. The standard Lagrangian is $L(m, V, q, q̇) = (m/2) q̇^2 - V(q)$.
background
The Quadratic Limit module works in the small-strain regime γ = 1 + ε with |ε| ≪ 1, where the cost functional J(γ) = (γ + γ^{-1})/2 - 1 reduces to its quadratic Taylor expansion ½ ε². This supplies the kinetic term that converts the J-action into ordinary mechanics. The module imports PathSpace, FunctionalConvexity and Cost to make the identification rigorous.
proof idea
The declaration is a direct definition that writes the standard form (m/2) qdot² - V q with no lemmas or tactics applied.
why it matters
It supplies the explicit Lagrangian whose Euler-Lagrange equation is shown in the same module to recover Newton's second law m q̈ = -V'(q). The definition therefore closes the bridge from the J-action to classical mechanics in the quadratic limit, as described in the paper companion RS_Least_Action.tex, Section Newton's Second Law as a Corollary. It sits downstream of the inflaton potential V(φ_inf) = J(1 + φ_inf) and upstream of the EL operator that yields the force law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.