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.

Two explicit free-rotation models checked: principal-axis spins, a non-uniform symmetric-top motion with its invariants, and the linearized frequencies of an asymmetric top

Physical scope

Worked checks inside the torque-free branch of the rigid-material model of Adoption of the rigid-material model branch: reference mass distribution, rigid placements, orientation and scope on the declared time window $I_{0} = R$ for both models and two declared inertia matrices: a symmetric model with body inertia matrix diag(1,1,2) and an asymmetric model with diag(1,2,3). The checks verify principal-axis spins and their invariants, an explicit non-uniform symmetric-top motion with conserved angular momentum and energy, and the linearized frequencies at the principal-axis spins of the asymmetric model. No measured value, no concrete body and no experiment is asserted; the numerical data are declared model parameters under the explicit numerical SI convention dimensionless t = T / (one second) in the Example.

Example

Numerical SI convention. Let $T$ denote physical elapsed time and fix $T_{*} = 1 s$ , $M_{*} = 1 k g$ and $D_{*} = 1 m$ . Below $t : = T / T_{*}$ is dimensionless and all quantities are numerical SI values: inertia is divided by $M_{*} D_{*}^{2}$ , angular velocity and its perturbations by $T_{*}^{- 1}$ , angular momentum by $M_{*} D_{*}^{2} / T_{*}$ , and energy by $M_{*} D_{*}^{2} / T_{*}^{2}$ . Primes differentiate with respect to $t$ . Restore physical angular velocity by $ω_{p h y s} (T) = ω (T / T_{*}) / T_{*}$ and angular momentum by $l_{p h y s} (T) = (M_{*} D_{*}^{2} / T_{*}) l (T / T_{*})$ . The displayed numerical rates $1$ , $2$ , $1 / \sqrt{3}$ mean physical rates $1 / T_{*}$ , $2 / T_{*}$ , $1 / (\sqrt{3} T_{*})$ ; $λ_{j}$ is restored by $λ_{j, p h y s} = λ_{j} / T_{*}^{2}$ . Thus $\cos t$ , $\sin t$ , $\cos (t / \sqrt{3})$ and the hyperbolic functions have dimensionless arguments; $t = π / 2$ means $T = π T_{*} / 2$ . For the reconstructed motion use $x_{p h y s} (T, ρ_{p h y s}) = D_{*} x (T / T_{*}, ρ_{p h y s} / D_{*})$ ; the chain rule restores $R_{p h y s}^{T} d R_{p h y s} / d T = [ω_{p h y s}]_{\times}$ and the dimensioned torque-free equation. This convention uses Dimensions and SI unit conventions of the non-relativistic classical mechanics framework and reports no measurement.

Assume the Axiom of Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), inherited for finite mass moments and inertial integrals through the rigid-material and torque-balance suppliers, and for the double-cover surjectivity used in the quaternion constructions below. Consider two declared models of the rigid-material branch Adoption of the rigid-material model branch: reference mass distribution, rigid placements, orientation and scope, each with body inertia matrix diagonal in the declared positively oriented orthonormal basis $(e_{1}, e_{2}, e_{3})$ and no other inertia data, each with time window $I_{0} = R$ (equivalently all physical times $T \in R$ ), each used in the torque-free branch of Adoption of the external-torque branch of the rigid-material model: declared torque data and the balance of angular momentum about the centre of mass clause (iv):

Model S (symmetric): $I = d i a g (1, 1, 2)$ in kilogram metres squared in the declared units (Dimensions and SI unit conventions of the non-relativistic classical mechanics framework); the principal moments are $I_{1} = I_{2} = 1$ , $I_{3} = 2$ .
Model A (asymmetric): $I = d i a g (1, 2, 3)$ ; the principal moments are $I_{1} = 1 < I_{2} = 2 < I_{3} = 3$ .

Verify the following.

Principal-axis spins. For each model, each $j$ and each $Ω \in R$ , the constant path $ω \equiv Ω e_{j}$ is the body angular velocity of a torque-free motion; along it $l = Ω I_{j} e_{j}$ is constant, $C = Ω^{2} I_{j}^{2}$ and $E = \frac{1}{2} Ω^{2} I_{j}$ . In Model S with $j = 3$ and $Ω = 2$ this gives $l = 4 e_{3}$ , $C = 16$ , $E = 4$ ; in Model A with $j = 1$ and $Ω = 1$ it gives $l = e_{1}$ , $C = 1$ , $E = \frac{1}{2}$ .
A non-uniform symmetric-top motion. For Model S the path $ω (t) = (\frac{1}{2} \cos t, \frac{1}{2} \sin t, 1) (t \in R)$ satisfies the torque-free Euler equations $l^{'} = l \times (I^{- 1} l)$ and is the body angular velocity of a torque-free motion of Model S; along it $l (t) = (\frac{1}{2} \cos t, \frac{1}{2} \sin t, 2), C = \frac{17}{4}, E = \frac{9}{8}, ∥ ω (t) ∥_{2}^{2} = \frac{5}{4},$ and $ω$ is not constant: $ω (\frac{π}{2}) - ω (0) = (- \frac{1}{2}, \frac{1}{2}, 0)$ .
Linearization of Model A at its principal-axis spins. At the spin $Ω e_{1}$ with $Ω = 1$ the linearized system of Linearization of the torque-free spin of the rigid-material model at a principal-axis spin: the oscillatory/exponential dichotomy and linear stability has $λ_{1} = - \frac{1}{3}$ , $κ_{1} = 1 / \sqrt{3}$ , and the pair $(δ_{2}, δ_{3}) = (\cos (t / \sqrt{3}), - \frac{1}{\sqrt{3}} \sin (t / \sqrt{3}))$ solves the transverse equations; at the intermediate spin $e_{2}$ with $Ω = 1$ the linearized system has $λ_{2} = \frac{1}{3} > 0$ and the solution with $δ_{1} (0) = 1$ , $δ_{3} (0) = 0$ has $δ_{1} (t) = \cosh (t / \sqrt{3})$ , which is unbounded on $[0, \infty)$ ; at the extreme spin $e_{3}$ with $Ω = 1$ one has $κ_{3} = 1$ .

Facts & Assumptions

Given: The two models S and A of the Example with time window $I_{0} = R$ and their declared diagonal inertia matrices, the torque-free branch, and the data $j$ , $Ω$ of each claim.

[L1]

Model data and nondegeneracy: for each model the body inertia matrix $I = \int (∥ ρ ∥_{2}^{2} I_{3} - ρ ρ^{T}) d ν$ is diagonal with the displayed positive entries in the declared basis, and the model is nondegenerate (Inertia matrix, spatial inertia tensor, inertia tensor about a point and moment of inertia about an axis of a rigid-material model clauses (a) and (d)-(e), Principal axes and principal moments of the inertia data of a rigid-material model, axis moments and extremal values clauses (a) and (d), The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[L2]

Principal-axis spins: for a nondegenerate torque-free model, every axis $j$ , rate $Ω$ and initial orientation there is a torque-free motion with constant body angular velocity $Ω e_{j}$ , and along the motions $l = Ω I_{j} e_{j}$ , $C = Ω^{2} I_{j}^{2}$ , $E = \frac{1}{2} Ω^{2} I_{j}$ (Principal-axis uniform rotations of the torque-free rigid-material model: existence, a fixed spatial direction, the invariants, and the converse classification clauses 1-3).

[L3]

Torque-free equations and invariants: $L_{c} = R l$ , and $l = I ω$ satisfies $l^{'} = l \times (I^{- 1} l)$ , and $⟨ l, l ⟩$ and $\frac{1}{2} ⟨ l, I^{- 1} l ⟩$ are constant along solutions; the latter is $E = \frac{1}{2} ω^{T} I ω$ (Torque-free motion of the rigid-material model: conservation of the angular momentum about the centre of mass, the energy-momentum invariants, the principal-axis equations and global existence of the spin dynamics clauses 2-3, Euler's equations with torque for the rigid-material model, the rotational power identity, the torque-free reduction and frame covariance clause 4).

[L4]

Realisability: for every continuous $ω : R \to R^{3}$ there is a $C^{2}$ rotation path with body angular velocity $ω$ if $ω$ is $C^{1}$ ; and a $C^{2}$ rotation path with any prescribed initial orientation exists by the surjectivity of the quaternion cover (The quaternion lift of a prescribed continuous angular velocity: $q^{'} = \frac{1}{2} q φ (ω (t))$ keeps $S^{3}$ invariant, its rotation path has body angular velocity $ω$ , and the initial value problem has a unique solution on the whole interval clauses 1-2, The quaternion rotation map $ρ$ : conjugation on the imaginary quaternions, the unit sphere $S^{3}$ , and quaternion lifts and its second remark).

[L5]

Linearization: the derivative of the torque-free spin field at $Ω e_{j}$ and the dichotomy with $λ_{j} = Ω^{2} (I_{a} - I_{j}) (I_{j} - I_{b}) / (I_{a} I_{b})$ and $κ_{j} = \sqrt{∣ λ_{j} ∣}$ , with the explicit $\cos, \sin$ and $\cosh, \sinh$ solutions (Linearization of the torque-free spin of the rigid-material model at a principal-axis spin: the oscillatory/exponential dichotomy and linear stability clauses 1-2).

[L6]

Calculus: $(\sin)^{'} = \cos$ , $(\cos)^{'} = - \sin$ , $(\sinh)^{'} = \cosh$ , $(\cosh)^{'} = \sinh$ , the sum, product and chain rules, $\sin^{2} + \cos^{2} = 1$ , and $\cosh t \geq 1$ with $\cosh t \to + \infty$ ; cross products are bilinear and alternating (The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine, The addition formulas for sine and cosine, The six hyperbolic functions and their natural domains, Addition formulas, identities, parity, and derivatives of the hyperbolic functions, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, The cross product is bilinear, alternating, and orthogonal to both factors, The cross product in $R^{3}$ ).

[L7]

Quarter-turn values: $π = 2 γ > 0$ for the smallest positive cosine zero $γ$ , and $\sin (π / 2) = 1$ , $\cos (π / 2) = 0$ (Pi as twice the smallest positive zero of cosine, Cosine has a smallest positive zero, lying strictly between zero and two, Quarter-turn values and shifts by pi/2 and pi); square roots denote unique nonnegative roots (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

Proof

technique · direct; instantiate the general statements on the declared diagonal data and check the displayed formulas by differentiation and expansion

1.1givenL1L2algebra

By [L2] applied to each model, each $j$ and each $Ω$ there is a torque-free motion with constant body angular velocity $Ω e_{j}$ , and $l = Ω I_{j} e_{j}$ , $C = Ω^{2} I_{j}^{2}$ , $E = \frac{1}{2} Ω^{2} I_{j}$ along it; for Model S with $I_{3} = 2$ , $j = 3$ , $Ω = 2$ this gives $l = 4 e_{3}$ , $C = (2 \cdot 2)^{2} = 16$ , $E = \frac{1}{2} \cdot 4 \cdot 2 = 4$ , and for Model A with $I_{1} = 1$ , $j = 1$ , $Ω = 1$ it gives $l = e_{1}$ , $C = 1$ , $E = \frac{1}{2}$ , which is claim 1.

1.2givenL1L3L6algebra

For the path $ω$ of claim 2 in Model S, $l = I ω = (\frac{1}{2} \cos t, \frac{1}{2} \sin t, 2)$ by [L1], so $l^{'} = (- \frac{1}{2} \sin t, \frac{1}{2} \cos t, 0)$ by [L6], while $l \times (I^{- 1} l) = l \times (\frac{1}{2} \cos t, \frac{1}{2} \sin t, 1)$ has components $(\frac{1}{2} \sin t \cdot 1 - 2 \cdot \frac{1}{2} \sin t, - (\frac{1}{2} \cos t \cdot 1 - 2 \cdot \frac{1}{2} \cos t), \frac{1}{2} \cos t \cdot \frac{1}{2} \sin t - \frac{1}{2} \sin t \cdot \frac{1}{2} \cos t) = (- \frac{1}{2} \sin t, \frac{1}{2} \cos t, 0)$ by the coordinate formula for the cross product in [L6]; hence $l^{'} = l \times (I^{- 1} l)$ , so $l$ solves the torque-free equations and $ω$ satisfies the Euler equations by [L3].

1.3givenL5L6algebra

For claim 3, [L5] gives $λ_{j} = Ω^{2} (I_{a} - I_{j}) (I_{j} - I_{b}) / (I_{a} I_{b})$ ; for Model A and $j = 1$ , with $a = 2$ , $b = 3$ : $λ_{1} = \frac{(2 - 1) (1 - 3)}{2 \cdot 3} = - \frac{1}{3}$ and $κ_{1} = 1 / \sqrt{3}$ ; for $j = 2$ , with the cyclic choice $a = 3$ , $b = 1$ : $λ_{2} = \frac{(3 - 2) (2 - 1)}{3 \cdot 1} = \frac{1}{3}$ and $κ_{2} = 1 / \sqrt{3}$ ; for $j = 3$ , with $a = 1$ , $b = 2$ : $λ_{3} = \frac{(1 - 3) (3 - 2)}{1 \cdot 2} = - 1$ and $κ_{3} = 1$ . In the first case the linearized field of [L5] satisfies $A e_{2} = - \frac{1}{3} e_{3}$ and $A e_{3} = e_{2}$ , and the pair $δ_{2} (t) = \cos (t / \sqrt{3})$ , $δ_{3} (t) = - \frac{1}{\sqrt{3}} \sin (t / \sqrt{3})$ satisfies $δ_{2}^{'} = δ_{3}$ and $δ_{3}^{'} = - \frac{1}{3} δ_{2}$ by [L6], so it solves the transverse linearized equations.

2.1step 1.2givenL1L6L7algebra

The quantities of claim 2: $∥ ω (t) ∥_{2}^{2} = \frac{1}{4} \cos^{2} t + \frac{1}{4} \sin^{2} t + 1 = \frac{1}{4} + 1 = \frac{5}{4}$ and $C = ⟨ l, l ⟩ = \frac{1}{4} \cos^{2} t + \frac{1}{4} \sin^{2} t + 4 = \frac{17}{4}$ by the Pythagorean identity in [L6]; and $E = \frac{1}{2} ω^{T} I ω = \frac{1}{2} (\frac{1}{4} \cos^{2} t + \frac{1}{4} \sin^{2} t + 2 \cdot 1) = \frac{1}{2} (\frac{1}{4} + 2) = \frac{9}{8}$ . The difference $ω (\frac{π}{2}) - ω (0) = (- \frac{1}{2}, \frac{1}{2}, 0) \neq 0$ has norm $\frac{\sqrt{2}}{2}$ , so $ω$ is not constant.

3.1step 1.2step 2.1givenL3L4L6

Since $ω$ is $C^{\infty}$ , hence $C^{1}$ , [L4] supplies a $C^{1}$ rotation path $R : R \to S O (3)$ with body angular velocity $ω$ and any prescribed initial orientation; then $R^{'} = R [ω]_{\times}$ is $C^{1}$ , so $R$ is of class $C^{2}$ , and $x : I_{0} \times R^{3} \to R^{3}$ , $x (t, ρ) : = R (t) ρ$ (that is, $c \equiv 0$ ), is a motion of Model S on its declared window $I_{0} = R$ by Adoption of the rigid-material model branch: reference mass distribution, rigid placements, orientation and scope clause (ii) with body angular velocity $ω$ and $l$ as in step 1.2. Its balance holds: $L_{c} = R l$ by [L3], so $(R l)^{'} = R^{'} l + R l^{'} = R (ω \times l + l^{'}) = 0$ because $l^{'} = l \times (I^{- 1} l) = l \times ω = - ω \times l$ from step 1.2 and the alternation of the cross product in [L6]; hence the motion is torque-free and realizes claim 2.

4.1step 1.3givenL5L6algebra∎

In the intermediate case $j = 2$ , the same formulas give $A e_{1} = - \frac{1}{3} e_{3}$ and $A e_{3} = - e_{1}$ , so the transverse system is $δ_{1}^{'} = - δ_{3}$ , $δ_{3}^{'} = - \frac{1}{3} δ_{1}$ ; with $δ_{1} (0) = 1$ , $δ_{3} (0) = 0$ the $\cosh, \sinh$ solution of [L5] is $δ_{1} (t) = \cosh (t / \sqrt{3})$ , $δ_{3} (t) = - \frac{1}{\sqrt{3}} \sinh (t / \sqrt{3})$ , and $δ_{1}$ is unbounded on $[0, \infty)$ by [L6]; hence the linearized system at the intermediate spin of Model A has an unbounded solution, which is claim 3.

Remarks

The two models are declared, not measured. The matrices $d i a g (1, 1, 2)$ and $d i a g (1, 2, 3)$ are model parameters in the declared units; no body is asserted to have these principal moments and no measurement is reported.
What the checks exhibit. Claim 2 exhibits a torque-free motion whose body angular velocity is not constant while both invariants and the spatial angular momentum are constant; claim 3 exhibits the oscillatory and the exponentially growing linearized behaviour on explicit data. The nonlinear consequences of the latter are proved in Nonlinear stability of the torque-free spin of the rigid-material model about an extreme principal axis, and instability about the intermediate axis, with an explicit escape time and the orientation caveat and instantiated on the companion page.

Two explicit free-rotation models checked: principal-axis spins, a non-uniform symmetric-top motion with its invariants, and the linearized frequencies of an asymmetric top

Example

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources