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.

Explicit escape from the intermediate-axis spin of the model with inertia diag(1,2,3): the constants, the perturbed invariant level, and the escape-time bound

Physical scope

A worked instance of the intermediate-axis instability of 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 on the declared model with body inertia matrix diag(1,2,3) and spin datum $l_{0} = e_{2}$ : the instability constants, a perturbed datum on the same invariant level with the checked proximity bound, and the resulting escape time and escape radius. The numerical data are declared model parameters; no measurement, no concrete body and no experiment is asserted.

Example

Use the numerical SI convention of 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: $t = T / (1 s)$ is dimensionless, inertia entries are in $1 k g m^{2}$ , and $l, L, q, δ_{0}, ε_{0}$ and all distances in angular-momentum space are numerical values in $1 k g m^{2} s^{- 1}$ . Restore the growth rate by $c_{0, p h y s} = c_{0} / (1 s)$ and the escape time by $T = t (1 s)$ ; $δ_{0} / q$ is dimensionless. The datum below is model data, not an observation.

Adopt the model A of 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: the rigid-material model of Adoption of the rigid-material model branch: reference mass distribution, rigid placements, orientation and scope with body inertia matrix $I = d i a g (1, 2, 3)$ in the declared orthonormal basis, 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). Its principal moments are $I_{1} = 1 < I_{2} = 2 < I_{3} = 3$ (Principal axes and principal moments of the inertia data of a rigid-material model, axis moments and extremal values clauses (a) and (d)). Take the intermediate-axis spin datum $l_{0} : = L e_{2}$ with $L = 1$ , and let $q : = \frac{1}{400}$ and $l^{q} : = (q, \sqrt{1 - 4 q^{2}}, - \sqrt{3} q),$ so that $q = 1 / 400$ and $\sqrt{1 - 4 q^{2}} = \sqrt{39999 / 40000}$ . Verify:

The instability constants of 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 clause 3.

$a = \sqrt{3}, c_{0} = \frac{1}{4}, δ_{0} = \frac{1}{4}, ε_{0} = \frac{1}{2} .$

The perturbed datum lies on the invariant level of the spin. $C (l^{q}) = C (l_{0}) = 1$ and $E (l^{q}) = E (l_{0}) = \frac{1}{4}$ , where $C (z) = ⟨ z, z ⟩$ and $E (z) = \frac{1}{2} ⟨ z, I^{- 1} z ⟩$ are the invariants of 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 clause 2.
The perturbed datum is close to the spin. $∥ l^{q} - l_{0} ∥_{2} < \frac{1}{100}$ and $q < \min {δ_{0}, \frac{1}{100}}$ .
The escape. There is a torque-free motion of model A whose $l$ -path has $l (0) = l^{q}$ and satisfies $∥ l (0) - e_{2} ∥_{2} < \frac{1}{100}, ∥ l (t) - e_{2} ∥_{2} \geq \frac{1}{2}$ at some time $0 \leq t \leq 4 \log 100 \approx 18.42$ ; in particular the intermediate-axis spin $e_{2}$ of model A is not Lyapunov stable, with an explicit effective escape at the displayed constants.

Facts & Assumptions

Given: The model A with $I = d i a g (1, 2, 3)$ and principal moments $I_{1} = 1 < I_{2} = 2 < I_{3} = 3$ , the spin datum $l_{0} = e_{2}$ , the number $q = 1 / 400$ and the datum $l^{q}$ of the statement.

[L1]

Model data: $I = d i a g (1, 2, 3)$ is symmetric positive definite in the declared basis, so model A is nondegenerate with the displayed principal moments (Inertia matrix, spatial inertia tensor, inertia tensor about a point and moment of inertia about an axis of a rigid-material model clause (a), Principal axes and principal moments of the inertia data of a rigid-material model, axis moments and extremal values clauses (a) and (d), Adoption of the rigid-material model branch: reference mass distribution, rigid placements, orientation and scope, 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).

[L2]

Instability statement: for a nondegenerate torque-free model with $I_{1} < I_{2} < I_{3}$ and $L \neq 0$ , the spin $L e_{2}$ is not Lyapunov stable, and with $a$ , $c_{0}$ , $δ_{0}$ , $ε_{0}$ as 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 clause 3, for every $δ > 0$ and every $q \in (0, \min {δ_{0}, δ})$ whose prescribed datum additionally satisfies $∥ l^{q} - L e_{2} ∥_{2} < δ$ , there is a torque-free motion with $∥ l (0) - L e_{2} ∥_{2} < δ$ and a time $t \leq c_{0}^{- 1} \log (δ_{0} / q)$ with $∥ l (t) - L e_{2} ∥_{2} \geq ε_{0}$ ; the motion's datum is the $l$ -path with $l (0) = l^{q}$ of the statement (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 clause 3).

[L3]

Invariants and global existence: $C$ and $E$ are constant along every solution of $l^{'} = l \times (I^{- 1} l)$ , which has a unique global maximal solution through every datum (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 and 4).

[L4]

Arithmetic: $\sqrt{3} \cdot \sqrt{3} = 3$ and the nonnegative square root is unique, $\sqrt{4} = 2$ , and for $0 \leq s \leq 1$ the elementary ordered-field inequalities used below hold; squares of nonnegative reals are ordered as their bases are (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, Dimensions and SI unit conventions of the non-relativistic classical mechanics framework).

Proof

technique · direct; compute the instability constants from the principal moments, check the invariants and the proximity of the perturbed datum by explicit arithmetic, and instantiate the escape statement

1.1givenL1L4algebra

With $I_{1} = 1$ , $I_{2} = 2$ , $I_{3} = 3$ and $L = 1$ : $1 / I_{1} - 1 / I_{2} = \frac{1}{2}$ , $1 / I_{2} - 1 / I_{3} = \frac{1}{6}$ , so $a^{2} = \frac{1 / 2}{1 / 6} = 3$ and $a = \sqrt{3} > 0$ by [L4]; then $c_{0} = a (1 / I_{2} - 1 / I_{3}) \frac{\sqrt{3}}{2} ∣ L ∣ = \sqrt{3} \cdot \frac{1}{6} \cdot \frac{\sqrt{3}}{2} = \frac{3}{12} = \frac{1}{4}$ by [L4]. Further $1 + a^{2} = 1 + 3 = 4$ , so $δ_{0} = \frac{∣ L ∣}{2 \sqrt{1 + a^{2}}} = \frac{1}{2 \cdot 2} = \frac{1}{4}$ by [L4] and $ε_{0} = \frac{∣ L ∣}{2} = \frac{1}{2}$ , which is claim 1.

2.1step 1.1givenL1L3L4algebra

Writing $s = \sqrt{1 - 4 q^{2}}$ , one has $s^{2} = 1 - 4 q^{2}$ ; hence $C (l^{q}) = q^{2} + s^{2} + 3 q^{2} = 4 q^{2} + 1 - 4 q^{2} = 1$ and $E (l^{q}) = \frac{1}{2} (q^{2} + \frac{s^{2}}{2} + \frac{3 q^{2}}{3}) = \frac{1}{2} (q^{2} + \frac{1 - 4 q^{2}}{2} + q^{2}) = \frac{1}{2} \cdot \frac{1}{2} = \frac{1}{4}$ by [L4]. For $l_{0} = e_{2}$ : $C (l_{0}) = 1$ and $E (l_{0}) = \frac{1}{2} ⟨ e_{2}, I^{- 1} e_{2} ⟩ = \frac{1}{2} \cdot \frac{1}{2} = \frac{1}{4}$ . This is claim 2, and by [L3] the perturbed datum and the spin datum lie on the same invariant level.

2.2step 1.1givenL4algebra

For the proximity bound: $∥ l^{q} - l_{0} ∥_{2}^{2} = q^{2} + (s - 1)^{2} + 3 q^{2} = 4 q^{2} + (1 - s)^{2}$ , and $1 - s = \frac{1 - s^{2}}{1 + s} = \frac{4 q^{2}}{1 + s} \leq 4 q^{2}$ because $s \geq 0$ ; with $q = \frac{1}{400}$ , $4 q^{2} = \frac{4}{160000} = \frac{1}{40000}$ and $(1 - s)^{2} \leq (4 q^{2})^{2} = \frac{16}{400^{4}} = \frac{1}{16 \cdot 10^{8}} < \frac{1}{10^{9}}$ , so $∥ l^{q} - l_{0} ∥_{2}^{2} \leq \frac{1}{40000} + \frac{1}{10^{9}} < \frac{1}{10000}$ , whence $∥ l^{q} - l_{0} ∥_{2} < \frac{1}{100}$ by [L4] applied to the nonnegative squares. Moreover $q = \frac{1}{400} < \frac{1}{100} = \min {δ_{0}, \frac{1}{100}}$ by step 1.1. This is claim 3.

3.1step 1.1step 2.2givenL2L3algebra∎

Apply clause 3 of 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 with $δ = \frac{1}{100}$ and $q = \frac{1}{400}$ , which is admissible by step 2.2 and [L2]: there is a torque-free motion of model A with $∥ l (0) - e_{2} ∥_{2} < \frac{1}{100}$ and a time $0 \leq t \leq c_{0}^{- 1} \log (δ_{0} / q)$ with $∥ l (t) - e_{2} ∥_{2} \geq ε_{0}$ . With the constants of step 1.1, $c_{0}^{- 1} \log (δ_{0} / q) = 4 \log (\frac{1 / 4}{1 / 400}) = 4 \log 100$ and $ε_{0} = \frac{1}{2}$ , so the escape-time bound and escape radius of claim 4 follow; by [L3] the motion's $l$ -path is defined for all times, so the escape time is finite as displayed.

Remarks

The escape is effective. The initial perturbation has $∥ l (0) - e_{2} ∥_{2} < 10^{- 2}$ while the escape radius is $\frac{1}{2}$ at a time at most $4 \log 100 \approx 18.421$ in the declared units; this is a quantitative instance of the statement that the intermediate-axis spin is not Lyapunov stable, not merely a linearized indication.
What is declared. The inertia matrix, the spin datum and the perturbation parameter $q$ are declared model data in the framework's units; no measurement is reported and no concrete body is asserted to have inertia $d i a g (1, 2, 3)$ .

Explicit escape from the intermediate-axis spin of the model with inertia diag(1,2,3): the constants, the perturbed invariant level, and the escape-time bound

Example

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources