IndisputableMonolith.Action.EnergyConservationDomainCert

   1import Mathlib
   2import IndisputableMonolith.Action.Hamiltonian
   3import IndisputableMonolith.Action.QuadraticLimit
   4import IndisputableMonolith.Action.Noether
   5
   6/-!
   7# Energy Conservation from the J-Action — Domain Certificate
   8(Plan v7 twenty-ninth pass continuation)
   9
  10## Status: THEOREM (0 sorry, 0 axiom).
  11
  12This module is the domain-cert wrapper for energy conservation along
  13Newtonian trajectories, as proved in `Action.Hamiltonian` from the
  14Lagrangian/EL chain. The standard mechanics Hamiltonian
  15`H(q, p) = p²/(2m) + V(q)` is the Legendre transform of
  16`L = ½ m q̇² - V(q)`; its conservation along the EL flow is Noether's
  17theorem applied to time-translation symmetry.
  18
  19## What it bundles
  20
  21- (1) Energy conservation: `H(γ(t₁), p(t₁)) = H(γ(t₂), p(t₂))` for any
  22  Newtonian trajectory under the standard regularity hypotheses
  23  (`hV_diff`, `hγ_diff`, `hγ_diff2`, `h_dE_factored`).
  24- (2) Hamilton's equations from the EL: the pair `(γ̇ = p/m, ṗ = -V'(γ))`
  25  is forced by the EL of the standard Lagrangian.
  26
  27## Falsifier
  28
  29A closed-system mechanical trajectory with potential `V` differentiable
  30on the trajectory image, regular accelerations, and EL satisfied, yet
  31total energy `H(γ, p)` measurably non-constant in time. This would
  32falsify clause (1) and therefore Noether's theorem on time-translation
  33symmetry of the J-action.
  34
  35Paper companion: `papers/RS_Least_Action.tex` (Paper A), §"Hamiltonian
  36Formulation as a Corollary".
  37-/
  38
  39namespace IndisputableMonolith
  40namespace Action
  41
  42open IndisputableMonolith.Action
  43
  44/-- Domain certificate for energy conservation along Newtonian
  45trajectories of the small-strain J-action. -/
  46structure EnergyConservationCert where
  47  energy_conserved : ∀ (m : ℝ) (_hm : 0 < m) (V : ℝ → ℝ) (γ : ℝ → ℝ),
  48      (∀ t, DifferentiableAt ℝ V (γ t)) →
  49      (∀ t, DifferentiableAt ℝ γ t) →
  50      (∀ t, DifferentiableAt ℝ (deriv γ) t) →
  51      (∀ t : ℝ,
  52        deriv (HamiltonianMech.totalEnergy m V γ) t =
  53          deriv γ t * (m * deriv (deriv γ) t + deriv V (γ t))) →
  54      (∀ t : ℝ, QuadraticLimit.standardEL m V γ t = 0) →
  55      ∀ t₁ t₂ : ℝ,
  56        HamiltonianMech.totalEnergy m V γ t₁ =
  57          HamiltonianMech.totalEnergy m V γ t₂
  58  hamilton_qdot : ∀ (m : ℝ) (_hm : m ≠ 0) (V : ℝ → ℝ) (γ : ℝ → ℝ)
  59      (_hV_diff : ∀ t, DifferentiableAt ℝ V (γ t))
  60      (_hγ_diff : ∀ t, DifferentiableAt ℝ γ t)
  61      (_hγ_diff2 : ∀ t, DifferentiableAt ℝ (deriv γ) t)
  62      (_hEL : ∀ t : ℝ, QuadraticLimit.standardEL m V γ t = 0),
  63      HamiltonianMech.hamiltonQDotEquation m γ
  64        (HamiltonianMech.conjugateMomentum m γ)
  65
  66/-- Inhabited witness — both clauses are theorems in
  67`Action.Hamiltonian`. -/
  68def energyConservationCert : EnergyConservationCert where
  69  energy_conserved := by
  70    intro m hm V γ hV_diff hγ_diff hγ_diff2 h_dE_factored hEL t₁ t₂
  71    exact HamiltonianMech.energy_conservation m hm V γ
  72      hV_diff hγ_diff hγ_diff2 h_dE_factored hEL t₁ t₂
  73  hamilton_qdot := by
  74    intro m hm V γ hV_diff hγ_diff hγ_diff2 hEL
  75    exact (HamiltonianMech.hamilton_equations_from_EL m hm V γ
  76      hV_diff hγ_diff hγ_diff2 hEL).1
  77
  78/-- One-statement summary: total energy is conserved along Newtonian
  79trajectories of the small-strain J-action. -/
  80theorem energy_conservation_one_statement :
  81    Nonempty EnergyConservationCert :=
  82  ⟨energyConservationCert⟩
  83
  84end Action
  85end IndisputableMonolith
  86