ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generated

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.

Finite checks of the Euler-angle parametrization, the angular-velocity formula and a steady precession of the heavy top

Example

All data are the exact ones of the heavy-top system of The Euler-angle parametrization and the heavy symmetric top system with the parameter choice $A = C = m = d = g = 1$ , and the rotation matrices are those of The coordinate rotation matrices $R_{z} (a)$ and $R_{y} (a)$ : values in $S O (3)$ , composition law, and derivatives. Three computations are performed: the value of the Euler-angle parametrization at a specific triple, the body angular velocity of a specific motion through the formula of Angular velocity in Euler angles: $ω_{3} = ψ^{'} + φ^{'} \cos θ$ and $ω_{1}^{2} + ω_{2}^{2} = θ^{' 2} + φ^{' 2} \sin^{2} θ$ checked against the definition, and a constant-rate precession checked against every clause of Reduction of the heavy symmetric top system: conserved momenta, one-dimensional $θ$ equation and conserved reduced energy. No physical measurement is involved and no claim about a physical top is made.

Facts & Assumptions

Given: The parametrization $Θ (φ, θ, ψ) = R_{z} (φ) R_{y} (θ) R_{z} (ψ)$ , the matrices $R_{z} (a) = (\begin{array}{ccc} \cos a & - \sin a & 0 \\ \sin a & \cos a & 0 \\ 0 & 0 & 1 \end{array})$ and $R_{y} (a) = (\begin{array}{ccc} \cos a & 0 & \sin a \\ 0 & 1 & 0 \\ - \sin a & 0 & \cos a \end{array})$ , the angular-velocity formula of Angular velocity in Euler angles: $ω_{3} = ψ^{'} + φ^{'} \cos θ$ and $ω_{1}^{2} + ω_{2}^{2} = θ^{' 2} + φ^{' 2} \sin^{2} θ$ , and the reduction clauses 1-4 of Reduction of the heavy symmetric top system: conserved momenta, one-dimensional $θ$ equation and conserved reduced energy.

[L1]

$R_{z} (a), R_{y} (a) \in S O (3)$ ; $R_{z} (a) e_{1} = \cos a e_{1} + \sin a e_{2}$ , $R_{z} (a) e_{2} = - \sin a e_{1} + \cos a e_{2}$ , $R_{z} (a) e_{3} = e_{3}$ , $R_{y} (a) e_{1} = \cos a e_{1} - \sin a e_{3}$ , $R_{y} (a) e_{2} = e_{2}$ , $R_{y} (a) e_{3} = \sin a e_{1} + \cos a e_{3}$ ; and the derivative rules of The coordinate rotation matrices $R_{z} (a)$ and $R_{y} (a)$ : values in $S O (3)$ , composition law, and derivatives.

[L2]

The body angular velocity is the unique $ω$ with $R^{T} R^{'} = [ω]_{\times}$ , and $[ω]_{\times} z = ω \times z$ ; for the Euler-angle curve it equals $(- φ^{'} \sin θ \cos ψ + θ^{'} \sin ψ, φ^{'} \sin θ \sin ψ + θ^{'} \cos ψ, ψ^{'} + φ^{'} \cos θ)$ in the standard basis Angular velocity in Euler angles: $ω_{3} = ψ^{'} + φ^{'} \cos θ$ and $ω_{1}^{2} + ω_{2}^{2} = θ^{' 2} + φ^{' 2} \sin^{2} θ$ , Rigid placements, body and spatial angular velocity, and material velocities, The skew-matrix/cross-product correspondence $[ω]_{\times} z = ω \times z$ and its conjugation law $R [ω]_{\times} R^{T} = [R ω]_{\times}$ .

[L3]

For a heavy-top trajectory, $b = C (ψ^{'} + φ^{'} \cos θ)$ and $a = A φ^{'} \sin^{2} θ + b \cos θ$ are constant, $φ^{'} = (a - b \cos θ) / (A \sin^{2} θ)$ , $ψ^{'} = b / C - (a - b \cos θ) \cos θ / (A \sin^{2} θ)$ , the reduced energy $E = \frac{1}{2} A θ^{' 2} + (a - b \cos θ)^{2} / (2 A \sin^{2} θ) + b^{2} / (2 C) + m g d \cos θ$ is constant, and $A θ^{''} = - U^{'} (θ)$ with $U = (a - b \cos θ)^{2} / (2 A \sin^{2} θ) + b^{2} / (2 C) + m g d \cos θ$ Reduction of the heavy symmetric top system: conserved momenta, one-dimensional $θ$ equation and conserved reduced energy.

[L4]

With $π$ of Pi as twice the smallest positive zero of cosine, $\sin (π / 2) = 1$ and $\cos (π / 2) = 0$ by Quarter-turn values and shifts by pi/2 and pi. For $c = \cos (π / 3)$ , the addition formulas give $4 c^{3} - 3 c = \cos π = - 1$ , hence $(c + 1) (2 c - 1)^{2} = 0$ ; strict decrease of cosine on $[0, π]$ implies $c > - 1$ , so $c = 1 / 2$ . Positivity of sine on $(0, π)$ and $\sin^{2} + \cos^{2} = 1$ give $\sin (π / 3) = \sqrt{3} / 2$ (The addition formulas for sine and cosine, Signs, monotonicity intervals, and ranges of sine and cosine, Pi is the first positive zero of sine, Parity and the Pythagorean identity for sine and cosine).

[L5]

Matrix multiplication is entrywise-accumulating, so the product of displayed matrices can be read off entrywise, and $∥ \cdot ∥_{2}$ is the Euclidean norm 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}$ .

Verification

technique · direct

1.1givenL1L4L5algebra

Value of the parametrization: $Θ (0, \frac{π}{2}, 0) = R_{z} (0) R_{y} (\frac{π}{2}) R_{z} (0) = R_{y} (\frac{π}{2}) = (\begin{array}{ccc} 0 & 0 & 1 \\ 0 & 1 & 0 \\ - 1 & 0 & 0 \end{array})$ by [L4] and [L5]; its columns $(0, 0, - 1), (0, 1, 0), (1, 0, 0)$ are orthonormal and its determinant is $1$ (expansion along the second row), so the value lies in $S O (3)$ , as the parametrization guarantees.

1.2givenL1L2L4L5algebra

Angular-velocity check: take $φ (t) = t$ , $θ (t) = \frac{π}{2}$ , $ψ (t) = 0$ , so $R (t) = R_{z} (t) R_{y} (\frac{π}{2})$ . Then $R^{'} (t) = R_{z}^{'} (t) R_{y} (\frac{π}{2}) = R_{z} (t) [e_{3}]_{\times} R_{y} (\frac{π}{2})$ by [L1], hence $R (t)^{T} R^{'} (t) = R_{y} (\frac{π}{2})^{T} [e_{3}]_{\times} R_{y} (\frac{π}{2}) = [R_{y} (\frac{π}{2})^{T} e_{3}]_{\times} = [- e_{1}]_{\times}$ by the conjugation identity; so $ω = - e_{1}$ . The formula of [L2] with $φ^{'} = 1$ , $θ^{'} = ψ^{'} = 0$ , $\cos ψ = 1$ , $\sin ψ = 0$ gives $(- \sin \frac{π}{2}, 0, \cos \frac{π}{2}) = (- 1, 0, 0)$ , in agreement.

1.3givenL3L4algebra

Steady precession: put $θ (t) \equiv \frac{π}{3}$ , $φ (t) = 2 t$ , $ψ (t) = \frac{1}{2} t$ . Then $b = C (ψ^{'} + φ^{'} \cos θ) = \frac{1}{2} + 2 \cdot \frac{1}{2} = \frac{3}{2}$ and $a = A φ^{'} \sin^{2} θ + b \cos θ = 2 \cdot \frac{3}{4} + \frac{3}{2} \cdot \frac{1}{2} = \frac{9}{4}$ are constants, so the first and third system equations hold identically; and the second equation reads $\frac{d}{d t} (A θ^{'}) = 0 = A φ^{' 2} \sin θ \cos θ - C (ψ^{'} + φ^{'} \cos θ) φ^{'} \sin θ + m g d \sin θ$ , the right side being $4 \cdot \frac{\sqrt{3}}{2} \cdot \frac{1}{2} - \frac{3}{2} \cdot 2 \cdot \frac{\sqrt{3}}{2} + \frac{\sqrt{3}}{2} = \sqrt{3} - \frac{3 \sqrt{3}}{2} + \frac{\sqrt{3}}{2} = 0$ ; hence this is a heavy-top trajectory.

2.1step 1.3givenL3L5algebra∎

The reduction clauses at this trajectory: $φ^{'} = \frac{a - b \cos θ}{A \sin^{2} θ} = \frac{\frac{9}{4} - \frac{3}{4}}{\frac{3}{4}} = 2$ and $ψ^{'} = \frac{b}{C} - \frac{(a - b \cos θ) \cos θ}{A \sin^{2} θ} = \frac{3}{2} - \frac{\frac{3}{2} \cdot \frac{1}{2}}{\frac{3}{4}} = \frac{1}{2}$ , recovering the chosen rates; and $U^{'} (θ) = φ^{'} \sin θ (b - A φ^{'} \cos θ) - m g d \sin θ = 2 \cdot \frac{\sqrt{3}}{2} \cdot (\frac{3}{2} - 1) - \frac{\sqrt{3}}{2} = 0$ , consistent with the constant $θ$ . The reduced energy evaluates to $\frac{1}{2} A θ^{' 2} + \frac{(a - b \cos θ)^{2}}{2 A \sin^{2} θ} + \frac{b^{2}}{2 C} + m g d \cos θ = 0 + \frac{9 / 4}{3 / 2} + \frac{9 / 8}{+} \frac{1}{2} = \frac{3}{2} + \frac{9}{8} + \frac{1}{2} = \frac{25}{8}$ , and directly as $\frac{1}{2} A φ^{' 2} \sin^{2} θ + \frac{1}{2} C (ψ^{'} + φ^{'} \cos θ)^{2} + m g d \cos θ = \frac{1}{2} \cdot 4 \cdot \frac{3}{4} + \frac{1}{2} \cdot \frac{9}{4} + \frac{1}{2} = \frac{3}{2} + \frac{9}{8} + \frac{1}{2} = \frac{25}{8}$ ; both agree, as the reduction theorem requires.

Finite checks of the Euler-angle parametrization, the angular-velocity formula and a steady precession of the heavy top

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources