PropositionStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Hamiltonian on an inverse Legendre branch: differential, equivalence with the Euler-Lagrange equation, and the energy identity

Statement

Let $L : J \times U \times R^{n} \to R$ be a fibre-full $C^{2}$ time-dependent Lagrangian chart that is hyperregular, with inverse Legendre branch $v (t, q, p)$ and Hamiltonian $H (t, q, p) = p \cdot v (t, q, p) - L (t, q, v (t, q, p))$ (The Legendre map of a time-dependent Lagrangian: regularity and hyperregularity). Then:

(differential) for every $(t, q, p) \in J \times U \times R^{n}$ ,

$H_{p} (t, q, p) = v (t, q, p), H_{q} (t, q, p) = - L_{q} (t, q, v (t, q, p)), H_{t} (t, q, p) = - L_{t} (t, q, v (t, q, p));$

(equivalence) for a $C^{1}$ curve $(q, p) : I \to U \times R^{n}$ on an open interval $I \subseteq J$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral) the following are equivalent: (a) $q$ is $C^{2}$ and $E_{L} (q) (t) = 0$ for all $t \in I$ , with $p (t) = L_{v} (t, q (t), q^{'} (t))$ ; (b) $(q, p)$ satisfies Hamilton's equations $q^{'} (t) = H_{p} (t, q (t), p (t))$ and $p^{'} (t) = - H_{q} (t, q (t), p (t))$ for all $t \in I$ ;
(energy) along any curve satisfying (a) or (b), the function $e (t) : = L_{v} (t, q, q^{'}) \cdot q^{'} (t) - L (t, q (t), q^{'} (t))$ equals $H (t, q (t), p (t))$ and satisfies $e^{'} (t) = - L_{t} (t, q (t), q^{'} (t))$ on $I$ ; in particular, if $L_{t}$ vanishes on the set ${(s, q (s), q^{'} (s)) : s \in I}$ , then $e$ is constant on $I$ .

Facts & Assumptions

Given: The hyperregular chart data $L$ , its inverse branch $v$ , the Hamiltonian $H$ , and a $C^{1}$ curve $(q, p) : I \to U \times R^{n}$ .

[F1]

Hyperregularity gives a $C^{1}$ map $v : J \times U \times R^{n} \to R^{n}$ with $L_{v} (t, q, v (t, q, p)) = p for all (t, q, p) \in J \times U \times R^{n},$ and $H$ is $C^{1}$ ; the chain rule computes derivatives of the composites $(t, q, p) \mapsto L (t, q, v (t, q, p))$ and $(t, q, p) \mapsto v_{j} (t, q, p)$ (The Legendre map of a time-dependent Lagrangian: regularity and hyperregularity, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , $C^{k}$ Euclidean maps are closed under componentwise algebra and composition, If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative, The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder, $C^{k}$ Euclidean maps and diffeomorphisms).

[F2]

The Euler–Lagrange expression and the meaning of its vanishing are those of A time-dependent Lagrangian chart, its action functional and its fixed-endpoint first variations: $E_{L} (q) = L_{q} (t, q, q^{'}) - \frac{d}{d t} (L_{v} (t, q, q^{'}))$ . Here $q : I \to U$ is $C^{2}$ on its open interval in the sense of $C^{k}$ Euclidean maps and diffeomorphisms. On each compact subinterval $[a, b] \subseteq I$ , its restriction has the extension required by the action definition, using $q$ itself on a slightly larger interval inside $I$ ; thus the same Euler–Lagrange expression applies locally throughout $I$ . Partial derivatives in the first and second slots are the entries of the gradient in the sense of The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case and Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ .

[F3]

Newton--Leibniz calculus of curves (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Absolute value in an ordered field): a $C^{1}$ curve with identically vanishing derivative on an interval is constant (A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant applied componentwise), and differentiating an identity between $C^{1}$ curves is legitimate term by term.

Proof

technique · direct; differentiate $H$ along the inverse branch using the inverse relation, then translate between the two systems of equations

1.1F1algebra

For fixed $(t, q, p)$ write $v : = v (t, q, p)$ . Differentiating the identity $H (t, q, p) = \sum_{j} p_{j} v_{j} (t, q, p) - L (t, q, v (t, q, p))$ with respect to $p_{k}$ by the product and chain rules [F1] gives $H_{p_{k}} = v_{k} + \sum_{j} (p_{j} - L_{v_{j}} (t, q, v)) \frac{\partial v_{j}}{\partial p_{k}} = v_{k},$ because $L_{v_{j}} (t, q, v) = p_{j}$ for every $j$ by the inverse relation. Hence $H_{p} (t, q, p) = v (t, q, p)$ .

1.2F1algebra

Differentiating the same identity with respect to $q_{k}$ gives $H_{q_{k}} = \sum_{j} (p_{j} - L_{v_{j}} (t, q, v)) \frac{\partial v_{j}}{\partial q_{k}} - L_{q_{k}} (t, q, v) = - L_{q_{k}} (t, q, v),$ and differentiating with respect to $t$ gives $H_{t} = \sum_{j} (p_{j} - L_{v_{j}}) \partial_{t} v_{j} - L_{t} (t, q, v) = - L_{t} (t, q, v)$ . This proves clause 1.

2.1F1F2step 1.1step 1.2given

Clause 2, (a) $\Rightarrow$ (b): assume (a). Then $p (t) = L_{v} (t, q (t), q^{'} (t))$ is $C^{1}$ as a composite of $C^{1}$ maps, and applying the inverse relation of [F1] with $(t, q (t), L_{v} (t, q (t), q^{'} (t)))$ gives $v (t, q (t), p (t)) = q^{'} (t)$ . Hence by clause 1 $q^{'} (t) = v (t, q (t), p (t)) = H_{p} (t, q (t), p (t)),$ and, differentiating the relation $p = L_{v} (t, q, q^{'})$ and using (a), $p^{'} (t) = \frac{d}{d t} L_{v} (t, q, q^{'}) = L_{q} (t, q, q^{'}) = - H_{q} (t, q (t), p (t)),$ where the last equality is clause 1 with $v (t, q, p) = q^{'}$ . Thus (b) holds.

2.2F1step 1.1step 1.2given

Clause 2, (b) $\Rightarrow$ (a): assume (b). By clause 1, $q^{'} = H_{p} (t, q, p) = v (t, q, p)$ is a composite of $C^{1}$ maps, hence $C^{1}$ on $I$ ; a curve with $C^{1}$ derivative is $C^{2}$ , so $q$ is $C^{2}$ . Applying $L_{v} (t, q, \cdot)$ to the identity $q^{'} = v (t, q, p)$ and using the inverse relation gives $L_{v} (t, q, q^{'}) = p$ , so $p (t) = L_{v} (t, q (t), q^{'} (t))$ . Now $p^{'} = - H_{q} (t, q, p) = L_{q} (t, q, q^{'})$ by clause 1, while also $p^{'} = \frac{d}{d t} L_{v} (t, q, q^{'})$ ; comparing gives $E_{L} (q) (t) = 0$ on $I$ . Thus (a) holds, and clause 2 is proved.

3.1F1step 1.1step 1.2step 2.1

Clause 3: for a curve satisfying (a) (equivalently (b)) put $v (t) : = q^{'} (t)$ and $p (t) : = L_{v} (t, q, q^{'})$ . Then $e (t) = p (t) \cdot v (t) - L (t, q (t), v (t)) = H (t, q (t), p (t))$ by the definition of $H$ and $v (t) = v (t, q (t), p (t))$ . By clause 1 and the chain rule, $e^{'} (t) = H_{t} + H_{q} \cdot q^{'} + H_{p} \cdot p^{'} = - L_{t} - L_{q} \cdot q^{'} + v \cdot p^{'} .$ Substituting $v = q^{'}$ and $p^{'} = L_{q} (t, q, q^{'})$ from (a) gives $e^{'} = - L_{t} - L_{q} \cdot q^{'} + q^{'} \cdot L_{q} = - L_{t}$ .

4.1F3step 3.1∎

If $L_{t}$ vanishes along the trajectory, then $e^{'} = 0$ identically on $I$ ; by [F3] $e$ is constant on $I$ .

Remarks

The identity $d H = - L_{t} d t - L_{q} \cdot d q + v \cdot d p$ is the coordinate expression of the displayed partial derivatives; it is the form in which the differential is usually quoted, and it makes manifest that the inverse-branch Hamiltonian is determined by $L$ and the branch alone.
Only the fibre bijectivity and $C^{1}$ inverse of hyperregularity are used. When $L$ is merely regular, Nonsingular velocity Hessian is equivalent to invertibility of the Legendre derivative, hence gives a local C^1 inverse supplies local branches and the same computations hold on each branch; the global statements above are then local, and the page keeps the two hypotheses separate.
The energy $e$ need not be bounded below or above and is not asserted to be a minimum of anything; it is conserved exactly when $L$ has no explicit time dependence along the trajectory, in which case $H$ is a first integral of the branch system.

The Hamiltonian on an inverse Legendre branch: differential, equivalence with the Euler-Lagrange equation, and the energy identity

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources