cascade

The Panteley–Loría cascade theorem — engine + instantiation (R4)

Seal

Rung rung-4 · Status interfaced — axiom-clean (#print axioms verbatim in 7. The machine seal; per-file build 2452 jobs, 2026-07-08), resting on the named cascade interfaces hsand (the 𝒦∞ sandwich) and hdi (the eq-35 interconnection inequality), the applier-side regularity hvc/hv, and — in the instantiation — the sealed com_gas interface (IsSolutionTo, hcpt, and the CoM operator hypotheses). See interfaces.
Links: module index · interface ledger · substrate comparison_functions, time_varying_comparison · driving stone com_lasalle · driven stone coupled_collapse · sources panteley2001growth, panteley1998global, giordano2019coordinated · pin pin_cascade.py

Sealed theorems

tendsto_zero_of_sandwich

The class-𝒦∞ squeeze: α ∈ 𝒦∞, α‖x t‖ ≤ w t eventually and w → 0 force x t → 0. The ISS-standard “Lyapunov value decays ⇒ state decays”, proved by inverting the lower sandwich on the sealed classKInv.

cascade_gas

The engine (attractivity). A vanishing driving output plus the reshaped sandwich (eq 10/13) plus the interconnection inequality (eq 35) drive the joint cascade state $(x_1{x}_2)$ to the origin.

cascade_bounded

Lemma 2’s boundedness / UGS half (eq 39): a bounded driving output keeps the reshaped Lyapunov value inside the ultimate bound $V(x_{1}0)+c{M}_x/a$.

propIV1_cascade_gas

The instantiation — a second, independent kernel-checked route to Prop IV.1’s conclusion: the sealed com_gas discharges the driving CoM loop, the coupled block is the driven subsystem, and the full closed-loop state converges.

What this seals, in one paragraph

Giordano’s Proposition IV.1 (giordano2019coordinated §IV) closes the loop by a cascade argument: the decoupled CoM-error loop is autonomously stable and drives the coupled base+end-effector block through the interconnection term. This module formalizes the cascade stability theorem those authors invoke — Panteley–Loría — in the exact form the sources state it, and then instantiates it with the sealed CoM-loop GAS (com_lasalle com_gas) as the driving subsystem. The result is a second, independent route to Prop IV.1’s conclusion that the full closed-loop state reaches the origin: the first route (coupled_gas, coupled_collapse) runs LaSalle on the coupled field directly; this one runs the cascade theorem with the CoM loop as the driver. The engine is cheap and honest because Panteley’s own proof of Lemma 2 rides a differential inequality (eq 35) that is exactly the shape the already-sealed comparison layer (time_varying_comparison) consumes, and the “Lyapunov value → 0 ⇒ state → 0” step is exactly the sealed 𝒦∞ inverse (comparison_functions).

The module is (/Code/vault/lean/Cascade.lean), build copy ~/lean/ctrllib/Ctrllib/Cascade.lean. SymPy/NumPy pin: (/Code/vault/lean/pin_cascade.py).

1. The source statements, verbatim

The two sources study the time-varying cascade (panteley2001growth eq 1–2; panteley1998global eq 4–5)

$${\Sigma }_1:{\dot{x}}_1=f_1(t{x}_1)+g(tx)x_2{\Sigma }_2:{\dot{x}}_2=f_2(t{x}_2)$$

with $x_1\in {\mathbb{R}}^n$ the driven state, $x_2\in {\mathbb{R}}^m$ the driving state, and $g(tx)x_2$ the interconnection. The driving subsystem ${\Sigma }_2$ is autonomous; its output $x_2(t)$ perturbs ${\Sigma }_1$.

The comparison-function notation (panteley2001growth, Notation; the substrate of comparison_functions). $\alpha \in \mathcal{K}$ iff continuous, strictly increasing, $\alpha (0)=0$; $\alpha \in {\mathcal{K}}_{\infty }$ iff in addition $\alpha (s)\to \infty$; $\beta \in \mathcal{K}\mathcal{L}$ iff $\beta (\cdot t)\in \mathcal{K}$ and $\beta (s\cdot )\in \mathcal{L}$.

The assembly lemma, quoted verbatim (panteley2001growth, Lemma 2):

Lemma 2. If systems (2) and (4) are UGAS and the solutions of (1) and (2) are globally uniformly bounded then (1) and (2) is UGAS.

Here (4) is the zero-input driven system ${\dot{x}}_1=f_1(t{x}_1)$. This is the non-autonomous form of "$\mathrm{GAS}+\mathrm{GAS}+\mathrm{BS}\Rightarrow \mathrm{GAS}$". The paper’s own remark: “From Lemma 2 it is clear that Theorems 3–5 follow if we prove for each case, that the solutions of the system are globally uniformly bounded.”

The reshaped Lyapunov function (panteley2001growth, Proposition 1). UGAS of (4) yields (converse Lyapunov) a ${\mathcal{C}}^1$ function $\mathcal{V}(t{x}_1)$ with ${\bar{\alpha }}_1{\bar{\alpha }}_2\in {\mathcal{K}}_{\infty }$, ${\bar{\alpha }}_4\in \mathcal{K}$ such that

$${\bar{\alpha }}_1(\Vert x_1\Vert )\le \mathcal{V}(t{x}_1)\le {\bar{\alpha }}_2(\Vert x_1\Vert )\text{\hspace{1em}(13)}$$ $${\dot{\mathcal{V}}}_{(4)}(t{x}_1)\le -\mathcal{V}(t{x}_1)\text{\hspace{1em}(14)}$$ $$\Vert \partial \mathcal{V}/\partial x_1\Vert \le {\bar{\alpha }}_4(\Vert x_1\Vert )\text{\hspace{1em}(15)}$$

The interconnection inequality, quoted verbatim (panteley2001growth, proof of Lemma 2, eq 35). Writing $v(t):=\mathcal{V}(t{x}_1(t))$, using (15), (14) and the linear growth bound (19),

$${\dot{v}}_{(1)}(t)\le -v(t)+c(r)\Vert x_2(t)\Vert \text{\hspace{1em}(35)}$$

where $c(r):=c_g(r){\bar{\alpha }}_4(\bar{c}(r)){\alpha }_5(\bar{c}(r))$ depends on the a-priori bound $r$ of the (globally uniformly bounded) trajectory. The companion paper gives the same object as eq 22, ${\dot{V}}_{(4)}(tx)\le {\alpha }_v\Vert x_2(t)\Vert$.

OCR note. Both markdown renders (Docs/raw/md/) carry the equations above cleanly; the 1998 render mangles some inline sub/superscripts in the running prose (e.g. x\_ <sup>1</sup>) but every displayed equation used here is intact and cross-checked between the two sibling papers. No statement below rests on a garbled line.

2. The engine — from eq 35 to cascade attractivity

The whole content of Lemma 2’s attractivity is that eq 35 is a scalar comparison inequality with a vanishing forcing term, because ${\Sigma }_2$ UGAS gives $\Vert x_2(t)\Vert \to 0$ (indeed $\Vert x_2(t)\Vert \le \beta (\Vert x_{20}\Vert t-t_0)$, $\beta \in \mathcal{K}\mathcal{L}$, eq 17). We formalize it at the trajectory level, which is both faithful to the source (it works with the solution functions $x_1(t)x_2(t)$) and the natural match for the library’s autonomous _gas stones.

Theorem cascade_gas. Let $a>0$, ${\alpha }_1\in {\mathcal{K}}_{\infty }$, and along the composite trajectory let $v(t)=V(x_1(t))$ satisfy the lower sandwich ${\alpha }_1(\Vert x_1(t)\Vert )\le V(x_1(t))$ (from eq 10/13), be continuous and right-differentiable, and obey

$$v^{\prime }(t)\le -aV(x_1(t))+c\Vert x_2(t)\Vert \forall t\ge 0\text{\hspace{1em}(eq 35, a=1 rescaled to a)}$$

If the driving output vanishes, $x_2(t)\to 0$, then the joint state converges,

$$(x_1(t)x_2(t))⟶0(t\to \infty )$$

Proof. Three moves, each a sealed stone.

1. The disturbance vanishes. $x_2\to 0$ gives $\Vert x_2(t)\Vert \to 0$ (continuity of the norm), so $\epsilon (t):=c\Vert x_2(t)\Vert \to 0$.
2. The Lyapunov value decays. The lower sandwich gives $0\le {\alpha }_1(\Vert x_1\Vert )\le V(x_1)$, so $v\ge 0$ — nonnegativity is read off the sandwich, not assumed. Then the sealed comparison_tendsto_zero (time_varying_comparison) — ”$v^{\prime }\le -av+\epsilon$, $v\ge 0$, $\epsilon \to 0$, $a>0$ ⇒ $v\to 0$” — gives $V(x_1(t))\to 0$.
3. The state decays. tendsto_zero_of_sandwich: from ${\alpha }_1(\Vert x_1(t)\Vert )\le V(x_1(t))\to 0$ and ${\alpha }_1\in {\mathcal{K}}_{\infty }$, invert — $\Vert x_1(t)\Vert \le {\alpha }_1^{-1}(V(x_1(t)))\to {\alpha }_1^{-1}(0)=0$ — so $x_1(t)\to 0$.

Pair $x_1\to 0$ with $x_2\to 0$ (Tendsto.prodMk_nhds) for the joint limit. $\square$

The 𝒦∞ squeeze in detail (tendsto_zero_of_sandwich, the one genuinely new lemma). We need: $\alpha \in {\mathcal{K}}_{\infty }$, $\alpha \Vert x_t\Vert \le w_t$ eventually, $w\to 0$ ⇒ $x_t\to 0$. The sealed comparison_functions gives the partial inverse classKInv α and proves it is again class 𝒦∞ (classKInv_isClassKInfinity) — hence continuous on $[0\infty )$, strictly increasing, with ${\alpha }^{-1}(0)=0$ — and a genuine left inverse (classKInv_leftInvOn, ${\alpha }^{-1}(\alpha s)=s$ for $s\ge 0$). Then for each $t$ in the eventual set: $\Vert x_t\Vert \ge 0$ and $\alpha \Vert x_t\Vert \ge 0$ (class-𝒦 nonneg), so $w_t\ge \alpha \Vert x_t\Vert \ge 0$; applying the monotone ${\alpha }^{-1}$ to $\alpha \Vert x_t\Vert \le w_t$ and collapsing the left side with the left-inverse identity gives $\Vert x_t\Vert \le {\alpha }^{-1}(w_t)$. The upper bound ${\alpha }^{-1}(w_t)\to {\alpha }^{-1}(0)=0$ by continuity of ${\alpha }^{-1}$ at $0$ within $[0\infty )$ (composing $w\to 0$, which stays in $[0\infty )$ eventually). The norm squeeze squeeze_zero_norm' finishes: $\Vert x_t\Vert$ is trapped between $0$ and a null sequence, so $x_t\to 0$. SymPy-pinned (pin_cascade.py A) on $\alpha (s)=s^2$: left-inverse $\sqrt{s^2}=s$, ${\alpha }^{-1}(0)=0$, monotone — the exact facts the Lean rides.

The boundedness half (cascade_bounded, Lemma 2’s UGS content, eq 39). With a bounded driving output $\Vert x_2\Vert \le M_x$ instead of a vanishing one, the sealed comparison_bounded gives the ultimate bound $V(x_1(t))\le V(x_{1}0)+c{M}_x/a$ directly. With properness of $V$ (the upper sandwich $V\le {\alpha }_2(\Vert x_1\Vert )$, eq 10) this is the uniform global boundedness Lemma 2 assumes and the paper’s eq 39 delivers. We record it at the Lyapunov level.

Why “GAS” here means global attractivity. As with the library’s other _gas stones (com_gas, coupled_gas), the operative deliverable is the global-attractivity conjunct $(x_1{x}_2)\to 0$; the uniform-stability conjunct is the sandwich/boundedness clause (cascade_bounded), exactly the split the sources make (UGS from eq 39, attractivity from the vanishing-forcing argument). No ε–δ stability is silently claimed.

3. ISS — deliberately absent

panteley2001growth Theorem 3 additionally concludes that ${\Sigma }_1$ is ISS w.r.t. $x_2$, but only Theorem 4 (majorization) is needed for cascade GAS, and its proof uses only the differential inequality — never the ISS characterization. Per the ratified done-bar (“ISS definitions ONLY where the theorem needs them”), this module introduces no ISS predicate. The engine is the Theorem-4 route.

4. The instantiation — com_gas as the driving subsystem

The physical decomposition (Docs/CLAUDE.md; current_sota §4.3): the com loop is the decoupled $3\times 3$ CoM-error block, inertially free and autonomously stable — the driving ${\Sigma }_2$. The coupled base+end-effector block $\breve{\mathbf{M}}$ receives the CoM error through the interconnection — the driven ${\Sigma }_1$.

Theorem propIV1_cascade_gas. Take the sealed CoM-loop hypotheses (a flow ${\phi }_c$ solving the CoM field with precompact orbit and the SPD operator facts). Then com_gas (com_lasalle) proves the driving output $x_2(t)={\phi }_c(t{z}_0)\to 0$ outright — this is the genuine kernel discharge. Feed it, together with the driven coupled block’s reshaped Lyapunov data (sandwich hsand, inequality hdi), into cascade_gas. Conclusion:

$$(x_1(t){\phi }_c(t{z}_0))⟶0$$

the convergence of the full closed-loop state — Prop IV.1’s conclusion, reached through the cascade.

What is genuinely discharged vs. named. The driving subsystem’s GAS is discharged with no residue by the sealed com_gas — the headline of the instantiation. The driven subsystem enters through two named interfaces, hsand and hdi, whose justification is itself sealed elsewhere: the coupled block’s zero-input GAS is coupled_gas (coupled_collapse), which is exactly Proposition 1’s premise for the existence of the reshaped $\mathcal{V}$ (eq 13–15) and thence eq 35. So both stones the charter names appear — com_gas as the Lean-wired driver, coupled_gas as the documented justification for the driven reshaping — and nothing is silently substituted.

Independence from the coupled_gas route. coupled_gas reaches the coupled origin by LaSalle on the coupled field. propIV1_cascade_gas reaches the joint origin by the cascade theorem, the driven convergence coming from the comparison/growth argument driven by the CoM loop — a different assembly resting on a different engine. Two independent kernel-checked routes to the same physical conclusion.

5. Interfaces, honestly (ponytail)

Proved outright: the 𝒦∞ squeeze (§2), the cascade attractivity assembly (§2), the boundedness bound (§2), and the driving discharge via com_gas (§4). Named hypotheses, never sorry:

• hsand — the class-𝒦∞ lower sandwich ${\alpha }_1(\Vert x_1\Vert )\le V(x_1)$ (eq 10/13). For Proposition 1’s reshaped $\mathcal{V}$ it is a converse-Lyapunov theorem; here the named modelling input. The comparison_functions substrate makes ${\alpha }_1$ and its inverse first-class.
• hdi — the interconnection differential inequality $v^{\prime }\le -aV(x_1)+c\Vert x_2\Vert$ (eq 35). It bundles the reshaped decrease (eq 14), the linear growth bound (A5/eq 19), and the a-priori boundedness that Theorem 4/5’s forward-completeness argument (the $\int \mathrm{d}s/{\alpha }_6=\infty$ non-escape) establishes upstream — the same status time_varying_comparison gives its hbound (“the honest input, exactly the object Panteley–Loría integrate”).
• hvc hv — continuity and right-differentiability of $V\circ x_1$; applier-side chain-rule regularity, as in time_varying_comparison.
• (instantiation) IsSolutionTo hcpt and the CoM operators hMsa/hKsa/hMinv/hDnn/hDdef/hKdef — the sealed com_gas interface, discharged for concrete SPD blocks exactly as com_lasalle documents.

6. Mathlib stones used

Tendsto.norm, Tendsto.const_mul, Tendsto.prodMk_nhds, squeeze_zero_norm', ContinuousOn.continuousWithinAt, tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within, norm_nonneg, mul_le_mul_of_nonneg_left. Sealed ctrllib stones reused by name: comparison_tendsto_zero, comparison_bounded (L2 time-varying), classKInv with classKInv_isClassKInfinity/classKInv_leftInvOn (class-𝒦), com_gas (rung-1).

7. The machine seal

#print axioms on the four sealed theorems, verbatim from the per-file lake build (2452 jobs, 2026-07-08):

info: Ctrllib/Cascade.lean:222:0: 'Ctrllib.IsClassKInfinity.tendsto_zero_of_sandwich' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Ctrllib/Cascade.lean:223:0: 'Ctrllib.cascade_gas' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Ctrllib/Cascade.lean:224:0: 'Ctrllib.cascade_bounded' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Ctrllib/Cascade.lean:225:0: 'Ctrllib.propIV1_cascade_gas' depends on axioms: [propext, Classical.choice, Quot.sound]

Nothing beyond {propext, Classical.choice, Quot.sound}; no sorryAx. The pin (pin_cascade.py) is green: the 𝒦∞ inverse squeeze, the driving-vanishing assembly, and Panteley Example 2 (x1 x2 → 0, eq 35 satisfied with $a=2$, $c(r)=2.25$).

8. Cost feel

One genuinely new lemma (the 𝒦∞ squeeze — no in-repo precedent, resolved with classKInv_isClassKInfinity + squeeze_zero_norm'), then two short assemblies on the sealed comparison layer and one on com_gas. Two fix cycles total: a (0,0)-vs-0 product-limit coercion and a deprecated left_mem_Ici. Well inside the stall gate.