König’s Second Theorem and the Inertially Decoupled Centre-of-Mass Row

At a glance

When the whole-body dynamics of a free-flying space manipulator are written in circumcentroidal coordinates — centre-of-mass motion split off from the coupled attitude-and-end-effector motion — the centre-of-mass row is claimed to be inertially decoupled and Coriolis-free: it reads $m{\dot{\mathbf{v}}}_c={\mathbf{f}}_c$, Newton’s law for the whole-body linear momentum, with no fictitious term. This page proves the algebraic heart of that claim, König’s second theorem for a finite family of point masses, and Lean’s kernel has checked all four results end-to-end on the three standard axioms [propext, Classical.choice, Quot.sound], with no sorry and no open assumption. What is machine-checked is the coordinate-free inner-product algebra: once the mass-weighted relative velocities balance about the centre of mass, the cross-term between the centre-of-mass velocity and any relative-velocity field vanishes; the inertia splits into a constant total-mass block for the centre of mass with zero coupling to the internal motion; and the kinetic energy separates into a translational part plus an internal part that is manifestly independent of the centre-of-mass velocity.

One step is deliberately not carried in Lean: the literal vanishing of the Christoffel–Coriolis rows for the centre-of-mass coordinates, which is a statement about derivatives of a configuration-dependent mass matrix rather than about a fixed inner-product space. That step is verified symbolically by the companion SymPy check (pin_koenig_p2.py, exact for one, two, and three arm joints and numeric at seven) and proved by hand on this page, where the two algebraic facts the Lean module supplies — a constant centre-of-mass block and zero coupling blocks — feed straight into the Christoffel formula and kill every term. One hypothesis rides underneath, stated in the open, and it is Giordano’s own definition rather than an addition: the centre-of-mass velocity ${\mathbf{v}}_c$ is resolved in a non-rotating frame.

Links: module index · assumptions ledger · consumed by the redundant seven-joint extension and its inertial-decoupling companion the self-motion inertial decoupling · stability substrate Lyapunov’s direct method · source giordano2019coordinated · pin pin_koenig_p2.py · derivation [(~/Code/generated_reports/math/derivation_7dof.md)]

Motivation

Giordano’s coordinated-control framing writes the augmented dynamics of the manipulator in the circumcentroidal coordinates $({\mathbf{v}}_c,{\mathbf{\omega }}_b,{\mathbf{\nu }}_e^{\oplus })$ — the centre-of-mass velocity, the base angular velocity, and the end-effector twist about the centre of mass. In that frame the inertia matrix takes the block form

$$\left[\begin{array}{ccc}m\mathbf{E}& 0& 0\\ 0& {\breve{\mathbf{M}}}_b& {\breve{\mathbf{M}}}_{be}\\ 0& {\breve{\mathbf{M}}}_{be}^{\top }& {\breve{\mathbf{M}}}_e\end{array}\right]$$

with the top-left $m\mathbf{E}$ block — total mass times the identity — sitting apart from the rest, its two off-diagonal coupling blocks identically zero. Giordano then asserts one thing more: the Coriolis and centrifugal terms of the centre-of-mass row cancel, so that the top row of the equations of motion collapses from its full circumcentroidal form all the way to $m{\dot{\mathbf{v}}}_c={\mathbf{f}}_c$. The paper states this cancellation and points, for its proof, to the appendix of one of its own references — a paper that is not in our corpus.

The 7-DOF derivation this library builds on inherited that gap. Its list of steps still to verify marked the centre-of-mass row as expected Coriolis-free, with the reasoning “König’s decomposition $T=\frac{1}{2}m\Vert {\mathbf{v}}_c{\Vert }^2+T_{\text{int}}$ holds no matter how the internal motion is parameterized,” and a note to verify the cited cancellation. This page is that verification, from first principles rather than by transcription. The question it answers precisely is: why is the centre-of-mass block a constant, decoupled $m\mathbf{E}$, and why does that force the Coriolis row to vanish for any number of arm joints?

The answer is a single classical theorem about kinetic energy, and the whole point of formalizing it here is that it settles the matter parameterization-independently. König’s theorem does not care how many joints the arm has, nor how they are coordinatized; it only asks that the internal velocities be measured relative to the centre of mass. So the seventh joint of the redundant arm — or the seven-hundredth — cannot touch the centre-of-mass block. That is a much stronger statement than “we checked it for our robot,” and it is worth pinning down exactly.

The objects

We work, as the Lean module does, over an arbitrary real inner-product space $E$ — in Lean a NormedAddCommGroup E with an InnerProductSpace ℝ E. The reader should picture $E={\mathbb{R}}^2$ (the planar model of the companion symbolic check) or $E={\mathbb{R}}^3$; nothing below depends on the dimension.

A finite family of bodies is indexed by a Finset $s$ over some index type. Each body $i$ carries a mass $m_i$, a real number (positivity is not needed for the decomposition, a point we return to). The kinematic decomposition is the one König’s theorem turns on: the inertial velocity of body $i$ is written as

$${\mathbf{v}}_i={\mathbf{v}}_c+{\mathbf{w}}_i$$

where ${\mathbf{v}}_c\in E$ is the velocity of the whole-body centre of mass and ${\mathbf{w}}_i\in E$ is the velocity of body $i$ relative to the centre of mass. In the Lean module these are the field vc and the map w : ι → E. The relative field is not arbitrary: because the centre of mass is the mass-weighted mean position, differentiating the defining identity ${\sum }_i{m}_i{\mathbf{r}}_i=m_t{\mathbf{r}}_c$ in time gives the balance condition

$$\sum _{i\in s}{m}_i{\mathbf{w}}_i=0$$

which is the hypothesis hbal throughout, with $m_t={\sum }_{i\in s}{m}_i$ the total mass. This one identity — the mass-weighted relative velocities sum to zero about the centre of mass — is the entire engine. Everything else is bilinearity of the inner product.

A second relative field ${\mathbf{w}}_i^{\prime }$ with its own balance ${\sum }_i{m}_i{\mathbf{w}}_i^{\prime }=0$ (the hypothesis hbal') appears in the polarized statement, so that the general bilinear identity can be stated before its diagonal, energy-shaped consequence.

The centre-of-mass cross-term vanishes (com_cross_term_zero)

The first result is the seed from which the others grow: the centre-of-mass velocity is inertially orthogonal to the whole relative-velocity field.

$$\sum _{i\in s}{m}_i⟨{\mathbf{v}}_c,{\mathbf{w}}_i⟩=0$$

Strategy

Work backward from the goal. We want a mass-weighted sum of inner products, each sharing the same left slot ${\mathbf{v}}_c$, to vanish. The inner product is linear in its right slot, so if we can move the scalar $m_i$ and the summation inside that right slot, the sum becomes a single inner product $⟨{\mathbf{v}}_c,{\sum }_i{m}_i{\mathbf{w}}_i⟩$ — and its right argument is exactly the quantity the balance hypothesis sends to zero. This is a direct proof: the technique is simply to exploit linearity in the right argument, because the hypothesis hbal is handed to us as a statement about ${\sum }_i{m}_i{\mathbf{w}}_i$, and we want the algebra to deliver that sub-expression untouched.

Proof

Fix the centre-of-mass velocity ${\mathbf{v}}_c\in E$. For each index $i$, real-bilinearity of the inner product lets the scalar $m_i$ pass into the right slot,

$$m_i⟨{\mathbf{v}}_c,{\mathbf{w}}_i⟩=⟨{\mathbf{v}}_c,m_i{\mathbf{w}}_i⟩$$

which in Lean is real_inner_smul_right. Summing over the family and then pulling the finite sum through the right slot — the additivity inner_sum — collects everything under one inner product:

$$\sum _{i\in s}{m}_i⟨{\mathbf{v}}_c,{\mathbf{w}}_i⟩=\sum _{i\in s}⟨{\mathbf{v}}_c,m_i{\mathbf{w}}_i⟩=⟨{\mathbf{v}}_c,\sum _{i\in s}{m}_i{\mathbf{w}}_i⟩$$

Now the balance hypothesis hbal says the right argument is the zero vector, and the inner product with the zero vector is zero (inner_zero_right):

$$⟨{\mathbf{v}}_c,\sum _{i\in s}{m}_i{\mathbf{w}}_i⟩=⟨{\mathbf{v}}_c,0⟩=0$$

Therefore the mass-weighted cross-term vanishes, as desired. $■$

What this shows

This is the whole physical content in miniature. The centre of mass is defined to make the relative momenta cancel, and cancelling relative momenta is precisely what it means for the centre-of-mass velocity to have no inner-product overlap with the internal motion. In the inertia matrix this identity is the statement that the off-diagonal block coupling the centre-of-mass coordinate to the shape coordinates is identically zero — not small, not approximately diagonal, but exactly zero. It is also, read the other way, why the centre-of-mass coordinate is cyclic: the internal energy cannot see where the centre of mass is, only how fast the bodies move around it.

The polarized König split — the inertia block-diagonalizes (koenig_inertia_bilinear)

The second result is the full bilinear identity, property (D) of the verification memo — the inertial block-diagonalization written out.

$$\sum _{i\in s}{m}_i⟨{\mathbf{v}}_c+{\mathbf{w}}_i,{\mathbf{v}}_c^{\prime }+{\mathbf{w}}_i^{\prime }⟩=\left(\sum _{i\in s}{m}_i\right)⟨{\mathbf{v}}_c,{\mathbf{v}}_c^{\prime }⟩+\sum _{i\in s}{m}_i⟨{\mathbf{w}}_i,{\mathbf{w}}_i^{\prime }⟩$$

Strategy

Two body-velocity fields ${\mathbf{v}}_c+{\mathbf{w}}_i$ and ${\mathbf{v}}_c^{\prime }+{\mathbf{w}}_i^{\prime }$ are paired in the inner product. Expanding by bilinearity produces four families of terms: a centre-of-mass–centre-of-mass part, an internal–internal part, and two cross parts. We want the two cross parts to disappear, and the previous result is built to do exactly that. So the plan writes the expansion, disposes of both cross-sums by com_cross_term_zero, and factors the constant scalar out of the surviving centre-of-mass term. One cross-sum has ${\mathbf{v}}_c^{\prime }$ in the wrong slot, so a single use of the symmetry $⟨{\mathbf{w}}_i,{\mathbf{v}}_c^{\prime }⟩=⟨{\mathbf{v}}_c^{\prime },{\mathbf{w}}_i⟩$ (real inner products are symmetric) lines it up with the form the previous lemma expects.

Proof

Expand the paired inner product by bilinearity in both arguments. For each index $i$,

$$⟨{\mathbf{v}}_c+{\mathbf{w}}_i,{\mathbf{v}}_c^{\prime }+{\mathbf{w}}_i^{\prime }⟩=⟨{\mathbf{v}}_c,{\mathbf{v}}_c^{\prime }⟩+⟨{\mathbf{v}}_c,{\mathbf{w}}_i^{\prime }⟩+⟨{\mathbf{w}}_i,{\mathbf{v}}_c^{\prime }⟩+⟨{\mathbf{w}}_i,{\mathbf{w}}_i^{\prime }⟩$$

Multiplying by $m_i$ and summing splits the total into four mass-weighted sums (in Lean this regrouping is Finset.sum_add_distrib applied thrice, closed by ring on the per-term identity):

$$\sum _{i\in s}{m}_i⟨{\mathbf{v}}_c+{\mathbf{w}}_i,{\mathbf{v}}_c^{\prime }+{\mathbf{w}}_i^{\prime }⟩=\underset{\text{CoM–CoM}}{\underbrace{\sum _i{m}_i⟨{\mathbf{v}}_c,{\mathbf{v}}_c^{\prime }⟩}}+\underset{\text{cross 1}}{\underbrace{\sum _i{m}_i⟨{\mathbf{v}}_c,{\mathbf{w}}_i^{\prime }⟩}}+\underset{\text{cross 2}}{\underbrace{\sum _i{m}_i⟨{\mathbf{w}}_i,{\mathbf{v}}_c^{\prime }⟩}}+\underset{\text{internal}}{\underbrace{\sum _i{m}_i⟨{\mathbf{w}}_i,{\mathbf{w}}_i^{\prime }⟩}}$$

Consider the two cross-sums. The first, ${\sum }_i{m}_i⟨{\mathbf{v}}_c,{\mathbf{w}}_i^{\prime }⟩$, is com_cross_term_zero applied to the balanced field ${\mathbf{w}}^{\prime }$ (using hbal') and vanishes outright. The second, ${\sum }_i{m}_i⟨{\mathbf{w}}_i,{\mathbf{v}}_c^{\prime }⟩$, has the fixed vector ${\mathbf{v}}_c^{\prime }$ in the right slot rather than the left; symmetry of the real inner product rewrites each term as $⟨{\mathbf{v}}_c^{\prime },{\mathbf{w}}_i⟩$ (Lean’s real_inner_comm), and then it too is com_cross_term_zero — now applied to $\mathbf{w}$ with hbal — and vanishes. Both cross-sums are therefore zero.

Two families remain. The internal sum is already in final form. The centre-of-mass sum has a summand $m_i⟨{\mathbf{v}}_c,{\mathbf{v}}_c^{\prime }⟩$ whose inner-product factor does not depend on $i$, so the constant factors out of the finite sum (Finset.sum_mul):

$$\sum _{i\in s}{m}_i⟨{\mathbf{v}}_c,{\mathbf{v}}_c^{\prime }⟩=\left(\sum _{i\in s}{m}_i\right)⟨{\mathbf{v}}_c,{\mathbf{v}}_c^{\prime }⟩$$

Assembling the two survivors — the Lean proof closes the rearrangement with abel — gives the claimed identity. $■$

What this shows

Read as a statement about the inertia matrix, this is property (D). The coefficient of the centre-of-mass–centre-of-mass pairing is the constant total mass $m_t={\sum }_i{m}_i$, so the centre-of-mass block of the inertia is $m_t$ times the identity — exactly Giordano’s $m\mathbf{E}$. Both cross-terms drop out, so both off-diagonal coupling blocks between the centre of mass and the internal motion are zero. And the internal pairing ${\sum }_i{m}_i⟨{\mathbf{w}}_i,{\mathbf{w}}_i^{\prime }⟩$ carries no ${\mathbf{v}}_c$ at all — it is the shape block, kept apart from the translational motion. The single identity block-diagonalizes the kinetic-energy metric into a constant translational part and a configuration-dependent internal part, and it does so without ever mentioning how many bodies there are or how their relative motion is parameterized.

The norm form and the energy split (koenig_kinetic_split, koenig_energy_split)

The remaining two results specialize the bilinear identity to the diagonal and dress it in the physicist’s notation. They are short, so we take them together.

Setting the second field equal to the first (${\mathbf{v}}_c^{\prime }={\mathbf{v}}_c$, ${\mathbf{w}}^{\prime }=\mathbf{w}$) in the polarized identity, and using that a real inner product of a vector with itself is its squared norm ($⟨\mathbf{x},\mathbf{x}⟩=\Vert \mathbf{x}{\Vert }^2$, Lean’s real_inner_self_eq_norm_sq), the paired form becomes a sum of squares. This is koenig_kinetic_split:

$$\sum _{i\in s}{m}_i\Vert {\mathbf{v}}_c+{\mathbf{w}}_i{\Vert }^2=\left(\sum _{i\in s}{m}_i\right)\Vert {\mathbf{v}}_c{\Vert }^2+\sum _{i\in s}{m}_i\Vert {\mathbf{w}}_i{\Vert }^2$$

Its Lean proof is a single rewrite that turns each squared norm back into an inner product and then invokes koenig_inertia_bilinear with the fields identified — the diagonal case genuinely is just the polarized case looked at on the diagonal.

Multiplying through by one-half puts the total kinetic energy $T=\frac{1}{2}{\sum }_i{m}_i\Vert {\mathbf{v}}_c+{\mathbf{w}}_i{\Vert }^2$ in the form the classical theorem is named for. This is koenig_energy_split:

$$T=\frac{1}{2}{m}_t\Vert {\mathbf{v}}_c{\Vert }^2+T_{\text{int}}{T}_{\text{int}}=\frac{1}{2}\sum _{i\in s}{m}_i\Vert {\mathbf{w}}_i{\Vert }^2{m}_t=\sum _{i\in s}{m}_i$$

The Lean proof is koenig_kinetic_split followed by ring.

What this shows

The total kinetic energy is the energy of a single point of mass $m_t$ moving with the centre of mass, plus an internal energy $T_{\text{int}}$ that depends only on the velocities of the bodies relative to the centre of mass. The decisive feature — the one the whole 7-DOF argument leans on — is written on the face of the formula: $T_{\text{int}}$ contains no ${\mathbf{v}}_c$. The gradient $\partial T_{\text{int}}/\partial {\mathbf{v}}_c$ is identically zero. That visible independence is what makes the centre-of-mass velocity a coordinate the internal dynamics cannot feel, and it is the algebraic reason the centre-of-mass row of the equations of motion decouples.

From the algebra to the Coriolis row: why the centre-of-mass row is Coriolis-free

Here is where the machine-checked layer ends, and the reason this section is written out by hand. The four theorems above live over a fixed inner-product space; they say nothing, on their own, about the derivatives of a mass matrix that varies with configuration. The claim Giordano makes — that the Coriolis and centrifugal terms of the centre-of-mass row vanish — is a Lagrangian statement, one level up. This section discharges it, using the two facts the Lean module has just established as its only inputs. The companion symbolic check (pin_koenig_p2.py) confirms the same conclusion independently and numerically; what follows is the argument a reader can carry in their head.

The setup

Write the generalized coordinates of the whole-body system as a split $q=({\mathbf{r}}_c,\mathbf{\sigma })$, where ${\mathbf{r}}_c$ are the centre-of-mass position coordinates and $\mathbf{\sigma }$ are the shape (internal) coordinates — base attitude and joint angles. The kinetic energy defines a configuration-dependent mass matrix $\mathbf{M}(q)$ through $T=\frac{1}{2}{\dot{q}}^{\top }\mathbf{M}(q)\dot{q}$. The equations of motion carry a Coriolis–centrifugal term built from the Christoffel symbols of the first kind,

$$c_{kij}=\frac{1}{2}({\partial }_i{M}_{kj}+{\partial }_j{M}_{ki}-{\partial }_k{M}_{ij})$$

where ${\partial }_i$ denotes the partial derivative with respect to the $i$-th generalized coordinate, and the contribution to the $k$-th row of the equations of motion is ${\sum }_{i,j}{c}_{kij}{\dot{q}}_i{\dot{q}}_j$. We must show that for every $k$ that is a centre-of-mass coordinate, every $c_{kij}$ is zero.

Two facts are available, both furnished by the algebra above and confirmed by the pin as properties (D) and (C):

• (D) — a constant, decoupled centre-of-mass block. The polarized König split says the centre-of-mass block of $\mathbf{M}$ is the constant $m_t\mathbf{E}$ and the centre-of-mass–shape coupling blocks are zero. So for a centre-of-mass row index $k$, the entry $M_{kj}$ equals $m_t$ when $j=k$ and equals $0$ for every other $j$ — in every case, a constant, free of the configuration $q$.
• (C) — the centre-of-mass coordinate is cyclic. The internal energy $T_{\text{int}}=\frac{1}{2}{\sum }_i{m}_i\Vert {\mathbf{w}}_i{\Vert }^2$ depends on the shape and its rate, never on where the centre of mass is; equivalently $\mathbf{M}$ is translation-invariant, so ${\partial }_k{M}_{ij}=0$ for every centre-of-mass coordinate $k$ and every $i,j$.

The proof that the Christoffel rows vanish

Let $k$ be a centre-of-mass coordinate and take any indices $i,j$. Examine the three terms of $c_{kij}$ in turn.

The third term is ${\partial }_k{M}_{ij}$. Since $k$ is a centre-of-mass coordinate and, by property (C), the mass matrix does not depend on any centre-of-mass coordinate, this derivative is zero for every choice of $i,j$.

The first term is ${\partial }_i{M}_{kj}$. Its differentiand $M_{kj}$ is an entry in the centre-of-mass row $k$. By property (D) that entry is a constant — either the total mass $m_t$ or zero — regardless of $q$. The derivative of a constant is zero, so ${\partial }_i{M}_{kj}=0$.

The second term is ${\partial }_j{M}_{ki}$, and $M_{ki}$ is again an entry of the centre-of-mass row $k$, hence again constant by (D); its derivative ${\partial }_j{M}_{ki}$ vanishes for the same reason.

All three terms are zero, so $c_{kij}=0$ for every $i,j$ and every centre-of-mass row $k$. Consequently the Coriolis–centrifugal contribution to the centre-of-mass row, ${\sum }_{i,j}{c}_{kij}{\dot{q}}_i{\dot{q}}_j$, is identically zero. What remains of that row is the inertial term alone; since the centre-of-mass block is $m_t\mathbf{E}$ and its coupling to the shape vanishes, the row reads

$$m_t{\ddot{\mathbf{r}}}_c={\mathbf{f}}_c$$

that is, $m{\dot{\mathbf{v}}}_c={\mathbf{f}}_c$. This is precisely Giordano’s cancellation $-{\mathbf{C}}_{bc}^{\top }{\mathbf{\omega }}_b-{\mathbf{C}}_{ec}^{\top }{\mathbf{\nu }}_e^{\oplus }=0$ and the collapse of the full centre-of-mass row to its momentum form. $■$

What this shows, and the division of labour

Notice how cleanly the two properties split the work. Property (C) — the centre of mass is cyclic — kills the third Christoffel term, the one that differentiates the metric along the centre-of-mass direction. Property (D) — the centre-of-mass row is a bank of constants — kills the first two terms, which differentiate that row along any direction. Neither alone suffices; together they annihilate the whole symbol. And both trace back to the one balance identity hbal proved above: the constant $m_t\mathbf{E}$ block and the zero coupling blocks are koenig_inertia_bilinear, while the cyclic property is the visible ${\mathbf{v}}_c$-independence of $T_{\text{int}}$ in koenig_energy_split. The Lagrangian statement is genuinely a corollary of the inner-product algebra — which is why formalizing the algebra, and proving this last step from it, settles the matter without a single derivative appearing in the Lean source.

Because König’s theorem is parameterization-independent, adding an arm joint only enlarges the shape block ${\mathbf{M}}_{\text{shape}}(\mathbf{\sigma })$; it cannot alter the constant centre-of-mass block or reintroduce a coupling. So the centre-of-mass row is Coriolis-free for every arm, not merely the one in front of us — the strong, joint-count-free conclusion the 7-DOF derivation wanted.

Scope and limitations

• What is machine-checked, and what is not. The four Lean theorems are the coordinate-free inner-product algebra over an arbitrary real inner-product space: the cross-term vanishing, the polarized inertia split, and the two energy forms. The literal statement that the Christoffel–Coriolis rows for the centre-of-mass coordinates vanish — property (R) — is not in the Lean module. It is a statement about derivatives of a configuration-dependent mass matrix, one level above the fixed inner-product space, and it lives in two places: the symbolic check pin_koenig_p2.py, which computes the full Christoffel rows, and the hand proof in the section above, which derives it from the machine-checked properties (D) and (C). This is a boundary of formalization, not an open assumption inside the module: the four theorems carry no interface hypotheses.
• The frame hypothesis is Giordano’s own definition, not an addition. The conclusion $m{\dot{\mathbf{v}}}_c={\mathbf{f}}_c$ is Coriolis-free only when ${\mathbf{v}}_c$ is the centre-of-mass velocity resolved in a non-rotating frame. This is exactly how Giordano defines frame $\mathcal{C}$ — “placed on the CoM of the space robot and whose axes are nonrotating w.r.t. the inertial space.” Were ${\mathbf{v}}_c$ instead resolved in a rotating base-attitude frame, a gyroscopic term ${\mathbf{\omega }}^{\times }m{\mathbf{v}}_c$ would appear; that is an artifact of the frame choice, not a failure of König’s theorem, and the paper’s stated result is the non-rotating-frame one. So the single hypothesis under which property (R) holds is a hypothesis the framing paper already made.
• Masses are arbitrary reals. The split needs only the balance identity ${\sum }_i{m}_i{\mathbf{w}}_i=0$; positivity of the masses is never used. The theorems are stated with $m_i\in \mathbb{R}$, so they apply verbatim to signed or reduced masses should the modelling ever call for them.
• The planar symbolic model is a floor, not a ceiling. The companion pin builds a planar free-flying base plus $n$-link arm — the minimal setting that still carries the rotational coupling that could, a priori, inject Coriolis terms into the centre-of-mass row. A translation-only “napkin” model has a constant mass matrix and would prove nothing. The planar check is exact (symbolic) for one, two, and three joints and numeric at seven; the Lean layer above it is dimension-free.

Provenance

• König’s second theorem. D. Cline, Variational Principles in Classical Mechanics, 2nd ed. (2018), §2.10, eq. (2.10.4): $T={\sum }_i\frac{1}{2}{m}_i{v}_i^{\prime 2}+\frac{1}{2}M{V}^2$, named there “Samuel König’s second theorem.” This is the classical statement the module formalizes. Cline is not yet corpus-filed — cited as plain text and flagged for a bibkey.
• The circumcentroidal dynamics and the cancellation claim. Giordano et al. (2019), A Coordinated Control Framework for a Free-Flying Space Robot, RA-L — eq. (21) exhibits the block inertia with the constant $m\mathbf{E}$ centre-of-mass block, and eq. (21)→(22a) states the Coriolis cancellation $-{\mathbf{C}}_{bc}^{\top }{\mathbf{\omega }}_b-{\mathbf{C}}_{ec}^{\top }{\mathbf{\nu }}_e^{\oplus }=0$ that collapses the row to $m{\dot{\mathbf{v}}}_c={\mathbf{f}}_c$; frame $\mathcal{C}$ is defined non-rotating in the paper’s notation section. → giordano2019coordinated.
• The cited appendix. Giordano’s “(see Appendix of [4])” resolves to A. M. Giordano, G. Garofalo, A. Albu-Schäffer, Momentum dumping for space robots, Proc. IEEE 56th CDC (2017), pp. 5243–5248 — reference [4] inside the RA-L paper, not a bibkey in our corpus. Its appendix could not be read directly; this page verifies the claim that appendix asserts from first principles rather than transcribing its algebra. Not corpus-filed — flagged; candidate DOI 10.1109/CDC.2017.8264435.
• Where it is used. The constant, decoupled centre-of-mass block is what lets the reduced attitude-and-end-effector dynamics be certified on their own by the Lyapunov and cascade machinery — see the redundant seven-joint extension and the Lyapunov direct-method substrate.

Machine verification (#print axioms)

Lean’s kernel reports the axiom dependency of each of the four results below. Nothing beyond [propext, Classical.choice, Quot.sound] appears on any of them; there is no sorryAx, and the module contains no sorry.

info: 'Ctrllib.com_cross_term_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Ctrllib.koenig_inertia_bilinear' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Ctrllib.koenig_kinetic_split' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Ctrllib.koenig_energy_split' depends on axioms: [propext, Classical.choice, Quot.sound]

The machine-checked source is [(~/Code/vault/lean/KoenigDecomposition.lean)] (build copy ~/lean/ctrllib/Ctrllib/KoenigDecomposition.lean; this directory’s copy is the tracked source of truth). The symbolic and numeric cross-check is pin_koenig_p2.py in this directory, run under new-pin-env, exit 0.