com_lasalle

The CoM tracking loop is globally asymptotically stable — TARGET 1

Seal

Rung rung-1 · Status interfaced — axiom-clean (#print axioms verbatim in 8. The machine seal; full-integration build 2640 jobs), resting on the named interfaces IsSolutionTo, hcpt, and the operator hypotheses hMsa/hKsa/hMinv/hDnn/hDdef/hKdef (theorems for concrete SPD blocks; matrix corollary is a boarded follow-up) — see interfaces. Public helper: comEnergy_differentiable; definitions ComState, comField, comEnergy.
Links: module index · interface ledger · related lasalle_invariance, reduction_cascade, block_lyapunov, coupled_collapse, coupled_field · source giordano2019coordinated · pin pin_com_lasalle.py

Sealed theorems

com_dissipation

The energy-dissipation identity $DV(z)[f(z)]=-⟨v,Dv⟩$ along the CoM loop, proved outright.

com_decrease

The negative-semidefinite decrease $DV[f]\le 0$ LaSalle consumes.

com_collapse

The LaSalle collapse, proved (not interfaced): any invariant set with $DV[f]=0$ sits inside $\{0\}$.

com_gas

The deliverable — every precompact orbit of the CoM driver converges to the origin, discharging Corollary 12’s cascade input.

What this seals, in one paragraph

The framing paper’s cascade proof (Giordano 2019 RA-L, Prop IV.1 / Corollary 12) needs, as its first step, that the autonomous CoM-error driver is a globally asymptotically stable equilibrium — Corollary 12 condition ”$y=0$ is a (globally) asymptotically stable equilibrium of $\dot{y}=g(y)$”. That driver is the homogeneous damped second-order loop

$$M{\ddot{\tilde{\mathbf{x}}}}_c+D{\dot{\tilde{\mathbf{x}}}}_c+K{\tilde{\mathbf{x}}}_c=0,M,D,K\succ 0\text{ symmetric}$$

(current_sota.md §4.3 line 402 / eq 4.9; Giordano 2019 eq 34a). Until now it entered the cascade as a hypothesis. This module proves it outright from the sealed L3 LaSalle engine, discharging that cascade input. Because the field is fully explicit and linear, the LaSalle collapse — the largest invariant set inside $\{{\dot{\tilde{x}}}_c=0\}$ is the origin — is proved, not interfaced (contrast propIV1_tendsto’s hzero, which had to assume the analogous collapse for the un-formalized nonlinear field).

The module is (/Code/vault/lean/ComLaSalle.lean), build copy ~/lean/leanpunov/Leanpunov/ComLaSalle.lean. SymPy pin (dissipation identity + collapse injectivity): (/Code/vault/lean/pin_com_lasalle.py).

1. The mathematical object

Work on a real inner-product space $H$ (the CoM space; $H={\mathbb{R}}^3$ in the thesis, but nothing here needs a dimension). The state is the pair $z=(v,x)\in H\times H$ with $v=\dot{x}$. The four operators $M,D,K,M^{-1}$ are continuous linear maps $H\to H$. The first-order form of the loop is the field

$$f(v,x)=(-M^{-1}(Dv+Kx),v),$$

and the storage function is the mechanical energy (eq 37 / eq 4.15, CoM block)

$$V(v,x)=\frac{1}{2}⟨v,Mv⟩+\frac{1}{2}⟨x,Kx⟩.$$

We use Mathlib’s Flow ℝ (H × H) and the L3 interface IsSolutionTo ϕ f (“every orbit of $\phi$ solves $\dot{z}=f(z)$ orbit-wise”), exactly as in LaSalle.lean.

2. The energy-dissipation identity — com_dissipation (proved outright)

Theorem. For $M,K$ symmetric and $M\circ M^{-1}=\mathrm{id}$,

$$DV(z)[f(z)]=-⟨v,Dv⟩,v=z_1.$$

Derivation. $\nabla V=(Mv,Kx)$ (symmetry of $M,K$ makes the $\frac{1}{2}(S+S^{\top })=S$ collapse exact), so

$$\dot{V}=⟨Mv,-M^{-1}(Dv+Kx)⟩+⟨Kx,v⟩=-⟨v,Dv+Kx⟩+⟨Kx,v⟩=-⟨v,Dv⟩-⟨v,Kx⟩+⟨v,Kx⟩=-⟨v,Dv⟩.$$

The first equality uses $⟨Mv,M^{-1}w⟩=⟨v,w⟩$ (self-adjointness of $M$ plus $M{M}^{-1}=\mathrm{id}$); the cross terms cancel because $⟨Kx,v⟩=⟨v,Kx⟩$ (symmetry of $K$). SymPy-pinned two ways in pin_com_lasalle.py: symbolically on fully symbolic $2\times 2$ $M,D,K$ (simplify returns exactly $0$), and numerically on random SPD blocks up to $n=9$ (residual $<10^{-12}$).

Lean route. V splits as $\frac{1}{2}⟨{\pi }_1\cdot ,M{\pi }_1\cdot ⟩+\frac{1}{2}⟨{\pi }_2\cdot ,K{\pi }_2\cdot ⟩$. Each block’s Fréchet derivative is Mathlib’s fderiv_inner_apply (derivative of $t\mapsto ⟨ft,gt⟩$) composed through the continuous projections ${\pi }_1,{\pi }_2$ (hasFDerivAt_fst/​snd) and the continuous operators $M,K$; fderiv_add / fderiv_const_mul assemble them. The resulting four inner products are reduced with $M,K$ symmetry (hMsa,hKsa), $M{M}^{-1}=\mathrm{id}$ (hMinv), real_inner_comm, inner_add_right, inner_neg_*; a final ring cancels the crossed $⟨v,Kx⟩$.

Corollary com_decrease. $DV(z)[f(z)]=-⟨v,Dv⟩\le 0$, since $D⪰0$ (hDnn). This is the negative-semidefinite decrease LaSalle consumes — flat on $\{v=0\}$, which is exactly why the bare comparison/Grönwall layer (L2) cannot finish and the invariance engine is needed.

3. The LaSalle collapse — com_collapse (the headline, proved outright)

Theorem. Let $S$ be any set invariant under the flow with $DV[f]=0$ on $S$. Then $S\subseteq \{0\}$.

This is the “largest invariant set” step. The zero set of the dissipation is $\{v=0\}$, which is not a single point — the collapse needs invariance, and this is precisely the content L3’s lasalle supplies (its ω-limit output is invariant) and that propIV1_tendsto discards (it consumed only the zero-set containment). Here we use invariance in full.

Derivation. Take $y\in S$.

1. Velocity vanishes on $S$. For every $w\in S$, com_dissipation turns $DV(w)[f(w)]=0$ into $⟨w_1,D{w}_1⟩=0$, and $D$ positive-definite (hDdef) gives $w_1=0$. In particular $y_1=0$, and along the whole orbit through $y$ (which stays in $S$ by invariance) the velocity component is identically $0$.

2. Acceleration vanishes. The map $s\mapsto ({\phi }_{s}y{)}_1$ is therefore the constant $0$, so its derivative at $s=0$ is $0$. But IsSolutionTo plus the chain rule through ${\pi }_1$ compute that same derivative as $(f(y){)}_1$. Uniqueness of derivatives (HasDerivAt.unique) gives $(f(y){)}_1=0$.

3. Position vanishes. With $y_1=0$, $(f(y){)}_1=-M^{-1}(D\cdot 0+K{y}_2)=-M^{-1}(K{y}_2)$. So $M^{-1}(K{y}_2)=0$; $M^{-1}$ is injective (it has $M$ as a left inverse, hMinv), so $K{y}_2=0$; $K$ injective (hKdef, from $K\succ 0$) gives $y_2=0$.

Hence $y=(0,0)=0$. $\square$

Step 2 mirrors the derivative-uniqueness argument in the sealed lasalle proof (the $\dot{V}=0$-on-ω-limit conjunct), reused here on the velocity projection instead of on $V$.

4. Global asymptotic stability — com_gas (the deliverable)

Theorem. For a flow $\phi$ solving $\dot{z}=f(z)$ with precompact orbit closure, every trajectory converges to the origin:

$${\phi }_t{z}_0⟶0(t\to +\infty ).$$

Proof. com_decrease gives $DV[f]\le 0$ everywhere and comEnergy_differentiable gives $V\in C^1$, so the sealed lasalle (L3) returns a nonempty invariant ω-limit set on which $DV[f]=0$. com_collapse places that set inside $\{0\}$, i.e. ${\omega }^{+}(z_0)\subseteq \{0\}$. The sealed reduction engine tendsto_infDist_of_omegaLimit_subset (L4a) then gives $\mathrm{infDist}({\phi }_t{z}_0,\{0\})\to 0$; since $\mathrm{infDist}(\cdot ,\{0\})=\mathrm{dist}(\cdot ,0)$ (Metric.infDist_singleton), this is ${\phi }_t{z}_0\to 0$. $\square$

This is the driver’s global attractivity — the Corollary 12 input — proved rather than assumed. (Global attractivity is the operative half; Lyapunov stability of the origin is the coercivity clause discussed in §5. “Asymptotic stability” in the paper’s cascade sense is the attractivity-to-the-invariant-set statement com_gas delivers.)

5. Interfaces, honestly (ponytail)

Proved outright: the dissipation identity (§2), the decrease, the LaSalle collapse (§3), and the GAS assembly (§4). The following are named hypotheses, never sorry — the L3/L4a IsSolutionTo/hStable precedent:

• IsSolutionTo ϕ f — existence of a flow solving the ODE. Picard–Lindelöf / completeness on the region of interest stays applier-side, exactly as in LaSalle.lean §sub-phase (i).
• hcpt — precompactness of the (two-sided) orbit closure. This is the same hypothesis the sealed lasalle and propIV1_tendsto already carry, and it is kept here for consistency. Note the honest subtlety: coercivity of $V$ bounds the forward orbit only ($V$ is nonincreasing forward, and $V(v,x)\ge c_1(\Vert v{\Vert }^2+\Vert x{\Vert }^2)$ with $c_1=\frac{1}{2}\min ({\lambda }_{\min }M,{\lambda }_{\min }K)$ — this is exactly the sealed Leanpunov.blockLyap_coercive). Mathlib’s Flow ℝ is two-sided, and a stable system’s backward orbit is unbounded, so full two-sided precompactness is genuinely more than forward coercivity yields. The clean discharge is a semiflow refactor of the L3 engine (forward-only ω-limits), after which blockLyap_coercive closes hcpt outright; that refactor is out of this target’s scope. So hcpt remains the established interface, and blockLyap_coercive is cited as the forward-boundedness witness.
• Operator positive-definiteness/symmetry — hMsa,hKsa (symmetry), hMinv ($M$ invertible), hDnn/hDdef ($D⪰0$, definite), hKdef ($K$ injective). For a concrete symmetric positive-definite matrix these are not assumptions but theorems, discharged by the sealed campaign: Leanpunov.le_dotProduct_mulVec (Rayleigh) gives $⟨v,Dv⟩\ge 0$; Matrix.PosDef definiteness gives hDdef; PosDef.isUnit + mulVec_injective_of_isUnit (the StiffnessResidual pattern) gives hKdef; and $M^{-1}$ is M.nonsingularInverse. The abstract operator statement is stated on an inner-product space because that is where the derivative of the quadratic form is clean (fderiv_inner_apply); a symmetric PosDef matrix on EuclideanSpace is the intended instance, and a matrix-corollary that mechanically discharges the six hypotheses is a bounded follow-up (it needs only the Matrix.toEuclideanCLM bridge already used in Rayleigh.quadSandwich_matrix).

6. Mathlib stones used

HasFDerivAt.inner / fderiv_inner_apply (derivative of an inner product), hasFDerivAt_fst/_snd, fderiv_add, fderiv_const_mul, HasFDerivAt.comp_hasDerivAt (chain rule through a projection), HasDerivAt.unique, real_inner_comm, inner_add_right, inner_neg_left/right, Metric.infDist_singleton, tendsto_iff_dist_tendsto_zero. Sealed leanpunov stones reused by name: lasalle (L3), tendsto_infDist_of_omegaLimit_subset (L4a), the IsSolutionTo interface (L3).

7. Cost feel

Comparable to a large L2-scale push: one genuinely new computation (the bilinear/​quadratic-form fderiv, §2 — no in-repo precedent, resolved with fderiv_inner_apply) plus a collapse that reuses the L3 derivative-uniqueness pattern, then a short assembly on the sealed engine. Well inside the stall gate; no fix cycle exceeded a single tactic edit.

8. The machine seal

#print axioms on the four sealed theorems, verbatim from the full-integration lake build (2640 jobs, 2026-07-06):

info: Leanpunov/ComLaSalle.lean:238:0: 'Leanpunov.com_dissipation' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/ComLaSalle.lean:239:0: 'Leanpunov.com_decrease' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/ComLaSalle.lean:240:0: 'Leanpunov.com_collapse' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/ComLaSalle.lean:241:0: 'Leanpunov.com_gas' depends on axioms: [propext, Classical.choice, Quot.sound]

Nothing beyond {propext, Classical.choice, Quot.sound}; no sorryAx. The full project (L1–L4a + TARGET 1, 19 theorems) builds clean.