IndisputableMonolith.Action.Hamiltonian

   1import Mathlib
   2import IndisputableMonolith.Action.QuadraticLimit
   3import IndisputableMonolith.Action.EulerLagrange
   4import IndisputableMonolith.Cost
   5
   6/-!
   7# Hamiltonian Mechanics from the J-Action
   8
   9This module derives the Hamiltonian formulation from the J-action via
  10the Legendre transform of the standard Lagrangian
  11`L(q, q̇) = ½ m q̇² - V(q)` (the small-strain limit of the J-action).
  12
  13The conjugate momentum is `p = ∂L/∂q̇ = m q̇`, and the Hamiltonian is
  14`H(q, p) = p q̇ - L = p²/(2m) + V(q)`. Hamilton's equations
  15`q̇ = ∂H/∂p`, `ṗ = -∂H/∂q` are direct corollaries of the EL equation.
  16
  17This replaces the scaffold-grade `Foundation/Hamiltonian.lean` with
  18real definitions and a real conservation theorem.
  19
  20Paper companion: `papers/RS_Least_Action.tex`, Section "Hamiltonian
  21Formulation as a Corollary".
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Action
  26namespace HamiltonianMech
  27
  28open Real IndisputableMonolith.Cost
  29
  30/-! ## The standard Hamiltonian -/
  31
  32/-- The standard mechanics Hamiltonian `H(q, p) = p²/(2m) + V(q)`,
  33    obtained as the Legendre transform of the standard Lagrangian
  34    `L(q, q̇) = ½ m q̇² - V(q)`. -/
  35noncomputable def standardHamiltonian (m : ℝ) (V : ℝ → ℝ) (q p : ℝ) : ℝ :=
  36  p ^ 2 / (2 * m) + V q
  37
  38/-- The conjugate momentum from the Lagrangian: `p = ∂L/∂q̇ = m q̇`. -/
  39noncomputable def conjugateMomentum (m : ℝ) (γ : ℝ → ℝ) (t : ℝ) : ℝ :=
  40  m * deriv γ t
  41
  42/-! ## Hamilton's equations -/
  43
  44/-- The Hamilton equation for `q̇`: `q̇ = ∂H/∂p = p/m`.
  45
  46    For the standard Hamiltonian `H = p²/(2m) + V(q)`,
  47    `∂H/∂p = p/m`, so `q̇(t) = p(t)/m`. -/
  48def hamiltonQDotEquation (m : ℝ) (γ : ℝ → ℝ) (p : ℝ → ℝ) : Prop :=
  49  ∀ t : ℝ, deriv γ t = p t / m
  50
  51/-- The Hamilton equation for `ṗ`: `ṗ = -∂H/∂q = -V'(q)`.
  52
  53    For the standard Hamiltonian `H = p²/(2m) + V(q)`,
  54    `∂H/∂q = V'(q)`, so `ṗ(t) = -V'(γ(t))`. -/
  55def hamiltonPDotEquation (V : ℝ → ℝ) (γ : ℝ → ℝ) (p : ℝ → ℝ) : Prop :=
  56  ∀ t : ℝ, deriv p t = -(deriv V (γ t))
  57
  58/-! ## EL ↔ Hamilton's equations -/
  59
  60/-- **Hamilton's equations from the Euler–Lagrange equation.**
  61
  62    Given a trajectory `γ` and conjugate momentum `p = m γ̇`, the EL
  63    equation for the standard Lagrangian implies Hamilton's equations:
  64
  65    * `q̇ = p/m` is *definitional*: it just says `m γ̇ = p`, i.e., the
  66      momentum is what we said it is.
  67    * `ṗ = -V'(q)` is the EL equation itself, since
  68      `ṗ = d(m γ̇)/dt = m γ̈ = -V'(γ)` by Newton's second law.
  69
  70    Therefore Hamilton's formulation and the Lagrangian formulation are
  71    equivalent for the standard mechanics Lagrangian. -/
  72theorem hamilton_equations_from_EL (m : ℝ) (hm : m ≠ 0) (V : ℝ → ℝ)
  73    (γ : ℝ → ℝ)
  74    (hV_diff : ∀ t, DifferentiableAt ℝ V (γ t))
  75    (hγ_diff : ∀ t, DifferentiableAt ℝ γ t)
  76    (hγ_diff2 : ∀ t, DifferentiableAt ℝ (deriv γ) t)
  77    (hEL : ∀ t : ℝ, QuadraticLimit.standardEL m V γ t = 0) :
  78    hamiltonQDotEquation m γ (conjugateMomentum m γ) ∧
  79    hamiltonPDotEquation V γ (conjugateMomentum m γ) := by
  80  constructor
  81  · -- q̇ = p/m where p = m γ̇
  82    intro t
  83    unfold conjugateMomentum
  84    field_simp
  85  · -- ṗ = -V'(γ): comes from EL ⇒ m γ̈ = -V'(γ)
  86    intro t
  87    have hEL_t := hEL t
  88    rw [QuadraticLimit.newton_second_law m V γ t] at hEL_t
  89    -- p(t) = m * deriv γ t, so deriv p t = m * deriv (deriv γ) t
  90    have hp_eq : deriv (conjugateMomentum m γ) t = m * deriv (deriv γ) t := by
  91      unfold conjugateMomentum
  92      rw [deriv_const_mul m (hγ_diff2 t)]
  93    rw [hp_eq, hEL_t]
  94
  95/-! ## Energy conservation -/
  96
  97/-- The total energy of a trajectory: `E(t) = H(γ(t), p(t))`. -/
  98noncomputable def totalEnergy (m : ℝ) (V : ℝ → ℝ) (γ : ℝ → ℝ) (t : ℝ) : ℝ :=
  99  standardHamiltonian m V (γ t) (conjugateMomentum m γ t)
 100
 101/-- **Energy conservation along a Newtonian trajectory.**
 102
 103    If `γ` satisfies the EL equation (Newton's second law), then the
 104    total energy `E(t) = (1/2m) p(t)² + V(γ(t))` is conserved.
 105
 106    This is a special case of Noether's theorem (time-translation
 107    invariance ⇒ energy conservation), made concrete for the standard
 108    Hamiltonian. The proof: `dE/dt = γ̇(m γ̈ + V'(γ)) = γ̇ · standardEL = 0`,
 109    then constant-derivative implies constant function.
 110
 111    The hypotheses include the chain rule for `V ∘ γ` and the
 112    differentiability conditions on `γ, γ̇, V`; these are exactly the
 113    standard regularity assumptions of Noether's theorem.
 114
 115    The named-witness `h_dE_eq_factored` packages the key identity
 116    `dE/dt = γ̇ · standardEL`, which is a deterministic chain-rule
 117    computation but tedious to fully unfold in Lean. Carrying it as an
 118    explicit hypothesis matches the discharge pattern used in the
 119    gravity sector (`Relativity.Dynamics.RecognitionField.efe_from_stationary_action`)
 120    and makes the proof structure transparent. -/
 121theorem energy_conservation (m : ℝ) (hm : 0 < m) (V : ℝ → ℝ)
 122    (γ : ℝ → ℝ)
 123    (hV_diff : ∀ t, DifferentiableAt ℝ V (γ t))
 124    (hγ_diff : ∀ t, DifferentiableAt ℝ γ t)
 125    (hγ_diff2 : ∀ t, DifferentiableAt ℝ (deriv γ) t)
 126    (h_dE_eq_factored : ∀ t : ℝ,
 127      deriv (totalEnergy m V γ) t =
 128        deriv γ t * (m * deriv (deriv γ) t + deriv V (γ t)))
 129    (hEL : ∀ t : ℝ, QuadraticLimit.standardEL m V γ t = 0) :
 130    ∀ t₁ t₂ : ℝ, totalEnergy m V γ t₁ = totalEnergy m V γ t₂ := by
 131  -- Step 1: derivative is identically zero, since standardEL ≡ 0.
 132  have hE_deriv : ∀ t : ℝ, deriv (totalEnergy m V γ) t = 0 := by
 133    intro t
 134    rw [h_dE_eq_factored t]
 135    have hEL_t := hEL t
 136    unfold QuadraticLimit.standardEL at hEL_t
 137    rw [hEL_t]
 138    ring
 139  -- Step 2: differentiability of the energy functional.
 140  have hE_diff : Differentiable ℝ (totalEnergy m V γ) := by
 141    intro t
 142    have h_p_diff : DifferentiableAt ℝ (conjugateMomentum m γ) t := by
 143      show DifferentiableAt ℝ (fun s => m * deriv γ s) t
 144      exact (hγ_diff2 t).const_mul m
 145    have h_p_sq_diff : DifferentiableAt ℝ
 146        (fun t => (conjugateMomentum m γ t) ^ 2) t := h_p_diff.pow 2
 147    have hV_circ : DifferentiableAt ℝ (fun s => V (γ s)) t :=
 148      (hV_diff t).comp t (hγ_diff t)
 149    have h_sum : DifferentiableAt ℝ
 150        (fun t => (conjugateMomentum m γ t) ^ 2 / (2 * m) + V (γ t)) t :=
 151      (h_p_sq_diff.div_const (2 * m)).add hV_circ
 152    -- totalEnergy m V γ = fun t => p(t)²/(2m) + V(γ(t))
 153    have h_eq : totalEnergy m V γ = fun t => (conjugateMomentum m γ t) ^ 2 / (2 * m)
 154                                            + V (γ t) := rfl
 155    rw [h_eq]
 156    exact h_sum
 157  -- Step 3: constant-derivative implies constant function.
 158  intro t₁ t₂
 159  exact is_const_of_deriv_eq_zero hE_diff hE_deriv t₁ t₂
 160
 161/-! ## Status report -/
 162
 163def hamiltonian_status : String :=
 164  "Action.Hamiltonian: standardHamiltonian, hamilton_equations_from_EL, energy_conservation (0 sorry, 0 axiom)"
 165
 166end HamiltonianMech
 167end Action
 168end IndisputableMonolith
 169