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.

The isotropic oscillator of the model: explicit solution, the determinant and matrix tests on each two-dimensional block, and the area and energy checks

Physical scope

A worked verification of the symplectic and volume-preserving character of the model's Hamiltonian flow on the isotropic oscillator instance: the explicit solution of the one-label model with potential $(k / 2) ∣ x ∣^{2}$ , the block matrix identity and unit determinant of its time- $t$ map, the area and six-volume checks on explicit boxes, and the constancy of the oscillator energy. All quantities are model values of the declared idealization; no measurement is reported.

Example

Declare the one-label model of the force branch Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance with $N = 1$ , mass $m > 0$ , time window $R$ , configuration domain $Q = R^{3}$ , the time-independent potential $U (x) = \frac{1}{2} k ∣ x ∣^{2}$ with $k > 0$ and no residual forces (Configuration domain of $N$ labeled particles: open admissible sets, regular holonomic constraints and the mass operator, Potential presentations of a force model, potential and mechanical energy, closed versus exact force fields, local potentials and equipotential level sets, The action functional of a force model with a potential presentation: the mechanical Lagrangian, its chart instance and its dimensions); this is the isotropic oscillator instance. By Every potential presentation is hyperregular in its charts, with inverse branch $v = M^{- 1} p$ (or $G (q)^{- 1} p$ ) and the explicit kinetic-plus-potential Hamiltonian the branch Hamiltonian is

$H (x, p) = \frac{∣ p ∣^{2}}{2 m} + \frac{k ∣ x ∣^{2}}{2}, ω_{0} : = \sqrt{k / m} > 0,$

The stiffness and angular frequency have dimensions $[k] = μ τ^{- 2}$ and $[ω_{0}] = τ^{- 1}$ . The grouped phase coordinates are $z = (x^{1}, x^{2}, x^{3}, p_{1}, p_{2}, p_{3})$ , with $[x^{a}] = ℓ$ and $[p_{a}] = μ ℓ τ^{- 1}$ ; hence the six-dimensional phase-volume unit is $[ω^{\land 3} / 3!] = (μ ℓ^{2} τ^{- 1})^{3}$ , action cubed.

on the Cartesian phase domain $R^{6}$ , with the two-form $ω = \sum_{a = 1}^{3} d x^{a} \land d p_{a}$ (The canonical one-form and the two-form of a potential presentation: $λ = p \cdot d x$ on the Cartesian momentum phase chart and the induced forms on each generalized-coordinate chart, The two-form of a potential presentation is closed and nondegenerate, and each generalized-coordinate momentum chart carries the same symplectic structure: $Φ_{X}^{*} λ = \sum P_{a} d q^{a}$ and $Φ_{X}^{*} ω = \sum d q^{a} \land d P_{a}$ ) and the Hamiltonian field $X_{H} = (M^{- 1} p, - \nabla_{x} U)$ (The Hamiltonian field of a phase function for a potential presentation: the unique field $X_{f}$ with $ι_{X_{f}} ω = d f$ , and $X_{H} = (H_{p}, - H_{x})$ for the branch Hamiltonian, Cartesian model motions on the potential branch and declared generalized-coordinate Lagrange equations integrate their Hamiltonian fields; the forced Cartesian field is Hamiltonian exactly when the residual force has a velocity-independent potential). Then:

for every initial datum $(x, p)$ the curve

$x^{a} (t) = x^{a} \cos (ω_{0} t) + \frac{p_{a}}{m ω_{0}} \sin (ω_{0} t), p_{a} (t) = - m ω_{0} x^{a} \sin (ω_{0} t) + p_{a} \cos (ω_{0} t) (a = 1, 2, 3)$

solves the Hamiltonian system for all $t \in R$ ; 2. in the grouped order $z = (x, p)$ its derivative is $D Φ_{t} = (\begin{array}{cc} c I_{3} & (m ω_{0})^{- 1} s I_{3} \\ - m ω_{0} s I_{3} & c I_{3} \end{array}), c = \cos (ω_{0} t), s = \sin (ω_{0} t),$ and for $J_{g r} = (\begin{array}{cc} 0 & I_{3} \\ - I_{3} & 0 \end{array})$ direct block multiplication gives $D Φ_{t}^{T} J_{g r} D Φ_{t} = J_{g r}$ because $c^{2} + s^{2} = 1$ . If $T (x^{1}, x^{2}, x^{3}, p_{1}, p_{2}, p_{3}) = (x^{1}, p_{1}, x^{2}, p_{2}, x^{3}, p_{3})$ is the permutation to interleaved order, then $T D Φ_{t} T^{- 1} = diag (A, A, A)$ and $T J_{g r} T^{- 1} = diag (J_{2}, J_{2}, J_{2})$ , where $A = (\begin{array}{cc} c & (m ω_{0})^{- 1} s \\ - m ω_{0} s & c \end{array})$ ; each block satisfies $A^{T} J_{2} A = J_{2}$ and $\det A = 1$ . Therefore $\det D Φ_{t} = (\det A)^{3} = 1$ , so the time- $t$ map is canonical (The Hamiltonian evolution of a potential presentation preserves the two-form, the bracket and the determinant on its actual time-slice domains, also when the Hamiltonian depends on time, 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}$ ); 3. explicit volume check in the numeric coordinates measured in the declared SI units: the image of the unit square $[0, 1]^{2} \subseteq {(x^{1}, p_{1})}$ under $A$ is the parallelogram with area $∣ \det A ∣ = 1$ , and the image of the box $[0, 1]^{3} \times [0, 1]^{3}$ has numeric six-volume $∣ \det D Φ_{t} ∣ = 1$ , corresponding to physical phase-volume dimension action cubed; 4. the energy is constant along the flow, $H (x (t), p (t)) = H (x, p)$ , and ${H, H} = 0$ (Evolution of phase functions along the model's Hamiltonian solutions: $d f / d t = \partial_{t} f + {f, H}$ , the first-integral criterion, and the closed bracket algebra of autonomous first integrals clause 2).

All quantities are model values of the declared idealization; no measurement is reported.

Facts & Assumptions

Given: The one-label isotropic oscillator instance with its Hamiltonian, field, two-form and bracket, and the displayed curve $t \mapsto (x (t), p (t))$ .

[F1]

Model and Hamiltonian (Every potential presentation is hyperregular in its charts, with inverse branch $v = M^{- 1} p$ (or $G (q)^{- 1} p$ ) and the explicit kinetic-plus-potential Hamiltonian, The Hamiltonian of a hyperregular potential presentation: the Legendre transform of the mechanical Lagrangian, its domain and its dimensions, Potential presentations of a force model, potential and mechanical energy, closed versus exact force fields, local potentials and equipotential level sets, Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance, Configuration domain of $N$ labeled particles: open admissible sets, regular holonomic constraints and the mass operator, Dimensions and SI unit conventions of the non-relativistic classical mechanics framework): $H = ∣ p ∣^{2} / (2 m) + k ∣ x ∣^{2} / 2$ with $H_{p} = m^{- 1} p$ , $H_{x} = k x$ , and $U_{x} = k x$ ; $[k] = μ τ^{- 2}$ , $[ω_{0}] = τ^{- 1}$ , and $[ω^{\land 3} / 3!] = (μ ℓ^{2} τ^{- 1})^{3}$ ; the oscillator equation is $m x^{''} = - k x$ .

[F2]

Field, forms and canonicity (The canonical one-form and the two-form of a potential presentation: $λ = p \cdot d x$ on the Cartesian momentum phase chart and the induced forms on each generalized-coordinate chart, The two-form of a potential presentation is closed and nondegenerate, and each generalized-coordinate momentum chart carries the same symplectic structure: $Φ_{X}^{*} λ = \sum P_{a} d q^{a}$ and $Φ_{X}^{*} ω = \sum d q^{a} \land d P_{a}$ , The Hamiltonian field of a phase function for a potential presentation: the unique field $X_{f}$ with $ι_{X_{f}} ω = d f$ , and $X_{H} = (H_{p}, - H_{x})$ for the branch Hamiltonian, Cartesian model motions on the potential branch and declared generalized-coordinate Lagrange equations integrate their Hamiltonian fields; the forced Cartesian field is Hamiltonian exactly when the residual force has a velocity-independent potential, The Hamiltonian evolution of a potential presentation preserves the two-form, the bracket and the determinant on its actual time-slice domains, also when the Hamiltonian depends on time, 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}$ ): the Hamiltonian system is $\dot{x} = m^{- 1} p$ , $\dot{p} = - k x$ ; the two-form is $ω = \sum_{a} d x^{a} \land d p_{a}$ with standard matrix $J$ , and a $C^{1}$ map with $D C^{T} J D C = J$ is canonical with $∣ \det D C ∣ = 1$ .

[F3]

Sine and cosine calculus (The derivatives of sine and cosine are cosine and minus sine, The addition formulas for sine and cosine, Sine and cosine defined by their real power series, The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ , Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, Linear map between vector spaces over the same field, For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , $C^{k}$ Euclidean maps and diffeomorphisms): the derivatives of sine and cosine are known, $\sin^{2} + \cos^{2} = 1$ , and the displayed derivatives, products and determinants are computed by the ordinary rules.

[F4]

Evolution identity (Evolution of phase functions along the model's Hamiltonian solutions: $d f / d t = \partial_{t} f + {f, H}$ , the first-integral criterion, and the closed bracket algebra of autonomous first integrals, The Poisson bracket of phase functions of a potential presentation: ${f, g} = ω (X_{f}, X_{g})$ and the coordinate formula in each canonical chart): along any solution of the Hamiltonian system, $\frac{d}{d t} f (x (t), p (t)) = {f, H} (x (t), p (t))$ for autonomous $C^{1}$ functions, and autonomous functions whose bracket with $H$ vanishes identically are constant along solutions.

Verification

technique · direct. Differentiate the displayed formulas, verify the two block identities by matrix multiplication, evaluate the determinant and the constancy of the energy

1.1F1F2F3algebra

The curve solves the system: differentiating the displayed formula with the derivatives of [F3] gives ${\dot{x}}^{a} = - x^{a} ω_{0} \sin + \frac{p_{a}}{m} \cos = m^{- 1} p_{a} (t)$ and ${\dot{p}}_{a} = - m ω_{0}^{2} x^{a} \cos - ω_{0} p_{a} \sin = - k x^{a} (t)$ because $m ω_{0}^{2} = k$ ; by [F2] this is exactly the Hamiltonian system, which proves claim 1.

1.2F2F3algebra

Grouped-order canonical identity: with $c = \cos (ω_{0} t)$ and $s = \sin (ω_{0} t)$ , the derivative is $M_{t} = (\begin{array}{cc} c I_{3} & (m ω_{0})^{- 1} s I_{3} \\ - m ω_{0} s I_{3} & c I_{3} \end{array})$ and $J_{g r} = (\begin{array}{cc} 0 & I_{3} \\ - I_{3} & 0 \end{array})$ . Block multiplication gives $M_{t}^{T} J_{g r} M_{t} = (\begin{array}{cc} 0 & (c^{2} + s^{2}) I_{3} \\ - (c^{2} + s^{2}) I_{3} & 0 \end{array}) = J_{g r}$ . Under the declared permutation $T$ from grouped to interleaved order, $T M_{t} T^{- 1} = diag (A, A, A)$ , so $\det M_{t} = (\det A)^{3} = (c^{2} + s^{2})^{3} = 1$ . Thus the full six-dimensional derivative is canonical in the grouped coordinates and has unit determinant, proving claim 2.

2.1step 1.2F1F3F4algebra

Volume checks and energy: on each coordinate pair $(x^{a}, p_{a})$ the linear action is $A$ , so the unit square maps to the parallelogram spanned by its columns and has numeric area $∣ \det A ∣ = 1$ . The permutation $T$ in claim 2 identifies the grouped map with the product of these three pair maps; permutation does not change determinant, so the numeric six-volume of the unit box is $∣ \det D Φ_{t} ∣ = ∣ \det A ∣^{3} = 1$ , which is one unit of action cubed under the declared SI coordinate scales (claim 3). For the energy, [F4] and ${H, H} = 0$ give constancy of $H$ along the curve, and the direct computation $∣ p (t) ∣^{2} = m^{2} ω_{0}^{2} ∣ x ∣^{2} s^{2} - 2 m ω_{0} (x \cdot p) c s + ∣ p ∣^{2} c^{2}$ , $∣ x (t) ∣^{2} = ∣ x ∣^{2} c^{2} + \frac{2 (x \cdot p)}{m ω_{0}} c s + \frac{∣ p ∣^{2}}{m^{2} ω_{0}^{2}} s^{2}$ gives $H (x (t), p (t)) = \frac{∣ p ∣^{2}}{2 m} + \frac{k ∣ x ∣^{2}}{2} = H (x, p)$ after substituting $k = m ω_{0}^{2}$ , the mixed terms cancelling; this proves claim 4.

The isotropic oscillator of the model: explicit solution, the determinant and matrix tests on each two-dimensional block, and the area and energy checks

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources