ExampleConstruction: AI-adaptedVerification: 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 free particle: the complete integral $S = q α - t α^{2} / (2 m)$ , its characteristics and its canonical labels

Example

Let $m > 0$ and let $H : R \times R \times R \to R$ , $H (t, q, p) : = p^{2} / (2 m)$ , be the free-particle Hamiltonian (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)$ ), and let $S : R \times R \times R \to R$ , $S (t, q, α) : = q α - t α^{2} / (2 m)$ . Then:

$S$ solves the Hamilton-Jacobi equation $S_{t} + H (t, q, S_{q}) = 0$ on $R^{3}$ and is a complete integral at every point, with $S_{q α} = 1$ (The Hamilton-Jacobi equation and a complete integral of it);
the Jacobi constants are $β : = S_{α} = q - t α / m$ , so the characteristics are $q (t) = β + t α / m$ with momentum $p = α$ ; these satisfy $q^{'} = p / m$ , $p^{'} = 0$ , and $β$ is constant along them (A complete integral produces Hamilton characteristics, the Jacobi constants, a local converse and canonical $(β, α)$ labels);
on $R^{3}$ at fixed $t$ one has $d q \land d p = d β \land d α$ : the pair $(β, α)$ is canonically conjugate to $(q, p)$ .

Facts & Assumptions

Given: The mass $m > 0$ , the free-particle Hamiltonian $H = p^{2} / (2 m)$ and the function $S = q α - t α^{2} / (2 m)$ on $R^{3}$ .

[F1]

Partial derivatives (Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ): $S_{t} = - α^{2} / (2 m)$ , $S_{q} = α$ , $S_{α} = q - t α / m$ , $S_{q α} = 1$ .

[F2]

Complete integral and characteristics (The Hamilton-Jacobi equation and a complete integral of it, A complete integral produces Hamilton characteristics, the Jacobi constants, a local converse and canonical $(β, α)$ labels): a $C^{3}$ function with $S_{t} + H (t, q, S_{q}) = 0$ and $\det S_{q α} \neq 0$ is a complete integral, and the characteristic equations $q^{'} = H_{p} (t, q, S_{q})$ , $p = S_{q}$ then satisfy Hamilton's equations, with $S_{α}$ constant.

[F3]

Two-form calculus (A phase domain, its canonical one-form and its standard symplectic two-form, The pullback of a differential form, The wedge product of differential forms): on a phase domain with coordinates $(q, p)$ the standard form is $d q \land d p$ , and $d β \land d α$ is computed from the differentials $d q, d α$ by bilinearity and alternation.

Verification

technique · direct; compute the derivatives, check the Hamilton-Jacobi equation and the characteristics, then compare the two two-forms

1.1F1F2algebra

By [F1], $S_{t} + H (t, q, S_{q}) = - α^{2} / (2 m) + α^{2} / (2 m) = 0$ on $R^{3}$ ; since $S_{q α} = 1 \neq 0$ , $S$ is a complete integral at every point by [F2], proving clause 1.

1.2F1F2algebra

Clause 2: by [F1], $β = S_{α} = q - t α / m$ , so for fixed $α$ and $β$ the characteristic curve is $q (t) = β + t α / m$ with $p (t) = S_{q} = α$ ; then $q^{'} = α / m = H_{p} (t, q, p)$ and $p^{'} = 0 = - H_{q}$ , and $β$ is constant along the curve by construction.

2.1F3step 1.2algebra∎

Clause 3: at fixed $t$ , $d β = d q - (t / m) d α$ and $d p = d α$ ; hence $d β \land d α = (d q - (t / m) d α) \land d α = d q \land d α = d q \land d p$ , since $d α \land d α = 0$ .

The free particle: the complete integral $S = q α - t α^{2} / (2 m)$ , its characteristics and its canonical labels

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources

The free particle: the complete integral S=qα−tα2/(2m)S=qα−tα2/(2m), its characteristics and its canonical labels

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources

The free particle: the complete integral $S = q α - t α^{2} / (2 m)$ , its characteristics and its canonical labels