block_lyapunov

The block Lyapunov candidate is positive-definite and coercive — TARGET 20 of the LeanPunov stream

Seal

Rung rung-1 · Status sealed · #print axioms for all four public theorems is [propext, Classical.choice, Quot.sound] — no sorryAx (recorded in The machine seal). No interface hypotheses. Public definition: blockLyap. blockLyap_coercive is the forward-boundedness witness cited by the hcpt interface — see interfaces.
Links: module index · interface ledger · related rayleigh_sandwich, com_lasalle, coupled_collapse · sources giordano2019coordinated, khalil1996nonlinear (no wiki page yet) · pin pin_block_lyapunov.py

Sealed theorems

blockLyap_sandwich

Two-sided eigenvalue bounds on each block sandwich the storage function between $\frac{1}{2}a\Vert \cdot {\Vert }^2$ sums.

blockLyap_coercive

There is $c_1=\frac{1}{2}\min ({\lambda }_{\min }\mathbf{M}{\lambda }_{\min }\mathbf{K})>0$ with $c_1(\Vert \mathbf{v}{\Vert }^2+\Vert \mathbf{x}{\Vert }^2)\le V$ — radial unboundedness.

blockLyap_nonneg

$0\le V$ everywhere.

blockLyap_eq_zero_iff

$V=0⟺\mathbf{v}=0\wedge \mathbf{x}=0$ — the Lyapunov positive-definite property.

Why this theorem, and why now

The framing paper closes its stability argument (giordano2019coordinated eqs 36-38; (~/Code/Inspection/GNC/equations/current_sota.md) §4.6 eq 4.15) with the storage function

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

where $\breve{\mathbf{M}}\succ 0$ is the reduced inertia and $\breve{\mathbf{K}}=\mathrm{blkdiag}({\mathbf{K}}_b{\mathbf{K}}_e)\succ 0$ the block-diagonal stiffness. The paper asserts that this $V$ is a valid Lyapunov candidate — positive-definite and radially unbounded — and moves straight to $\dot{V}$. A pencil-and-paper PhD defense cannot leave that admissibility leg unproven: the decrease $\dot{V}\le 0$ certifies stability only if $V$ is genuinely positive-definite and coercive. This file seals exactly that leg.

It is a direct instance of the Rayleigh sandwich (L-target 4, (~/Code/vault/lean/Rayleigh.lean)) applied to each block. Because eq 4.15 is literally the sum of two quadratic forms — not one quadratic form on a stacked vector — the honest and shortest route is to bound each summand by its own Rayleigh sandwich and add, with no Matrix.fromBlocks single-matrix detour (which would drag in block-diagonal eigenvalue bookkeeping for zero mathematical gain). The block-diagonal single-matrix form $\mathrm{blkdiag}(\breve{\mathbf{M}}\breve{\mathbf{K}})$ is equivalent; the additive form is what the source states.

The precise statements

Work over $\mathbb{R}$ with finite index types $nm$ (physically $n=m=9$). Define

$$\text{blockLyap}\mathbf{M}\mathbf{K}\mathbf{v}\mathbf{x}=\frac{1}{2}({\mathbf{v}}^{\top }\mathbf{Mv})+\frac{1}{2}({\mathbf{x}}^{\top }\mathbf{Kx})$$

written in Lean as (1/2) * (v ⬝ᵥ M *ᵥ v) + (1/2) * (x ⬝ᵥ K *ᵥ x). The self dot products v ⬝ᵥ v and x ⬝ᵥ x are exactly $\Vert \mathbf{v}{\Vert }^2$ and $\Vert \mathbf{x}{\Vert }^2$ (Euclidean), so v ⬝ᵥ v + x ⬝ᵥ x is the squared norm of the stacked state $(\mathbf{v}\mathbf{x})$ — written transparently to avoid any WithLp / product-norm bookkeeping.

Sandwich (blockLyap_sandwich, $\mathbf{M}\mathbf{K}$ Hermitian). Given uniform eigenvalue bounds $a_M\le {\lambda }_i(\mathbf{M})\le b_M$ and $a_K\le {\lambda }_i(\mathbf{K})\le b_K$,
$\frac{1}{2}{a}_M\Vert \mathbf{v}{\Vert }^2+\frac{1}{2}{a}_K\Vert \mathbf{x}{\Vert }^2\le V\le \frac{1}{2}{b}_M\Vert \mathbf{v}{\Vert }^2+\frac{1}{2}{b}_K\Vert \mathbf{x}{\Vert }^2.$

Coercivity / radial unboundedness (blockLyap_coercive, $\mathbf{M}\mathbf{K}\succ 0$, $nm$ nonempty). There is $c_1>0$ with $c_1(\Vert \mathbf{v}{\Vert }^2+\Vert \mathbf{x}{\Vert }^2)\le V$ for all $\mathbf{v}\mathbf{x}$; explicitly $c_1=\frac{1}{2}\min ({\lambda }_{\min }\mathbf{M}{\lambda }_{\min }\mathbf{K})$. As the state grows, $V\to \infty$.

Nonnegativity (blockLyap_nonneg). $0\le V$ everywhere.

Positive-definiteness (blockLyap_eq_zero_iff). $V(\mathbf{v}\mathbf{x})=0⟺\mathbf{v}=0\wedge \mathbf{x}=0$. With nonnegativity this is the Lyapunov positive-definite property: $V(0)=0$ and $V>0$ off the origin.

Together, coercivity + nonnegativity + the zero-iff give precisely “positive-definite and radially unbounded (coercive)” — the admissibility leg the thesis states without proof.

Source and provenance

The Lyapunov candidate is giordano2019coordinated eq 37 (= current_sota.md eq 4.15). That a quadratic form in a positive-definite matrix is bounded below and above by its extreme eigenvalues times the squared norm — hence positive-definite and radially unbounded — is the Rayleigh–Ritz theorem (Horn & Johnson, Matrix Analysis 2nd ed. Thm 4.2.2; Khalil, Nonlinear Systems Lyapunov chapter). “Radially unbounded” / “coercive” and “positive-definite” are Khalil’s standard Lyapunov-candidate vocabulary; no coined terminology is introduced.

Scratch work — where the bounds come from

Each block is a single quadratic form, so the per-block Rayleigh bound (already sealed) gives

$$a_M\Vert \mathbf{v}{\Vert }^2\le {\mathbf{v}}^{\top }\mathbf{Mv}\le b_M\Vert \mathbf{v}{\Vert }^2{a}_K\Vert \mathbf{x}{\Vert }^2\le {\mathbf{x}}^{\top }\mathbf{Kx}\le b_K\Vert \mathbf{x}{\Vert }^2.$$

Halving and adding gives the sandwich immediately. For the single-constant coercive form, collapse the two lower coefficients with the elementary fact

$$\min (ab)(p+q)\le ap+bq(pq\ge 0)$$

which holds because, taking $a\le b$ wlog, $ap+bq-a(p+q)=(b-a)q\ge 0$. With $a=a_M$, $b=a_K$, $p=\Vert \mathbf{v}{\Vert }^2$, $q=\Vert \mathbf{x}{\Vert }^2$ this yields $c_1(\Vert \mathbf{v}{\Vert }^2+\Vert \mathbf{x}{\Vert }^2)\le V$ with $c_1=\frac{1}{2}\min (a_M{a}_K)$. For a positive-definite matrix every eigenvalue is $>0$, so the minimum over a nonempty finite index is $>0$, hence $c_1>0$. Positive-definiteness is then a corollary: if $V=0$ then $c_1(\Vert \mathbf{v}{\Vert }^2+\Vert \mathbf{x}{\Vert }^2)\le 0$ with $c_1>0$ forces $\Vert \mathbf{v}{\Vert }^2=\Vert \mathbf{x}{\Vert }^2=0$, i.e. $\mathbf{v}=\mathbf{x}=0$.

(The per-block bound is pinned in pin_rayleigh.py; the NEW content — the sum of two sandwiches and the min/max collapse — is pinned in (~/Code/vault/lean/pin_block_lyapunov.py): the collapse identity symbolically, and the full bound + positive-definiteness numerically over 4000 random SPD $9\times 9$ blocks.)

Proof (teacher-verifiable), and how the Lean mirrors it

The Lean factors through two private lemmas, exactly matching the scratch work:

1. blockLyap_lower / blockLyap_upper — halve and add the two per-block Rayleigh bounds. Each calls the sealed le_dotProduct_mulVec / dotProduct_mulVec_le on its block, then linarith scales by $\frac{1}{2}$ and sums. blockLyap_sandwich is their conjunction.

2. blockLyap_coercive — take $a_M=\text{univ.inf’}\lambda (\mathbf{M})$, $a_K=\text{univ.inf’}\lambda (\mathbf{K})$ (the least eigenvalues, needing $nm$ nonempty for inf'). Positivity $0<a_M$ is Finset.lt_inf'_iff fed by Matrix.PosDef.eigenvalues_pos; Finset.inf'_le supplies the uniform lower bound the sandwich consumes. The witness is $c_1=\frac{1}{2}\min (a_M{a}_K)$, positive by lt_min. The bound closes by feeding blockLyap_lower, the two collapse inequalities min aM aK * (v ⬝ᵥ v) ≤ aM * (v ⬝ᵥ v) (via mul_le_mul_of_nonneg_right (min_le_left …) and self-dot-product nonnegativity), and their $\mathbf{x}$ analogue into nlinarith.

3. blockLyap_nonneg — from coercivity: $V\ge c_1\cdot (\text{nonneg})\ge 0$.

4. blockLyap_eq_zero_iff — ($\Leftarrow$) simp [blockLyap] at $\mathbf{v}=\mathbf{x}=0$ (mulVec/dot of zero). ($\Rightarrow$) from coercivity $c_1(\Vert \mathbf{v}{\Vert }^2+\Vert \mathbf{x}{\Vert }^2)\le 0$; mul_pos rules out a positive sum, so both self dot products vanish, and Matrix.dotProduct_self_eq_zero turns each into $\mathbf{v}=0$, $\mathbf{x}=0$.

What is interfaced (nothing) and what is assumed

No interface hypotheses, no sorry. The only hypotheses are the mathematical content itself: $\mathbf{M}\mathbf{K}$ positive-definite (via Matrix.PosDef) and the index types nonempty.

Honest notes for the reviewer:

• Nonemptiness ($nm$ nonempty) is required only so Finset.inf' has a least eigenvalue to name; it is physically automatic ($n=m=9$). On an empty block the corresponding quadratic form is identically zero and the statement degenerates, which is why the hypothesis is kept rather than worked around.
• The norm is transparent, not ambient. Results are stated with v ⬝ᵥ v + x ⬝ᵥ x, which is the squared Euclidean norm of the concatenated state; this avoids committing to a product-space norm convention (Prod’s default sup norm would blur the additive constant). A reader reads v ⬝ᵥ v + x ⬝ᵥ x as $\Vert \mathbf{v}{\Vert }^2+\Vert \mathbf{x}{\Vert }^2$ directly.
• Additive, not fromBlocks. Faithful to eq 4.15 and strictly shorter; the block-diagonal single-matrix form is equivalent and needs no separate seal.
• DecidableEq in-type linter is silenced at file scope: the instance is genuinely used by the eigenvalue machinery in the proofs, it simply does not appear in the statement types.

Mathlib stones used

Matrix.PosDef.isHermitian, Matrix.PosDef.eigenvalues_pos; the sealed Leanpunov.le_dotProduct_mulVec / Leanpunov.dotProduct_mulVec_le (Rayleigh, TARGET 4); Matrix.dotProduct_self_eq_zero; Finset.inf'_le, Finset.lt_inf'_iff, Finset.univ_nonempty; min_le_left, min_le_right, lt_min, mul_le_mul_of_nonneg_right, mul_pos, mul_nonneg; Finset.sum_nonneg, mul_self_nonneg; nlinarith / linarith.

The machine seal

BlockLyapunov.lean holds dp_self_nonneg, blockLyap_lower, blockLyap_upper (private) and the four public results. #print axioms for blockLyap_sandwich, blockLyap_coercive, blockLyap_nonneg, blockLyap_eq_zero_iff is [propext, Classical.choice, Quot.sound] — no sorryAx. The build copy lives at ~/lean/leanpunov/Leanpunov/BlockLyapunov.lean; this directory’s copy is the tracked source of truth, imported into Leanpunov.lean after TimeVaryingComparison.

Cost feel. Well under one L2-scale push: ~120 lines, one SymPy/numeric pin, three fix cycles (all mechanical — noncomputable on the Real-division def, the removed le_or_lt swapped for by_contra, and a deprecated push_neg cleaned to not_le.mp). No wall; comfortably inside the stall budget. The entire difficulty is discharged by reusing the sealed Rayleigh stones.