TheoremStatement: AI-adaptedProof: 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.

Instability of spin about the intermediate principal axis of the torque-free top

Statement

Let $I_{1} < I_{2} < I_{3}$ be positive reals, let $I : R^{3} \to R^{3}$ be the linear map with $I e_{j} = I_{j} e_{j}$ on the standard orthonormal basis, and consider the torque-free Euler system $l^{'} = F (l)$ , $F (l) = l \times (I^{- 1} l)$ , on $U = R^{3}$ (Euler's equations $I ω^{'} + ω \times I ω = R^{T} τ$ under an adopted torque balance, and the torque-free invariants and principal-axis equations, Equilibria, Lyapunov stability and asymptotic stability of an autonomous first-order system). Let $L \neq 0$ . Then $l_{0} : = L e_{2}$ is an equilibrium of $F$ and is not Lyapunov stable: with $ε_{0} : = \frac{∣ L ∣}{2}, a : = \sqrt{\frac{1 / I_{1} - 1 / I_{2}}{1 / I_{2} - 1 / I_{3}}} > 0, c_{0} : = a (\frac{1}{I_{2}} - \frac{1}{I_{3}}) \frac{\sqrt{3}}{2} ∣ L ∣ > 0,$ for every $δ > 0$ there is a solution $l$ with $∥ l (0) - l_{0} ∥_{2} < δ$ and some $t \geq 0$ with $∥ l (t) - l_{0} ∥_{2} \geq ε_{0}$ ; Moreover, with $δ_{0} : = ∣ L ∣ / (2 \sqrt{1 + a^{2}})$ , the escape can be arranged at a time $t \leq c_{0}^{- 1} \log (δ_{0} / η)$ where $η = l_{1} (0) > 0$ may be chosen as small as desired.

Facts & Assumptions

Given: Positive reals $I_{1} < I_{2} < I_{3}$ , the diagonal map $I$ , the field $F (l) = l \times (I^{- 1} l)$ on $U = R^{3}$ , and $L \neq 0$ .

[L1]

The system $l^{'} = F (l)$ is read as First-order systems, initial value problems, and solutions on intervals. For $∥ x ∥_{2}, ∥ y ∥_{2} \leq r$ , bilinearity gives $F (x) - F (y) = (x - y) \times (I^{- 1} x) + y \times (I^{- 1} (x - y))$ ; since $I^{- 1}$ is diagonal with entries at most $1 / I_{1}$ in absolute value and $∥ u \times v ∥_{2} \leq ∥ u ∥_{2} ∥ v ∥_{2}$ , this yields $∥ F (x) - F (y) ∥_{2} \leq (2 r / I_{1}) ∥ x - y ∥_{2}$ . This bound makes $F$ locally Lipschitz in the state variable and also continuous at each state point by the $ε$ - $δ$ definition (Local Lipschitz continuity in the state variable, locally uniform in time and parameters, The cross product in $R^{3}$ , The squared cross-product norm is the Gram determinant of two vectors). Picard-Lindelof gives local existence and uniqueness, hence a unique maximal solution through every datum (Picard-Lindelöf local existence and uniqueness for first-order systems, Extensions, maximal solutions, maximal intervals, and global solutions, Every Picard–Lindelöf initial value problem has one maximal solution on an open interval); a solution trapped in a compact subset of $U = R^{3}$ near a finite endpoint extends past it (First-order systems, initial value problems, and solutions on intervals, A non-extendable solution leaves every compact subset of the domain near its finite endpoint; an autonomous solution trapped in a compact subset of its state domain cannot break down there).

[L2]

Along every solution the invariants $C (l) = ∥ l ∥_{2}^{2}$ and $E (l) = \frac{1}{2} ⟨ l, I^{- 1} l ⟩$ are constant; in the eigenbasis $I e_{j} = I_{j} e_{j}$ one has $C = \sum_{j} l_{j}^{2}$ , $E = \sum_{j} l_{j}^{2} / (2 I_{j})$ , and the component equations $l_{1}^{'} = (1 / I_{3} - 1 / I_{2}) l_{2} l_{3}$ , $l_{2}^{'} = (1 / I_{1} - 1 / I_{3}) l_{1} l_{3}$ , $l_{3}^{'} = (1 / I_{2} - 1 / I_{1}) l_{1} l_{2}$ The same algebra as in Euler's equations $I ω^{'} + ω \times I ω = R^{T} τ$ under an adopted torque balance, and the torque-free invariants and principal-axis equations applies directly to the present diagonal map: $I^{- 1}$ is symmetric, so $C' = 2 ⟨ l \times (I^{- 1} l), l ⟩ = 0$ and $E' = ⟨ l \times (I^{- 1} l), I^{- 1} l ⟩ = 0$ by cross-product orthogonality. Both scalar functions are continuous and differentiable on the solution interval; A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant therefore makes them constant there. These computations require only the given positive diagonal entries, and no realization as a mass-distribution inertia matrix.

[L3]

The Euler field is even: $F (- l) = (- l) \times (I^{- 1} (- l)) = F (l)$ , by bilinearity and linearity (The cross product in $R^{3}$ ). Put $σ : = L / ∣ L ∣ \in {- 1, 1}$ , so $σ^{2} = 1$ and $L = σ ∣ L ∣$ .

[L4]

The cross product is bilinear and $∥ u \times v ∥_{2} \leq ∥ u ∥_{2} ∥ v ∥_{2}$ ; the Euclidean inner product is positive definite The cross product in $R^{3}$ , 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}$ , Real and complex inner product spaces, with the inner product linear in the first argument.

[L5]

If $f : I \to R$ is differentiable on an interval with $f^{'} (t) \geq 0$ for all interior $t$ , then $f$ is nondecreasing; and the product rule $(g h)^{'} = g^{'} h + g h^{'}$ holds; $(e^{λ t})^{'} = λ e^{λ t}$ for real $λ$ On an interval $I$ , for $f$ continuous on $I$ and differentiable at every interior point: $f^{'} \geq 0$ throughout gives $f$ nondecreasing, $f^{'} > 0$ gives $f$ increasing, $f^{'} \leq 0$ and $f^{'} < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f^{'} \geq 0$ and a nonincreasing $f$ has $f^{'} \leq 0$ wherever it is differentiable, and no strict converse is claimed, 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, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , The exponential function is smooth and $(\exp)^{'} = \exp$ .

[L8]

For $r > 0$ , $\log r$ is the inverse value of the strictly increasing exponential: $\exp (\log r) = r$ (The natural logarithm as the inverse of the exponential function, The exponential is a continuous bijection from $R$ onto $(0, \infty)$ , The exponential function is strictly increasing).

[L6]

A closed bounded subset of $R^{3}$ is compact by Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, clause 2.

[L7]

The Euclidean norm satisfies the triangle inequality, so $∣ ∥ x ∥_{2} - ∥ y ∥_{2} ∣ \leq ∥ x - y ∥_{2}$ ; hence each sphere ${z : ∥ z ∥_{2} = r}$ is closed (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

Proof

technique · direct

1.1givenL1L3

$F (L e_{2}) = L e_{2} \times (L / I_{2}) e_{2} = 0$ , so $l_{0}$ is an equilibrium. Put $σ = L / ∣ L ∣$ as in [L3]. Choose the second and third coordinates of the initial datum with signs $σ$ and $- σ$ , respectively.

2.1step 1.1givenL2L3L4algebra

Let $0 < η_{0} < δ_{0} : = ∣ L ∣ / (2 \sqrt{1 + a^{2}})$ and let $0 < η < η_{0}$ . Put $s (η) : = \sqrt{∣ L ∣^{2} - (1 + a^{2}) η^{2}} > 0$ and $l^{η} : = (η, σ s (η), - σ a η)$ , so that $C (l^{η}) = L^{2}$ and $E (l^{η}) = L^{2} / (2 I_{2})$ : indeed $C (l^{η}) = η^{2} + ∣ L ∣^{2} - (1 + a^{2}) η^{2} + a^{2} η^{2} = L^{2}$ and $E (l^{η}) = \frac{1}{2} (η^{2} / I_{1} + (∣ L ∣^{2} - (1 + a^{2}) η^{2}) / I_{2} + a^{2} η^{2} / I_{3}) = \frac{1}{2} L^{2} / I_{2} + \frac{1}{2} η^{2} (1 / I_{1} - 1 / I_{2} - a^{2} (1 / I_{2} - 1 / I_{3})) = L^{2} / (2 I_{2})$ by the definition of $a$ . Also $∥ l^{η} - l_{0} ∥_{2} \to 0$ as $η ↓ 0$ , since $s (η) \to ∣ L ∣$ .

3.1step 2.1givenL1L2L4algebraL6L7

Let $l$ be the unique maximal solution with $l (0) = l^{η}$ ; it is defined for all $t \geq 0$ , because its invariant sphere $C = L^{2}$ is closed by [L7] and bounded, hence compact by Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, and [L1] rules out breakdown inside a compact set. Let $τ : = \inf {t > 0 : l_{1} (t) \geq δ_{0} or l_{1} (t) \leq 0}$ , so $0 < τ \leq + \infty$ , and on $(0, τ)$ one has $0 < l_{1} < δ_{0}$ . On that interval $l_{1} (t)^{2} + l_{3} (t)^{2} \leq l_{1}^{2} + a^{2} l_{1}^{2} < δ_{0}^{2} (1 + a^{2}) = L^{2} / 4$ by [L2] (which gives $l_{3} = \pm a l_{1}$ on the invariant level set $E = L^{2} / (2 I_{2})$ , since $E - C / (2 I_{2}) = 0$ and $(1 / I_{2} - 1 / I_{3}) > 0$ ), so $l_{2} (t)^{2} = L^{2} - l_{1}^{2} - l_{3}^{2} > 3 L^{2} / 4$ and $l_{2}$ has the constant sign $σ$ on $[0, τ)$ , its initial sign. Likewise $l_{3} = \pm a l_{1}$ cannot change sign on $[0, τ)$ without vanishing, which would force $l_{1} = l_{3} = 0$ contrary to $l_{1} > 0$ ; since $l_{3} (0) = - σ a η$ , one has $l_{3} (t) = - σ a l_{1} (t)$ there.

4.1step 3.1L2algebra

On $(0, τ)$ , the first component equation of [L2] and step 3.1 give $l_{1}^{'} = (1 / I_{3} - 1 / I_{2}) l_{2} l_{3} = a (1 / I_{2} - 1 / I_{3}) (σ l_{2}) l_{1} \geq c_{0} l_{1}$ with $c_{0} = a (1 / I_{2} - 1 / I_{3}) \frac{\sqrt{3}}{2} ∣ L ∣ > 0$ , because $σ l_{2} \geq \frac{\sqrt{3}}{2} ∣ L ∣$ .

5.1step 3.14.1givenL5L8algebra

By step 4.1 and the product and chain rules [L5], $(e^{- c_{0} t} l_{1} (t))^{'} = e^{- c_{0} t} (l_{1}^{'} (t) - c_{0} l_{1} (t)) \geq 0$ on $(0, τ)$ ; since $e^{- c_{0} t} l_{1} (t)$ is continuous on $[0, τ)$ , it is nondecreasing there by [L5], so $l_{1} (t) \geq η e^{c_{0} t}$ for $t \in [0, τ)$ . If $τ = + \infty$ , this would give $l_{1} (t) \geq η e^{c_{0} t} > δ_{0}$ for $t > c_{0}^{- 1} \log (δ_{0} / η)$ , contradicting $l_{1} < δ_{0}$ on $(0, τ)$ ; hence $τ < + \infty$ .

6.1step 3.15.1givenL4algebra

At the time $τ$ one has $l_{1} (τ) = δ_{0}$ : indeed $l_{1} (τ) \neq 0$ by step 5.1 and continuity, so by the definition of $τ$ and continuity it is the alternative $l_{1} (τ) \geq δ_{0}$ that occurs, and on $[0, τ]$ the bound $l_{1} < δ_{0}$ holds on $(0, τ)$ with $l_{1}$ continuous, so $l_{1} (τ) = δ_{0}$ ; moreover $τ \leq c_{0}^{- 1} \log (δ_{0} / η)$ . Therefore $∥ l (τ) - l_{0} ∥_{2}^{2} \geq l_{1} (τ)^{2} + l_{3} (τ)^{2} = (1 + a^{2}) δ_{0}^{2} = L^{2} / 4$ , so $∥ l (τ) - l_{0} ∥_{2} \geq ∣ L ∣ / 2 = ε_{0}$ .

7.1step 2.16.1givenalgebra∎

It remains to make the initial point as close to $l_{0}$ as prescribed: for any $δ > 0$ choose $η > 0$ with $η < \min {δ_{0}, δ}$ and $∥ l^{η} - l_{0} ∥_{2} < δ$ , possible because $∥ l^{η} - l_{0} ∥_{2} \to 0$ by step 2.1. The corresponding solution then has $∥ l (0) - l_{0} ∥_{2} < δ$ and, by step 6.1, escapes the ball of radius $ε_{0}$ at time $τ \leq c_{0}^{- 1} \log (δ_{0} / η)$ . This is instability of $l_{0}$ in the sense of Equilibria, Lyapunov stability and asymptotic stability of an autonomous first-order system, with the explicit time bound of the statement.

Instability of spin about the intermediate principal axis of the torque-free top

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources