LemmaStatement: 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.

Hamiltonian flows and the exact splitting map preserve the complexified canonical form and the Poisson bracket

Statement

Let $d \geq 1$ and let $(U, U_{ρ}, \tilde{A}, \tilde{B}, M, K, δ, Ψ_{h})$ be analytic splitting data as in Analytic splitting data with uniform holomorphic neighbourhood, and the exact symmetric splitting map $Ψ_{h}$ , with $J$ the standard matrix and $ω_{C}$ , ${\cdot, \cdot}$ the complexified form and bracket of Complex phase domains, holomorphic maps on $C^{m}$ , and the complexified canonical form and bracket. Let $F \in {\tilde{A}, \tilde{B}}$ and let $φ_{F}^{t}$ be the flow of $X_{F}$ as in The flow of a bounded holomorphic field on a polydisc: existence in complex time, displacement bound, holomorphy, and the composition law, on the domain where it is defined.

For every $(t, Z)$ in the flow domain, $φ_{F}^{t}$ is holomorphic near $Z$ , its derivative is invertible, and $D φ_{F}^{t} (Z)^{T} J D φ_{F}^{t} (Z) = J .$
For every $h$ and every point $Z$ where $Ψ_{h}$ is defined and holomorphic, $D Ψ_{h} (Z)$ is invertible and $D Ψ_{h} (Z)^{T} J D Ψ_{h} (Z) = J .$
For all holomorphic $f, g$ on an open set containing $Ψ_{h} (Z)$ , ${f \circ Ψ_{h}, g \circ Ψ_{h}} (Z) = {f, g} (Ψ_{h} (Z)) .$

Facts & Assumptions

Given: The analytic splitting data of Analytic splitting data with uniform holomorphic neighbourhood, and the exact symmetric splitting map $Ψ_{h}$ ; a field $F \in {\tilde{A}, \tilde{B}}$ with $∥ X_{F} ∥ \leq M$ on $U_{ρ}$ ; the flow $φ_{F}^{t}$ of $X_{F}$ ; the exact splitting map $Ψ_{h} = φ_{\tilde{A}}^{h / 2} \circ φ_{\tilde{B}}^{h} \circ φ_{\tilde{A}}^{h / 2}$ .

[L1]

The flow is holomorphic, and holomorphic maps are $C^{\infty}$ : the coordinate derivatives of a holomorphic map are again holomorphic (Iterated Cauchy formula, power-series expansion and Cauchy estimates for functions continuous and separately holomorphic on a polydisc clause 3, Calculus of holomorphic maps: chain rule, Wirtinger derivatives, coefficient extraction in one variable, and locally uniform limits clause 1 and 2, Complex phase domains, holomorphic maps on $C^{m}$ , and the complexified canonical form and bracket).

[L2]

The variational equation. Since $t \mapsto φ_{F}^{t} (Z)$ solves $\partial_{t} φ = X_{F} (φ)$ and both sides are $C^{1}$ in $(t, Z)$ by [L1], Clairaut's theorem permits exchanging the mixed partials, and the chain rule gives $\partial_{t} (D φ_{F}^{t} (Z)) = D X_{F} (φ_{F}^{t} (Z)) \circ D φ_{F}^{t} (Z)$ (Clairaut--Schwarz theorem for continuous second partial derivatives, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder, Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ).

[L3]

For holomorphic $H : D \to C$ , its gradient column $\nabla H$ has total derivative $D (\nabla H) (Z) = Hess H (Z) = (\partial_{z_{k}} \partial_{z_{l}} H (Z))_{k, l}$ , a complex-symmetric matrix, and $D X_{H} = J Hess H$ because $X_{H} = J \nabla H$ (Calculus of holomorphic maps: chain rule, Wirtinger derivatives, coefficient extraction in one variable, and locally uniform limits clause 2, Clairaut--Schwarz theorem for continuous second partial derivatives, Complex phase domains, holomorphic maps on $C^{m}$ , and the complexified canonical form and bracket).

[L4]

Matrix algebra: $J^{T} = - J$ , $J^{2} = - I_{2 d}$ , hence $J^{T} J = I_{2 d}$ ; for invertible $A$ , the identity $A^{T} J A = J$ is equivalent to $A J A^{T} = J$ ; and products of matrices satisfying the identity satisfy it again (Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, The transpose $A^{T}$ of a matrix, Invertible matrices and the general linear group ${GL}_{n} (F)$ ).

[L5]

Bracket matrix identity: for holomorphic $f, g$ , ${f, g} = (\nabla f)^{T} J \nabla g$ (Calculus of holomorphic maps: chain rule, Wirtinger derivatives, coefficient extraction in one variable, and locally uniform limits clause 2).

Proof

technique · direct; differentiate the matrix identity along the flow with the variational equation, then compose and rewrite the bracket

1.1givenL1L2L3L4algebra

The derivative of the matrix identity along the flow. Fix $(Z, t)$ in the flow domain and put $A (τ) : = D φ_{F}^{τ} (Z)$ . By [L2], $A^{'} (τ) = D X_{F} (φ_{F}^{τ} (Z)) A (τ)$ , and by [L3], $D X_{F} = J Hess F$ with $Hess F$ symmetric. Then $\frac{d}{d τ} (A (τ)^{T} J A (τ)) = A^{T} [(J Hess F)^{T} J + J (J Hess F)] A = A^{T} [Hess F^{T} J^{T} J + J^{2} Hess F] A = 0,$ using $J^{T} J = I$ , $J^{2} = - I$ and $Hess F^{T} = Hess F$ ([L4]). Since the expression is continuous in $τ$ and has zero derivative on the connected flow interval, it equals its value at $τ = 0$ , namely $I^{T} J I = J$ . Thus $D φ_{F}^{t} (Z)^{T} J D φ_{F}^{t} (Z) = J$ .

2.1givenstep 1.1L4

Invertibility. Along the reverse continuation of the same solution branch, clause 3 of The flow of a bounded holomorphic field on a polydisc: existence in complex time, displacement bound, holomorphy, and the composition law supplies the local inverse $φ_{F}^{- t}$ near $φ_{F}^{t} (Z)$ . The chain rule gives $D φ_{F}^{- t} (φ_{F}^{t} (Z)) \circ D φ_{F}^{t} (Z) = I$ : the derivative is invertible with inverse $D φ_{F}^{- t} (φ_{F}^{t} (Z))$ , and the identity of step 1.1 transfers to $A J A^{T} = J$ by [L4].

3.1givenstep 1.1step 2.1L4algebra

Composition. The chain rule gives $D Ψ_{h} (Z) = A_{1} A_{2} A_{3}$ with $A_{1} = D φ_{\tilde{A}}^{h / 2}$ at $φ_{\tilde{B}}^{h} (φ_{\tilde{A}}^{h / 2} (Z))$ , $A_{2} = D φ_{\tilde{B}}^{h}$ at $φ_{\tilde{A}}^{h / 2} (Z)$ and $A_{3} = D φ_{\tilde{A}}^{h / 2}$ at $Z$ . Each $A_{i}$ satisfies $A_{i}^{T} J A_{i} = J$ by step 1.1 and is invertible by step 2.1; hence $D Ψ_{h} (Z)^{T} J D Ψ_{h} (Z) = A_{3}^{T} (A_{2}^{T} (A_{1}^{T} J A_{1}) A_{2}) A_{3} = J$ by [L4], and $D Ψ_{h} (Z)$ is invertible as a product of invertible matrices.

4.1givenstep 3.1L4L5algebra

Bracket identity. Let $f, g$ be holomorphic near $Ψ_{h} (Z)$ . By the chain rule, $\nabla (f \circ Ψ_{h}) (Z) = D Ψ_{h} (Z)^{T} \nabla f (Ψ_{h} (Z))$ , and likewise for $g$ ; hence by [L5] ${f \circ Ψ_{h}, g \circ Ψ_{h}} (Z) = \nabla f (Ψ_{h} (Z))^{T} (D Ψ_{h} (Z) J D Ψ_{h} (Z)^{T}) \nabla g (Ψ_{h} (Z)) .$ By step 3.1 and the equivalence of [L4] (applicable because $D Ψ_{h} (Z)$ is invertible), $D Ψ_{h} J D Ψ_{h}^{T} = J$ , so the last display equals $\nabla f (Ψ_{h} (Z))^{T} J \nabla g (Ψ_{h} (Z)) = {f, g} (Ψ_{h} (Z))$ by [L5] again.

5.1step 1.1step 3.1step 4.1∎

Conclusion. Step 1.1 gives clause 1 for the two fields, step 3.1 gives clause 2, and step 4.1 gives clause 3.

Remarks

Whether the flows are globally defined on the whole of $U_{ρ}$ is not asserted; all identities hold wherever the flows and compositions exist, which is the only form used on this page. The lemma is the complexified counterpart of the real symplecticity of the splitting map in The drift, kick and velocity-Verlet maps are canonical: $(D C)^{T} J D C = J$ and $C^{*} ω = ω$ ; for the mechanical data the velocity-Verlet variant is obtained by interchanging the analytic splitting labels.
The bracket identity is the hypothesis that makes the formal logarithm a derivation of the Poisson bracket in The binomial family of the splitting pullback is multiplicative and bracket-preserving, and its logarithm is a derivation.

Hamiltonian flows and the exact splitting map preserve the complexified canonical form and the Poisson bracket

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources