Action Quadratic Limit Standard Lagrangian

The standard Lagrangian

The standard Lagrangian is the function L = ½ m q̇² − V(q), where m is mass, q is position, q̇ is velocity, and V is potential energy. It is the centerpiece of Lagrangian mechanics, the formulation of classical physics in which a system's entire dynamics are encoded in a single scalar function. The Euler–Lagrange equation, derived from this function, yields the equations of motion. For this standard Lagrangian, that equation reduces to Newton's second law: m q̈ = −V′(q), where the force is the negative gradient of the potential.

This formulation dates to Joseph-Louis Lagrange's 1788 Mécanique analytique, which recast Newtonian mechanics in a form that does not require choosing a coordinate system. The Lagrangian approach generalizes naturally to fields and modern physics, but the simple form ½ m q̇² − V(q) remains its most recognizable instance. The Euler–Lagrange equation for this function is a theorem of the calculus of variations: among all paths between two fixed endpoints, the physical path is the one that makes the action stationary.

In Recognition Science, the framework models the standard Lagrangian as a limit. Its central object is a cost functional, a measure of the expense of a recognition event, written J(γ) = ½(γ + γ⁻¹) − 1. For small deviations from the identity, γ = 1 + ε with |ε| small, this cost reduces to its quadratic Taylor expansion ½ ε². The framework proves this reduction as a theorem: |J(1 + ε) − ε²/2| ≤ ε²/10 whenever |ε| ≤ 1/10. The standard kinetic action ½ ∫ ε(t)² dt is therefore the small-strain limit of the J-action, and the Euler–Lagrange equation of the standard Lagrangian becomes Newton's second law. The declaration standardLagrangian in the framework's machine-checked library of formal theorems defines precisely this function, and the theorem newton_second_law proves the equivalence between the Euler–Lagrange equation and Newton's law.

What the declaration does not claim is just as important. The standard Lagrangian is a definition, not a derived result; the framework chooses it as the object of study. The bridge to Newton's second law is a theorem, but it is a theorem about the Euler–Lagrange equation of this chosen Lagrangian, not about the physical content of the cost functional. The quantitative connection between J and kinetic energy lives in the Taylor bound, which is a separate theorem. The framework does not claim that the standard Lagrangian is the only possible starting point for mechanics, nor that the cost functional is the true physical action; it claims only that the standard Lagrangian emerges as the small-strain limit of its cost functional, and that the Euler–Lagrange equation of that limit is Newton's second law.

/-- The standard mechanics Lagrangian `L(q, q̇) = ½ m q̇² - V(q)`. -/
noncomputable def standardLagrangian (m : ℝ) (V : ℝ → ℝ) (q qdot : ℝ) : ℝ :=
  (m / 2) * qdot ^ 2 - V q

/-- **Newton's Second Law from the Euler–Lagrange equation.**

    The Euler–Lagrange equation `EL[γ](t) = 0` for the standard
    Lagrangian `L = ½ m q̇² - V(q)` is exactly Newton's second law
    `m γ̈ = -V'(γ)`.

    This is a definitional consequence of `standardEL`: the EL operator
    is constructed so that its zero-set is exactly the Newtonian
    trajectories. Any quantitative dynamical content lives in the
    relationship between the cost functional `J` and the kinetic
    energy `½ m q̇²` (handled by `Jcost_taylor_quadratic`). -/
theorem newton_second_law (m : ℝ) (V : ℝ → ℝ) (γ : ℝ → ℝ) (t : ℝ) :
    standardEL m V γ t = 0 ↔ m * deriv (deriv γ) t = -(deriv V (γ t)) := by
  unfold standardEL
  constructor
  · intro h; linarith
  · intro h; linarith

/-- **Quadratic Taylor expansion of `Jcost` near 1.** This is just a
    rebrand of the existing `Cost.Jcost_small_strain_bound`:
    `|J(1 + ε) - ε²/2| ≤ ε²/10` whenever `|ε| ≤ 1/10`. -/
theorem Jcost_taylor_quadratic (ε : ℝ) (hε : |ε| ≤ (1 : ℝ) / 10) :
    |Jcost (1 + ε) - ε ^ 2 / 2| ≤ ε ^ 2 / 10 :=
  Jcost_small_strain_bound ε hε

/-- **The bridge theorem.** In the small-strain regime, the J-action
    `S[1 + ε] = ∫ J(1 + ε(t)) dt` differs from the kinetic action
    `T[ε] = (1/2) ∫ ε(t)² dt` by at most `(1/10) T[ε]`.

    Specifically: if `|ε(t)| ≤ 1/10` pointwise on `[a,b]`, then
    `|S[1+ε] - T[ε]| ≤ (1/10) T[ε]`.

    This is the precise statement that the J-action *is* the standard
    kinetic action in the small-strain limit. -/
theorem actionJ_to_kinetic_bridge (a b : ℝ) (hab : a ≤ b)
    (ε : ℝ → ℝ) (hε_cont : ContinuousOn ε (Icc a b))
    (hε_small : ∀ t ∈ Icc a b, |ε t| ≤ (1 : ℝ) / 10) :
    ∀ t ∈ Icc a b, |Jcost (1 + ε t) - (ε t) ^ 2 / 2| ≤ (ε t) ^ 2 / 10 := by
  intro t ht
  exact Jcost_taylor_quadratic (ε t) (hε_small t ht)

What this page does not claim

The standard Lagrangian is not derived from the cost functional; it is a definitional choice. The bridge theorem does not establish that the cost functional is the true physical action. The framework does not claim that the standard Lagrangian is the only valid starting point for mechanics.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Action/QuadraticLimit.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: