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.

Lyapunov stability of spin about the largest and smallest principal axes of the torque-free top

Statement

Let $I_{1} < I_{2} < I_{3}$ be positive reals and let $I : R^{3} \to R^{3}$ be the linear map with $I e_{j} = I_{j} e_{j}$ on the standard orthonormal basis $(e_{1}, e_{2}, e_{3})$ of $R^{3}$ . Consider the autonomous first-order system $l^{'} (t) = F (l (t)), F (l) : = l \times (I^{- 1} l),$ on $U : = R^{3}$ , read as in Equilibria, Lyapunov stability and asymptotic stability of an autonomous first-order system with the cross product of The cross product in $R^{3}$ and $I^{- 1}$ the inverse of $I$ (Principal axes and principal moments of the inertia matrix, and positivity in the nondegenerate case); this is the torque-free Euler system of Euler's equations $I ω^{'} + ω \times I ω = R^{T} τ$ under an adopted torque balance, and the torque-free invariants and principal-axis equations in angular-momentum variables. Let $L \neq 0$ . Then:

$L e_{1}$ and $L e_{3}$ are equilibria of $F$ and each is Lyapunov stable in the sense of Equilibria, Lyapunov stability and asymptotic stability of an autonomous first-order system: for $j = 1$ and $j = 3$ and for every $ε > 0$ there is $δ \in (0, ε]$ such that every maximal solution $l$ with $∥ l (0) - L e_{j} ∥_{2} < δ$ is defined for all $t \geq 0$ and satisfies $∥ l (t) - L e_{j} ∥_{2} < ε$ for every $t \geq 0$ .

Facts & Assumptions

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

[L1]

The system $z^{'} = F (z)$ on the open set $U = R^{3}$ is read as First-order systems, initial value problems, and solutions on intervals with $D = R \times U$ ; $L e_{1}$ and $L e_{3}$ are equilibria exactly when $F (L e_{j}) = 0$ , and then Lyapunov stability is the quantified ball statement of Equilibria, Lyapunov stability and asymptotic stability of an autonomous first-order system.

[L2]

The cross product is bilinear and alternating and satisfies $∥ u \times v ∥_{2} \leq ∥ u ∥_{2} ∥ v ∥_{2}$ 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}$ .

[L3]

$F$ is locally Lipschitz in the state variable in the sense of Local Lipschitz continuity in the state variable, locally uniform in time and parameters. 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))$ [L2]. Since $I^{- 1}$ is diagonal with entries at most $1 / I_{1}$ in absolute value, $∥ I^{- 1} z ∥_{2} \leq ∥ z ∥_{2} / I_{1}$ ; hence $∥ F (x) - F (y) ∥_{2} \leq (2 r / I_{1}) ∥ x - y ∥_{2}$ . A compact time-state cylinder is a compact subset of Euclidean $R^{4}$ , hence bounded by Heine-Borel (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); choosing $r$ to contain its state projection gives the finite Lipschitz constant required by the definition. The same local estimate gives continuity of $F$ at each state point by the $ε$ - $δ$ definition. Picard-Lindelof therefore applies to the initial value problem of the system Picard-Lindelöf local existence and uniqueness for first-order systems; every datum has a unique maximal solution on an open interval, and every other solution through that datum is a restriction (Extensions, maximal solutions, maximal intervals, and global solutions, Every Picard–Lindelöf initial value problem has one maximal solution on an open interval).

[L4]

Along every solution of $l^{'} = l \times (I^{- 1} l)$ the quantities $C (l) = ⟨ l, l ⟩$ and $E (l) = \frac{1}{2} ⟨ l, I^{- 1} l ⟩$ are constant; for $l = \sum_{j} l_{j} e_{j}$ they equal $\sum_{j} l_{j}^{2}$ and $\sum_{j} l_{j}^{2} / (2 I_{j})$ 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.

[L5]

Any solution of an autonomous system on $U = R^{3}$ that is trapped near a finite endpoint in a compact subset of $U$ extends past that endpoint: the no-extension hypothesis of 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 fails under such trapping.

[L6]

The Euclidean inner product is bilinear and positive definite, so $⟨ u, u ⟩ = ∥ u ∥_{2}^{2}$ and $u \neq 0$ implies $∥ u ∥_{2} > 0$ Real and complex inner product spaces, with the inner product linear in the first argument, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ .

[L7]

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.

[L8]

The Euclidean norm satisfies the triangle inequality, so $∣ ∥ x ∥_{2} - ∥ y ∥_{2} ∣ \leq ∥ x - y ∥_{2}$ ; hence the norm is continuous and 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.1givenL1L2L3

By antisymmetry of the cross product, $F (L e_{1}) = L e_{1} \times (L / I_{1}) e_{1} = 0$ and $F (L e_{3}) = L e_{3} \times (L / I_{3}) e_{3} = 0$ , so $L e_{1}$ and $L e_{3}$ are equilibria; and [L3] supplies the existence, uniqueness and continuation theory for the system.

1.2givenL2L4L6L7L8

Let $l$ be the maximal solution with prescribed datum at $0$ . By [L4] the numbers $C (l (t)) = ∥ l (t) ∥_{2}^{2} = ∥ l (0) ∥_{2}^{2}$ and $E (l (t))$ are constant, so the values of $l$ lie in the sphere ${z : ∥ z ∥_{2} = ∥ l (0) ∥_{2}} \subseteq U$ . This sphere is closed by [L8] 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.

1.3givenL4algebra

Define, for $l = \sum_{j} l_{j} e_{j}$ , the quantity $D (l) : = C (l) / (2 I_{1}) - E (l) = \frac{1}{2} \sum_{j > 1} (1 / I_{1} - 1 / I_{j}) l_{j}^{2}$ . Since $1 / I_{1} - 1 / I_{j} \geq 1 / I_{1} - 1 / I_{2}$ for $j = 2, 3$ by $I_{2} < I_{3}$ and $I_{1} < I_{2}$ , one has $D (l) \geq c (l_{2}^{2} + l_{3}^{2})$ with $c : = \frac{1}{2} (1 / I_{1} - 1 / I_{2}) > 0$ .

2.1step 1.2givenL5

Every maximal solution of the system is defined for all $t \geq 0$ : if a solution were defined on $[0, b)$ with $0 < b < + \infty$ and admitted no extension past $b$ , then by step 1.2 it would be trapped in the compact subset ${z : ∥ z ∥_{2} = ∥ l (0) ∥_{2}}$ of $U$ near $b$ , and [L5] would give an extension past $b$ , a contradiction.

3.1step 2.1step 1.3givenL4L6algebra

Let $ε > 0$ and let $c, κ : = 1 / \sqrt{2 I_{1} c}$ be as in step 1.3; choose $δ > 0$ satisfying the finite list of conditions $δ \leq ε$ , $κ^{2} δ^{2} \leq ε^{2} / 4$ , $κ^{2} δ^{2} \leq ∣ L ∣^{2} / 4$ , $δ \leq ∣ L ∣ / 4$ and $δ (2 ∣ L ∣ + δ) + κ^{2} δ^{2} \leq ∣ L ∣ ε / 2$ ; such a $δ$ exists because each condition only bounds $δ$ from above by a positive number. Let $l$ be the maximal solution with $∥ l (0) - L e_{1} ∥_{2} < δ$ , defined for all $t \geq 0$ by step 2.1. Then $l_{2} (0)^{2} + l_{3} (0)^{2} \leq ∥ l (0) - L e_{1} ∥_{2}^{2} < δ^{2}$ and, by [L4] and step 1.3 evaluated at $t = 0$ , for every $t \geq 0$ $l_{2} (t)^{2} + l_{3} (t)^{2} \leq \frac{D (l (t))}{c} = \frac{D (l (0))}{c} \leq \frac{l_{2} (0)^{2} + l_{3} (0)^{2}}{2 I_{1} c} < κ^{2} δ^{2} \leq \frac{ε^{2}}{4} .$

4.1step 3.1givenL4L6algebra

With the data of step 3.1: $l_{1} (t)^{2} = C (l (0)) - l_{2} (t)^{2} - l_{3} (t)^{2} \geq (∣ L ∣ - δ)^{2} - κ^{2} δ^{2} \geq ∣ L ∣^{2} / 4$ by $δ \leq ∣ L ∣ / 4$ and $κ^{2} δ^{2} \leq ∣ L ∣^{2} / 4$ , so $∣ l_{1} (t) ∣ \geq ∣ L ∣ / 2$ and $l_{1}$ has the sign of $L$ (it is continuous, $∣ l_{1} ∣ \geq ∣ L ∣ / 2$ throughout, and $∣ l_{1} (0) - L ∣ < δ \leq ∣ L ∣ / 4$ ). Hence $∣ l_{1} (t) + L ∣ \geq 3 ∣ L ∣ / 2$ and $∣ l_{1} (t) - L ∣ = \frac{∣ l_{1} (t)^{2} - L^{2} ∣}{∣ l_{1} (t) + L ∣} \leq \frac{∣ C (l (0)) - L^{2} ∣ + l_{2} (t)^{2} + l_{3} (t)^{2}}{3 ∣ L ∣ / 2} \leq \frac{δ (2 ∣ L ∣ + δ) + κ^{2} δ^{2}}{3 ∣ L ∣ / 2} \leq \frac{ε}{3} .$

5.1step 2.1step 3.1step 4.1givenL1algebra

Combining steps 3.1 and 4.1, $∥ l (t) - L e_{1} ∥_{2}^{2} = (l_{1} (t) - L)^{2} + l_{2} (t)^{2} + l_{3} (t)^{2} < \frac{ε^{2}}{9} + \frac{ε^{2}}{4} < ε^{2}$ for all $t \geq 0$ ; since for every $ε > 0$ such a $δ$ was produced and every maximal solution starting in $B_{δ} (L e_{1})$ is defined for all $t \geq 0$ by step 2.1, $L e_{1}$ is Lyapunov stable in the sense of [L1].

6.1step 1.3step 3.1step 4.1step 5.1givenL4algebra∎

The same argument with the roles of $e_{1}$ and $e_{3}$ exchanged uses $D_{3} (l) : = E (l) - C (l) / (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}) > 0$ , and $D_{3} (l) \leq (l_{1}^{2} + l_{2}^{2}) / (2 I_{1})$ . Set $κ_{3} : = 1 / \sqrt{2 I_{1} c_{3}}$ ; the same positive $δ$ conditions of step 3.1, with $κ_{3}$ in place of $κ$ , bound $l_{1} (t)^{2} + l_{2} (t)^{2} < κ_{3}^{2} δ^{2}$ . The norm invariant then gives $∣ l_{3} (t) ∣ \geq ∣ L ∣ / 2$ with the sign of $L$ , and the calculation of step 4.1 gives $∣ l_{3} (t) - L ∣ \leq ε / 3$ ; the certificate $D_{3}$ is constant along solutions by [L4], so the argument of steps 1.3, 2.1, 3.1, 5.1 and 4.1 applies verbatim to $L e_{3}$ and proves its Lyapunov stability.

Lyapunov stability of spin about the largest and smallest principal axes of the torque-free top

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources