newton_second_law
plain-language theorem explainer
The Euler-Lagrange equation for the standard Lagrangian equals Newton's second law by direct algebraic expansion of the operator. Classical mechanicians recovering Newtonian trajectories from variational principles cite the result. The proof is a one-line wrapper that unfolds the EL definition and applies linear arithmetic in both directions of the biconditional.
Claim. For the Lagrangian $L = (1/2) m q̇² - V(q)$, the Euler-Lagrange operator evaluated at time $t$ along trajectory $γ$ satisfies $EL[γ](t) = 0$ if and only if $m γ̈(t) = -V'(γ(t))$.
background
The QuadraticLimit module works in the small-strain regime where the J-cost functional reduces to quadratic kinetic energy. standardEL is the Euler-Lagrange operator $m · (d²γ/dt²) + V'(γ(t))$ for the standard Lagrangian. Jcost_taylor_quadratic supplies the pointwise bound that justifies identifying the integrated J-action with the kinetic action $½ ∫ ε² dt$. The module_doc states that any quantitative dynamical content lives in the J-to-kinetic bridge, with this theorem handling the EL-to-Newton step as a definitional consequence.
proof idea
The term proof unfolds standardEL to obtain the sum $m · γ̈(t) + V'(γ(t))$, splits the biconditional with constructor, and applies linarith on each leg to reach the negated form.
why it matters
newton_second_law is invoked by hamilton_equations_from_EL and by newtonSecondLawCert to populate the NewtonSecondLawCert witness. It supplies the paper proposition in RS_Least_Action.tex that Newton's second law is a corollary of the J-action in the quadratic regime. The result closes one link in the chain from T5 J-uniqueness through the quadratic limit to classical mechanics while leaving the full forcing chain (T0-T8) and RCL untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.