A Class-K∞ Lower Bound for the Coupled Block Energy

At a glance

The cascade attractivity argument asks the driven block to carry a lower bound of the form ${\alpha }_1(\Vert x_1\Vert )\le V(x_1)$, where ${\alpha }_1$ is a class-$\mathcal K_\infty$ function and $V$ is the block’s energy. In the general theorem that inequality is an assumption taken as given — a modelling input reshaped from Panteley & Loría’s growth-rate lemma. This page proves that for the concrete positive-definite coupled block it is not an assumption at all: the block already owns a machine-checked quadratic lower bound on its energy, and this module turns that bound into exactly the required class-${\mathcal{K}}_{\infty }$ inequality, with witness ${\alpha }_1(s)=c_1{s}^2$. All three results are checked end to end by Lean’s kernel on the three standard axioms (propext, Classical.choice, Quot.sound), with no sorry and no open assumption. So the cascade module’s lower-sandwich hypothesis becomes, for the concrete block, a theorem its consumers may cite rather than assume.

This closes one hypothesis, not the cascade result $v^{\prime }\le -aV(x_1)+c\Vert x_2\Vert$ — stays an assumption taken as given by design: it is a converse-Lyapunov statement absent from Mathlib, and the block's natural energy decreases only semidefinitely, so no already-checked object supplies it. Because the cascade attractivity theorem needs both hypotheses, it is not closed by the work here. See Scope and limitations.

This module discharges the lower-sandwich hypothesis only. Its companion — the strict interconnection decrease

Links: module index · assumptions ledger · builds on the block Lyapunov candidate and the comparison-function algebra · serves the cascade attractivity theorem and the seven-degree-of-freedom null-space damping · sources panteley2001growth, giordano2019coordinated, khalil1996nonlinear.

Motivation

A cascaded system is one where a driving block evolves on its own and a driven block is forced by it. Panteley & Loría’s growth-rate theorem certifies that if the driving block tends to the origin and the driven block satisfies two structural conditions, then the whole joint state tends to the origin. The first of those two conditions is a lower bound on the driven block’s Lyapunov energy $V$: there must be a class-$\mathcal K_\infty$ function ${\alpha }_1$ — continuous, strictly increasing from zero, and growing without bound — for which

${\alpha }_1(\Vert x_1\Vert )\le V(x_1)$

holds along the driven trajectory $x_1$. In the abstract cascade theorem this is a modelling input: for a general reshaped Lyapunov function one obtains such an ${\alpha }_1$ only from a converse-Lyapunov construction, which is exactly why the cascade module records it as an assumption taken as given.

The point of this module is that our driven block is not general. It is the concrete base-plus-arm block whose energy is the quadratic form studied in the block Lyapunov module, and that module has already proved — and had the machine check — that the energy is bounded below by a strictly positive multiple of the squared state norm. A quadratic lower bound is a class-${\mathcal{K}}_{\infty }$ lower bound; the only work left is to say so precisely and wire the two facts together. Doing that converts the cascade’s lower-sandwich hypothesis, for this block, from an assumption into a theorem. It is bookkeeping in the best sense: a fact we already possess, restated in the exact shape a downstream consumer demands.

Why bother, if it does not by itself close the cascade result? Because a proof’s remaining open boundary is most informative when it is drawn as tightly as possible. Discharging the cheap half tells the reader precisely where the genuine open problem lives — in the decrease hypothesis, not the lower-bound hypothesis — and removes a modelling input that a pencil-and-paper reader would otherwise have to take on faith for the concrete block.

The objects

Work over the real numbers with two finite index sets $n$ and $m$ (physically $n=m=9$), both nonempty. The driven block’s state lives in the product Euclidean space ${\mathbb{R}}^n\times {\mathbb{R}}^m$ (in Lean, EuclideanSpace ℝ n × EuclideanSpace ℝ m). A stacked state is $\mathbf{y}=({\mathbf{y}}_1{\mathbf{y}}_2)$, whose two components ${\mathbf{y}}_1$ (the base block) and ${\mathbf{y}}_2$ (the arm block) are exactly the two arguments the block energy consumes.

The block energy is the value function of the block Lyapunov module (blockLyap),

$V(\mathbf{y})=\text{blockLyap}\mathbf{M}\mathbf{K}{\mathbf{y}}_1{\mathbf{y}}_2=\frac{1}{2}({\mathbf{y}}_1^{\top }\mathbf{M}{\mathbf{y}}_1)+\frac{1}{2}({\mathbf{y}}_2^{\top }\mathbf{K}{\mathbf{y}}_2)$

where $\mathbf{M}$ is a real $n\times n$ matrix and $\mathbf{K}$ a real $m\times m$ matrix, both taken positive-definite (Matrix.PosDef). The single fact we import from that module is its coercivity bound (blockLyap_coercive): there is a strictly positive constant $c_1$ with

$c_1({\mathbf{y}}_1\cdot {\mathbf{y}}_1+{\mathbf{y}}_2\cdot {\mathbf{y}}_2)\le V(\mathbf{y})c_1=\frac{1}{2}\min ({\lambda }_{\min }\mathbf{M}{\lambda }_{\min }\mathbf{K})$

for every pair of blocks, where ${\mathbf{y}}_1\cdot {\mathbf{y}}_1$ denotes the self dot product (Lean’s ⬝ᵥ). This bound is Lyapunov-candidate coercivity in the sense of Khalil, and it is the sole raw material for everything below.

One convention deserves a word, because it is where the argument does its real work. Mathlib equips the product space with the sup norm

$\Vert \mathbf{y}\Vert =\max (\Vert {\mathbf{y}}_1\Vert \Vert {\mathbf{y}}_2\Vert )$

(Prod.norm_def), not the Euclidean norm of the concatenation. We must therefore be careful: the class-${\mathcal{K}}_{\infty }$ inequality is stated in this sup norm, while the coercivity bound speaks of the two blocks separately. Reconciling the two is a small inequality about the maximum, and it goes the friendly way for a lower bound, as we will see.

The squaring map is class K∞ (isClassKInfinity_sq)

The witness we intend to use is ${\alpha }_1(s)=c_1{s}^2$, and before scaling by the constant $c_1$ we need the bare squaring map $s\mapsto s^2$ to be class ${\mathcal{K}}_{\infty }$.

Strategy

A class-${\mathcal{K}}_{\infty }$ function, in the definition the comparison-function module uses, is a real function that is continuous on the ray $[0,\infty )$, strictly increasing there, zero at the origin, and unbounded above. So the claim splits into four independent checks, one per clause, and each is a standard fact about squaring. The technique is direct construction: we simply hand the four properties to the record. This mirrors the identity map’s membership (isClassKInfinity_id) already in the comparison-function algebra, one entry over.

Proof

We verify the four defining clauses of IsClassKInfinity for $f(s)=s^2$.

Continuity. The squaring map is a polynomial, hence continuous everywhere; restricting to the ray gives continuity on $[0,\infty )$ ((continuous_pow 2).continuousOn).

Strict monotonicity on the ray. For $0\le a<b$ we have $a^2<b^2$, since squaring is strictly increasing on the nonnegatives (pow_lt_pow_left₀, with the hypothesis $0\le a$ read off membership in the ray). Thus $f$ is strictly increasing on $[0,\infty )$.

Value at the origin. Directly, $f(0)=0^2=0$ (norm_num).

Unboundedness. As $s\to \infty$ we have $s^2\to \infty$, because a positive power tends to infinity along with its base (tendsto_pow_atTop).

All four hold, so $s\mapsto s^2$ is class ${\mathcal{K}}_{\infty }$, as desired.

What this shows

This is the reusable building block. Scaling a class-${\mathcal{K}}_{\infty }$ function by a positive constant keeps it class ${\mathcal{K}}_{\infty }$ — that is the algebra’s IsClassKInfinity.const_mul — so ${\alpha }_1(s)=c_1{s}^2$ is class ${\mathcal{K}}_{\infty }$ the moment $c_1>0$, which coercivity guarantees. We now have our comparison function; the remaining work is to earn the inequality.

The pointwise coupled-block sandwich (blockLyap_classKInfinity_sandwich)

The central result of the module states that for positive-definite blocks the energy dominates a concrete class-${\mathcal{K}}_{\infty }$ function of the stacked-state norm:

$\exists {\alpha }_1\in {\mathcal{K}}_{\infty }\text{such that}{\alpha }_1(\Vert \mathbf{y}\Vert )\le V(\mathbf{y})\text{ for every stacked state }\mathbf{y}.$

The witness is ${\alpha }_1(s)=c_1{s}^2$ with $c_1$ the coercivity constant. This is the lower half of Panteley & Loría’s sandwich, delivered as a theorem rather than assumed.

Strategy

Work backward from the goal $c_1\Vert \mathbf{y}{\Vert }^2\le V(\mathbf{y})$. On the right, coercivity already gives us $c_1({\mathbf{y}}_1\cdot {\mathbf{y}}_1+{\mathbf{y}}_2\cdot {\mathbf{y}}_2)\le V(\mathbf{y})$. So it would suffice to know

$c_1\Vert \mathbf{y}{\Vert }^2\le c_1({\mathbf{y}}_1\cdot {\mathbf{y}}_1+{\mathbf{y}}_2\cdot {\mathbf{y}}_2)$

and then chain the two. Two gaps remain. First, coercivity speaks of self dot products, while the goal speaks of norms — we need the identity $\Vert {\mathbf{y}}_{\mathbf{i}}{\Vert }^2={\mathbf{y}}_{\mathbf{i}}\cdot {\mathbf{y}}_{\mathbf{i}}$ to translate between them. Second, and this is the crux, the product norm is the maximum of the two block norms, so we must compare $\Vert \mathbf{y}{\Vert }^2=\max (\Vert {\mathbf{y}}_1\Vert \Vert {\mathbf{y}}_2\Vert {)}^2$ against the sum $\Vert {\mathbf{y}}_1{\Vert }^2+\Vert {\mathbf{y}}_2{\Vert }^2$. Here the direction of the inequality is our friend: a maximum of two nonnegative numbers is at most their sum, because the other one only adds. A lower sandwich needs precisely this friendly direction — an upper sandwich would need the reverse and would fail without a $\sqrt{2}$ factor. So the lower bound holds with room to spare, and the technique is a direct chain of two inequalities, with a case split to handle the maximum.

The norm-to-dot-product bridge

Before the main chain, record the translation as a small lemma (norm_sq_eq_dotProduct): on a Euclidean space the squared norm is the self dot product,

$\Vert \mathbf{x}{\Vert }^2={\sum }_i{x}_i^2=\mathbf{x}\cdot \mathbf{x}.$

The proof is unfolding: the $L^2$ norm’s defining sum is ${\sum }_i(x_i{)}^2$ (EuclideanSpace.real_norm_sq_eq), and the dot product $\mathbf{x}\cdot \mathbf{x}$ is by definition ${\sum }_i{x}_i\cdot x_i$ (dotProduct); the two sums are equal term by term, since $(x_i{)}^2=x_i\cdot x_i$ (pow_two). This is the exact bridge that carries coercivity’s y₁ ⬝ᵥ y₁ over to the comparison function’s $\Vert \cdot \Vert$.

Proof

Assume $\mathbf{M}$ and $\mathbf{K}$ are positive-definite. Coercivity (blockLyap_coercive) hands us a constant $c_1>0$ together with the bound $c_1({\mathbf{y}}_1\cdot {\mathbf{y}}_1+{\mathbf{y}}_2\cdot {\mathbf{y}}_2)\le V(\mathbf{y})$ for every $\mathbf{y}$. Take the witness ${\alpha }_1(s)=c_1{s}^2$; it is class ${\mathcal{K}}_{\infty }$ by the squaring result of the previous section scaled by $c_1$ (isClassKInfinity_sq.const_mul, using $c_1>0$). Fix a stacked state $\mathbf{y}$; it remains to prove $c_1\Vert \mathbf{y}{\Vert }^2\le V(\mathbf{y})$.

First, the product-norm inequality. Rewriting the sup norm (Prod.norm_def) turns the goal’s left factor into $\max (\Vert {\mathbf{y}}_1\Vert \Vert {\mathbf{y}}_2\Vert {)}^2$, and we claim

$\Vert \mathbf{y}{\Vert }^2\le \Vert {\mathbf{y}}_1{\Vert }^2+\Vert {\mathbf{y}}_2{\Vert }^2.$

Split on which block norm is larger. If $\Vert {\mathbf{y}}_1\Vert \le \Vert {\mathbf{y}}_2\Vert$, the maximum is $\Vert {\mathbf{y}}_2\Vert$, so $\Vert \mathbf{y}{\Vert }^2=\Vert {\mathbf{y}}_2{\Vert }^2\le \Vert {\mathbf{y}}_1{\Vert }^2+\Vert {\mathbf{y}}_2{\Vert }^2$, the inequality being exactly the nonnegativity of the discarded term $\Vert {\mathbf{y}}_1{\Vert }^2$ (sq_nonneg, closed by nlinarith). The other case is symmetric, discarding $\Vert {\mathbf{y}}_2{\Vert }^2$ instead. This is the “room to spare” the strategy promised.

Next, put coercivity into norm form. Applying the bridge lemma to each block rewrites the self dot products as squared norms, so coercivity reads

$c_1(\Vert {\mathbf{y}}_1{\Vert }^2+\Vert {\mathbf{y}}_2{\Vert }^2)\le V(\mathbf{y}).$

Now chain. Since $c_1\ge 0$, multiplying the product-norm inequality on the left by $c_1$ preserves it (mul_le_mul_of_nonneg_left), and then coercivity finishes the second step:

$c_1\Vert \mathbf{y}{\Vert }^2\le c_1(\Vert {\mathbf{y}}_1{\Vert }^2+\Vert {\mathbf{y}}_2{\Vert }^2)\le V(\mathbf{y}).$

The left end is ${\alpha }_1(\Vert \mathbf{y}\Vert )$, so ${\alpha }_1(\Vert \mathbf{y}\Vert )\le V(\mathbf{y})$, as desired.

What this shows

The concrete coupled block satisfies the class-${\mathcal{K}}_{\infty }$ lower bound with an explicit witness, ${\alpha }_1(s)=c_1{s}^2$ and $c_1=\frac{1}{2}\min ({\lambda }_{\min }\mathbf{M}{\lambda }_{\min }\mathbf{K})$. No converse-Lyapunov construction was needed: the quadratic energy already is its own class-${\mathcal{K}}_{\infty }$ lower bound, and the only subtlety was reconciling the product’s sup norm with the block-wise coercivity — a reconciliation that a lower bound gets for free. This is the pointwise fact; the next section serves it along a trajectory in the precise shape the cascade consumers read.

The lower-sandwich hypothesis, discharged along any trajectory (blockLyap_hsand)

The cascade attractivity theorem does not consume the pointwise inequality directly; it consumes it at each instant along the driven trajectory. This final result restates the sandwich in that form: for any trajectory $x_1$ in the stacked state space,

$\exists {\alpha }_1\in {\mathcal{K}}_{\infty }\text{such that}{\alpha }_1(\Vert x_1(t)\Vert )\le V(x_1(t))\text{ for every }t\ge 0.$

Strategy

There is nothing new to prove — only to specialise. The pointwise sandwich holds at every stacked state, so in particular it holds at the state $x_1(t)$ for each time $t$. The technique is direct instantiation.

Proof

Let $x_1:\mathbb{R}\to {\mathbb{R}}^n\times {\mathbb{R}}^m$ be any trajectory. The pointwise sandwich (blockLyap_classKInfinity_sandwich) supplies a class-${\mathcal{K}}_{\infty }$ function ${\alpha }_1$ and the bound ${\alpha }_1(\Vert \mathbf{y}\Vert )\le V(\mathbf{y})$ for every $\mathbf{y}$. Reuse the same ${\alpha }_1$, and for any time $t\ge 0$ instantiate the pointwise bound at the particular state $\mathbf{y}=x_1(t)$. This yields ${\alpha }_1(\Vert x_1(t)\Vert )\le V(x_1(t))$ for every $t\ge 0$, as desired.

What this shows

The energy $V(\mathbf{y})=\text{blockLyap}\mathbf{M}\mathbf{K}{\mathbf{y}}_1{\mathbf{y}}_2$ is exactly the function the cascade’s driven block carries, and the inequality above is exactly the shape the attractivity engine and its instantiation on the coupled block read as their lower-sandwich input. So for the concrete positive-definite block that input is now a theorem. A consumer that once wrote it as a hypothesis can instead cite this result.

Assumptions taken as given

None. This module assumes no named hypotheses and contains no sorry. Its only inputs are the mathematical content of the claim — the two blocks positive-definite and their index sets nonempty — together with facts imported from already fully machine-checked modules: the coercivity bound of the block Lyapunov module and the class-${\mathcal{K}}_{\infty }$ algebra of the comparison-function module. There is nothing here for a later module to discharge; what this module does is discharge something for others, namely the lower-sandwich hypothesis of the cascade module for the concrete block.

Scope and limitations

This is the point to be scrupulous about, because it is easy to overstate what a partial result buys.

• The companion decrease hypothesis stays open, by design. The cascade attractivity theorem needs two things of the driven block: the lower sandwich proved here, and a strict interconnection decrease, $v^{\prime }(t)\le -aV(x_1(t))+c\Vert x_2(t)\Vert$ with $a>0$ (Panteley & Loría, eq. 35). That second hypothesis is a converse-Lyapunov statement — it demands a strictly, proportionally decreasing energy — and it is genuinely open. Mathlib version 4.31.0 contains no Lyapunov-stability theory at all (a search of the pinned source returns zero files mentioning Lyapunov, Massera, or Kurzweil’s converse theorems), and the coupled block’s natural energy decreases only semidefinitely: its Lyapunov-derivative zero set is an entire subspace, not the origin alone, which is precisely why the block’s own asymptotic result had to route through the LaSalle invariance principle rather than a strict Lyapunov argument. A negative-semidefinite decrease can never yield the strict $-aV$ the hypothesis needs. The dossier at [(~/Code/tasks/streams/ctrllib/scope_hsand_hdi.md)] records this as a documented boundary.
• The cascade result itself is not closed by this module. Because attractivity needs both hypotheses, discharging the lower sandwich alone leaves the cascade attractivity theorem and its downstream consumers (the coupled-block instantiation and the seven-degree-of-freedom null-space damping) still resting on the open decrease hypothesis. The assumptions ledger’s status for those results does not change. What changes is how much remains assumed: one of the two named inputs is now a theorem for the concrete block, so the open edge sits entirely on the decrease.
• Same block, same energy. The energy that makes the lower sandwich cheap is exactly the one that cannot supply the strict decrease. One cannot mix and match — a strictly decreasing energy would have to be manufactured by the very converse-Lyapunov construction that is absent. So the two hypotheses do not separate into “both cheap”; only the lower one is.
• Positive-definite blocks, nonempty index sets. The result is stated for $\mathbf{M}$ and $\mathbf{K}$ positive-definite with $n$ and $m$ nonempty. Nonemptiness is what lets the coercivity constant name a least eigenvalue; it is physically automatic at $n=m=9$.
• Lower sandwich only. This module proves the lower half of Panteley & Loría’s two-sided sandwich. The upper half (properness, $V\le {\alpha }_2(\Vert x_1\Vert )$) is used only for the boundedness reading of the cascade and is not needed for attractivity, so it is not treated here.

Provenance

The two-sided class-${\mathcal{K}}_{\infty }$ sandwich on a reshaped Lyapunov function is Panteley & Loría (2001), Growth rate conditions for uniform asymptotic stability of cascaded time-varying systems, Proposition 1 — specifically the lower comparison bound of eq. 13. The block energy $V$ and its positive-definiteness trace to the coordinated-control storage function of Giordano et al. (2019), formalized in the block Lyapunov module; that a quadratic form in a positive-definite matrix is bounded below by its least eigenvalue times the squared norm is the Rayleigh–Ritz theorem (Horn & Johnson, Matrix Analysis, 2nd ed., Thm 4.2.2). The class-${\mathcal{K}}_{\infty }$ vocabulary — continuous, strictly increasing, zero at zero, radially unbounded — is Khalil’s standard comparison-function language (Khalil, Nonlinear Systems, Class $\mathcal{K}$/${\mathcal{K}}_{\infty }$ definitions). That the squaring map is class ${\mathcal{K}}_{\infty }$ is elementary. No coined terminology is introduced.

Machine verification (#print axioms)

CoupledSandwich.lean holds the private bridge lemma norm_sq_eq_dotProduct together with the three public results. Running #print axioms on each reports the three standard axioms and nothing else — no sorryAx, and no sorry anywhere in the module:

'Ctrllib.isClassKInfinity_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.blockLyap_classKInfinity_sandwich' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.blockLyap_hsand' depends on axioms: [propext, Classical.choice, Quot.sound]

The module imports BlockLyapunov and ComparisonFunctions and edits neither. The Mathlib results the proofs lean on: continuous_pow, pow_lt_pow_left₀, tendsto_pow_atTop (the squaring map); EuclideanSpace.real_norm_sq_eq, Matrix.dotProduct (the norm-to-dot-product bridge); Prod.norm_def, max_eq_left, max_eq_right, sq_nonneg, mul_le_mul_of_nonneg_left (the product-norm step); and the project’s own blockLyap_coercive and IsClassKInfinity.const_mul. The tracked source of truth is the Lean file beside this page; the build copy lives at ~/lean/ctrllib/Ctrllib/CoupledSandwich.lean, imported into Ctrllib.lean after BlockLyapunov and ComparisonFunctions.