com_lasalle_matrix

The CoM loop is GAS for a concrete SPD model — G1 sub-item (b)

Seal

Rung G1 · Status sealed — axiom-clean (#print axioms verbatim in The machine seal; full build 2654 jobs). Discharges the six operator hypotheses com_gas carries (hMsa/hKsa/hMinv/hDnn/hDdef/hKdef) as theorems for a concrete symmetric-positive-definite model, leaving only IsSolutionTo and hcpt (now forward-only) applier-side — see interfaces.
Links: module index · interface ledger · related com_lasalle, rayleigh_sandwich, coupled_collapse_matrix · source giordano2019coordinated · pin pin_com_matrix.py

What this seals, in one paragraph

com_gas (com_lasalle) proves the CoM-error driver globally asymptotically stable for every system with the stated structure — but it carries the inertia/damping/stiffness as abstract continuous linear operators $M,D,K:H\to H$ with their defining identities (symmetry, invertibility, damping sign, stiffness injectivity) as named hypotheses. For the actual thesis model those operators are concrete symmetric positive-definite matrices (current_sota.md §4.3, $m{\ddot{\tilde{\mathbf{x}}}}_c+D{\dot{\tilde{\mathbf{x}}}}_c+K{\tilde{\mathbf{x}}}_c=0$), so the six hypotheses are not assumptions but theorems. This module proves each one via Matrix.toEuclideanCLM and the sealed rayleigh_sandwich/PosDef stones, then wires them into com_gas to give com_gas_matrix. This is the concrete-model half of the G1 defense line: kernel-proved for every system with the stated structure; our model verifiably has it.

The bridge

Matrix.toEuclideanCLM sends a matrix $\mathbf{A}$ to the continuous linear operator it induces on $\mathrm{EuclideanSpace}\mathbb{R}n$. The load-bearing Mathlib fact is

$⟨x,\mathrm{toEuclideanCLM}\mathbf{A}y⟩=x\cdot (\mathbf{A}y)$

(inner_toEuclideanCLM): the Euclidean inner product of $x$ with $\mathbf{A}y$ is exactly $x^{\top }\mathbf{A}y$. Every operator hypothesis reduces, through this, to a plain matrix fact.

Sealed theorems (the six discharges + the capstone)

• euclideanCLM_self_adjoint — hMsa/hKsa: for symmetric $\mathbf{A}$, $⟨\mathbf{A}x,y⟩=⟨x,\mathbf{A}y⟩$. Reduces to the quadratic-form symmetry $b\cdot \mathbf{A}a=a\cdot \mathbf{A}b$ (proved from ${\mathbf{A}}^{\top }=\mathbf{A}$, real Hermitian).
• euclideanCLM_inv — hMinv: $\mathbf{M}({\mathbf{M}}^{-1}w)=w$, from Matrix.mul_nonsing_inv ($\mathbf{M}{\mathbf{M}}^{-1}=1$ when $\mathbf{M}$ is a unit — PosDef.isUnit), through ofLp injectivity.
• euclideanCLM_dotProduct_nonneg — hDnn: $0\le ⟨v,\mathbf{D}v⟩$, the sealed Rayleigh lower bound le_dotProduct_mulVec with $c_1=0$ (eigenvalues $\ge 0$ from PosDef.eigenvalues_pos).
• euclideanCLM_dotProduct_def — hDdef: $⟨v,\mathbf{D}v⟩=0\Rightarrow v=0$, the contrapositive of PosDef.dotProduct_mulVec_pos.
• euclideanCLM_injective — hKdef: $\mathbf{K}x=0\Rightarrow x=0$, from PosDef.isUnit + mulVec_injective_of_isUnit (the stiffness_residual pattern).
• com_gas_matrix — the capstone: given concrete SPD $\mathbf{M},\mathbf{D},\mathbf{K}$, every forward-precompact orbit of the closed-loop CoM field converges to the origin. All six operator hypotheses discharged here; only IsSolutionTo (flow existence) and hcpt (ForwardPrecompact) remain applier-side.

SymPy pin

pin_com_matrix.py witnesses the concrete SPD model (3×3 CoM block, plus 6, 9): self-adjointness, $\mathbf{M}{\mathbf{M}}^{-1}=1$, $⟨v,\mathbf{D}v⟩>0$ off the origin (${\lambda }_{\min }(\mathbf{D})>0$), and ${\sigma }_{\min }(\mathbf{K})>0$ — all six operator facts, checked through the $x^{\top }\mathbf{A}y$ bridge, to $10^{-10}$ or better.

The machine seal

Verbatim #print axioms (full build, 2654 jobs, no sorryAx):

'Ctrllib.euclideanCLM_self_adjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.euclideanCLM_inv' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.euclideanCLM_dotProduct_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.euclideanCLM_dotProduct_def' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.euclideanCLM_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.com_gas_matrix' depends on axioms: [propext, Classical.choice, Quot.sound]

The module is (/Code/vault/lean/ComLaSalleMatrix.lean), build copy ~/lean/ctrllib/Ctrllib/ComLaSalleMatrix.lean. SymPy pin (/Code/vault/lean/pin_com_matrix.py).