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. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.