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.

Fundamental brackets and Bracket evolution on explicit one-label data: ${x^{a}, H} = p_{a} / m$ , ${p_{a}, H} = - U_{x^{a}}$ , and the oscillator check

Physical scope

A worked computation of the bracket of a declared one-label potential presentation: the fundamental brackets of the canonical coordinates, the bracket of the coordinates with the branch Hamiltonian reproducing velocity and force, and the evolution identity and energy constancy on the isotropic oscillator instance. 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 $I_{0} = R$ , configuration domain $Q = R^{3}$ , a $C^{2}$ potential $U : R \times Q \to R$ 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). 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 presentation is hyperregular on the Cartesian chart with $H (t, x, p) = \frac{1}{2} m^{- 1} ∣ p ∣^{2} + U (t, x)$ (The Hamiltonian of a hyperregular potential presentation: the Legendre transform of the mechanical Lagrangian, its domain and its dimensions), the two-form is $ω = \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 bracket is The Poisson bracket of phase functions of a potential presentation: ${f, g} = ω (X_{f}, X_{g})$ and the coordinate formula in each canonical chart. Then:

the canonical coordinates satisfy the fundamental brackets ${x^{a}, x^{b}} = 0$ , ${p_{a}, p_{b}} = 0$ and ${x^{a}, p_{b}} = δ_{b}^{a}$ for all $a, b \in {1, 2, 3}$ (The bracket of a potential presentation is bilinear, skew, a derivation in each slot, satisfies the Jacobi identity, and reproduces the fundamental brackets and the Hamiltonian field clause 5);
the brackets of the coordinates with the Hamiltonian recover the model's velocities and forces: ${x^{a}, H} = H_{p_{a}} = m^{- 1} p_{a}$ and ${p_{a}, H} = - H_{x^{a}} = - U_{x^{a}} (t, x)$ ; hence Hamilton's equations read ${\dot{x}}^{a} = {x^{a}, H}$ , ${\dot{p}}_{a} = {p_{a}, H}$ (The bracket of a potential presentation is bilinear, skew, a derivation in each slot, satisfies the Jacobi identity, and reproduces the fundamental brackets and the Hamiltonian field clause 4, 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 clause 1);
along every solution of the Hamiltonian system and for every $C^{1}$ phase function $f$ , $\frac{d}{d t} f (t, x (t), p (t)) = \partial_{t} f + {f, H}$ (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 1);
on the isotropic oscillator instance $U (x) = \frac{1}{2} k ∣ x ∣^{2}$ with $k > 0$ , one has ${p_{a}, H} = - k x^{a}$ and ${H, H} = 0$ , and every solution of the Hamiltonian system has constant $H = \frac{1}{2} m^{- 1} ∣ p ∣^{2} + \frac{1}{2} k ∣ x ∣^{2}$ on its domain, the Hamiltonian form of the model's energy conservation (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, 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).

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

Facts & Assumptions

Given: The one-label model with its potential, the branch Hamiltonian $H$ and the bracket of the presentation on the Cartesian chart.

[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 (t, x, p) = \frac{1}{2} m^{- 1} ∣ p ∣^{2} + U (t, x)$ with $H_{p} = m^{- 1} p$ and $H_{x} = \nabla_{x} U$ , and dimensions are read by the cited units item.

[F2]

Bracket, field and equations (The Poisson bracket of phase functions of a potential presentation: ${f, g} = ω (X_{f}, X_{g})$ and the coordinate formula in each canonical chart, 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, The bracket of a potential presentation is bilinear, skew, a derivation in each slot, satisfies the Jacobi identity, and reproduces the fundamental brackets and the Hamiltonian field, 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 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)$ ): ${f, g} = \sum_{a} (f_{x^{a}} g_{p_{a}} - f_{p_{a}} g_{x^{a}})$ , the coordinate functions satisfy the fundamental brackets, ${f, g} = X_{g} (f)$ , and a curve solves the Hamiltonian system exactly when it satisfies $\dot{x} = H_{p}$ , $\dot{p} = - H_{x}$ .

[F3]

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): along a solution, $\frac{d}{d t} f (t, z (t)) = \partial_{t} f (t, z (t)) + {f_{t}, H_{t}} (z (t))$ for every $C^{1}$ phase function $f$ ; autonomous functions whose bracket with $H$ vanishes identically are constant along solutions.

[F4]

Calculus (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, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , $C^{k}$ Euclidean maps and diffeomorphisms, The associated first-order system, motions, maximal motions and the Newtonian flow of a force model): coordinate functions have the displayed partial derivatives, $\nabla_{x} ∣ x ∣^{2} = 2 x$ and $\nabla_{p} ∣ p ∣^{2} = 2 p$ in the Euclidean product, and the oscillator equation is $m x^{''} = - \nabla_{x} U = - k x$ .

Verification

technique · direct. Evaluate the coordinate formula of the bracket on the coordinate functions and on the Hamiltonian, then apply the evolution identity to the oscillator instance

1.1F2F4algebra

Fundamental brackets: by [F2] the bracket of two coordinate functions is computed from their constant or linear derivatives; explicitly ${x^{a}, x^{b}} = \sum_{c} (δ_{c}^{a} \cdot 0 - 0 \cdot δ_{c}^{b}) = 0$ , ${p_{a}, p_{b}} = \sum_{c} (0 \cdot δ_{c}^{b} - δ_{a}^{c} \cdot 0) = 0$ and ${x^{a}, p_{b}} = \sum_{c} (δ_{c}^{a} δ_{b}^{c} - 0) = δ_{b}^{a}$ ; this is claim 1.

1.2F1F2algebra

Bracket with the Hamiltonian: by [F1] and [F2], ${x^{a}, H} = \sum_{b} (δ_{b}^{a} H_{p_{b}} - 0 \cdot H_{x^{b}}) = H_{p_{a}} = m^{- 1} p_{a}$ and ${p_{a}, H} = \sum_{b} (0 \cdot H_{p_{b}} - δ_{a}^{b} H_{x^{b}}) = - H_{x^{a}} = - U_{x^{a}} (t, x)$ , so the Hamilton equations ${\dot{x}}^{a} = H_{p_{a}}$ , ${\dot{p}}_{a} = - H_{x^{a}}$ read ${\dot{x}}^{a} = {x^{a}, H}$ , ${\dot{p}}_{a} = {p_{a}, H}$ ; this is claim 2.

2.1step 1.2F3F4algebra

Evolution and oscillator: [F3] gives claim 3 directly; for the oscillator instance [F4] gives ${p_{a}, H} = - k x^{a}$ and skew-symmetry of [F2] gives ${H, H} = 0$ , so by [F3] $H$ is constant along every solution, which is claim 4.

Fundamental brackets and Bracket evolution on explicit one-label data: ${x^{a}, H} = p_{a} / m$ , ${p_{a}, H} = - U_{x^{a}}$ , and the oscillator check

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources

Fundamental brackets and Bracket evolution on explicit one-label data: {xa,H}=pa/m{xa,H}=pa​/m, {pa,H}=−Uxa{pa​,H}=−Uxa​, and the oscillator check

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources

Fundamental brackets and Bracket evolution on explicit one-label data: ${x^{a}, H} = p_{a} / m$ , ${p_{a}, H} = - U_{x^{a}}$ , and the oscillator check