coupled_collapse

L4B-WIRE — discharging Prop IV.1’s hzero through the closed-loop field

Seal

Rung rung-2 · Status interfaced — all three theorems axiom-clean per the rung-2 seal record on the stream note (~/Code/tasks/streams/leanpunov.md): “Proof campaign rung 2 CORE sealed 4/4, 2026-07-06 ~05:20 … 15 theorems, all axiom-clean, final build green 2644 jobs”, i.e. [propext, Classical.choice, Quot.sound]. This page carries no verbatim per-theorem #print axioms block of its own — the stream line is the recorded evidence. Interfaces per 4. Interface boundary (the honest list the defense will ask about); supersedes hzero for the coupled block via the invariance route (the pointwise hzero ⊆ {0} is provably false — pin 5000/5000 — and was never sealed). See interfaces.
Links: module index · interface ledger · related coupled_dissipation, coupled_field, reduction_cascade, lasalle_invariance, stiffness_residual, com_lasalle, block_lyapunov · source giordano2019coordinated · pin pin_coupled_collapse.py

Sealed theorems

coupled_collapse

The field-level LaSalle collapse: on any flow-invariant set where $DV[f]$ vanishes, the state is the origin.

coupled_gas

The capstone — Prop IV.1’s convergence assembled end-to-end: every precompact orbit of the driven block converges to the origin.

coupled_velocity_tendsto

The literal propIV1_tendsto instantiation — convergence to $\{\breve{\mathbf{v}}=0\}$ only, recorded to make the $\{\breve{\mathbf{v}}=0\}$ vs $\{0\}$ gap explicit and machine-checked.

The framing paper (giordano2019coordinated §IV.D) closes its Prop IV.1 cascade with one sentence:

“Applying LaSalle to (34b), $\breve{v}\equiv 0$ implies $\tilde{x}=0$.”

Every piece of that sentence is now a sealed Lean lemma: the field ($g_2$, CoupledField), the total dissipation rate ($\dot{V}=-{\breve{v}}^{\top }\breve{D}\breve{v}$, CoupledDissipation), the LaSalle engine (lasalle, tendsto_infDist_of_omegaLimit_subset), and the algebra of the residual collapse ($J_{\tilde{x}}^{\top }\breve{K}\tilde{x}=0\Rightarrow \tilde{x}=0$, StiffnessResidual). This module wires them together and delivers Prop IV.1’s convergence conclusion for the driven block: coupled_gas, ϕ t y₀ → 0.

1. The structural fact the pin forced (why this is not propIV1_tendsto)

The sealed propIV1_tendsto (Reduction.lean) discharges convergence from a pointwise hypothesis

$\text{hzero}:\{y\mid \mathrm{D}V(y)[f(y)]=0\}\subseteq {\Gamma }_1.$

The charter asked for hzero “discharged at the field level” with ${\Gamma }_1=\{0\}$. That statement is false for the coupled block, and the pin proves it false before any Lean is written.

The previous lane gives the total rate (via the passivity collapse):

$\dot{V}(y)=\mathrm{D}V(y)[f(y)]=-⟨\breve{v},\breve{D}\breve{v}⟩,y=(\tilde{x},\breve{v}),\breve{v}=y.2.$

This depends only on $\breve{v}$. Its zero-set is therefore the whole subspace

$\{y\mid \dot{V}(y)=0\}=\{y\mid ⟨\breve{v},\breve{D}\breve{v}⟩=0\}\stackrel{\breve{D}\succ 0}{=}\{\breve{v}=0\}=\{(\tilde{x},0):\tilde{x}\in H\}⊋\{0\}.$

pin_coupled_collapse.py check (1) exhibits this: 5000/5000 nonzero states $(\tilde{x},0)$ satisfy $\dot{V}=0$. So a pointwise hzero ⊆ {0} would be a false seal; instantiating propIV1_tendsto can reach at most $\{\breve{v}=0\}$, never the origin.

The origin is reached by the invariance argument — the same reason the sealed com_gas uses com_collapse (invariant-set) instead of propIV1_tendsto. This module follows that precedent exactly.

2. The two theorems

coupled_collapse — the field-level LaSalle collapse

On any flow-invariant set $S$ on which $\mathrm{D}V[f]$ vanishes, $S\subseteq \{0\}$.

Move 1 — $\breve{v}=0$ on $S$ (the Rayleigh step). For $w\in S$, hvanish gives $\mathrm{D}V(w)[f(w)]=0$; hrate rewrites the LHS to $-⟨w.2,\breve{D}w.2⟩$, so $⟨w.2,\breve{D}w.2⟩=0$; and hDdef (definiteness of $\breve{D}$) forces $w.2=0$. hDdef is the abstract face of the sealed Rayleigh bound le_dotProduct_mulVec with $c_1={\lambda }_{\min }(\breve{D})>0$: ${\lambda }_{\min }\Vert w.2{\Vert }^2\le ⟨w.2,\breve{D}w.2⟩=0\Rightarrow w.2=0$. Pin check (2).

Move 2 — the invariance collapse. Fix $y\in S$; $y.2=0$ from Move 1. Because $S$ is invariant, $s\mapsto ({\varphi }_{s}y).2$ is constant $0$ on all of $\mathbb{R}$, so its derivative at $0$ is $0$. But that derivative, read off the flow, is $(fy).2$ (project the orbit’s velocity via HasFDerivAt.comp_hasDerivAt with ContinuousLinearMap.snd, then derivative uniqueness HasDerivAt.unique). Hence

$(fy).2=0.$

Now hfield says the true field’s velocity component is the eq-34b right-hand side $g_2$‘s second component; unfolding g2Field and substituting $y.2=0$ (so $\breve{C}0=\breve{D}0=0$) gives

$(fy).2=-{\breve{M}}^{-1}\left(J_{\tilde{x}}^{\top }\breve{K}\tilde{x}\right)=-\text{Minv}(\text{Jadj}(\text{K}y.1)).$

So $\text{Minv}(\text{Jadj}(\text{K}y.1))=0$; hMinj (${\breve{M}}^{-1}$ injective) gives $J_{\tilde{x}}^{\top }\breve{K}\tilde{x}=0$; and hJKinj — the abstract face of the sealed stiffness_residual_injective' — gives $\tilde{x}=y.1=0$. With $y.2=0$ already, $y=0$. Pin check (3): a nonzero $\tilde{x}$ produces a nonzero $\dot{\breve{v}}$ (5000/5000), so $\{\breve{v}=0\}$ genuinely fails to be invariant off the origin — the collapse is doing real work.

This is com_collapse component-swapped: velocity is the second coordinate here (state $y=(\tilde{x},\breve{v})$) rather than the first, and the terminal injectivity is $J_{\tilde{x}}^{\top }\breve{K}$ (StiffnessResidual) rather than the bare $\breve{K}$.

coupled_gas — the capstone

Every precompact orbit converges to the origin: ${\varphi }_t{y}_0\to 0$.

Assembly (mirrors com_gas):

1. Build the total rate from the sealed previous lane: hrate := fun y => (hreal y).trans (coupled_total_dissipation hMsa hKsa hMinv hJadj hpass y). This is the one place the passivity collapse / Coriolis kill of CoupledDissipation is consumed — no re-proof.
2. hdec := -⟨v,Dv⟩ ≤ 0 from hDnn ($\breve{D}⪰0$).
3. lasalle (L3) $\Rightarrow$ the $\omega$-limit set is invariant (hlas.2.1) and $\mathrm{D}V[f]=0$ on it (hlas.2.2.2).
4. coupled_collapse $\Rightarrow {\omega }^{+}\subseteq \{0\}$.
5. tendsto_infDist_of_omegaLimit_subset (L4a engine) + Metric.infDist_singleton + tendsto_iff_dist_tendsto_zero $\Rightarrow {\varphi }_t{y}_0\to 0$.

coupled_velocity_tendsto — the literal propIV1_tendsto instantiation

The charter named “propIV1_tendsto instantiated with hdec + hzero”. Sealed here honestly: hdec = coupled_hdec (previous lane), hzero = Set.Subset.refl _. Conclusion: convergence to $\{y\mid \mathrm{D}V(y)[f(y)]=0\}$, which by §1 is $\{\breve{v}=0\}$ — the ceiling of the pointwise route, strictly weaker than coupled_gas. It is recorded precisely to make the $\{\breve{v}=0\}$ vs $\{0\}$ gap explicit and machine-checked; the pin’s 5000/5000 counterexamples are the points in this set that the invariance collapse (§2) removes.

3. Mathlib / house stones

Stone	Source	Role
coupled_total_dissipation	CoupledDissipation (sealed)	$\dot{V}=-⟨\breve{v},\breve{D}\breve{v}⟩$ (Coriolis kill)
coupled_hdec	CoupledDissipation (sealed)	$\dot{V}\le 0$ for coupled_velocity_tendsto
g2Field	CoupledField (sealed)	eq-34b velocity dynamics, unfolded in hval
lasalle	LaSalle (sealed L3)	invariant $\omega$-limit + derivative vanishing
tendsto_infDist_of_omegaLimit_subset	Reduction (sealed L4a)	${\omega }^{+}\subseteq \{0\}\Rightarrow$ convergence
propIV1_tendsto	Reduction (sealed L4a)	consumed by coupled_velocity_tendsto
HasFDerivAt.comp_hasDerivAt, HasDerivAt.unique	Mathlib	orbit velocity projection + derivative uniqueness
ContinuousLinearMap.snd … .hasFDerivAt	Mathlib	project the flow’s velocity coordinate
Metric.infDist_singleton, tendsto_iff_dist_tendsto_zero	Mathlib	singleton target $\to$ pointwise limit

4. Interface boundary (the honest list the defense will ask about)

coupled_gas closes Prop IV.1’s attractivity for the driven block modulo exactly these named hypotheses — none a silent sorry, each with its discharge route:

• hϕ : IsSolutionTo ϕ f — the flow solves the ODE (Picard–Lindelöf). The L3 interface precedent; stays applier-side.
• hcpt — precompactness of the orbit closure. Coercivity of $V$ (sealed blockLyap_coercive) bounds the forward orbit; the two-sided closure under Mathlib’s Flow ℝ stays interfaced, identical to com_gas (see com_lasalle.md §5).
• hreal — the state-dependent-operator calculus: the TRUE field carries $\breve{M}(q),\breve{C}(q),\dots$, and its Lyapunov Fréchet-derivative realizes the assembled coupledLyapRate. The single modelling interface CoupledDissipation already names; $g_2$ is its constant-operator linearization.
• hfield : ∀ y, (f y).2 = (g2Field …).2 — new to this lane. The true field’s velocity component is the eq-34b right-hand side. The CoM block did not need this ($f=\text{comField}$ exactly, no Coriolis); here $f\ne g_2$ because hreal needs the state-dependent inertia, so the velocity dynamics enter as their own physical fact. It constrains only the second coordinate and is independent of hreal (which constrains the scalar energy rate).
• hMsa, hKsa, hMinv, hJadj, hpass, hDnn — the CoupledField/CoupledDissipation operator hypotheses (symmetry, inverse, adjoint, passivity, $\breve{D}⪰0$); theorems for the concrete SPD blocks.
• hDdef — $\breve{D}$ definite; concretely the sealed Rayleigh le_dotProduct_mulVec, $c_1={\lambda }_{\min }(\breve{D})>0$.
• hMinj — $\breve{M}$ invertible.
• hJKinj — the abstract transcription of the sealed stiffness_residual_injective' ($\breve{K}\succ 0$, $J_{\tilde{x}}$ square nonsingular). The com hKdef precedent.

The remaining topological cores of the full EHM Theorem 10 assembly — set-stability (hStable) and the relative-attraction collapse (hLandsInΓ₁) of reduction_asymptotic_stability — are the L4b / rung-5 targets and are not touched here; coupled_gas delivers the attractivity half (convergence to the origin), which is what Prop IV.1’s cascade step 2 consumes.

5. What was proven vs. interfaced (one line)

Proven outright: the entire algebraic + LaSalle assembly turning the sealed dissipation identity and residual injectivity into convergence to the origin. Interfaced (named, discharge routes above): the ODE-to-flow bridge, precompactness, the state-dependent-operator calculus, and the eq-34b velocity dynamics. The pin certified the one thing that would have been a false seal — the pointwise hzero ⊆ {0} — and it is not sealed.