stiffness_residual

The stiffness-residual injectivity step, formalized — L4b (TARGET 5)

Seal

Rung rung-1 · Status sealed · #print axioms verbatim in 7. The machine seal — no interface hypotheses in the theorems themselves. This module seals the algebra behind Prop IV.1’s hzero step; the coordinate wiring through the closed-loop field stays with coupled_collapse — see interfaces.
Links: module index · interface ledger · related reduction_cascade, coupled_collapse, rayleigh_sandwich · source giordano2019coordinated · pin pin_stiffness_residual.py

Sealed theorems

stiffness_residual_injective

For $\mathbf{K}\succ 0$ and square $\mathbf{J}$ with injective mulVec, $({\mathbf{J}}^{\top }\mathbf{K})\mathbf{x}=0$ forces $\mathbf{x}=0$.

stiffness_residual_injective’

The physical grouping ${\mathbf{J}}^{\top }(\mathbf{Kx})=0\Rightarrow \mathbf{x}=0$, matching eq 31 verbatim.

stiffness_gram_posDef

The rectangular-safe congruence: full column rank $\mathbf{J}$ and $\mathbf{K}\succ 0$ give $({\mathbf{J}}^{\top }\mathbf{KJ})\succ 0$.

What this seals, in one paragraph

Giordano 2019 Prop IV.1 closes its cascade proof with one algebraic sentence: “Applying LaSalle to (34b), $\breve{\mathbf{v}}\equiv 0$ implies $\tilde{\mathbf{x}}=0$.” L4a (/Code/vault/lean/reduction_cascade.md) carried the LaSalle output through the reduction engine to the paper’s convergence conclusion, but had to keep that closing sentence as the named hypothesis hzero in the sealed propIV1_tendsto, because it needs field-specific linear algebra no Flow fact supplies. L4b seals exactly that linear algebra: on the $\omega$-limit set where $\breve{\mathbf{v}}=0$, the driven dynamics (eq 34b) collapse to the stiffness residual ${\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}=0$, and with $\breve{\mathbf{K}}\succ 0$ and ${\mathbf{J}}_{\tilde{x}}$ of full column rank this forces $\tilde{\mathbf{x}}=0$. The module is (/Code/vault/lean/StiffnessResidual.lean), build copy ~/lean/leanpunov/Leanpunov/StiffnessResidual.lean; the SymPy pin is (~/Code/vault/lean/pin_stiffness_residual.py).

1. Where the residual comes from (the physical setup)

The framing paper partitions the closed-loop state into the decoupled CoM-error driver ${\mathbf{z}}_1$ (eq 34a, Hurwitz) and the coupled base+end-effector block ${\mathbf{z}}_2=[{\breve{\mathbf{v}}}^{\top }{\tilde{\mathbf{x}}}^{\top }{\mathbf{q}}^{\top }{]}^{\top }$ (eq 34b-d). The relevant quantities, read from the clean source (not the OCR — see §5):

• the velocity $\breve{\mathbf{v}}=[{\mathbf{\omega }}_b^{\top }{\mathbf{\nu }}_e^{\oplus \top }{]}^{\top }\in {\mathbb{R}}^9$ (eq 15/27),
• the pose error $\tilde{\mathbf{x}}=[{\tilde{\mathbf{x}}}_b^{\top }{\tilde{\mathbf{x}}}_e^{\top }{]}^{\top }\in {\mathbb{R}}^9$ with ${\tilde{\mathbf{x}}}_b\in {\mathbb{R}}^3$ (base attitude, eq 25) and ${\tilde{\mathbf{x}}}_e\in {\mathbb{R}}^6$ (end-effector pose, eq 24),
• the block stiffness $\breve{\mathbf{K}}=\mathrm{blkdiag}({\mathbf{K}}_b,{\mathbf{K}}_e)\in {\mathbb{R}}^{9\times 9}$, symmetric positive definite (${\mathbf{K}}_b,{\mathbf{K}}_e\succ 0$ by eqs 29-30),
• the representation Jacobian ${\mathbf{J}}_{\tilde{x}}=\mathrm{blkdiag}({\mathbf{J}}_{{\tilde{x}}_b},{\mathbf{J}}_{{\tilde{x}}_e})\in {\mathbb{R}}^{9\times 9}$, defined by $\dot{\tilde{\mathbf{x}}}={\mathbf{J}}_{\tilde{x}}\breve{\mathbf{v}}$ (eq 26).

The driven dynamics (eq 34b) read

$\breve{\mathbf{M}}\dot{\breve{\mathbf{v}}}+\breve{\mathbf{C}}\breve{\mathbf{v}}+\breve{\mathbf{D}}\breve{\mathbf{v}}+{\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}=-\left({\mathbf{C}}_c+\breve{\mathbf{D}}{\breve{\mathbf{G}}}_{v_c}\right){\dot{\tilde{\mathbf{x}}}}_c$

On the invariant set LaSalle isolates, $\breve{\mathbf{v}}\equiv 0$ (from $\dot{V}=-{\breve{\mathbf{v}}}^{\top }\breve{\mathbf{D}}\breve{\mathbf{v}}$ with $\breve{\mathbf{D}}\succ 0$), hence $\dot{\breve{\mathbf{v}}}\equiv 0$; and ${\dot{\tilde{\mathbf{x}}}}_c=0$ on ${\Gamma }_2$. Every velocity term drops and what remains is the stiffness residual

\boldsymbol J_{\tilde x}^\top\breve{\boldsymbol K}\tilde{\boldsymbol x}=0 \tag{eq 31/34b, on the invariant set}

This is a linear equation in $\tilde{\mathbf{x}}$. The whole content of "$\breve{\mathbf{v}}\equiv 0\Rightarrow \tilde{\mathbf{x}}=0$" is that this linear map is injective.

2. The exact claim, pinned before formalizing

The crucial reading question — flagged in the L4a charter — is what ”${\mathbf{J}}_{\tilde{x}}$ full column rank” buys, and whether the prose map $\tilde{\mathbf{x}}\mapsto {\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}$ is genuinely injective. The SymPy pin settles it before any Lean is written (all four blocks pass):

(A) The faithful square claim is TRUE. Because ${\mathbf{J}}_{\tilde{x}}$ is $9\times 9$ square (eq 26 maps ${\mathbb{R}}^9\to {\mathbb{R}}^9$), “full column rank” means nonsingular. Then $\det ({\mathbf{J}}^{\top }\breve{\mathbf{K}})=\det \mathbf{J}\cdot \det \breve{\mathbf{K}}\ne 0$, so ${\mathbf{J}}^{\top }\breve{\mathbf{K}}$ is invertible and ${\mathbf{J}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}=0\Rightarrow \tilde{\mathbf{x}}=0$. Verified symbolically ($3\times 3$ generic) and on 5000 random $9\times 9$ instances (min $1/\mathrm{cond}=0.15>0$).

(B) The rectangular reduced form is FALSE — and this is why the statement must pin square. For a genuinely rectangular full-column-rank $\mathbf{J}$ ($m\times k$, $m>k$), ${\mathbf{J}}^{\top }\breve{\mathbf{K}}$ maps ${\mathbb{R}}^m\to {\mathbb{R}}^k$ and always has a nontrivial kernel. The pin exhibits the counterexample: $\mathbf{J}=\begin{array}{cc}1& 0\\ 0& 1\\ 0& 0\end{array}$ (full column rank), $\breve{\mathbf{K}}=\mathbf{I}$, then $\tilde{\mathbf{x}}=[001{]}^{\top }\ne 0$ satisfies ${\mathbf{J}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}=0$. So a Lean lemma stated for rectangular $\mathbf{J}$ with the reduced residual would be a false seal. The square hypothesis is load-bearing, not cosmetic. This resolves the reduction_cascade.md §7 wording flag (”${\mathbf{J}}_{\tilde{x}}$ full column rank on $\Omega$”): for the square ${\mathbf{J}}_{\tilde{x}}$ it is correct and means nonsingular.

(C) The rank-robust reason is sign-definiteness. The general (rectangular-safe) truth is the congruence: for full-column-rank $\mathbf{J}$ ($\mathbf{J}$-mulVec injective) and $\breve{\mathbf{K}}\succ 0$, ${\mathbf{J}}^{\top }\breve{\mathbf{K}}\mathbf{J}\succ 0$, because ${\tilde{\mathbf{x}}}^{\top }({\mathbf{J}}^{\top }\breve{\mathbf{K}}\mathbf{J})\tilde{\mathbf{x}}=(\mathbf{J}\tilde{\mathbf{x}}{)}^{\top }\breve{\mathbf{K}}(\mathbf{J}\tilde{\mathbf{x}})>0$ off the origin. Pinned symbolically ($2\times 1$) and on 3000 random $9\times 5$ instances (all eigenvalues $>0$). This is the “sign-definiteness on generic full-column-rank $\mathbf{J}$” the charter asked to verify. Note it is not the eq-34b residual (which is ${\mathbf{J}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}$, not ${\mathbf{J}}^{\top }\breve{\mathbf{K}}\mathbf{J}\tilde{\mathbf{x}}$) — it is recorded as the reason the square map is injective and as the honest rectangular statement.

(D) ${\mathbf{J}}_{\tilde{x}}$ really is nonsingular near the target. The base block ${\mathbf{J}}_{{\tilde{x}}_b}=-{\eta }_{b{b}_d}\mathbf{E}+[{\mathbf{ϵ}}_{b{b}_d}{]}^{\times }$ (unit quaternion $(\eta ,\mathbf{ϵ})$) has $\det =-\eta$ (pinned: on ${\eta }^2+\Vert \mathbf{ϵ}{\Vert }^2=1$, $\det =-\eta$), and ${\mathbf{J}}_{{\tilde{x}}_e}=\mathrm{blkdiag}(\mathbf{E},-{\eta }_{e{e}_d}\mathbf{E}+[{\mathbf{ϵ}}_{e{e}_d}{]}^{\times })$ has $\det =-{\eta }_{e{e}_d}$. So ${\mathbf{J}}_{\tilde{x}}$ is nonsingular exactly when each quaternion scalar part $\eta \ne 0$ — automatic near the target $\tilde{\mathbf{x}}=0$ ($\eta =\pm 1$), which is the neighbourhood the local Prop IV.1 claim lives in. (Provenance refinement: the true nonsingularity condition for ${\mathbf{J}}_{\tilde{x}}$ is $\eta \ne 0$, a quaternion-representation condition, distinct from $\Omega =\{{\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })>0\}$ which excludes the manipulator-Jacobian singularities. Both hold near $\bar{\mathbf{z}}$.)

3. The Lean statements

Over n : Type* with [Fintype n] [DecidableEq n] (the thesis uses Fin 9), K J : Matrix n n ℝ.

Headline — stiffness_residual_injective. Given hK : K.PosDef and hJ : Function.Injective J.mulVec (full column rank; for the square J this is nonsingularity), if (Jᵀ * K) *ᵥ x = 0 then x = 0.

Physical grouping — stiffness_residual_injective'. The same with the residual written Jᵀ *ᵥ (K *ᵥ x) = 0 (transpose Jacobian applied to the elastic wrench $\breve{\mathbf{K}}\tilde{\mathbf{x}}$, matching eq 31 verbatim). One mulVec_mulVec rewrite off the headline.

Sign-definiteness — stiffness_gram_posDef. For K.PosDef and hJ : Function.Injective J.mulVec with J : Matrix n m ℝ (rectangular allowed), (Jᵀ * K * J).PosDef. The (C) statement.

4. Proof narrative and the Mathlib stones

The headline is a three-line invertibility argument.

1. K is a unit. Matrix.PosDef.isUnit (over a field with DecidableEq): a positive-definite matrix has trivial mulVec kernel, hence is invertible. So IsUnit K.
2. J is a unit. For a square matrix over a field, injective mulVec $\iff$ invertible: Matrix.mulVec_injective_iff_isUnit. The hypothesis hJ (full column rank) therefore gives IsUnit J; Jᵀ is a unit too, via isUnit_iff_isUnit_det and det_transpose ($\det {\mathbf{J}}^{\top }=\det \mathbf{J}$).
3. The product Jᵀ * K is a unit (IsUnit.mul), so its action is injective: Matrix.mulVec_injective_of_isUnit gives Function.Injective (Jᵀ * K).mulVec. Applying injectivity to (Jᵀ * K) *ᵥ x = 0 = (Jᵀ * K) *ᵥ 0 (mulVec_zero) closes x = 0.

The sign-definiteness lemma is one Mathlib congruence stone: Matrix.PosDef.conjTranspose_mul_mul_same (for A.PosDef and B.mulVec injective, (Bᴴ * A * B).PosDef), with conjTranspose_eq_transpose_of_trivial turning ${\mathbf{J}}^{\mathrm{H}}$ into ${\mathbf{J}}^{\top }$ over $\mathbb{R}$ (trivial star). This is the same real-conjTranspose peeling used in the sealed Rayleigh module.

No new heavy machinery: the lemma stands on Mathlib’s positive-definite and nonsingular-inverse libraries. It is a genuinely small stone (cost feel: below an L2-scale push — one SymPy pin, one module, one omit/linter fixup cycle, no proof-search struggle).

5. The OCR reconciliation (charter mandatory step, discharged — no PDF needed)

The L4a extraction flagged two garbles to reconcile before committing any coordinate-level set definition. Both are resolved against the rendered clean source, unambiguously, so the original PDF is not required:

• Prop IV.1 set symbols "${\hat{\mathbf{x}}}_c$", "$\tilde{\mathbf{v}}$" are OCR corruption of ${\dot{\tilde{\mathbf{x}}}}_c$ and $\breve{\mathbf{v}}$. Forced by the explicit state partition (giordano eq 21/26): ${\mathbf{z}}_1=[{\tilde{\mathbf{x}}}_c^{\top }{\dot{\tilde{\mathbf{x}}}}_c^{\top }{]}^{\top }$ and $\breve{\mathbf{v}}=[{\mathbf{\omega }}_b^{\top }{\mathbf{\nu }}_e^{\oplus \top }{]}^{\top }$. The set $\bar{\mathbf{z}}=\{{\mathbf{z}}_1=0,\breve{\mathbf{v}}=0,\tilde{\mathbf{x}}=0\}$ has no other consistent reading; "$\tilde{\mathbf{v}}$" is not a defined symbol anywhere in the paper. Not ambiguous.
• The eq-34b residual appears mangled in the OCR ($\mathbf{J}{\ddot{\mathbf{x}}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}$, $\breve{\mathbf{v}}$ as $\dot{\mathbf{v}}$) but the clean eq 31 (line 235 of the source md) gives it verbatim as ${\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}+\breve{\mathbf{D}}\breve{\mathbf{v}}$, and the eq-38 $\dot{V}$ line confirms the term ${\breve{\mathbf{v}}}^{\top }{\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}$. The residual ${\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}$ is unambiguous.

TARGET 5’s lemma is symbol-independent of the set garble anyway (it is pure matrix algebra), so nothing here blocked the seal.

6. What is proven vs. what stays an interface

Proven (real content, non-vacuous, machine-checked): the finite-dimensional injectivity of the stiffness residual — the exact algebra of Prop IV.1’s "$\breve{\mathbf{v}}\equiv 0\Rightarrow \tilde{\mathbf{x}}=0$" — and the sign-definiteness behind it.

Interface boundary (honest, unchanged from L4a). This module does not by itself discharge propIV1_tendsto.hzero ({y | fderiv V y (f y) = 0} ⊆ Γ₁) at the abstract Flow level. Doing so additionally needs the coordinate-level closed-loop field ${\mathbf{g}}_2$ (eq 34b) to turn the abstract derivative condition fderiv V y (f y) = 0 into $\breve{\mathbf{v}}=0$ (via $\breve{\mathbf{D}}\succ 0$ and the sealed Rayleigh machinery) and then into the residual ${\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}=0$. That field is deliberately un-formalized across this campaign — the IsSolutionTo interface precedent — so the coordinate wiring stays applier-side. L4b is the final, machine-checked link of that chain: once an applier supplies the field and the collapse to the residual, this lemma delivers $\tilde{\mathbf{x}}=0$, i.e. membership in $\bar{\mathbf{z}}$ (with $\mathbf{q}\in {\mathbb{T}}^n$ free).

7. The machine seal

#print axioms, verbatim from the build (lake build, 2639 jobs, 2026-07-06):

info: Leanpunov/StiffnessResidual.lean:118:0: 'Leanpunov.stiffness_residual_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/StiffnessResidual.lean:119:0: 'Leanpunov.stiffness_residual_injective'' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/StiffnessResidual.lean:120:0: 'Leanpunov.stiffness_gram_posDef' depends on axioms: [propext, Classical.choice, Quot.sound]

Nothing beyond {propext, Classical.choice, Quot.sound}; no sorryAx. The full project (L1-L4b) builds clean.

Mathlib stones used

• Matrix.PosDef.isUnit — positive-definite $\Rightarrow$ invertible.
• Matrix.mulVec_injective_iff_isUnit — square, over a field: full column rank $\iff$ nonsingular.
• Matrix.mulVec_injective_of_isUnit — a unit acts injectively.
• Matrix.isUnit_iff_isUnit_det, Matrix.det_transpose — transpose of a unit is a unit.
• Matrix.PosDef.conjTranspose_mul_mul_same, Matrix.conjTranspose_eq_transpose_of_trivial — the congruence sign-definiteness over $\mathbb{R}$.