reduction_cascade

The El-Hawwary–Maggiore reduction step, formalized — L4a

Seal

Rung L4a · Status interfaced — axiom-clean (#print axioms verbatim in 6. The machine seal), with the two EHM Appendix-A topology cores as named hypotheses: hStable (Theorem 6 $\epsilon$–$\delta$ set stability) and hLandsInΓ₁ (Theorem 8 / Lemma 22 relative-attraction collapse), plus the application-specific hzero and the L3 IsSolutionTo/hcpt pair. See interfaces. Public definitions: StableSet, AttractiveSet, AsymStableSet, StableRelativeTo, AttractiveRelativeTo, AsymStableRelativeTo, LocallyStableNear, LocallyAttractiveNear, LUBNear (EHM Defs 3–5).
Links: module index · interface ledger · related lasalle_invariance, com_lasalle, coupled_collapse, stiffness_residual · sources elhawwary2013reduction (no wiki page yet), giordano2019coordinated

Sealed theorems

tendsto_infDist_of_omegaLimit_subset

The reduction engine, proved outright: precompact orbit and ${\omega }^{+}(x_0)\subseteq \Gamma$ give $\mathrm{infDist}({\phi }_t{x}_0,\Gamma )\to 0$.

reduction_asymptotic_stability

EHM Theorem 10 (compact branch) as an honest assembly: hStable + hLandsInΓ₁ fed through the engine yield AsymStableSet.

propIV1_tendsto

Prop IV.1’s attractivity conclusion: LaSalle’s output carried through hzero and the engine to convergence toward ${\Gamma }_1$.

What this seals, in one paragraph

The framing paper’s Proposition IV.1 (Giordano 2019, §IV.D) proves the invariant set $\bar{\mathbf{z}}$ asymptotically stable by a cascade argument that closes, verbatim, with “Applying LaSalle to (34b), $\breve{v}\equiv 0$ implies $\tilde{x}=0$” and cites “cascade theorems for compact invariant sets [13]”, where [13] is El-Hawwary & Maggiore’s reduction theorems. L3 sealed the LaSalle engine (~/Code/vault/lean/lasalle_invariance.md). L4a seals the step that carries LaSalle’s output — an invariant set on which the Lyapunov derivative vanishes — to the paper’s actual conclusion: the trajectory converges to the invariant target $\bar{\mathbf{z}}$. That carrying step is the reduction engine tendsto_infDist_of_omegaLimit_subset, proved outright; the full El-Hawwary–Maggiore Theorem 10 is stated as an honest assembly consuming its Appendix-A topological cores as named hypotheses, exactly the L3 IsSolutionTo interface precedent.

The module is (/Code/vault/lean/Reduction.lean), build copy ~/lean/leanpunov/Leanpunov/Reduction.lean. Verbatim ground for every quoted El-Hawwary–Maggiore statement is (/Code/tasks/streams/leanpunov/ehm_extraction.md); the raw source is bibkey elhawwary2013reduction, (~/Code/Docs/raw/md/elhawwary2013reduction/elhawwary2013reduction.md).

1. The mathematical object

We work with a Mathlib Flow ℝ E on a real normed space $E$, written $\phi$, and the point-to-set distance $\mathrm{infDist}(x,\Gamma )={\inf }_{y\in \Gamma }\mathrm{dist}(x,y)$ (Metric.infDist). “The trajectory from $x_0$ converges to $\Gamma$” is $\mathrm{infDist}({\phi }_t{x}_0,\Gamma )\to 0$ as $t\to +\infty$, i.e. Tendsto (fun t => Metric.infDist (ϕ t x₀) Γ) atTop (𝓝 0). EHM’s ball notation $B_{\delta }(\Gamma )$ is the sublevel set $\{x:\mathrm{infDist}(x,\Gamma )<\delta \}$; membership $x\in B_{\delta }(\Gamma )$ is the predicate $\mathrm{infDist}(x,\Gamma )<\delta$.

The $\omega$-limit set of the point orbit is ${\omega }^{+}(x_0)$ (ω⁺ ϕ.toFun {x₀}), the Mathlib omegaLimit atTop. L3 delivered, on this same substrate, the attraction fact this file consumes:

eventually_mem_of_omegaLimit_subset (LaSalle.lean:121): for a flow with precompact orbit closure and any open $u\supseteq {\omega }^{+}(x_0)$, the orbit is eventually inside $u$ — ${\forall }^{\infty }t,{\phi }_t{x}_0\in u$.

2. The reduction engine — proved

Theorem (tendsto_infDist_of_omegaLimit_subset). Let $\phi$ be a flow, $x_0$ a point whose forward orbit closure $\overline{\{{\phi }_t{x}_0:t\in \mathbb{R}\}}$ is compact, and $\Gamma \subseteq E$ any set with ${\omega }^{+}(x_0)\subseteq \Gamma$. Then $\mathrm{infDist}({\phi }_t{x}_0,\Gamma )\to 0$ as $t\to +\infty$.

Proof (the four lines the Lean proof runs). Fix $\epsilon >0$; by Metric.tendsto_atTop it suffices to find $N$ with $\mathrm{infDist}({\phi }_t{x}_0,\Gamma )<\epsilon$ for all $t\ge N$. The set $U_{\epsilon }=\{z:\mathrm{infDist}(z,\Gamma )<\epsilon \}$ is open, because $z\mapsto \mathrm{infDist}(z,\Gamma )$ is continuous (Metric.continuous_infDist_pt) and $U_{\epsilon }$ is a strict-sublevel set (isOpen_lt). It contains ${\omega }^{+}(x_0)$: any $y\in {\omega }^{+}(x_0)\subseteq \Gamma$ has $\mathrm{infDist}(y,\Gamma )=0<\epsilon$ (Metric.infDist_zero_of_mem). So L3’s eventually_mem_of_omegaLimit_subset gives ${\forall }^{\infty }t,{\phi }_t{x}_0\in U_{\epsilon }$; unfolding “eventually at $\text{atTop}$” produces the $N$, and $\mathrm{dist}(\mathrm{infDist}({\phi }_t{x}_0,\Gamma ),0)=\mathrm{infDist}({\phi }_t{x}_0,\Gamma )$ since $\mathrm{infDist}\ge 0$ (Metric.infDist_nonneg). $\square$

This is the textbook “the trajectory converges to (any set containing) its $\omega$-limit set” clause — the missing half-sentence between LaSalle’s invariant-set output and a convergence statement. No closedness of $\Gamma$ and no NormedSpace structure are used; only the metric and L3’s attraction stone.

3. The El-Hawwary–Maggiore statements (verbatim) and how L4a discharges them

All quotes are transcribed word-for-word in (~/Code/tasks/streams/leanpunov/ehm_extraction.md §3), which took them from the raw markdown; only symbol notation is rendered in LaTeX.

Theorem 10 (Asymptotic Stability — the RPAS solution), p.216

Let ${\Gamma }_1$ and ${\Gamma }_2$, ${\Gamma }_1\subset {\Gamma }_2\subset X$, be two closed positively invariant sets. Then, ${\Gamma }_1$ is (globally) asymptotically stable if the following conditions hold: (i) ${\Gamma }_1$ is (globally) asymptotically stable relative to ${\Gamma }_2$, (ii) ${\Gamma }_2$ is locally stable near ${\Gamma }_1$, (iii) ${\Gamma }_2$ is locally attractive near ${\Gamma }_1$ (${\Gamma }_2$ is globally attractive), (iv) if ${\Gamma }_1$ is unbounded, then $\Sigma$ is LUB near ${\Gamma }_1$, (v) (all trajectories of $\Sigma$ are bounded).

Theorem 10 is Theorem 6 (Stability) plus Theorem 8 (Attractivity); its proof of both halves is the paper’s Appendix A (the relative-stability machinery, Lemma 22). Proposition IV.1 uses only the compact-${\Gamma }_1$ branch: $\bar{\mathbf{z}}$ is compact because ${\mathbb{T}}^n$ is compact, so condition (iv)‘s LUB rider is vacuous and (v)‘s global boundedness is unused for the local claim.

What L4a proves vs. interfaces. The genuine topological reduction — that conditions (i)–(iii) upgrade relative asymptotic stability to full asymptotic stability — is EHM’s Appendix A and is beyond L4a’s stall gate; formalizing it in full is a project of its own, and a faithful-statement Theorem 10 whose proof simply reasserted its conclusion would be vacuous. Following the charter’s documented fallback and the L3 IsSolutionTo precedent, L4a instead states Theorem 10 as an assembly whose two Appendix-A cores enter as named hypotheses, and proves the reduction of attractivity to those cores through the engine of §2.

Theorem (reduction_asymptotic_stability). For a flow $\phi$ and set ${\Gamma }_1$, given

• hStable $:$ StableSet ϕ Γ₁ — the $\epsilon$–$\delta$ set stability (EHM Theorem 6, compact branch);
• hLandsInΓ₁ $:$ there is $\delta >0$ such that every $x$ with $\mathrm{infDist}(x,{\Gamma }_1)<\delta$ has precompact orbit closure and ${\omega }^{+}(x)\subseteq {\Gamma }_1$ — the relative-attraction collapse (EHM Theorem 8 core / Appendix-A Lemma 22, which places $\omega$-limits of near-${\Gamma }_1$ trajectories inside ${\Gamma }_1$),

then AsymStableSet ϕ Γ₁.

Proof. AsymStableSet unfolds to StableSet ∧ AttractiveSet; the first conjunct is hStable. For the second, take the $\delta$ of hLandsInΓ₁; for each $x$ in $B_{\delta }({\Gamma }_1)$ its orbit is precompact and ${\omega }^{+}(x)\subseteq {\Gamma }_1$, so the engine of §2 gives $\mathrm{infDist}({\phi }_{t}x,{\Gamma }_1)\to 0$ — that is AttractiveSet ϕ Γ₁. $\square$

The attractivity conclusion here is real reduction content produced by the engine, not an assumption; the two hypotheses are precisely the pieces EHM prove topologically, named and flagged rather than smuggled. The predicates StableSet, AttractiveSet, AsymStableSet, their relative forms StableRelativeTo / AttractiveRelativeTo / AsymStableRelativeTo (EHM Def 4), and LocallyStableNear / LocallyAttractiveNear (EHM Def 3), LUBNear (EHM Def 5) are transcribed in the module’s T1 block in the $\epsilon$–$\delta$ form the definitions carry — for the record and to type the interface hypotheses.

Corollary 12 (Cascade-connected systems), p.216 — the operative citation

Moreover, ${\Gamma }_1$ is (globally) asymptotically stable if (iv) ${\tilde{\Gamma }}_1$ is (globally) asymptotically stable for $\dot{x}=f(x,0)$, (v) $y=0$ is a (globally) asymptotically stable equilibrium of $\dot{y}=g(y)$, (vi) if ${\Gamma }_1$ is unbounded, then (3) is LUB near ${\Gamma }_1$, (vii) (all trajectories of (3) are bounded).

Corollary 12 specializes Theorem 10 to the cascade $\dot{x}=f(x,y),\dot{y}=g(y)$ with ${\Gamma }_2=\{y=0\}$. For Prop IV.1 the identification (ehm_extraction §4) is $y\leftrightarrow {\mathbf{z}}_1$ (the Hurwitz CoM-error driver, eq 34a) and $x\leftrightarrow {\mathbf{z}}_2$ (the driven base+arm block, eq 34b–d), so $\dot{x}=f(x,0)$ is ${\dot{\mathbf{z}}}_2={\mathbf{g}}_2(0,{\mathbf{z}}_2)$ — exactly the subsystem LaSalle handles. Conditions (vi),(vii) are the two boundedness riders: (vi) is vacuous because $\bar{\mathbf{z}}$ is compact, (vii) is unused for the local claim. Corollary 12 is not separately formalized — it is Theorem 10 with ${\Gamma }_2=\{y=0\}$, and the assembly of §4 wires its content directly.

4. Proposition IV.1 assembly — wiring L3’s lasalle through the engine

Proposition IV.1’s second cascade step (Giordano 2019, eq 37–38) takes the Lyapunov function $V=\frac{1}{2}{\breve{\mathbf{v}}}^{\top }\breve{\mathbf{M}}\breve{\mathbf{v}}+\frac{1}{2}{\tilde{\mathbf{x}}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}$ with, verbatim,

$\dot{V}=\frac{1}{2}{\breve{\mathbf{v}}}^{\top }(\dot{\breve{\mathbf{M}}}-2\breve{\mathbf{C}})\breve{\mathbf{v}}-{\breve{\mathbf{v}}}^{\top }\breve{\mathbf{D}}\breve{\mathbf{v}}=-{\breve{\mathbf{v}}}^{\top }\breve{\mathbf{D}}\breve{\mathbf{v}}\le 0$

(the skew term $\dot{\breve{\mathbf{M}}}-2\breve{\mathbf{C}}$ vanishing is the sealed Leanpunov.passivity_identity), then closes with “Applying LaSalle to (34b), $\breve{v}\equiv 0$ implies $\tilde{x}=0$”.

L3’s lasalle (LaSalle.lean:71), for a flow solving $x^{\prime }=f(x)$ with differentiable $V$ satisfying $DV(y)[f(y)]\le 0$ everywhere and precompact orbit closure, returns among its conjuncts

$\forall y\in {\omega }^{+}(x_0),DV(y)[f(y)]=0.$

Theorem (propIV1_tendsto). For a flow $\phi$ solving $x^{\prime }=f(x)$ (IsSolutionTo ϕ f), a differentiable $V$ with $DV(y)[f(y)]\le 0$ for all $y$, a set ${\Gamma }_1$ with the zero-set containment

$\{y:DV(y)[f(y)]=0\}\subseteq {\Gamma }_1(\text{hypothesis }‘hzero‘),$

and a point $x_0$ with precompact orbit closure, the trajectory converges to ${\Gamma }_1$: $\mathrm{infDist}({\phi }_t{x}_0,{\Gamma }_1)\to 0$.

Proof. Apply lasalle; its fourth conjunct gives $DV(y)[f(y)]=0$ for every $y\in {\omega }^{+}(x_0)$, so by hzero every such $y$ lies in ${\Gamma }_1$, i.e. ${\omega }^{+}(x_0)\subseteq {\Gamma }_1$. The engine of §2 then gives $\mathrm{infDist}({\phi }_t{x}_0,{\Gamma }_1)\to 0$. $\square$

Why hzero is the honest interface, and what it stands for. The containment $\{DV[f]=0\}\subseteq {\Gamma }_1$ is exactly the paper’s ”$\breve{v}\equiv 0$ implies $\tilde{x}=0$” step, made precise. On the eq-38 field, $DV(y)[f(y)]=-{\breve{\mathbf{v}}}^{\top }\breve{\mathbf{D}}\breve{\mathbf{v}}$ with $\breve{\mathbf{D}}\succ 0$, so $DV[f]=0$ forces $\breve{\mathbf{v}}=0$. Substituting $\breve{\mathbf{v}}=0$ (and ${\tilde{\mathbf{x}}}_c=0$, the driver already zeroed on ${\Gamma }_2$) into the residual of the driven dynamics (34b) leaves ${\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}=0$; with $\breve{\mathbf{K}}\succ 0$ and ${\mathbf{J}}_{\tilde{x}}$ full column rank on the singularity-free region $\Omega$, the map $\tilde{\mathbf{x}}\mapsto {\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}$ is injective, so $\tilde{\mathbf{x}}=0$. Hence on the zero set $\breve{\mathbf{v}}=0$ and $\tilde{\mathbf{x}}=0$, which is exactly membership in $\bar{\mathbf{z}}={\Gamma }_1$ ($\mathbf{q}\in {\mathbb{T}}^n$ free). This chain uses the un-formalized closed-loop field ${\mathbf{g}}_2$, the positive-definiteness of $\breve{\mathbf{D}},\breve{\mathbf{K}}$, and the rank of ${\mathbf{J}}_{\tilde{x}}$ on $\Omega$ — none of which is a Flow ℝ E fact — so it enters as the named hypothesis hzero, in the same spirit as L3 kept Picard–Lindelöf existence out of the theorem body. propIV1_tendsto is therefore the machine-checked form of Prop IV.1’s attractivity conclusion, with the field-specific algebra flagged as its single interface.

5. Scope, honestly (ponytail)

• Proved outright: the reduction engine (§2), and the two assemblies (§3, §4) that carry it to AsymStableSet and to Prop IV.1’s convergence.
• Interfaced (named hypotheses, not sorry): the EHM Appendix-A topological core — the $\epsilon$–$\delta$ set stability hStable (Theorem 6) and the relative-attraction collapse hLandsInΓ₁ (Theorem 8 / Lemma 22) — and the application-specific zero-set containment hzero.
• Not built: Theorem 8’s global branch, the LUB machinery, and Proposition 14’s $l$-fold induction. Prop IV.1 needs one compact two-set reduction, not the hierarchy; building the rest would be speculative.

The interfaces are the genuine content of EHM’s Appendix and of the un-formalized dynamics; they are exposed in the theorem signatures and named here so the professor sees precisely where the machine check stops and the paper-level argument resumes.

6. The machine seal

#print axioms on the three sealed theorems, verbatim from the full integration lake build (2243 jobs, 2026-07-05):

info: Leanpunov/Reduction.lean:188:0: 'Leanpunov.tendsto_infDist_of_omegaLimit_subset' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/Reduction.lean:189:0: 'Leanpunov.reduction_asymptotic_stability' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/Reduction.lean:190:0: 'Leanpunov.propIV1_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound]

Nothing beyond {propext, Classical.choice, Quot.sound}; no sorryAx. The full project (L1–L4a, 15 theorems) builds clean at 2243 jobs.