ExampleConstruction: AI-generatedVerification: AI-generatedprecheck 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.

Parallel-axis check for the equilateral-triangle model: inertia tensor about a vertex computed two ways

Physical scope

A worked instance of the parallel-axis theorem in the rigid-material model branch of Adoption of the rigid-material model branch: reference mass distribution, rigid placements, orientation and scope: for the equilateral-triangle model of the companion example, the inertia tensor of the model about a vertex is computed from the supplier's shifted-point formula and independently from the finite sum defining it, and the two agree; the axis moment about the vertex axis is compared with the central axis moment. The item asserts no measured inertia and no concrete physical body.

Example

Adopt the equilateral-triangle rigid-material model of An equilateral-triangle rigid-material model: inertia matrix, principal axes, rotational term and the threefold-symmetry check: three equal point masses $m_{0} > 0$ at $x_{k} = a (\cos \frac{2 π k}{3}, \sin \frac{2 π k}{3}, 0)$ , $k = 0, 1, 2$ , with total mass $m = 3 m_{0}$ , body inertia matrix $I = d i a g (\frac{3 m_{0} a^{2}}{2}, \frac{3 m_{0} a^{2}}{2}, 3 m_{0} a^{2})$ and reference coordinates centred at the origin. The kilogram/metre input conventions and kilogram metres squared inertia units are inherited from the companion example. Then:

for every motion of the model, every $t \in I_{0}$ and every spatial point $p$ , the inertia tensor of the model about $p$ satisfies the spatial parallel-axis form $I (t, p) = I (t) + m (∥ p - c (t) ∥_{2}^{2} I_{3} - (p - c (t)) (p - c (t))^{T});$
at any reference-placement time $t_{*} \in I_{0}$ satisfying $(c (t_{*}), R (t_{*})) = (0, I_{3})$ , the inertia tensor about the vertex $p = a e_{1}$ is $I (t_{*}, a e_{1}) = d i a g (\frac{3 m_{0} a^{2}}{2}, \frac{9 m_{0} a^{2}}{2}, 6 m_{0} a^{2});$
the same matrix is obtained by the direct finite sum over the three material points, confirming the identity of clause 1 on this data;
the moment of inertia about the axis through the vertex $a e_{1}$ in direction $e_{3}$ equals $6 m_{0} a^{2}$ , while the moment about the parallel central axis is $3 m_{0} a^{2}$ ; their difference is $m a^{2}$ , in agreement with the axis-shift form of the theorem.

Facts & Assumptions

Given: The model of An equilateral-triangle rigid-material model: inertia matrix, principal axes, rotational term and the threefold-symmetry check, its reference mass distribution $ν$ , its total mass $m = 3 m_{0}$ , its body inertia matrix $I$ , a motion $x (t, ρ) = c (t) + R (t) ρ$ of the model, a spatial point $p$ , and the notation of Inertia matrix, spatial inertia tensor, inertia tensor about a point and moment of inertia about an axis of a rigid-material model and The inertia tensor of a finite bounded Borel measure about any point of $R^{3}$ . For clauses 2-4, assume a time $t_{*} \in I_{0}$ with $c (t_{*}) = 0$ , $R (t_{*}) = I_{3}$ . Such motions exist on every allowed time window (take the constant reference placement); an arbitrary motion need not attain it, and $0$ need not lie in $I_{0}$ .

[L1]

The companion-model data (An equilateral-triangle rigid-material model: inertia matrix, principal axes, rotational term and the threefold-symmetry check): $ν = m_{0} \sum_{k} δ_{x_{k}}$ is a centred mass distribution of total mass $m = 3 m_{0}$ , its body inertia matrix is $I = d i a g (\frac{3 m_{0} a^{2}}{2}, \frac{3 m_{0} a^{2}}{2}, 3 m_{0} a^{2})$ and the finite-atomic formula $\int f d ν = m_{0} \sum_{k} f (x_{k})$ holds for $ν$ -integrable $f$ .

[L2]

Mathematical supplier, parallel axis (Parallel-axis theorem: the inertia tensor about a displaced point of a centred mass distribution, The inertia tensor of a finite bounded Borel measure about any point of $R^{3}$ , Finiteness and a uniform bound for the entries of the inertia tensor about an arbitrary point, Mass distributions on $R^{3}$ : total mass, first moment and inertia matrix, The Axiom of Countable Choice ( ${A C}_{ω}$ )): under ${A C}_{ω}$ , for a centred mass distribution with total mass $m$ and inertia matrix $I$ , and for every $a \in R^{3}$ , the inertia tensor of the distribution about $a$ satisfies $I_{ν} (a) = I + m (∥ a ∥_{2}^{2} I_{3} - a a^{T})$ .

[L3]

The model's shifted tensor (Inertia matrix, spatial inertia tensor, inertia tensor about a point and moment of inertia about an axis of a rigid-material model clause (c)): for a spatial point $p$ , $I (t, p) = R (t) I_{ν} (a (t, p)) R (t)^{T}$ with $a (t, p) = R (t)^{T} (p - c (t))$ .

[L4]

Rotation and matrix algebra (The orthogonal group $O (3)$ and the rotation group $S O (3)$ , The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations, Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes): $R \in S O (3)$ preserves the Euclidean inner product and norm; for the product $R a (t, p) = p - c (t)$ one has $∥ a (t, p) ∥_{2} = ∥ p - c (t) ∥_{2}$ and $R (a a^{T}) R^{T} = (R a) (R a)^{T}$ .

[L5]

Finite sums and trigonometric values (Laws of finite sums and finite products, Sine and cosine defined by their real power series, The addition formulas for sine and cosine, Parity and the Pythagorean identity for sine and cosine): $\cos (0) = 1$ , $\cos (\pm \frac{2 π}{3}) = - \frac{1}{2}$ and $\sin (\pm \frac{2 π}{3}) = \pm \frac{\sqrt{3}}{2}$ ; finite sums are additive and distribute over scalar multiples.

Verification

technique · direct; conjugate the supplier's shifted-point formula into the spatial frame, then evaluate both sides of the identity on the triangle data

1.1givenL2L3L4algebra

Spatial parallel-axis form: by [L3] and [L2], $I (t, p) = R (t) [I + m (∥ a (t, p) ∥_{2}^{2} I_{3} - a (t, p) a (t, p)^{T})] R (t)^{T} = I (t) + m (∥ a ∥_{2}^{2} I_{3} - R a (R a)^{T}),$ distributing the conjugation and using [L4]; substituting $R a = p - c (t)$ and $∥ a ∥_{2} = ∥ p - c (t) ∥_{2}$ [L4] gives the displayed form of clause 1.

2.1step 1.1L2L3algebra

Constructor notation is consistent: $I (t, c (t)) = I (t)$ , because $a (t, c (t)) = 0$ and $I_{ν} (0) = I$ by [L2] with $a = 0$ ; this is the statement of Inertia matrix, spatial inertia tensor, inertia tensor about a point and moment of inertia about an axis of a rigid-material model clause (c) that the tensor about the centre of mass is the spatial tensor.

2.2step 1.1L1L2L3algebra

Vertex evaluation from the supplier: evaluate at the assumed reference-placement time $t_{*}$ , where $c (t_{*}) = 0$ , $R (t_{*}) = I_{3}$ , so $I (t_{*}) = I$ and $a (t_{*}, a e_{1}) = a e_{1}$ by [L3]; then step 1.1 gives $I (t_{*}, a e_{1}) = I + m (a^{2} I_{3} - a^{2} e_{1} e_{1}^{T}) = I + 3 m_{0} a^{2} (I_{3} - e_{1} e_{1}^{T}),$ and adding the diagonal contributions gives $d i a g (\frac{3 m_{0} a^{2}}{2} + 0, \frac{3 m_{0} a^{2}}{2} + \frac{6 m_{0} a^{2}}{2}, 3 m_{0} a^{2} + 3 m_{0} a^{2})$ , which is the matrix of clause 2.

3.1step 2.2L1L5algebra

Direct finite-sum check: by the definition of the shifted tensor [L2] and the finite-atomic formula [L1], $I (t_{*}, a e_{1}) = \int (∥ ρ - a e_{1} ∥_{2}^{2} I_{3} - (ρ - a e_{1}) (ρ - a e_{1})^{T}) d ν (ρ) = m_{0} \sum_{k} (∥ x_{k} - a e_{1} ∥_{2}^{2} I_{3} - (x_{k} - a e_{1}) (x_{k} - a e_{1})^{T}) .$ The contribution of $k = 0$ vanishes because $x_{0} = a e_{1}$ . For $k = 1, 2$ , the displacement vectors are $d_{k} : = x_{k} - a e_{1} = (- \frac{3 a}{2}, \pm \frac{\sqrt{3} a}{2}, 0)$ with $∥ d_{k} ∥_{2}^{2} = 3 a^{2}$ , and $d_{1} d_{1}^{T} + d_{2} d_{2}^{T} = d i a g (\frac{9 a^{2}}{2}, \frac{3 a^{2}}{2}, 0)$ because the off-diagonal products cancel by [L5]. Hence $I (t_{*}, a e_{1}) = m_{0} (2 \cdot 3 a^{2} I_{3} - d i a g (\frac{9 a^{2}}{2}, \frac{3 a^{2}}{2}, 0)) = d i a g (\frac{3 m_{0} a^{2}}{2}, \frac{9 m_{0} a^{2}}{2}, 6 m_{0} a^{2})$ , in agreement with step 2.2. This is clause 3.

4.1step 2.2step 3.1L1L2L5algebra

Axis moments: by clause (c) of Principal axes and principal moments of the inertia data of a rigid-material model, axis moments and extremal values the moment about a spatial axis through $p$ with unit direction $n$ is $n^{T} I (t, p) n$ ; for the axis through the vertex $a e_{1}$ in direction $e_{3}$ this is the $(3, 3)$ entry of the matrix of clause 2, namely $6 m_{0} a^{2}$ ; for the parallel axis through the centre of mass the moment is $e_{3}^{T} I e_{3} = 3 m_{0} a^{2}$ by the companion example [L1]. Directly, the squared distance of the three material points from the vertex axis is $0, 3 a^{2}, 3 a^{2}$ (using [L5] for the coordinates of $d_{1}, d_{2}$ ), giving $2 m_{0} \cdot 3 a^{2} = 6 m_{0} a^{2}$ . The difference $6 m_{0} a^{2} - 3 m_{0} a^{2} = 3 m_{0} a^{2} = m a^{2}$ is the product of the total mass and the squared distance between the parallel axes, as the axis-shift form of [L2] predicts. This is clause 4.

5.1step 1.1step 2.2step 3.1step 4.1∎

Interpretation: the spatial parallel-axis form of clause 1 is the model's reading of the mathematical supplier [L2], and the two independent computations of clauses 2-3 agree on the triangle data. The computation exercises the shifted tensor about a point of the body that is not the centre of mass; the entries are model quantities computed from $m_{0}$ and $a$ , and no measured inertia or concrete body is asserted.

Remarks

The theorem behind the shift. The relation between the tensors about the centre of mass and about a displaced point is the mathematical theorem Parallel-axis theorem: the inertia tensor about a displaced point of a centred mass distribution; the example only instantiates it in the model's notation and checks both sides on explicit data. Its hypotheses are the centred reference shape of Adoption of the rigid-material model branch: reference mass distribution, rigid placements, orientation and scope and the countably-choice-founded finiteness of the integrals, both inherited by the model's definition Inertia matrix, spatial inertia tensor, inertia tensor about a point and moment of inertia about an axis of a rigid-material model.
Why a vertex. The shifted tensor about a point of the body is used whenever a rotation axis is not through the centre of mass — for example a body pivoting about a corner. The example shows the bookkeeping: the shift enters only through the centre-of-mass displacement $p - c (t)$ in the spatial form of clause 1.
No measured value. The parameters $m_{0}$ and $a$ are model data; the example asserts no measured moment of inertia.

Parallel-axis check for the equilateral-triangle model: inertia tensor about a vertex computed two ways

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources