ExampleConstruction: AI-generatedVerification: 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 point-mass inertia matrices computed and checked against the positivity criterion

Example

Throughout, the ambient data are the Euclidean inner product and cross product of $R^{3}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , The cross product in $R^{3}$ ), and $ν$ is a finite weighted sum of Dirac measures at distinct points $x_{1}, \dots, x_{n} \in R^{3}$ with weights $c_{1}, \dots, c_{n} > 0$ (The Dirac set function at a point, Nonnegative scalar multiples and countable weighted sums of measures are measures), which is a mass distribution of total mass $m = \sum_{k} c_{k}$ in the sense of Mass distributions on $R^{3}$ : total mass, first moment and inertia matrix; let $I = I (ν)$ be its inertia matrix. Assume the Axiom of Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), used only through the Borel measurability of the polynomial integrands, which is what makes the entries of $I$ finite real numbers (Finiteness of the moments of a bounded finite Borel measure on $R^{3}$ ). Three cases are computed and each is checked against the positivity criterion of Symmetry, the quadratic identity $ω^{T} I ω = \int ∥ ω \times ρ ∥_{2}^{2} d ν$ , and the positive-definiteness criterion for the inertia matrix and the principal-axis corollary Principal axes and principal moments of the inertia matrix, and positivity in the nondegenerate case.

(i) Two unit masses on the third axis. $n = 2$ , $x_{1} = e_{3}$ , $x_{2} = - e_{3}$ , $c_{1} = c_{2} = 1$ : then $m = 2$ , $μ (ν) = e_{3} - e_{3} = 0$ , and $I = d i a g (2, 2, 0)$ .

(ii) Three unit masses at an equilateral triangle in the plane $e_{3} = 0$ . $n = 3$ , $c_{k} = 1$ and $x_{k} = \cos (2 π k / 3) e_{1} + \sin (2 π k / 3) e_{2}$ for $k = 0, 1, 2$ : then $m = 3$ , $μ (ν) = 0$ and $I = d i a g (\frac{3}{2}, \frac{3}{2}, 3)$ .

(iii) Two unit masses on the first axis. $n = 2$ , $x_{1} = e_{1}$ , $x_{2} = 2 e_{1}$ , $c_{1} = c_{2} = 1$ : then $m = 2$ , $μ (ν) = 3 e_{1} \neq 0$ , and $I = d i a g (0, 5, 5)$ .

Facts & Assumptions

Given: Distinct points $x_{1}, \dots, x_{n} \in R^{3}$ , weights $c_{1}, \dots, c_{n} > 0$ , the measure $ν = \sum_{k = 1}^{n} c_{k} δ_{x_{k}}$ , and the three concrete data sets (i)-(iii).

[L1]

$ν$ is a measure, $ν (E) = \sum_{k = 1}^{n} c_{k} δ_{x_{k}} (E)$ for every measurable $E$ , and $ν ({x_{k}}) = c_{k}$ ; the inertia matrix is $I_{j k} = \int (∥ ρ ∥_{2}^{2} δ_{j k} - ρ_{j} ρ_{k}) d ν$ Nonnegative scalar multiples and countable weighted sums of measures are measures, Nonnegative scalar multiples and countable weighted sums of measures, The Dirac set function at a point, A Dirac set function is a probability measure, Mass distributions on $R^{3}$ : total mass, first moment and inertia matrix.

[L2]

For a finite-valued nonnegative measurable $f$ one has $\int f d ν = \sum_{k} c_{k} f (x_{k})$ ; for a real measurable $f$ that is bounded on the finite set ${x_{1}, \dots, x_{n}}$ and vanishes outside a bounded set, the same identity holds with $f = f^{+} - f^{-}$ and linearity of the integral The nonnegative Lebesgue integral, Nonnegative simple measurable functions, The integral of a nonnegative simple function, Integral over a measurable subset, Integrable real and complex functions, and their integrals, The Lebesgue integral is linear on $L^{1} (μ)$ , Monotonicity and nonnegative homogeneity of the nonnegative integral.

[L3]

$ω^{T} I ω = \int ∥ ω \times ρ ∥_{2}^{2} d ν$ , and $I$ is positive definite exactly when $ν (R^{3} ∖ R ω) > 0$ for every $ω \neq 0$ ; the eigenvalues of $I$ are its principal moments Symmetry, the quadratic identity $ω^{T} I ω = \int ∥ ω \times ρ ∥_{2}^{2} d ν$ , and the positive-definiteness criterion for the inertia matrix, Principal axes and principal moments of the inertia matrix, and positivity in the nondegenerate case.

[L4]

$∥ u \times v ∥_{2}^{2} = ∥ u ∥_{2}^{2} ∥ v ∥_{2}^{2} - ⟨ u, v ⟩^{2}$ 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}$ .

[L5]

Here $π$ is twice the smallest positive cosine zero (Pi as twice the smallest positive zero of cosine). The quarter-turn values, addition formulas and strict decrease of cosine on $[0, π]$ give $\cos (π / 3) = 1 / 2$ : writing $c = \cos (π / 3)$ , the triple-angle formula gives $4 c^{3} - 3 c = - 1$ , or $(c + 1) (2 c - 1)^{2} = 0$ , and $c > - 1$ . Positivity of sine on $(0, π)$ and the Pythagorean identity give $\sin (π / 3) = \sqrt{3} / 2$ ; the addition and shift formulas therefore give the points $(1, 0)$ , $(- 1 / 2, \sqrt{3} / 2)$ , $(- 1 / 2, - \sqrt{3} / 2)$ (Quarter-turn values and shifts by pi/2 and pi, Pi is the first positive zero of sine, Signs, monotonicity intervals, and ranges of sine and cosine). Finite sums are additive and distribute over scalar multiples; $\cos^{2} + \sin^{2} = 1$ , and $\sum_{k = 0}^{2} \cos (2 π k / 3) = \sum_{k = 0}^{2} \sin (2 π k / 3) = 0$ , $\sum_{k = 0}^{2} \cos^{2} (2 π k / 3) = \sum_{k = 0}^{2} \sin^{2} (2 π k / 3) = \frac{3}{2}$ , $\sum_{k} \cos (2 π k / 3) \sin (2 π k / 3) = 0$ Laws of finite sums and finite products, Parity and the Pythagorean identity for sine and cosine, The addition formulas for sine and cosine, Sine and cosine defined by their real power series.

[L6]

The matrices $d i a g (a, b, c)$ act by scaling components; $ρ ρ^{T}$ has entries $ρ_{i} ρ_{j}$ Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations.

Verification

technique · direct

1.1givenL1L2algebra

First the finite-atomic integration formula is recorded: if $s = \sum_{j} a_{j} χ_{E_{j}}$ is a nonnegative simple function, then $\int s d ν = \sum_{j} a_{j} ν (E_{j}) = \sum_{j} a_{j} \sum_{k : x_{k} \in E_{j}} c_{k} = \sum_{k} c_{k} s (x_{k})$ , and the identity $ν (E_{j}) = \sum_{k} c_{k} δ_{x_{k}} (E_{j})$ is [L1]; taking the supremum over simple $0 \leq s \leq f$ in the definition of the nonnegative integral gives $\int f d ν \geq \sum_{k} c_{k} f (x_{k})$ from the minorant $s_{0} : = \sum_{k} f (x_{k}) χ_{{x_{k}}} \leq f$ , and $\int f d ν \leq \sum_{k} c_{k} f (x_{k})$ from $\int s d ν = \sum_{k} c_{k} s (x_{k}) \leq \sum_{k} c_{k} f (x_{k})$ for every simple $0 \leq s \leq f$ ; hence $\int f d ν = \sum_{k} c_{k} f (x_{k})$ , and the real case follows by $f = f^{+} - f^{-}$ .

2.1step 1.1givenL1L6algebra

With the formula of step 1.1, $I_{j k} = \sum_{l} c_{l} (∥ x_{l} ∥_{2}^{2} δ_{j k} - (x_{l})_{j} (x_{l})_{k})$ for arbitrary data, by [L1]; in particular $I$ is the sum over the atoms of $c_{l} (∥ x_{l} ∥_{2}^{2} I_{3} - x_{l} x_{l}^{T})$ [L6].

2.2step 1.12.1givenL5L6algebra

Case (ii): $μ (ν) = \sum_{k} x_{k} = 0$ and $\sum_{k} (x_{k})_{1}^{2} = \frac{3}{2}$ , $\sum_{k} (x_{k})_{2}^{2} = \frac{3}{2}$ , $\sum_{k} (x_{k})_{3}^{2} = 0$ , $\sum_{k} (x_{k})_{1} (x_{k})_{2} = 0$ , $\sum_{k} (x_{k})_{1} (x_{k})_{3} = \sum_{k} (x_{k})_{2} (x_{k})_{3} = 0$ by [L5]; hence $I_{11} = \sum_{k} ((x_{k})_{2}^{2} + (x_{k})_{3}^{2}) = \frac{3}{2}$ , $I_{22} = \sum_{k} ((x_{k})_{1}^{2} + (x_{k})_{3}^{2}) = \frac{3}{2}$ , $I_{33} = \sum_{k} ((x_{k})_{1}^{2} + (x_{k})_{2}^{2}) = 3$ and the off-diagonal entries vanish, so $I = d i a g (\frac{3}{2}, \frac{3}{2}, 3)$ by steps 1.1 and 2.1.

3.1step 1.12.1givenL3L6algebra

Case (i): $I = (1 \cdot (I_{3} - e_{3} e_{3}^{T})) + (1 \cdot (I_{3} - e_{3} e_{3}^{T})) = 2 (I_{3} - e_{3} e_{3}^{T}) = d i a g (2, 2, 0)$ by step 2.1 and [L6], and the moment vanishes by symmetry; for $ω = e_{3}$ the line $R e_{3}$ contains both atoms, so $ν (R^{3} ∖ R e_{3}) = 0$ , so $I$ is not positive definite by [L3], matching the zero eigenvalue.

3.2step 2.2givenL3L4L5algebra

Case (ii) checked against the quadratic identity: for $ω = e_{1}$ , $\sum_{k} ∥ e_{1} \times x_{k} ∥_{2}^{2} = \sum_{k} (1 - (x_{k})_{1}^{2}) = 3 - \frac{3}{2} = \frac{3}{2} = ω^{T} I ω$ , and for $ω = e_{3}$ , $\sum_{k} ∥ e_{3} \times x_{k} ∥_{2}^{2} = \sum_{k} ((x_{k})_{1}^{2} + (x_{k})_{2}^{2}) = 3$ ; both agree with $I = d i a g (\frac{3}{2}, \frac{3}{2}, 3)$ , and no line through the origin contains all three $x_{k}$ , so for every $ω \neq 0$ at most two of the three points satisfy $ω \times x_{k} = 0$ , at least one atom of weight $1$ lies off $R ω$ , so $ν (R^{3} ∖ R ω) \geq 1 > 0$ ; by [L3] and [L4] this is exactly positive definiteness of $I$ , matching the positive eigenvalues.

4.1step 1.12.1givenL3L6algebra∎

Case (iii): $I = (I_{3} - e_{1} e_{1}^{T}) + (4 I_{3} - 4 e_{1} e_{1}^{T}) = 5 I_{3} - 5 e_{1} e_{1}^{T} = d i a g (0, 5, 5)$ by steps 2.1 and [L6]; the support lies on the line $R e_{1}$ , which is the zero set of $ω \mapsto ω \times ρ$ for $ω = e_{1}$ , and the complement of that line has $ν$ -measure $0$ , so $I$ is not positive definite by [L3], matching the zero eigenvalue; the first moment is $μ (ν) = e_{1} + 2 e_{1} = 3 e_{1} \neq 0$ , so this distribution is not centred and its inertia matrix is computed about the origin of coordinates, not about its centre of mass. This last observation is a bookkeeping check, not a claim about any translated inertia matrix.

Finite point-mass inertia matrices computed and checked against the positivity criterion

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources