IndisputableMonolith.Action.NewtonSecondLawDomainCert

   1import Mathlib
   2import IndisputableMonolith.Action.QuadraticLimit
   3import IndisputableMonolith.Action.Hamiltonian
   4
   5/-!
   6# Newton's Second Law from the J-Action — Domain Certificate
   7(Plan v7 twenty-ninth pass continuation)
   8
   9## Status: THEOREM (0 sorry, 0 axiom).
  10
  11This module is the domain-cert wrapper for Newton's second law as the
  12small-strain Euler-Lagrange equation of the J-action. It packages the
  13key equivalence proved in `Action.QuadraticLimit` into a single `*Cert`
  14suitable for the master `UnifiedReality` chain.
  15
  16## What it bundles
  17
  18- (1) `EL ↔ Newton`: the EL equation of `L = ½ m q̇² - V(q)` is exactly
  19  `m γ̈ = -V'(γ)`.
  20- (2) Quadratic Taylor bound: `|J(1+ε) - ε²/2| ≤ ε²/10` for `|ε| ≤ 1/10`.
  21  This is the analytic content that turns the J-action into the standard
  22  kinetic-action in the small-strain regime.
  23- (3) Hessian calibration: `J''(1) = 1`. The leading-order kinetic
  24  coefficient is forced by the d'Alembert calibration of `Jcost` at the
  25  ground state.
  26
  27## Falsifier
  28
  29A measured trajectory `γ(t)` of a classical particle in potential `V` for
  30which `m γ̈(t) ≠ -V'(γ(t))` at any `t` would falsify clause (1) and
  31therefore the small-strain limit of the J-action.
  32
  33Paper companion: `papers/RS_Least_Action.tex` (Paper A), §"Newton's
  34Second Law as a Corollary".
  35-/
  36
  37namespace IndisputableMonolith
  38namespace Action
  39
  40open IndisputableMonolith.Action.QuadraticLimit
  41open IndisputableMonolith.Cost
  42
  43/-- Domain certificate for Newton's second law as a corollary of the
  44J-action variational principle. -/
  45structure NewtonSecondLawCert where
  46  el_iff_newton : ∀ (m : ℝ) (V : ℝ → ℝ) (γ : ℝ → ℝ) (t : ℝ),
  47      QuadraticLimit.standardEL m V γ t = 0 ↔
  48      m * deriv (deriv γ) t = -(deriv V (γ t))
  49  quadratic_taylor_bound : ∀ (ε : ℝ), |ε| ≤ (1 : ℝ) / 10 →
  50      |Jcost (1 + ε) - ε ^ 2 / 2| ≤ ε ^ 2 / 10
  51  hessian_one : deriv (deriv Jcost) 1 = 1
  52
  53/-- Inhabited witness — every clause is a theorem in
  54`Action.QuadraticLimit`. -/
  55def newtonSecondLawCert : NewtonSecondLawCert where
  56  el_iff_newton := QuadraticLimit.newton_second_law
  57  quadratic_taylor_bound := Jcost_taylor_quadratic
  58  hessian_one := Jcost_quadratic_leading_coeff
  59
  60/-- One-statement summary: Newton's second law is the EL equation of
  61the small-strain J-action. -/
  62theorem newton_second_law_one_statement :
  63    Nonempty NewtonSecondLawCert :=
  64  ⟨newtonSecondLawCert⟩
  65
  66end Action
  67end IndisputableMonolith
  68