ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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.

Determinant tests on explicit linear maps: $\det A = 1$ is equivalent to canonicity in dimension two, and strictly weaker in dimension four (the volume-preserving shear)

Example

Let $J_{2} = (\begin{array}{cc} 0 & 1 \\ - 1 & 0 \end{array})$ and, in the ordered coordinates $(q^{1}, p_{1}, q^{2}, p_{2})$ of $R^{4}$ , let $J_{4} = diag (J_{2}, J_{2})$ be the standard symplectic matrix of the phase domain $R^{4}$ (A phase domain, its canonical one-form and its standard symplectic two-form); recall that a linear map $A$ is canonical exactly when $A^{T} J A = J$ (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}$ ). Then:

(dimension two) For $A = (\begin{array}{cc} a & b \\ c & d \end{array})$ one has

$A^{T} J_{2} A = (a d - b c) J_{2} = (\det A) J_{2},$

so an invertible $A$ is canonical if and only if $\det A = 1$ : in one degree of freedom canonicity and oriented area preservation coincide. For instance $A = (\begin{array}{cc} 2 & 1 \\ 1 & 1 \end{array})$ has $\det A = 1$ and is canonical. 2. (scaling) For $λ \neq 0$ the block-diagonal map $C (q, p) = (λ q, λ^{- 1} p)$ on the phase domain $R^{2 n}$ is canonical: its derivative $diag (λ I_{n}, λ^{- 1} I_{n})$ satisfies $D C^{T} J D C = J$ and $\det D C = 1$ ; it even preserves the canonical one-form, $C^{*} λ = λ$ , because $(λ^{- 1} p) \cdot d (λ q) = p \cdot d q$ . 3. (volume preservation is weaker in dimension four) The linear shear

$C (q^{1}, q^{2}, p_{1}, p_{2}) = (q^{1}, q^{2} + q^{1}, p_{1}, p_{2})$

is written in grouped coordinates $(q^{1}, q^{2}, p_{1}, p_{2})$ , whose symplectic matrix is $J_{g r p} = (\begin{array}{cc} 0 & I_{2} \\ - I_{2} & 0 \end{array})$ . It has $\det D C = 1$ , so it preserves volume, but $D C^{T} J_{g r p} D C = J_{g r p} + e_{1} e_{4}^{T} - e_{4} e_{1}^{T} \neq J_{g r p}$ : the $(1, 4)$ -entry is $1$ instead of $0$ . Equivalently the fundamental bracket ${Q^{2}, P_{1}} = 1$ does not vanish, while canonicity would force ${Q^{2}, P_{1}} = δ_{1}^{2} = 0$ . Hence $∣ \det D C ∣ = 1$ does not imply canonicity in dimension $4$ . 4. (positive control) If $A = diag (A_{1}, A_{2})$ in the ordered coordinates $(q^{1}, p_{1}, q^{2}, p_{2})$ with each $2 \times 2$ block satisfying $A_{i}^{T} J_{2} A_{i} = J_{2}$ , then $A^{T} J_{4} A = J_{4}$ : canonicity is preserved blockwise.

Facts & Assumptions

Given: The standard symplectic matrices $J_{2}$ and $J_{4} = diag (J_{2}, J_{2})$ , the displayed linear maps, and the coordinate functions of the phase domains.

[F1]

Symplectic matrix and canonical tests (A phase domain, its canonical one-form and its standard symplectic two-form, 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}$ , 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}$ ): $J^{T} = - J$ , $J^{2} = - I$ ; a $C^{1}$ map between phase domains is canonical exactly when $D C^{T} J D C = J$ ; canonicity is equivalent to the preservation of the standard two-form.

[F2]

Brackets (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)$ , A phase domain, its canonical one-form and its standard symplectic two-form): the coordinate functions of a phase domain satisfy ${z^{i}, z^{j}} = J^{i j}$ ; in particular ${q^{i}, p_{j}} = δ_{j}^{i}$ , ${q^{i}, q^{j}} = {p_{i}, p_{j}} = 0$ .

[F3]

Matrix algebra (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix, 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)$ , Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, The transpose $A^{T}$ of a matrix, Linear map between vector spaces over the same field, $C^{k}$ Euclidean maps and diffeomorphisms): matrix products, transposes and determinants are computed entrywise by the ordinary rules, $\det (A^{T}) = \det A$ , and a linear map has constant derivative equal to its matrix.

Verification

technique · direct. Multiply the explicit matrices, read the determinant, and evaluate the fundamental bracket that distinguishes the shear from a canonical map

1.1F1F3algebra

Dimension two: multiplying $A^{T} J_{2} A$ by [F3] gives $(\begin{array}{cc} 0 & a d - b c \\ - (a d - b c) & 0 \end{array}) = (a d - b c) J_{2}$ ; for invertible $A$ this equals $J_{2}$ exactly when $\det A = a d - b c = 1$ by [F1], and $A = (\begin{array}{cc} 2 & 1 \\ 1 & 1 \end{array})$ has determinant $2 - 1 = 1$ , which is claim 1.

1.2F1F3algebra

Scaling: $D C = diag (λ I_{n}, λ^{- 1} I_{n})$ computed by [F3], and $diag (λ I_{n}, λ^{- 1} I_{n})^{T} J diag (λ I_{n}, λ^{- 1} I_{n})$ has the off-diagonal blocks $λ \cdot I \cdot λ^{- 1} I = I_{n}$ and $- λ^{- 1} I \cdot λ I = - I_{n}$ , so it equals $J$ ; the determinant is $λ^{n} λ^{- n} = 1$ , and $C^{*} λ = \sum_{a} (λ^{- 1} p_{a}) d (λ q^{a}) = λ$ ; this is claim 2.

1.3F1F2F3algebra

Shear: the derivative of $C$ computed by [F3] is $D C = I_{4} + e_{2} e_{1}^{T}$ (in grouped coordinates), with $\det D C = 1$ because it is triangular with unit diagonal; expanding $D C^{T} J_{g r p} D C = (I + e_{1} e_{2}^{T}) J_{g r p} (I + e_{2} e_{1}^{T})$ gives $J_{g r p} + e_{1} e_{4}^{T} - e_{4} e_{1}^{T}$ , whose $(1, 4)$ -entry is $1$ , so the matrix identity fails; equivalently, by [F2], ${Q^{2}, P_{1}} = \sum_{a} (Q_{q^{a}}^{2} P_{1, p_{a}} - Q_{p_{a}}^{2} P_{1, q^{a}}) = \partial Q^{2} / \partial q^{1} \cdot \partial P_{1} / \partial p_{1} = 1 \neq δ_{1}^{2}$ , and canonicity would force the vanishing of this bracket; this is claim 3.

1.4F1F3algebra

Block positive control: in the ordered coordinates $J_{4} = diag (J_{2}, J_{2})$ , so $diag (A_{1}, A_{2})^{T} J_{4} diag (A_{1}, A_{2}) = diag (A_{1}^{T} J_{2} A_{1}, A_{2}^{T} J_{2} A_{2}) = diag (J_{2}, J_{2}) = J_{4}$ whenever each block satisfies its two-dimensional identity; this is claim 4.

2.1F1F3step 1.3algebra

Necessity of determinant $+ 1$ in dimension four: put $ω (v, w) = v^{T} J_{4} w$ and define $T (v_{1}, v_{2}, v_{3}, v_{4}) = ω (v_{1}, v_{2}) ω (v_{3}, v_{4}) - ω (v_{1}, v_{3}) ω (v_{2}, v_{4}) + ω (v_{1}, v_{4}) ω (v_{2}, v_{3})$ . Bilinearity and skew-symmetry make $T$ multilinear and alternating (interchanging any adjacent pair negates the displayed expression), and $T (e_{1}, e_{2}, e_{3}, e_{4}) = 1$ . Expanding each argument in the coordinate basis therefore gives $T (A e_{1}, A e_{2}, A e_{3}, A e_{4}) = \det A$ by the permutation definition of the determinant. If $A^{T} J_{4} A = J_{4}$ , each pairing in $T$ is preserved, so that value is $T (e_{1}, e_{2}, e_{3}, e_{4}) = 1$ . Thus every canonical $A$ has $\det A = 1$ , while step 1.3 gives a noncanonical map with determinant $1$ . The grouped-coordinate version has the same determinant by conjugation with the coordinate permutation.

3.1step 1.1step 1.2step 1.3step 1.4step 2.1∎

Collecting steps 1.1-1.4 and 2.1 proves the four claims; in particular the determinant test is equivalent to canonicity in dimension two and strictly weaker in dimension four.

Determinant tests on explicit linear maps: $\det A = 1$ is equivalent to canonicity in dimension two, and strictly weaker in dimension four (the volume-preserving shear)

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources

Determinant tests on explicit linear maps: det⁡A=1detA=1 is equivalent to canonicity in dimension two, and strictly weaker in dimension four (the volume-preserving shear)

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources

Determinant tests on explicit linear maps: $\det A = 1$ is equivalent to canonicity in dimension two, and strictly weaker in dimension four (the volume-preserving shear)