CorollaryStatement: 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.

Principal axes and principal moments of the inertia matrix, and positivity in the nondegenerate case

Statement

Assume the Axiom of Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), used through Symmetry, the quadratic identity $ω^{T} I ω = \int ∥ ω \times ρ ∥_{2}^{2} d ν$ , and the positive-definiteness criterion for the inertia matrix to ensure finiteness of the inertia integrals. Let $ν$ be a mass distribution on $R^{3}$ with inertia matrix $I = I (ν)$ (Mass distributions on $R^{3}$ : total mass, first moment and inertia matrix), and write $I ω$ for the matrix-vector product and $⟨ \cdot, \cdot ⟩$ for the Euclidean inner product on $R^{3}$ (Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ). Then:

there is an orthonormal basis $(e_{1}, e_{2}, e_{3})$ of $R^{3}$ (Orthogonal vectors and subspaces, orthogonal and orthonormal sets, and orthonormal bases) and real numbers $I_{1}, I_{2}, I_{3}$ with $I e_{j} = I_{j} e_{j}$ for $j = 1, 2, 3$ ;
for any such basis and any $ω = \sum_{j} ω_{j} e_{j}$ one has $I ω = \sum_{j} I_{j} ω_{j} e_{j}$ , $I_{j} = e_{j}^{T} I e_{j}$ , and $ω^{T} I ω = \sum_{j} I_{j} ω_{j}^{2} = \int ∥ ω \times ρ ∥_{2}^{2} d ν (ρ) \geq 0$ ;
each $I_{j}$ vanishes exactly when $ν (R^{3} ∖ R e_{j}) = 0$ , that is, the whole mass lies on the line $R e_{j}$ ; if the inertia form is positive definite then every $I_{j} > 0$ and $I$ is invertible with $I^{- 1} e_{j} = I_{j}^{- 1} e_{j}$ ; and if $ν$ is not supported on any line through the origin, meaning that $ν (R^{3} ∖ R ω) > 0$ for every $ω \neq 0$ , then every $I_{j} > 0$ .

Facts & Assumptions

Given: A mass distribution $ν$ with inertia matrix $I$ , an orthonormal basis $(e_{1}, e_{2}, e_{3})$ of eigenvectors of $I$ with eigenvalues $I_{1}, I_{2}, I_{3}$ , and a vector $ω = \sum_{j} ω_{j} e_{j}$ .

[L1]

$I$ is symmetric and $ω^{T} I ω = \int ∥ ω \times ρ ∥_{2}^{2} d ν \geq 0$ ; for each $ω \neq 0$ , its quadratic form vanishes exactly when $ν (R^{3} ∖ R ω) = 0$ , and the associated bilinear form is positive definite exactly when $ν (R^{3} ∖ R ω) > 0$ for every $ω \neq 0$ , and then $I ω \neq 0$ for $ω \neq 0$ Symmetry, the quadratic identity $ω^{T} I ω = \int ∥ ω \times ρ ∥_{2}^{2} d ν$ , and the positive-definiteness criterion for the inertia matrix.

[L2]

The map $ω \mapsto I ω$ is self-adjoint with respect to the Euclidean inner product, because $⟨ I ω, z ⟩ = (I ω)^{T} z = ω^{T} I^{T} z = ω^{T} I z = ⟨ ω, I z ⟩$ by symmetry of $I$ and the product and transpose rules Symmetry, the quadratic identity $ω^{T} I ω = \int ∥ ω \times ρ ∥_{2}^{2} d ν$ , and the positive-definiteness criterion for the inertia matrix, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ .

[L3]

Every self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal basis of eigenvectors Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis, Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space; in an orthonormal basis, self-adjointness is symmetry of the matrix In an orthonormal basis, self-adjoint means conjugate-transpose symmetry and normal means commuting with the conjugate transpose.

[L4]

A linear map is determined by its values on a basis, and $I e_{j} = I_{j} e_{j}$ for the eigenbasis A finite list $v : n \to V$ is an ordered basis if and only if every $x \in V$ equals $\sum_{i < n} λ_{i} v_{i}$ for exactly one $λ : n \to F$ ; those scalars are the coordinates of $x$ in that ordered basis.

[L5]

A square matrix is invertible exactly when its nullspace is ${0}$ , and the inverse is unique Invertible matrix theorem: invertibility, full pivot rank, RREF $I$ , trivial nullspace and unique solvability are equivalent, Invertible matrices and the general linear group ${GL}_{n} (F)$ , Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes.

Proof

technique · direct

1.1givenL1L2

The map $T ω : = I ω$ is linear and, by [L1] and [L2], self-adjoint on the Euclidean space $R^{3}$ .

2.1step 1.1L3

Applying [L3] to $T$ produces an orthonormal basis $(e_{1}, e_{2}, e_{3})$ and reals $I_{j}$ with $I e_{j} = I_{j} e_{j}$ ; this is clause 1.

3.1step 2.1givenL1L4algebra

For $ω = \sum_{j} ω_{j} e_{j}$ , linearity of $T$ [L4] gives $I ω = \sum_{j} I_{j} ω_{j} e_{j}$ and hence $ω^{T} I ω = \sum_{j, k} ω_{j} ω_{k} I_{j} ⟨ e_{j}, e_{k} ⟩ = \sum_{j} I_{j} ω_{j}^{2}$ by orthonormality; setting $ω = e_{j}$ gives $I_{j} = e_{j}^{T} I e_{j} = \int ∥ e_{j} \times ρ ∥_{2}^{2} d ν$ by [L1], and the displayed chain of equalities of clause 2 follows.

4.1step 3.1L1algebra

Each $I_{j} = \int ∥ e_{j} \times ρ ∥_{2}^{2} d ν$ is nonnegative, and it is zero exactly when $ν (R^{3} ∖ R e_{j}) = 0$ , by [L1]; this is the vanishing criterion of clause 3.

4.2step 3.14.1givenL4L5algebra

If the inertia form is positive definite, then $I_{j} = e_{j}^{T} I e_{j} > 0$ for every $j$ ; moreover $I ω \neq 0$ for every $ω \neq 0$ by [L1], so the nullspace of $T$ is ${0}$ and $I$ is invertible with unique inverse by [L5]. Define $S$ on the basis by $S e_{j} : = I_{j}^{- 1} e_{j}$ and extend linearly; then $S I e_{j} = S e_{j} I_{j} = I_{j} \cdot I_{j}^{- 1} e_{j} = e_{j}$ and $I S e_{j} = I (I_{j}^{- 1} e_{j}) = I_{j}^{- 1} I e_{j} = e_{j}$ for every $j$ , so $S I = I S = I d$ by [L4], whence $S = I^{- 1}$ by uniqueness and $I^{- 1} e_{j} = I_{j}^{- 1} e_{j}$ .

5.1step 4.1givenalgebra∎

If $ν$ is not supported on any line through the origin, then for $e_{j} \neq 0$ $ν (R^{3} ∖ R e_{j}) > 0$ , so $I_{j} = \int ∥ e_{j} \times ρ ∥_{2}^{2} d ν > 0$ by step 4.1. This completes clause 3.

Principal axes and principal moments of the inertia matrix, and positivity in the nondegenerate case

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources