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 derivative of the Hamiltonian flow satisfies $Y^{T} J Y = J$ and $\det Y = 1$

Statement

Let $n \geq 1$ , let $U$ be a phase domain with standard two-form $ω_{U}$ and matrix $J$ , let $H \in C^{2} (U)$ , and let $Φ$ be the local flow of the Hamiltonian field $X_{H} = J \nabla H$ (The Hamiltonian field of a $C^{2}$ function on a phase domain is $J \nabla H$ , and the Poisson bracket is $\sum_{i} (\partial_{q^{i}} f \partial_{p_{i}} g - \partial_{p_{i}} f \partial_{q^{i}} g)$ , The local flow of an autonomous first-order system). Let $z_{0} \in U$ , let $I \subseteq R$ be the open interval of times $t$ with $(t, z_{0})$ in the flow domain, and for $t \in I$ put

$Y (t) : = D_{z} Φ_{t} (z_{0}) \in M_{2 n} (R) .$

Then $t \mapsto Y (t)$ is of class $C^{1}$ on $I$ and, for every $t \in I$ :

(variational equation) $Y^{'} (t) = J H e s s H (Φ_{t} (z_{0})) Y (t)$ and $Y (0) = I_{2 n}$ ;
(canonical matrix identity) $Y (t)^{T} J Y (t) = J$ ;
(unit determinant) $\det Y (t) = 1$ .

The same conclusions hold for a time-dependent Hamiltonian $H : T \times U \to R$ of class $C^{2}$ , where $T$ is an open real interval. For $t_{0} \in T$ and $z_{0} \in U$ , write $E (t, t_{0}, z)$ for the maximal solution of $z^{'} = J \nabla_{z} H (t, z)$ with $z (t_{0}) = z$ ; its domain consists of the triples where this solution exists. On the maximal open time interval $I_{t_{0}, z_{0}}$ set $Y (t) = D_{z} E (t, t_{0}, z_{0})$ . Then $Y^{'} = J {Hess}_{z} H (t, E (t, t_{0}, z_{0})) Y, Y (t_{0}) = I_{2 n}, Y^{T} J Y = J, \det Y = 1.$ The evolution $E$ is $C^{1}$ on its open domain, and each fixed-endpoint map has inverse $E (t_{0}, t, \cdot)$ on its image. Autonomous $H$ is recovered by $H (t, z) = H (z)$ and $E (t, t_{0}, z) = Φ (t - t_{0}, z)$ .

Facts & Assumptions

Given: The phase domain $U$ , the $C^{2}$ Hamiltonian $H$ , the local flow $Φ$ , the point $z_{0} \in U$ and the derivative $Y (t) = D_{z} Φ_{t} (z_{0})$ ; for the additional case the open interval $T$ , jointly $C^{2}$ Hamiltonian $H$ , and initial time $t_{0} \in T$ are given.

[F1]

Put $F : = X_{H}$ . The local smooth-dependence theorem supplies the initial-state derivative and variational equation on each sufficiently small time-state cylinder (C¹ dependence of an autonomous flow on the initial condition, and the variational equation); the maximal flow is $C^{1}$ on its open domain (The flow domain of a C¹ autonomous field is open and the flow is C¹ on it), and its composition law is The local flow is a partial one-parameter group: identity, composition and inverse-time laws. In particular the derivative of the field is $D F = J H e s s H$ , because $X_{H} = J \nabla H$ and $J$ is constant (The Hamiltonian field of a $C^{2}$ function on a phase domain is $J \nabla H$ , and the Poisson bracket is $\sum_{i} (\partial_{q^{i}} f \partial_{p_{i}} g - \partial_{p_{i}} f \partial_{q^{i}} g)$ , The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, The Hessian matrix and critical points of a scalar field).

[F2]

The Hessian $H e s s H (z)$ is the matrix $(\partial_{i} \partial_{j} H (z))$ , and for $H \in C^{2}$ it is symmetric: $H e s s H (z)^{T} = H e s s H (z)$ (The Hessian matrix and critical points of a scalar field, The Hessian of a $C^{2}$ scalar field is symmetric).

[F3]

Block identities $J^{T} = - J$ , $J^{2} = - I_{2 n}$ , $J^{- 1} = J^{T}$ and $ω_{z} (v, w) = v^{T} J w$ (The standard two-form of a phase domain is closed and nondegenerate, with contraction $ι_{v} ω = \sum_{i} a_{i} d p_{i} - \sum_{i} b_{i} d q^{i}$ ).

[F4]

Determinant calculus: the determinant is a polynomial in the matrix entries (For every fixed finite size at least one, the determinant of a real square matrix is a polynomial in its matrix entries), and a finite sum of finite products of continuous real functions is continuous (Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined, with the metric and topological notions of continuity identified by Metric continuity characterisations, with countable choice for the sequential converse); the entry functions $t \mapsto Y_{i j} (t)$ are continuous as components of the continuous map $Y$ (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form), so $t \mapsto \det Y (t)$ is continuous on $I$ . The Leibniz formula gives $\det I_{2 n} = 1$ (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix); moreover $\det (A B) = \det (A) \det (B)$ and $\det (A^{T}) = \det (A)$ for square matrices (For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ , For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$ ), and $\det J \neq 0$ because $J$ is invertible with $J^{- 1} = J^{T} = - J$ and over the field $R$ a square matrix is invertible exactly when its determinant is nonzero (A positive-sized square matrix over a commutative ring is invertible if and only if its determinant is a unit, Invertible Euclidean linear maps).

[F5]

Sign rigidity on an interval (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length): a continuous $g : I \to R$ on an interval with $g (t)^{2} = 1$ for all $t \in I$ and $g (0) = 1$ equals $1$ ; indeed, if $g (t) = - 1$ for some $t > 0$ , the intermediate value theorem on $[0, t]$ gives $c$ with $g (c) = 0$ , contradicting $g (c)^{2} = 1$ , and the case $t < 0$ is identical on $[t, 0]$ .

Proof

technique · direct; the variational equation gives the derivative, the antisymmetry of $J$ cancels the quadratic form, and continuity upgrades the squared determinant

1.1F1algebra

Clause 1: by [F1] the initial-state derivative $Y$ exists on $I$ . On a small cylinder the local variational theorem makes it $C^{1}$ with the stated initial condition. For any compact reference orbit segment from $0$ to an admissible $t$ , finitely many such local cylinders cover the segment. Flow composition expresses the initial-state derivative as a product of the local derivatives; on each successive patch the chain rule differentiates this product in the last time variable and gives the same variational equation with the preceding product as its initial value. This extends the $C^{1}$ derivative and its equation to the entire segment, for negative times using the reversed field. Since $t$ is arbitrary, $Y$ is $C^{1}$ on $I$ and solves $Y^{'} = D F (Φ_{t} (z_{0})) Y$ with $Y (0) = I_{2 n}$ ; since $X_{H} = J \nabla H$ and $J$ is constant, the chain rule gives $D F (z) = J H e s s H (z)$ , so $Y^{'} (t) = J H e s s H (Φ_{t} (z_{0})) Y (t)$ .

1.2F1givenconstruct

For the time-dependent case use the autonomous $C^{1}$ field $\tilde{F} (s, z) = (1, J \nabla_{z} H (s, z))$ on the open set $T \times U$ . Its maximal flow $\tilde{Φ}$ has open domain and is $C^{1}$ by The flow domain of a C¹ autonomous field is open and the flow is C¹ on it. Its first coordinate is $s + r$ at elapsed time $r$ , so define $E (t, t_{0}, z)$ as the second coordinate of $\tilde{Φ} (t - t_{0}, (t_{0}, z))$ . The preimage of the open flow domain under this change of variables is open, and $E$ is $C^{1}$ by composition. The composition and inverse laws for the extended autonomous flow give $E (t_{0}, t, E (t, t_{0}, z)) = z$ and the reverse identity, with both domains included; thus fixed-endpoint maps are $C^{1}$ diffeomorphisms onto open images.

2.1F1F2F3step 1.1algebra

Clause 2: put $A (t) : = J H e s s H (Φ_{t} (z_{0}))$ . By [F2] and [F3], $A^{T} = (H e s s H)^{T} J^{T} = (H e s s H) (- J) = - H e s s H J$ and $J A = J^{2} H e s s H = - H e s s H$ , so $A^{T} J + J A = - H e s s H J J - H e s s H = (H e s s H) (- J^{2}) - H e s s H = 0$ ; hence $\frac{d}{d t} (Y^{T} J Y) = Y^{' T} J Y + Y^{T} J Y^{'} = Y^{T} (A^{T} J + J A) Y = 0$ , and $Y (t)^{T} J Y (t) = Y (0)^{T} J Y (0) = J$ for all $t \in I$ .

3.1step 2.1F4F5algebra

Clause 3: taking determinants in clause 2 and using [F4] gives $\det (Y^{T} J Y) = \det (Y^{T}) \det (J) \det (Y) = (\det Y)^{2} \det J$ , so $(\det Y (t))^{2} \det J = \det J$ ; since $\det J \neq 0$ , $(\det Y (t))^{2} = 1$ for all $t \in I$ ; by [F4] the function $t \mapsto \det Y (t)$ is continuous with $\det Y (0) = \det I_{2 n} = 1$ , so the sign rigidity [F5] gives $\det Y \equiv 1$ .

4.1F1F2F3F4F5step 2.1step 3.1step 1.2∎

Apply the autonomous smooth-dependence/variational theorem to $\tilde{F}$ on small balls along an extended solution, and use the flow composition law to concatenate the initial-state derivatives over finitely many such local patches on each compact subinterval of its lifetime. This gives the variational equation for the derivative with respect to the original $z$ -initial coordinates on the full maximal interval. The first coordinate $t$ does not depend on those coordinates, so its derivative block is zero; the remaining block is $Y$ , and its equation is $Y^{'} = J {Hess}_{z} H (t, E (t, t_{0}, z_{0})) Y$ with $Y (t_{0}) = I$ . The $z$ -Hessian is symmetric at each time. The cancellation in step 2.1 therefore applies with this time-dependent symmetric Hessian, giving $\frac{d}{d t} (Y^{T} J Y) = 0$ and $Y^{T} J Y = J$ . The determinant argument of step 3.1 applies on the interval containing $t_{0}$ with the initial sign $\det Y (t_{0}) = 1$ , yielding $\det Y = 1$ . All conclusions, including the nonautonomous case, follow.

Remarks

Clauses 2 and 3 are the differentiated form of the published statement that Hamiltonian flows preserve the symplectic form (Hamiltonian flows preserve the symplectic form) and the Liouville volume (Liouville volume preservation); the present item records the matrix identity that a chart computation, rather than the Cartan formula, produces, and it is this identity that the canonical-map test of A $C^{1}$ map between phase domains preserves the standard two-form iff $D C^{T} J D C = J$ , and a canonical diffeomorphism carries $X_{H \circ C}$ to $X_{H}$ compares with.
The statement is local in $t$ and on the actual flow domain; no completeness of $X_{H}$ is assumed, exactly as in The local flow of an autonomous first-order system.

The derivative of the Hamiltonian flow satisfies $Y^{T} J Y = J$ and $\det Y = 1$

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

The derivative of the Hamiltonian flow satisfies YTJY=JYTJY=J and det⁡Y=1detY=1

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

The derivative of the Hamiltonian flow satisfies $Y^{T} J Y = J$ and $\det Y = 1$