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 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)$

Statement

Let $n \geq 1$ , let $U$ be a phase domain with standard two-form $ω_{U} = \sum_{i} d q^{i} \land d p_{i}$ (A phase domain, its canonical one-form and its standard symplectic two-form), and let $H : U \to R$ be of class $C^{2}$ ( $C^{k}$ Euclidean maps and diffeomorphisms). Write $\nabla H = (H_{q^{1}}, \dots, H_{q^{n}}, H_{p_{1}}, \dots, H_{p_{n}})$ for the Euclidean gradient (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case) and $J$ for the standard symplectic matrix. Then:

there is exactly one $C^{1}$ vector field $X_{H}$ on $U$ with $ι_{X_{H}} ω_{U} = d H$ , and it is $X_{H} = J \nabla H = (H_{p_{1}}, \dots, H_{p_{n}}, - H_{q^{1}}, \dots, - H_{q^{n}});$
an integral curve $t \mapsto (q (t), p (t))$ of $X_{H}$ satisfies Hamilton's equations ${\dot{q}}^{i} = H_{p_{i}} (q, p), {\dot{p}}_{i} = - H_{q^{i}} (q, p) (i = 1, \dots, n);$
for $f, g \in C^{2} (U)$ the Poisson bracket ${f, g} : = ω_{U} (X_{f}, X_{g})$ (in the finite-regularity convention of Finite-regularity differential forms, Hamiltonian fields and canonical maps in phase charts) is ${f, g} = \nabla f^{T} J \nabla g = \sum_{i = 1}^{n} (f_{q^{i}} g_{p_{i}} - f_{p_{i}} g_{q^{i}}),$ hence ${f, g} = - {g, f}$ , and ${f, g}$ is $C^{1}$ on $U$ .

Facts & Assumptions

Given: The phase domain $U$ , the $C^{2}$ function $H$ , and the $C^{2}$ functions $f, g$ on $U$ (A phase domain, its canonical one-form and its standard symplectic two-form, $C^{k}$ Euclidean maps and diffeomorphisms).

[F1]

Contraction formula and block identities: for $v = (a, b)$ one has $ι_{v} ω_{z} = \sum_{i} a_{i} d p_{i} - \sum_{i} b_{i} d q^{i}$ , and $J^{T} = - J$ , $J^{2} = - I_{2 n}$ (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}$ ).

[F2]

The differential of a $C^{1}$ function is $d h = \sum_{i} h_{q^{i}} d q^{i} + \sum_{i} h_{p_{i}} d p_{i}$ , and the gradient is the vector of partial derivatives (Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ , The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder).

[F3]

A Hamiltonian vector field is a vector field $X$ with $ι_{X} ω = d H$ for a smooth function $H$ , and the Poisson bracket is ${F, G} = ω (X_{F}, X_{G})$ (Hamiltonian vector field and Hamiltonian function, Poisson bracket on a symplectic manifold). For the present $C^{2}$ functions the field and bracket mean the explicitly defined finite-regularity coordinate objects of Finite-regularity differential forms, Hamiltonian fields and canonical maps in phase charts, with the same sign convention; the imported smooth definitions are used only in the smooth subcase.

[F4]

Chain rule and linear-algebra bookkeeping: matrix-vector multiplication distributes over sums, and the Euclidean pairing $u \cdot w = u^{T} w$ satisfies $u^{T} (J v) = (J^{T} u)^{T} v$ (Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, Linear map between vector spaces over the same field, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , A smooth vector field is a smooth section of the tangent bundle).

Proof

technique · direct; compare coefficients in the coordinate bases and use the block identities for the bracket formula

1.1F1F2F4algebra

Existence: define $X_{H} : = J \nabla H$ , whose components are $C^{1}$ because $H$ is $C^{2}$ ; by [F1] and [F2], $ι_{X_{H}} ω_{U} = \sum_{i} (J \nabla H)_{i} d p_{i} - \sum_{i} (J \nabla H)_{n + i} d q^{i}$ with $(J \nabla H)_{i} = H_{p_{i}}$ and $(J \nabla H)_{n + i} = - H_{q^{i}}$ , i.e. $ι_{X_{H}} ω_{U} = d H$ ; in particular $X_{H} = J \nabla H$ has the displayed components.

1.2F1

Uniqueness: if $X, Y$ are $C^{1}$ fields with $ι_{X} ω_{U} = d H = ι_{Y} ω_{U}$ , then $ι_{X - Y} ω_{U} = 0$ ; by [F1] the map $v \mapsto ι_{v} ω_{z}$ is injective at every $z$ , so $X - Y = 0$ pointwise.

2.1F1F3step 1.1algebra

Hamilton's equations and the bracket: an integral curve of $X_{H}$ solves $\dot{z} = X_{H} (z)$ , which in coordinates is ${\dot{q}}^{i} = H_{p_{i}}$ and ${\dot{p}}_{i} = - H_{q^{i}}$ , proving clause 2. For $f, g \in C^{2} (U)$ , step 1.1 applied to each function and [F1] give $ω_{U} (X_{f}, X_{g}) = (J \nabla f)^{T} J (J \nabla g) = \nabla f^{T} J^{T} J^{2} \nabla g = \nabla f^{T} J \nabla g$ . The last expression is the coordinate bracket defined in [F3], and block multiplication expands it to $\sum_{i} (f_{q^{i}} g_{p_{i}} - f_{p_{i}} g_{q^{i}})$ . Thus its equality with $ω_{U} (X_{f}, X_{g})$ is established directly, without assuming that equality for nonsmooth inputs.

3.1step 2.1F1algebra∎

Skew symmetry and regularity: swapping $f$ and $g$ in the coordinate formula negates every summand because $J^{T} = - J$ , so ${f, g} = - {g, f}$ ; the coordinate expression is a sum of products of $C^{1}$ partial derivatives, hence is $C^{1}$ .

Remarks

The published Hamiltonian vector fields exist uniquely for smooth functions and Hamilton equations in canonical cotangent coordinates give existence, uniqueness and the Hamilton equations for smooth functions on a cotangent bundle (the latter under countable choice). The point of this item is the choice-free local statement for $C^{2}$ data on a phase domain, together with the explicit block form of the field that the flow and canonical-map items below differentiate.
Part 3 is the coordinate formula on which the published Coordinate formula for the Poisson bracket and the bracket identities of the root library (bilinearity, skew symmetry, the derivation rule and the Jacobi identity in The Poisson bracket is bilinear, skew, and a derivation in each entry and The Poisson bracket satisfies the Jacobi identity) can be invoked by consumers in the smooth subcase; no second proof of the Jacobi identity is developed on this page.

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)$

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

The Hamiltonian field of a C2C2 function on a phase domain is J∇HJ∇H, and the Poisson bracket is ∑i(∂qif ∂pig−∂pif ∂qig)∑i​(∂qi​f∂pi​​g−∂pi​​f∂qi​g)

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

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)$