ExampleConstruction: AI-adaptedVerification: 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 torque-free spin results: stability certificates, an escape-time bound, and the linearized dichotomy

Example

Fix the diagonal inertia map with principal moments $(I_{1}, I_{2}, I_{3}) = (1, 2, 3)$ (Principal axes and principal moments of the inertia matrix, and positivity in the nondegenerate case) and the torque-free Euler system $l^{'} = l \times (I^{- 1} l)$ of Euler's equations $I ω^{'} + ω \times I ω = R^{T} τ$ under an adopted torque balance, and the torque-free invariants and principal-axis equations on $R^{3}$ . The three computations below check the certificates of Lyapunov stability of spin about the largest and smallest principal axes of the torque-free top, the escape bound of Instability of spin about the intermediate principal axis of the torque-free top, and the linearized formulas of Linearization of the torque-free Euler system at a principal-axis spin, and the oscillatory/exponential dichotomy at explicit data. The inertia values and component calculations are exact rationals or square roots; the escape-time upper bound is the exact expression $4 \log 25$ . No measurement or simulation is involved, and no claim about a physical top is made.

Facts & Assumptions

Given: The moments $(I_{1}, I_{2}, I_{3}) = (1, 2, 3)$ , the field $l^{'} = l \times (I^{- 1} l)$ , the certificates $D = C / (2 I_{1}) - E$ and $D_{3} = E - C / (2 I_{3})$ of the stability theorem, the constants $a, c_{0}, δ_{0}, ε_{0}$ of the instability theorem, and the linearization data of the linearized theorem.

[L1]

Along every solution $C = \sum_{j} l_{j}^{2}$ and $E = \sum_{j} l_{j}^{2} / (2 I_{j})$ are constant; the torque-free equations in components are $l_{1}^{'} = (1 / I_{3} - 1 / I_{2}) l_{2} l_{3}$ and cyclic analogues; and $l_{0} = L e_{j}$ is an equilibrium for $L \neq 0$ Euler's equations $I ω^{'} + ω \times I ω = R^{T} τ$ under an adopted torque balance, and the torque-free invariants and principal-axis equations.

[L2]

For the extreme axes: $D = \frac{1}{2} \sum_{j > 1} (1 / I_{1} - 1 / I_{j}) l_{j}^{2} \geq c (l_{2}^{2} + l_{3}^{2})$ with $c = \frac{1}{2} (1 / I_{1} - 1 / I_{2})$ , and $D_{3} = E - C / (2 I_{3}) = \frac{1}{2} \sum_{j < 3} (1 / I_{j} - 1 / I_{3}) l_{j}^{2} \geq c_{3} (l_{1}^{2} + l_{2}^{2})$ with $c_{3} = \frac{1}{2} (1 / I_{2} - 1 / I_{3})$ ; both $D$ and $D_{3}$ are constant along solutions Lyapunov stability of spin about the largest and smallest principal axes of the torque-free top.

[L3]

For the intermediate axis with $L > 0$ : $a = \sqrt{(1 / I_{1} - 1 / I_{2}) / (1 / I_{2} - 1 / I_{3})}$ , $c_{0} = a (1 / I_{2} - 1 / I_{3}) \frac{\sqrt{3}}{2} L$ , $δ_{0} = L / (2 \sqrt{1 + a^{2}})$ , $ε_{0} = L / 2$ ; the initial point $(η, \sqrt{L^{2} - (1 + a^{2}) η^{2}}, - a η)$ lies on the level set $C = L^{2}$ , $E = L^{2} / (2 I_{2})$ and its solution reaches $∥ l - l_{0} ∥_{2} \geq ε_{0}$ by time $\leq c_{0}^{- 1} \log (δ_{0} / η)$ Instability of spin about the intermediate principal axis of the torque-free top.

[L4]

For the spin $ω_{0} = Ω e_{3}$ the linearized system is $δ_{1}^{'} = Ω (I_{2} - I_{3}) δ_{2} / I_{1}$ , $δ_{2}^{'} = Ω (I_{3} - I_{1}) δ_{1} / I_{2}$ , $δ_{3}^{'} = 0$ , with $λ = Ω^{2} (I_{2} - I_{3}) (I_{3} - I_{1}) / (I_{1} I_{2})$ ; for $λ < 0$ , $κ = \sqrt{- λ}$ and the solution with data $(δ_{1} (0), δ_{2} (0))$ is $δ_{1} (t) = δ_{1} (0) \cos (κ t) + \frac{Ω (I_{2} - I_{3})}{I_{1} κ} δ_{2} (0) \sin (κ t)$ , $δ_{2} (t) = δ_{2} (0) \cos (κ t) + \frac{Ω (I_{3} - I_{1})}{I_{2} κ} δ_{1} (0) \sin (κ t)$ ; for $λ > 0$ the same with $\cosh, \sinh$ , and $δ_{2} (0) = 0 \neq δ_{1} (0)$ gives an unbounded solution Linearization of the torque-free Euler system at a principal-axis spin, and the oscillatory/exponential dichotomy, The six hyperbolic functions and their natural domains.

[L5]

$∥ ω \times ρ ∥_{2}^{2} = ∥ ω ∥_{2}^{2} ∥ ρ ∥_{2}^{2} - ⟨ ω, ρ ⟩^{2}$ and the Euclidean norm is computed componentwise The squared cross-product norm is the Gram determinant of two vectors, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , The cross product in $R^{3}$ ; $e^{κ t} \to + \infty$ for $κ > 0$ The exponential is a continuous bijection from $R$ onto $(0, \infty)$ .

Verification

technique · direct

1.1givenL2L3algebra

Certificates at $(1, 2, 3)$ : $c = \frac{1}{2} (1 - \frac{1}{2}) = \frac{1}{4}$ and $c_{3} = \frac{1}{2} (\frac{1}{2} - \frac{1}{3}) = \frac{1}{12}$ ; the instability data are $a = \sqrt{(1 - \frac{1}{2}) / (\frac{1}{2} - \frac{1}{3})} = \sqrt{3}$ , $1 + a^{2} = 4$ , $δ_{0} = \frac{1}{4}$ , $c_{0} = \sqrt{3} \cdot \frac{1}{6} \cdot \frac{\sqrt{3}}{2} = \frac{1}{4}$ and $ε_{0} = \frac{1}{2}$ for $L = 1$ .

2.1step 1.1givenL1L2L5algebra

Stability certificate check about $e_{3}$ with $L = 1$ and initial data $l (0) = \frac{1}{10} e_{1} + \frac{3 \sqrt{11}}{10} e_{3}$ on the unit sphere, where $\frac{3 \sqrt{11}}{10} = \sqrt{\frac{99}{100}}$ : $D_{3} (0) = \frac{1}{2} (1 / I_{1} - 1 / I_{3}) l_{1} (0)^{2} = \frac{1}{2} \cdot \frac{2}{3} \cdot \frac{1}{100} = \frac{1}{300}$ (the $l_{2}$ -term of $D_{3}$ vanishes at $t = 0$ ), so the bound $l_{1} (t)^{2} + l_{2} (t)^{2} \leq D_{3} (0) / c_{3} = \frac{12}{300} = \frac{1}{25}$ holds at all times by [L2]; moreover $C (0) = \frac{1}{100} + \frac{99}{100} = 1$ , so $l_{3} (t)^{2} = 1 - (l_{1}^{2} + l_{2}^{2}) \geq \frac{24}{25}$ , and since $l_{3}$ is continuous with $l_{3} (0) = \frac{3 \sqrt{11}}{10} > 0$ we have $l_{3} (t) \geq \sqrt{\frac{24}{25}} \geq \frac{97}{100}$ , whence $∣ l_{3} (t) - 1 ∣ = \frac{l_{1} (t)^{2} + l_{2} (t)^{2}}{1 + l_{3} (t)} \leq \frac{4}{197} < \frac{21}{1000}$ ; hence $∥ l (t) - e_{3} ∥_{2}^{2} \leq \frac{1}{25} + (\frac{21}{1000})^{2} = \frac{40441}{10^{6}} < \frac{41}{1000}$ for all $t \geq 0$ : the certificate inequality of [L2] is verified at explicit data, $e_{3}$ being the extreme axis of largest moment.

2.2step 1.1givenL1L3algebra

Instability check about $e_{2}$ with $L = 1$ and $η = \frac{1}{100}$ : with $a = \sqrt{3}$ the initial point is $l^{η} = (\frac{1}{100}, \frac{\sqrt{2499}}{50}, - \frac{\sqrt{3}}{100})$ , with $C (l^{η}) = \frac{1}{10^{4}} + \frac{2499}{2500} + \frac{3}{10^{4}} = 1$ and $E (l^{η}) = \frac{1}{2} (\frac{1}{10^{4}} + \frac{2499}{5000} + \frac{1}{10^{4}}) = \frac{1}{4} = \frac{L^{2}}{2 I_{2}}$ exactly, so it lies on the invariant level set of [L1] and [L3] requires no further hypothesis; the escape time is bounded by $c_{0}^{- 1} \log (δ_{0} / η) = 4 \log 25$ , and there is an escape time no later than this bound at which the solution is at distance at least $ε_{0} = \frac{1}{2}$ from $e_{2}$ .

2.3step 1.1givenL4L5algebra

Linearization check, first case: keep $(I_{1}, I_{2}, I_{3}) = (1, 2, 3)$ and take $Ω = 2$ , so $λ = 4 \cdot (2 - 3) (3 - 1) / (1 \cdot 2) = - 4$ and $κ = 2$ ; with data $(1, 0, 0)$ the formulas of [L4] give $δ_{1} = \cos 2 t$ , $δ_{2} = \sin 2 t$ , and indeed $δ_{1}^{'} = - 2 \sin 2 t = Ω (I_{2} - I_{3}) δ_{2} / I_{1} = - 2 \sin 2 t$ and $δ_{2}^{'} = 2 \cos 2 t = Ω (I_{3} - I_{1}) δ_{1} / I_{2} = 2 \cos 2 t$ : the solution is bounded, in the oscillatory branch, and $e_{3}$ is an extreme moment for these data.

3.1step 1.1givenL4L5algebra∎

Linearization check, second case: take $(I_{1}, I_{2}, I_{3}) = (1, 3, 2)$ , so $I_{3} = 2$ is the intermediate moment, and $Ω = 2$ : then $λ = 4 \cdot (3 - 2) (2 - 1) / (1 \cdot 3) = \frac{4}{3} > 0$ , $κ = \frac{2}{\sqrt{3}}$ , and the data $(1, 0, 0)$ give $δ_{1} (t) = \cosh (κ t)$ and $δ_{2} (t) = \frac{Ω (I_{3} - I_{1})}{I_{2} κ} \sinh (κ t) = \frac{2 \cdot 1}{3 κ} \sinh (κ t)$ , both unbounded as $t \to + \infty$ because $\cosh (κ t) \geq \frac{1}{2} e^{κ t}$ by [L5]; this exhibits the exponential branch of the dichotomy and the linearized instability of the intermediate axis.

Finite checks of the torque-free spin results: stability certificates, an escape-time bound, and the linearized dichotomy

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources