lasalle_invariance

LaSalle’s invariance principle, formalized — L3 sub-phases (i), (ii), (iv)

The problem, and a surprise in the inventory

The framing paper’s stability proof does not close with a strict Lyapunov decrease. Its derivative (eq 38) is only negative semidefinite — $\dot{V}=-{\breve{\mathbf{v}}}^{\top }\breve{\mathbf{D}}\breve{\mathbf{v}}\le 0$, flat in the error directions — and the proof of Proposition IV.1 closes, verbatim, with “Applying LaSalle to (34b), $\breve{v}\equiv 0$ implies $\tilde{x}=0$”. L2 identified this invariance layer as the wall. This phase builds it.

The L2 recon summary said Lyapunov, passivity, LaSalle, and ISS are absent from Mathlib, and as named theories they are. But the L3 inventory read of Mathlib.Dynamics.Flow and Mathlib.Dynamics.OmegaLimit (2026-07-05) revised the picture in our favor: of the four stones LaSalle stands on, Mathlib already holds three —

1. Invariance of ω-limit sets: Flow.isInvariant_omegaLimit, proved at monoid level (any flow time-monoid whose translations preserve the filter), so it covers semiflows too.
2. Nonemptiness over a compact absorber: nonempty_omegaLimit_of_isCompact_absorbing.
3. Attraction — the orbit is eventually inside any open neighbourhood of its ω-limit set: eventually_mapsTo_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset.

What no library holds is the Lyapunov-specific pair: a converging Lyapunov function is constant on the ω-limit set, and — through the ODE — its derivative along the field vanishes there. Those two stones, plus the assembly, are this phase’s contribution. The result is, to our knowledge, the first LaSalle-shaped theorem sitting on Mathlib’s dynamics substrate; the heavy topology was already there, waiting for the control-theoretic keystone.

Sources and provenance

• giordano2019coordinated: Prop IV.1 statement (“The invariant set $\bar{z}=\{z\in \Omega :{\tilde{x}}_c={\hat{x}}_c=0,\tilde{x}=\tilde{v}=0\}$ is asymptotically stable”), eq 38, and the LaSalle + cascade invocations in its proof (verbatim quotes extracted 2026-07-05).
• Mathlib: Mathlib.Dynamics.Flow (flows as continuous monoid actions, IsInvariant), Mathlib.Dynamics.OmegaLimit (filter-parametric ω-limits and the three stones above), mem_omegaLimit_singleton_iff_mapClusterPt (membership = cluster point), tendsto_atTop_ciInf (antitone bounded convergence), antitone_of_deriv_nonpos (mean value), Gronwall/chain-rule machinery already used in L2.
• Terminology rows for $\omega$-limit set, flow/semiflow, invariant set, and the El-Hawwary–Maggiore reduction theorems: (~/Code/notes/terminology.md).

Sub-phase (i): the ODE-solutions-to-flow bridge — an interface, by design

To speak of ω-limit sets Mathlib wants a flow $\phi :\mathbb{R}\to E\to E$; to speak of Lyapunov derivatives the thesis wants the ODE $\dot{x}=f(x)$. The bridge could be a construction — Picard–Lindelöf existence, uniqueness, continuous dependence, completeness on the singularity-free region $\Omega$, all packaged into a Flow — and that is a formalization project of its own (Mathlib’s PicardLindelof provides local existence but no packaged flow; nothing connects ODE solutions to Flow).

We chose the interface instead:

$$\text{IsSolutionTo}\phi f:⟺\forall x,\forall t,\frac{d}{ds}{|}_{s=t}{\phi }_s(x)=f({\phi }_t(x))$$

— the flow is given and asserted to solve the ODE, orbitwise, with the derivative in Mathlib’s HasDerivAt sense. Everything downstream consumes only this Prop, through one chain-rule lemma (IsSolutionTo.hasDerivAt_comp, the L2 pattern). How such a flow arises on $\Omega$ — completeness of the closed-loop field, forward-only versus two-sided time — stays on the applier’s side, stated in the application, not smuggled into the theorem. This is the documented design choice: the theorem’s mathematical content is invariance-plus-constancy, not existence theory, and gluing a half-built existence layer underneath would have made the seal weaker, not stronger.

One honest limitation follows from using Mathlib’s Flow ℝ E: orbits are two-sided (the flow is defined for all real $t$, negative included), so applying lasalle to the thesis presumes completeness of the closed-loop field in both time directions on the region of interest. The mathematics of the proof never uses negative time except through Mathlib’s invariance lemma — which is proved at monoid level and instantiates equally at $t\in {\mathbb{R}}_{\ge 0}$ — and our constancy stone is filter-generic already, so a semiflow variant is a re-instantiation, not new mathematics.

Sub-phase (ii): the two new stones and the assembled principle

Stone 1 (constancy). Let $\phi :\tau \to \alpha \to \alpha$ be any family of maps on a topological space, $f$ a nontrivial filter on $\tau$, and $V:\alpha \to \mathbb{R}$ continuous with $V({\phi }_t(x_0))\to c$ along $f$. Then $V\equiv c$ on ${\omega }_f(x_0)$.

Proof. Membership in the ω-limit of a singleton is exactly the cluster-point property: $y\in {\omega }_f(x_0)$ iff ${\phi }_t(x_0)$ frequently visits every neighbourhood of $y$ (Mathlib’s mem_omegaLimit_singleton_iff_mapClusterPt). Since $V$ is continuous at $y$, the value $V(y)$ is then a cluster value of the net $t\mapsto V({\phi }_t(x_0))$. But that net converges to $c$, and in a Hausdorff space a convergent net has exactly one cluster value: the filter $\mathcal{N}(V(y))\sqcap \text{map}(V\circ {\phi }_{\cdot }(x_0))f$ is nontrivial and lies below $\mathcal{N}(V(y))\sqcap \mathcal{N}(c)$, which forces $V(y)=c$ by the T2 separation characterisation. $\square$

Note what is not needed: no flow structure, no compactness, no monotonicity — the stone is pure topology, which is why it slots under any future semiflow variant unchanged.

Stone 2 (derivative vanishing) and the assembly. Now take a flow $\phi$ with $\text{IsSolutionTo}\phi f$, a differentiable $V$ with $DV(y)[f(y)]\le 0$ everywhere (the weak-decrease instance of L2’s LyapunovDecrease), and a point $x_0$ whose orbit closure is compact. Then:

Theorem (lasalle). The set $\omega (x_0)$ is nonempty, invariant, $V$ is constant on it (with value ${\inf }_{t}V({\phi }_t(x_0))$), and $DV(y)[f(y)]=0$ for every $y\in \omega (x_0)$.

Proof. Along the orbit, $g(t)=V({\phi }_t(x_0))$ has derivative $DV[f]\le 0$ by the chain rule, so $g$ is antitone (antitone_of_deriv_nonpos); its range sits inside the continuous image of the compact orbit closure, hence is bounded below; an antitone function bounded below converges to its infimum (tendsto_atTop_ciInf). Stone 1 then makes $V$ constant on $\omega (x_0)$. Invariance and nonemptiness are Mathlib’s stones. For the vanishing: fix $y\in \omega (x_0)$; by invariance the whole orbit of $y$ stays in $\omega (x_0)$, where $V$ is constant — so $s\mapsto V({\phi }_s(y))$ is a constant function, whose derivative at $s=0$ is zero; but the chain rule computes that same derivative as $DV({\phi }_0(y))[f({\phi }_0(y))]=DV(y)[f(y)]$, and derivatives are unique. $\square$

Attraction (the classical principle’s convergence clause) is Mathlib’s third stone, specialized to point orbits as eventually_mem_of_omegaLimit_subset: the orbit eventually enters any open neighbourhood of $\omega (x_0)$. Together with lasalle this is LaSalle’s invariance principle in its textbook reading: the trajectory converges to the largest invariant subset of $\{y:DV(y)[f(y)]=0\}$ — “largest” needs no extra Lean, since lasalle delivers $\omega (x_0)$ itself as an invariant subset of that zero set and attraction delivers convergence to it.

Application shape for Prop IV.1 (eq 38). There $DV[f]=-{\breve{\mathbf{v}}}^{\top }\breve{\mathbf{D}}\breve{\mathbf{v}}$ with $\breve{\mathbf{D}}\succ 0$, so the vanishing conjunct forces $\breve{\mathbf{v}}=0$ on the ω-limit set — exactly the "$\breve{v}\equiv 0$" from which the paper concludes $\tilde{x}=0$ on the invariant set. That last implication (zero velocity forces zero error within the invariant set, using the closed-loop dynamics) is the remaining Prop IV.1-specific step; see the closing paragraph of the final report.

Sub-phase (iv): El-Hawwary–Maggiore versus the strict-decrease retreat — decided

The framing paper’s proof opens with “cascade theorems for compact invariant sets [13] apply”, where [13] is El-Hawwary & Maggiore, “Reduction theorems for stability of closed sets with application to backstepping control design”, Automatica 49(1):214–222, 2013. The corpus check (2026-07-05) is unambiguous: the paper is not on disk — it appears only as a bibliography line in two rendered sources. The house provenance bar forbids formalizing (or even paraphrasing) theorems whose source we cannot read. Decision, on that evidence: retreat. L3 delivers the LaSalle engine and the cascade-facing comparison layer (L2’s ultimate-bound corollary is precisely the strict-decrease cascade step in quantitative form); the reduction-theorem layer waits for the PDF. The unlock is a one-item user task on the stream board: fetch the El-Hawwary–Maggiore paper into Docs/sources/inbox/. No mathematics was substituted silently.

The machine seal

LaSalle.lean in this directory (build copy at ~/lean/leanpunov/Leanpunov/LaSalle.lean). Verbatim #print axioms (build 2026-07-05):

info: Leanpunov/LaSalle.lean:137:0: 'Leanpunov.eq_on_omegaLimit_of_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/LaSalle.lean:138:0: 'Leanpunov.lasalle' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/LaSalle.lean:139:0: 'Leanpunov.eventually_mem_of_omegaLimit_subset' depends on axioms: [propext, Classical.choice, Quot.sound]