coupled_collapse_matrix

The coupled block is GAS for a concrete SPD model — G1 sub-item (d)

Seal

Rung G1 · Status sealed — axiom-clean (#print axioms verbatim in The machine seal; full build 2654 jobs). Discharges the operator hypotheses coupled_gas carries beyond the CoM ones (hJadj/hpass/hMinj/hJKinj, plus the CoM-shared hMsa/hKsa/hMinv/hDnn/hDdef reused from com_lasalle_matrix) as theorems for a concrete SPD model — the hzero step on the concrete g2Field — and seals the Ω J-rank fact. Only IsSolutionTo, hcpt, and the moving-metric bracket hreal/hfield remain applier-side.
Links: module index · interface ledger · related coupled_collapse, coupled_field, stiffness_residual, gamma_invertible, com_lasalle_matrix · source giordano2019coordinated · pin pin_coupled_matrix.py

What this seals, in one paragraph

coupled_gas (coupled_collapse) proves Prop IV.1’s convergence for the driven attitude+EE block through the invariance (LaSalle) route — rung-2’s honest finding was that the pointwise hzero is FALSE (the Lyapunov-derivative zero set is the whole subspace $\{\breve{\mathbf{v}}=0\}$, not $\{0\}$), so the origin is reached only via invariance $\breve{\mathbf{v}}\equiv 0\Rightarrow \dot{\breve{\mathbf{v}}}\equiv 0\Rightarrow {\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}=0\Rightarrow \tilde{\mathbf{x}}=0$. coupled_gas carries nine operator hypotheses. For the concrete SPD model each is a theorem; this module proves the four beyond the CoM set (adjoint, passivity, ${\mathbf{M}}^{-1}$ injectivity, stiffness-residual injectivity) via Matrix.toEuclideanCLM and the sealed stiffness_residual/passivity_transport stones, reuses the five CoM discharges from com_lasalle_matrix, and wires all nine into coupled_gas to give coupled_gas_matrix — the concrete witness that the LaSalle-route collapse (never the false pointwise form) holds for the SPD model.

Sealed theorems

• euclideanCLM_adjoint — hJadj: $⟨\mathbf{J}a,b⟩=⟨a,{\mathbf{J}}^{\top }b⟩$; $\mathrm{toEuclideanCLM}{\mathbf{J}}^{\top }$ is the adjoint of $\mathrm{toEuclideanCLM}\mathbf{J}$, through inner_toEuclideanCLM + the transpose.
• euclideanCLM_passivity — hpass: from the Christoffel relation $\dot{\breve{\mathbf{M}}}=\breve{\mathbf{C}}+{\breve{\mathbf{C}}}^{\top }$ (the sealed passivity_transport content), $⟨v,\dot{\breve{\mathbf{M}}}v⟩=2⟨v,\breve{\mathbf{C}}v⟩$ (using $v\cdot {\mathbf{C}}^{\top }v=v\cdot \mathbf{C}v$).
• euclideanCLM_injective_of_isUnit — hMinj: for a unit matrix $\mathbf{A}$, $\mathrm{toEuclideanCLM}\mathbf{A}$ is injective; applied to ${\breve{\mathbf{M}}}^{-1}$ (a unit since $\breve{\mathbf{M}}$ is), via isUnit_nonsing_inv_iff.
• euclideanCLM_stiffness_injective — hJKinj: for $\breve{\mathbf{K}}\succ 0$ and ${\mathbf{J}}_{\tilde{x}}$ full column rank, ${\mathbf{J}}_{\tilde{x}}^{\top }(\breve{\mathbf{K}}\tilde{\mathbf{x}})=0\Rightarrow \tilde{\mathbf{x}}=0$ — the operator transcription of the sealed stiffness_residual_injective' (stiffness_residual).
• gamma_jacobian_mulVec_injective — the Ω J-rank fact: where the 12×12 coordinated transform $\mathbf{\Gamma }$ is invertible, the 6×6 circumcentroidal Jacobian ${\mathbf{J}}_{\nu }^{\oplus }$ has full column rank (mulVec injective), built on gamma_invertible gamma_isUnit_iff. This is the concrete content of current_sota’s ”$\mathbf{J}$ full-rank on $\Omega$”.
• coupled_gas_matrix — the capstone: given concrete SPD $\breve{\mathbf{M}},\breve{\mathbf{D}},\breve{\mathbf{K}}$, the Christoffel $\breve{\mathbf{C}}$ with $\dot{\breve{\mathbf{M}}}=\breve{\mathbf{C}}+{\breve{\mathbf{C}}}^{\top }$, and a nonsingular representation Jacobian ${\mathbf{J}}_{\tilde{x}}$, every forward-precompact orbit converges to the origin. All nine operator hypotheses discharged; only IsSolutionTo, hcpt, and the moving-metric bracket hreal/hfield (the deferred analytic step, not the algebra) remain named.

SymPy pin

pin_coupled_matrix.py witnesses the concrete SPD coupled model (9×9 base+ee block, plus 6): the adjoint identity $(\mathbf{J}a)\cdot b=a\cdot ({\mathbf{J}}^{\top }b)$, the passivity identity $v\cdot (\dot{\mathbf{M}}v)=2v\cdot (\mathbf{C}v)$ with $\dot{\mathbf{M}}=\mathbf{C}+{\mathbf{C}}^{\top }$, ${\sigma }_{\min }({\mathbf{J}}^{\top }\mathbf{K})>0$, and the Γ rank fact $\det \mathbf{\Gamma }=\det {\mathbf{J}}_{\nu }^{\oplus }$ (Rot $\in SO(3)$) with the invertible-$\Gamma$ ⟺ injective-${\mathbf{J}}_{\nu }^{\oplus }$ agreement — all to $10^{-10}$ or the singular-value floor.

The machine seal

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

'Ctrllib.euclideanCLM_adjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.euclideanCLM_passivity' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.euclideanCLM_injective_of_isUnit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.euclideanCLM_stiffness_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.gamma_jacobian_mulVec_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.coupled_gas_matrix' depends on axioms: [propext, Classical.choice, Quot.sound]

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