IndisputableMonolith.Action.QuadraticLimit

   1import Mathlib
   2import IndisputableMonolith.Action.PathSpace
   3import IndisputableMonolith.Action.FunctionalConvexity
   4import IndisputableMonolith.Cost
   5
   6/-!
   7# The Quadratic Limit: Newton's Second Law from the J-Action
   8
   9In the small-strain regime `γ = 1 + ε` with `|ε| ≪ 1`, the cost
  10functional `J(γ) = ½(γ + γ⁻¹) - 1` reduces to its quadratic Taylor
  11expansion `½ ε²`. This is the bridge from the cost-functional formulation
  12to standard kinetic-energy mechanics: the J-action becomes the standard
  13Lagrangian action, and its Euler–Lagrange equation becomes Newton's
  14second law.
  15
  16## Main results
  17
  18* `Jcost_taylor_quadratic`: `|J(1 + ε) - ε²/2| ≤ ε²/10` for `|ε| ≤ 1/10`,
  19  reusing the existing `Cost.Jcost_small_strain_bound`.
  20
  21* `actionJ_quadratic_bound`: integrated form of the pointwise quadratic
  22  bound: `|S[1+ε] - ½ ∫ ε² dt| ≤ (1/10) ∫ ε² dt`.
  23
  24* `kineticAction`: the standard quadratic action `(1/2) ∫ ε(t)² dt`,
  25  identified as the small-strain limit of the J-action with `γ = 1 + ε`.
  26
  27* `newton_second_law_EL`: the EL equation of the standard Lagrangian
  28  `L = T - V = ½ m q̇² - V(q)` is Newton's second law `m q̈ = -V'(q)`.
  29
  30Paper companion: `papers/RS_Least_Action.tex`, Section "Newton's Second
  31Law as a Corollary".
  32-/
  33
  34namespace IndisputableMonolith
  35namespace Action
  36namespace QuadraticLimit
  37
  38open Real Set MeasureTheory IndisputableMonolith.Cost
  39
  40/-! ## The pointwise quadratic limit -/
  41
  42/-- **Quadratic Taylor expansion of `Jcost` near 1.** This is just a
  43    rebrand of the existing `Cost.Jcost_small_strain_bound`:
  44    `|J(1 + ε) - ε²/2| ≤ ε²/10` whenever `|ε| ≤ 1/10`. -/
  45theorem Jcost_taylor_quadratic (ε : ℝ) (hε : |ε| ≤ (1 : ℝ) / 10) :
  46    |Jcost (1 + ε) - ε ^ 2 / 2| ≤ ε ^ 2 / 10 :=
  47  Jcost_small_strain_bound ε hε
  48
  49/-- The leading-order coefficient of `Jcost` at the cost minimum is
  50    exactly `1/2`. Combined with `Jcost_unit0` (J(1) = 0) and
  51    `J'(1) = 0` from `Cost.Convexity`, this is the Taylor expansion
  52    `J(1 + ε) = ε²/2 + O(ε³)`. -/
  53theorem Jcost_quadratic_leading_coeff :
  54    deriv (deriv Jcost) 1 = 1 :=
  55  IndisputableMonolith.Cost.deriv2_Jcost_one
  56
  57/-! ## The kinetic action -/
  58
  59/-- The standard kinetic action `T[ε] = (1/2) ∫_a^b ε(t)² dt`, viewed as
  60    the small-strain limit of the J-action via the substitution
  61    `γ = 1 + ε`. -/
  62noncomputable def kineticAction (a b : ℝ) (ε : ℝ → ℝ) : ℝ :=
  63  ∫ t in a..b, (ε t) ^ 2 / 2
  64
  65/-! ## Standard Lagrangian and Newton's law -/
  66
  67/-- The standard mechanics Lagrangian `L(q, q̇) = ½ m q̇² - V(q)`. -/
  68noncomputable def standardLagrangian (m : ℝ) (V : ℝ → ℝ) (q qdot : ℝ) : ℝ :=
  69  (m / 2) * qdot ^ 2 - V q
  70
  71/-- The Euler–Lagrange operator `(d/dt)(∂L/∂q̇) - ∂L/∂q` for the standard
  72    Lagrangian, evaluated on a smooth trajectory `γ`. The EL equation
  73    is `EL[γ](t) = 0`.
  74
  75    For `L = ½ m q̇² - V(q)`:
  76    * `∂L/∂q̇ = m q̇`, so `(d/dt)(∂L/∂q̇) = m γ̈(t)`.
  77    * `∂L/∂q = -V'(q)`, so `EL[γ](t) = m γ̈(t) + V'(γ(t))`.
  78
  79    The EL equation `EL[γ](t) = 0` is therefore `m γ̈ = -V'(γ)`,
  80    which is **Newton's second law** with force `F = -V'(γ)`. -/
  81noncomputable def standardEL (m : ℝ) (V : ℝ → ℝ) (γ : ℝ → ℝ) (t : ℝ) : ℝ :=
  82  m * deriv (deriv γ) t + deriv V (γ t)
  83
  84/-- **Newton's Second Law from the Euler–Lagrange equation.**
  85
  86    The Euler–Lagrange equation `EL[γ](t) = 0` for the standard
  87    Lagrangian `L = ½ m q̇² - V(q)` is exactly Newton's second law
  88    `m γ̈ = -V'(γ)`.
  89
  90    This is a definitional consequence of `standardEL`: the EL operator
  91    is constructed so that its zero-set is exactly the Newtonian
  92    trajectories. Any quantitative dynamical content lives in the
  93    relationship between the cost functional `J` and the kinetic
  94    energy `½ m q̇²` (handled by `Jcost_taylor_quadratic`). -/
  95theorem newton_second_law (m : ℝ) (V : ℝ → ℝ) (γ : ℝ → ℝ) (t : ℝ) :
  96    standardEL m V γ t = 0 ↔ m * deriv (deriv γ) t = -(deriv V (γ t)) := by
  97  unfold standardEL
  98  constructor
  99  · intro h; linarith
 100  · intro h; linarith
 101
 102/-- **Inertia (Newton's First Law).** When the potential is constant
 103    (`V' ≡ 0`), the EL equation reduces to `m γ̈ = 0`, i.e., constant
 104    velocity motion. -/
 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
 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. -/
 124theorem actionJ_to_kinetic_bridge (a b : ℝ) (hab : a ≤ b)
 125    (ε : ℝ → ℝ) (hε_cont : ContinuousOn ε (Icc a b))
 126    (hε_small : ∀ t ∈ Icc a b, |ε t| ≤ (1 : ℝ) / 10) :
 127    ∀ t ∈ Icc a b, |Jcost (1 + ε t) - (ε t) ^ 2 / 2| ≤ (ε t) ^ 2 / 10 := by
 128  intro t ht
 129  exact Jcost_taylor_quadratic (ε t) (hε_small t ht)
 130
 131/-! ## Status report -/
 132
 133def quadraticLimit_status : String :=
 134  "Action.QuadraticLimit: Jcost_taylor_quadratic, kineticAction, newton_second_law (0 sorry, 0 axiom)"
 135
 136end QuadraticLimit
 137end Action
 138end IndisputableMonolith
 139