Action Quadratic Limit Jcost Taylor Quadratic

The quadratic bridge

The declaration Jcost_taylor_quadratic establishes a precise quantitative bridge between a cost functional and standard Newtonian mechanics. The cost functional in question, Jcost (a measure of the price of a recognition event), takes the form J(γ) = ½(γ + γ⁻¹) - 1. The theorem states that when the strain γ is close to 1, written as γ = 1 + ε with |ε| ≤ 1/10, the cost functional is well approximated by the quadratic term ε²/2. Specifically, the absolute difference |J(1 + ε) - ε²/2| is bounded by ε²/10. This is a quantitative statement: the error is at most ten percent of the leading quadratic term itself.

The bound is not merely an asymptotic statement but a concrete inequality with an explicit constant. The theorem reuses a previously established small-strain bound, so the proof is short and the result is machine-checked. The leading coefficient of the Taylor expansion is exactly 1/2, which matches the familiar coefficient in the kinetic energy term ½mv². This is the point of contact: the cost functional, when expanded near its minimum, reproduces the standard quadratic form that appears in the Lagrangian of classical mechanics.

In Recognition Science, this result is the bridge from the cost-functional formulation to standard kinetic-energy mechanics. The framework models the J-action as the integral of the cost functional, and the theorem shows that in the small-strain regime this action differs from the standard kinetic action (1/2)∫ε(t)² dt by at most (1/10) of that kinetic action. The Euler-Lagrange equation of the standard Lagrangian L = ½m q̇² - V(q) is then exactly Newton's second law, m q̈ = -V'(q). The framework's library proves this as a definitional consequence of the Euler-Lagrange operator, not as a separate physical postulate.

What the declaration does not claim is equally important. The theorem is a local approximation result; it holds only for |ε| ≤ 1/10 and does not assert that the cost functional equals the quadratic form globally. The identification of the kinetic action as the small-strain limit of the J-action is a definitional choice, not a derived equality. Newton's second law follows from the Euler-Lagrange equation of the standard Lagrangian, which is a definitional consequence of how the Euler-Lagrange operator is constructed, not a new physical law. The bridge theorem shows consistency, not derivation of mechanics from first principles.

/-- **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 leading-order coefficient of `Jcost` at the cost minimum is
    exactly `1/2`. Combined with `Jcost_unit0` (J(1) = 0) and
    `J'(1) = 0` from `Cost.Convexity`, this is the Taylor expansion
    `J(1 + ε) = ε²/2 + O(ε³)`. -/
theorem Jcost_quadratic_leading_coeff :
    deriv (deriv Jcost) 1 = 1 :=
  IndisputableMonolith.Cost.deriv2_Jcost_one

/-- **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

/-- The standard kinetic action `T[ε] = (1/2) ∫_a^b ε(t)² dt`, viewed as
    the small-strain limit of the J-action via the substitution
    `γ = 1 + ε`. -/
noncomputable def kineticAction (a b : ℝ) (ε : ℝ → ℝ) : ℝ :=
  ∫ t in a..b, (ε t) ^ 2 / 2

What this page does not claim

The theorem does not claim that Jcost equals the quadratic form for all strains, only within the stated bound. The identification of kinetic action as the small-strain limit is a definition, not a derived equality. Newton's second law is a definitional consequence of the Euler-Lagrange operator, not a new physical postulate.

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: