newton_first_law
plain-language theorem explainer
Newton's first law follows directly as the zero-potential case of the Euler-Lagrange equation for the standard Lagrangian. A physicist recovering classical mechanics inside the Recognition Science quadratic limit would cite this to confirm inertial trajectories. The proof is a one-line algebraic reduction that invokes the second-law equivalence, inserts the constant-potential condition, and cancels the nonzero mass factor.
Claim. Let $m > 0$ be a mass and let $V$ be the zero potential. If the Euler-Lagrange operator satisfies $mddot{gamma}(t) + V'(gamma(t)) = 0$ at time $t$, then $ddot{gamma}(t) = 0$.
background
The module establishes the quadratic limit in which the J-cost $J(gamma) = frac12(gamma + gamma^{-1}) - 1$ reduces to the kinetic term $frac12 epsilon^2$ for small strain $gamma = 1 + epsilon$. The operator standardEL is defined as $m dot{gamma}''(t) + V'(gamma(t))$, so that its zero set is precisely the Newtonian equation of motion. The upstream theorem newton_second_law states the equivalence between this operator vanishing and the second-law form $m gamma'' = -V'(gamma)$.
proof idea
The proof rewrites the given EL hypothesis via newton_second_law, substitutes the supplied zero-force condition to reach $m gamma''(t) = 0$, and cancels the nonzero mass using mul_left_cancel_0 together with the arithmetic fact mul_zero.
why it matters
The result supplies the inertia case inside the quadratic-limit bridge from J-action to Newtonian mechanics. It confirms that the Recognition Science cost functional reproduces constant-velocity motion when forces vanish, consistent with the T5 J-uniqueness and T8 three-dimensional forcing chain. No downstream uses are recorded in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.