newton_first_law
Newton's first law follows when the potential vanishes: for nonzero mass the Euler-Lagrange equation of the standard Lagrangian reduces to constant velocity. A physicist extracting classical mechanics from the J-cost functional in the small-strain regime would cite this corollary. The proof is a short algebraic reduction that invokes the second-law equivalence, substitutes the zero-force hypothesis, and cancels the mass factor.
claimLet $m > 0$ be a nonzero mass, let $V$ be the zero potential, and let $L = m/2 |q̇|^2 - V(q)$ be the standard Lagrangian. If the Euler-Lagrange operator for $L$ vanishes at time $t$ on trajectory $γ$, then the second time derivative of $γ$ at $t$ is zero.
background
The module derives Newton's laws as the small-strain limit of the J-cost functional. For $γ = 1 + ε$ with $|ε| ≪ 1$, $J(γ) = ½(γ + γ^{-1}) - 1$ reduces to the quadratic $½ε²$, so the J-action becomes the kinetic action $½∫ε² dt$. The Euler-Lagrange operator is defined by standardEL m V γ t := m · γ̈(t) + V'(γ(t)). The upstream theorem newton_second_law states that this operator vanishes if and only if m γ̈ = -V'(γ).
proof idea
The term proof rewrites the hypothesis h_EL by the newton_second_law equivalence, substitutes the zero-force condition deriv(0) = 0 to obtain m · γ̈(t) = 0, and cancels the nonzero mass factor with mul_left_cancel₀.
why it matters in Recognition Science
The declaration supplies the inertia case of the bridge from J-action to classical mechanics, completing the main results listed in the module doc (Jcost_taylor_quadratic through newton_second_law_EL). It realizes the paper companion claim that Newton's laws are corollaries of the quadratic limit of the Recognition cost functional, with no further hypotheses required beyond the small-strain regime.
scope and limits
- Does not apply when mass is zero.
- Does not cover trajectories with nonzero potential.
- Does not address relativistic or quantum corrections.
- Does not quantify deviation from the quadratic approximation outside |ε| ≤ 1/10.
formal statement (Lean)
105theorem newton_first_law (m : ℝ) (hm : m ≠ 0) (γ : ℝ → ℝ) (t : ℝ)
106 (h_no_force : deriv (fun _ : ℝ => (0 : ℝ)) (γ t) = 0)
107 (h_EL : standardEL m (fun _ => 0) γ t = 0) :
108 deriv (deriv γ) t = 0 := by
proof body
Term-mode proof.
109 rw [newton_second_law] at h_EL
110 rw [h_no_force, neg_zero] at h_EL
111 exact (mul_left_cancel₀ hm (by rw [h_EL, mul_zero]))
112
113/-! ## The bridge: J-action ↔ kinetic action ↔ Newton -/
114
115/-- **The bridge theorem.** In the small-strain regime, the J-action
116 `S[1 + ε] = ∫ J(1 + ε(t)) dt` differs from the kinetic action
117 `T[ε] = (1/2) ∫ ε(t)² dt` by at most `(1/10) T[ε]`.
118
119 Specifically: if `|ε(t)| ≤ 1/10` pointwise on `[a,b]`, then
120 `|S[1+ε] - T[ε]| ≤ (1/10) T[ε]`.
121
122 This is the precise statement that the J-action *is* the standard
123 kinetic action in the small-strain limit. -/