coupled_field

The closed-loop coupled-block field $g_2$, once — TARGET G2 (infrastructure)

Seal

Rung rung-2 · Status interfaced — axiom-clean (#print axioms verbatim in 8. The machine seal; build 2643 jobs), with the operator hypotheses hMsa/hKsa/hMinv/hJadj as named interfaces. Discharges the g2 coordinate field that reduction_cascade and stiffness_residual had to leave un-formalized — as a constant-operator field; the moving-metric calculus (hreal/hfield) stays with the downstream lanes. See interfaces. Public definitions: CoupledState, g2Field, coupledEnergy.
Links: module index · interface ledger · related com_lasalle, coupled_dissipation, coupled_collapse, passivity_transport · source giordano2019coordinated · pin pin_g2_field.py

Sealed theorems

g2Field_origin

${\mathbf{g}}_2(0)=0$ — the origin is an equilibrium of the coupled block.

coupledEnergy_origin

$V(0)=0$.

coupledEnergy_differentiable

The storage function is $C^1$ — the quadratic form of continuous operators is smooth.

coupledEnergy_fderiv

The reusable stone: $DV(y)[w]=⟨\breve{\mathbf{v}},\breve{\mathbf{M}}{w}_2⟩+⟨\tilde{\mathbf{x}},\breve{\mathbf{K}}{w}_1⟩$ for any direction $w$.

coupledEnergy_fderiv_field

The frozen field form: $DV(y)[{\mathbf{g}}_2(y)]=-⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩-⟨\breve{\mathbf{v}},\breve{\mathbf{D}}\breve{\mathbf{v}}⟩$ — the state-space partial, not a stability claim.

What this seals, in one paragraph

Prop IV.1’s cascade (Giordano 2019 RA-L, §IV.D) proves stability in two steps: step 1 is the autonomous CoM driver (sealed in ComLaSalle), step 2 is the driven coupled block ${\dot{\mathbf{z}}}_2={\mathbf{g}}_2({\mathbf{z}}_1,{\mathbf{z}}_2)$ evaluated on the driver-zeroed manifold ${\mathbf{z}}_1=0$. Every downstream stability lane — the $\dot{V}\le 0$ dissipation (hdec), the LaSalle collapse v̆≡0⇒x̃=0 (whose algebra StiffnessResidual already sealed) — differentiates the same storage function $V$ along the same field $g_2$. This module defines that field and that storage function once, in Lean, with the well-formedness and the fderiv-friendly derivative lemma the downstream lanes consume. It makes no stability claim: the sign-definiteness $\dot{V}\le 0$ is deliberately left to the hdec lane, because it is the total time derivative and needs the time-varying-inertia term plus the sealed passivity identity (§5). What is proved here is the field, its equilibrium at the origin, the energy’s smoothness, and the exact algebraic derivative — the shared substrate, frozen against a SymPy pin before a single Lean symbol was written.

The module is (/Code/vault/lean/CoupledField.lean), build copy ~/lean/leanpunov/Leanpunov/CoupledField.lean. SymPy pin (/Code/vault/lean/pin_g2_field.py).

1. The mathematical object

Work on a real inner-product space $H$ (the reduced coupled space; $H={\mathbb{R}}^9$ in the thesis — $\breve{\mathbf{v}}=[{\mathbf{\omega }}_b;{\mathbf{\nu }}_e^{\oplus }]$ and $\tilde{\mathbf{x}}=[{\tilde{\mathbf{x}}}_b;{\tilde{\mathbf{x}}}_e]$ are both $9$-vectors — but nothing here fixes a dimension). Following the brief’s ordering the state is $y=(\tilde{\mathbf{x}},\breve{\mathbf{v}})\in H\times H$, so $y_1=\tilde{\mathbf{x}}$ (the stacked outer-loop error) and $y_2=\breve{\mathbf{v}}$ (the stacked attitude+EE velocity). The seven operators $\breve{\mathbf{M}},\breve{\mathbf{C}},\breve{\mathbf{D}},\breve{\mathbf{K}},{\mathbf{J}}_{\tilde{x}},{\breve{\mathbf{M}}}^{-1},{\mathbf{J}}_{\tilde{x}}^{\top }$ are continuous linear maps $H\to H$ (M C D K J Minv Jadj in the Lean).

The field. On the singularity-free region, with the CoM driver zeroed (${\tilde{\mathbf{x}}}_c={\dot{\tilde{\mathbf{x}}}}_c=0$ on ${\Gamma }_2$, so the $-({\mathbf{C}}_c+\breve{\mathbf{D}}{\breve{\mathbf{G}}}_{v_c}){\dot{\tilde{\mathbf{x}}}}_c$ forcing of eq 4.10 vanishes), the coupled block

$$\dot{\tilde{\mathbf{x}}}={\mathbf{J}}_{\tilde{x}}\breve{\mathbf{v}},\breve{\mathbf{M}}\dot{\breve{\mathbf{v}}}=-\breve{\mathbf{C}}\breve{\mathbf{v}}-\breve{\mathbf{D}}\breve{\mathbf{v}}-{\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}$$

(current_sota.md eq 26 + eq 4.10 / Giordano eq 34b) is the first-order field

$${\mathbf{g}}_2(y)=({\mathbf{J}}_{\tilde{x}}\breve{\mathbf{v}},-{\breve{\mathbf{M}}}^{-1}(\breve{\mathbf{C}}\breve{\mathbf{v}}+\breve{\mathbf{D}}\breve{\mathbf{v}}+{\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}\left)\right).$$

The storage function is the mechanical energy (eq 37 / eq 4.15)

$$V(y)=\frac{1}{2}⟨\breve{\mathbf{v}},\breve{\mathbf{M}}\breve{\mathbf{v}}⟩+\frac{1}{2}⟨\tilde{\mathbf{x}},\breve{\mathbf{K}}\tilde{\mathbf{x}}⟩.$$

Only the inverse ${\breve{\mathbf{M}}}^{-1}$ and the adjoint ${\mathbf{J}}_{\tilde{x}}^{\top }$ enter the field (not $\breve{\mathbf{M}}$ itself); they are supplied operators carrying their defining identities as named hypotheses — hMinv: $\breve{\mathbf{M}}({\breve{\mathbf{M}}}^{-1}w)=w$, and hJadj: $⟨{\mathbf{J}}_{\tilde{x}}a,b⟩=⟨a,{\mathbf{J}}_{\tilde{x}}^{\top }b⟩$. This is the exact ComLaSalle precedent (there $M^{-1}$ was Minv + hMinv), and it keeps the module on a bare inner-product space with no CompleteSpace/adjoint machinery. For a concrete symmetric-PosDef matrix on EuclideanSpace, hMinv is Matrix.nonsingularInverse and hJadj is the standard $⟨Jv,w⟩=⟨v,J^{\top }w⟩$ via Matrix.toEuclideanCLM.

2. Choice of formulation, and why

The brief allows an abstract inner-product space or a concrete EuclideanSpace with matrix operators, “whichever lets the NEXT lane compute fderiv V along the field cleanly.” I chose the abstract inner-product-space formulation, byte-for-byte parallel to ComLaSalle (ComState H = H × H, comField, comEnergy). Reasons:

1. The next lane’s core computation is $DV(y)[\cdot ]$, a Fréchet derivative of a bilinear form. Mathlib’s fderiv_inner_apply is stated on an inner-product space and there is a live in-repo precedent (ComLaSalle.com_dissipation) that this route closes cleanly. A matrix mulVec formulation would force the derivative through Matrix.toEuclideanCLM/WithLp bookkeeping (the rung-1 gotcha: EuclideanSpace elements are not defeq to n → ℝ).
2. The stiffness algebra it eventually feeds — StiffnessResidual — is already sealed at matrix level, so nothing downstream needs $g_2$ to be matrix-shaped; the two meet at the interface, not inside this field.
3. Dimension-freeness: the same field serves the $9$-dim thesis block and any sub-block without re-statement.

State ordering follows the brief: $y=(\tilde{\mathbf{x}},\breve{\mathbf{v}})$, i.e. position first, velocity second — the transpose of ComLaSalle’s $(v,x)$. So here the $\breve{\mathbf{M}}$-block sits on the second projection and the $\breve{\mathbf{K}}$-block on the first; every fst/snd in the Lean is swapped relative to ComLaSalle.

3. The SymPy pin (frozen before the Lean)

pin_g2_field.py verifies four facts; the field definition was frozen only after all four passed.

(1) Total-derivative identity (the house derivation, current_sota eq 38). With $\breve{\mathbf{M}}$ time-varying and $\breve{\mathbf{M}},\breve{\mathbf{K}}$ symmetric,

$$\frac{d}{dt}V=⟨\breve{\mathbf{v}},\breve{\mathbf{M}}\dot{\breve{\mathbf{v}}}⟩+\frac{1}{2}⟨\breve{\mathbf{v}},\dot{\breve{\mathbf{M}}}\breve{\mathbf{v}}⟩+⟨\tilde{\mathbf{x}},\breve{\mathbf{K}}\dot{\tilde{\mathbf{x}}}⟩=-⟨\breve{\mathbf{v}},\breve{\mathbf{D}}\breve{\mathbf{v}}⟩+\frac{1}{2}⟨\breve{\mathbf{v}},(\dot{\breve{\mathbf{M}}}-2\breve{\mathbf{C}})\breve{\mathbf{v}}⟩.$$

Substituting the dynamics: $⟨\breve{\mathbf{v}},\breve{\mathbf{M}}\dot{\breve{\mathbf{v}}}⟩=-⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩-⟨\breve{\mathbf{v}},\breve{\mathbf{D}}\breve{\mathbf{v}}⟩-⟨\breve{\mathbf{v}},{\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}⟩$ (the $\breve{\mathbf{M}}{\breve{\mathbf{M}}}^{-1}=\mathbf{E}$ collapse, symmetry-blind), and $⟨\tilde{\mathbf{x}},\breve{\mathbf{K}}\dot{\tilde{\mathbf{x}}}⟩=⟨\tilde{\mathbf{x}},\breve{\mathbf{K}}{\mathbf{J}}_{\tilde{x}}\breve{\mathbf{v}}⟩$. The two stiffness cross terms $-⟨\breve{\mathbf{v}},{\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}⟩$ and $+⟨\tilde{\mathbf{x}},\breve{\mathbf{K}}{\mathbf{J}}_{\tilde{x}}\breve{\mathbf{v}}⟩$ cancel because $\breve{\mathbf{K}}$ is symmetric and ${\mathbf{J}}_{\tilde{x}}^{\top }$ is the adjoint of ${\mathbf{J}}_{\tilde{x}}$ — this is the “cross-term bookkeeping” the brief names. What remains is $-⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩-⟨\breve{\mathbf{v}},\breve{\mathbf{D}}\breve{\mathbf{v}}⟩+\frac{1}{2}⟨\breve{\mathbf{v}},\dot{\breve{\mathbf{M}}}\breve{\mathbf{v}}⟩=-⟨\breve{\mathbf{v}},\breve{\mathbf{D}}\breve{\mathbf{v}}⟩+\frac{1}{2}⟨\breve{\mathbf{v}},(\dot{\breve{\mathbf{M}}}-2\breve{\mathbf{C}})\breve{\mathbf{v}}⟩$. Pinned symbolic $n=2,3$ (simplify → 0) and numeric $n=3,6,9$ (residual $<3\times 10^{-13}$).

(2) State-space partial — the exact Lean field lemma, no $\dot{\breve{\mathbf{M}}}$ term:

$$DV(y)[{\mathbf{g}}_2(y)]=-⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩-⟨\breve{\mathbf{v}},\breve{\mathbf{D}}\breve{\mathbf{v}}⟩.$$

Same cross-term cancellation, gradient with $\breve{\mathbf{M}},\breve{\mathbf{K}}$ held constant. Pinned symbolic $n=2,3$.

(3) ${\mathbf{g}}_2(0)=0$ (numeric, exact zero). (4) $\breve{\mathbf{M}}$ symmetry is load-bearing for the gradient’s half-term collapse $\frac{1}{2}(S+S^{\top })=S$: with the honest gradient $\frac{1}{2}{\breve{\mathbf{v}}}^{\top }(\breve{\mathbf{M}}+{\breve{\mathbf{M}}}^{\top })$, dropping symmetry leaves a residual $\propto (\breve{\mathbf{M}}-{\breve{\mathbf{M}}}^{\top })$ that vanishes iff $m_{01}=m_{10}$ (symbolic $n=2$, nonzero). Note the subtlety the pin exposed: the $\breve{\mathbf{M}}{\breve{\mathbf{M}}}^{-1}=\mathbf{E}$ term in the field is symmetry-blind; symmetry is used only in collapsing the storage-form gradient, i.e. exactly where hMsa enters the Lean.

4. The Lean, theorem by theorem

g2Field_origin : ${\mathbf{g}}_2(0)=0$. Pure linearity — map_zero on every operator, no hypotheses. The origin is an equilibrium of the coupled block, the target of the whole stability argument.

coupledEnergy_origin : $V(0)=0$, and coupledEnergy_differentiable : $V\in C^1$ — the quadratic form of continuous operators is smooth (differentiableAt_fst/snd, ContinuousLinearMap.differentiableAt, .inner, .const_mul, .add), verbatim the comEnergy_differentiable pattern with the block projections swapped.

coupledEnergy_fderiv (the reusable stone). For $\breve{\mathbf{M}},\breve{\mathbf{K}}$ symmetric and any direction $w$,

$$DV(y)[w]=⟨\breve{\mathbf{v}},\breve{\mathbf{M}}{w}_2⟩+⟨\tilde{\mathbf{x}},\breve{\mathbf{K}}{w}_1⟩.$$

Route. $V$ splits as $\frac{1}{2}⟨{\pi }_2\cdot ,\breve{\mathbf{M}}{\pi }_2\cdot ⟩+\frac{1}{2}⟨{\pi }_1\cdot ,\breve{\mathbf{K}}{\pi }_1\cdot ⟩$; each block’s Fréchet derivative is fderiv_inner_apply composed through the continuous projections (hasFDerivAt_fst/snd) and the operators, assembled by fderiv_add/fderiv_const_mul. fderiv_inner_apply produces, per block, the symmetric pair $⟨y_i,S{w}_i⟩+⟨w_i,S{y}_i⟩$; the reversed term collapses by $⟨w_i,S{y}_i⟩=⟨S{w}_i,y_i⟩=⟨y_i,S{w}_i⟩$ (hMsa/hKsa then real_inner_comm), and the two halves sum to drop the $\frac{1}{2}$. This is the general-direction generalization of com_dissipation’s internal computation, kept direction-free so the hdec lane can instantiate it both at $w={\mathbf{g}}_2(y)$ (below) and at the time-varying-$\breve{\mathbf{M}}$ correction direction that carries the $\frac{1}{2}⟨\breve{\mathbf{v}},\dot{\breve{\mathbf{M}}}\breve{\mathbf{v}}⟩$ term.

coupledEnergy_fderiv_field (the frozen field form). Instantiating $w={\mathbf{g}}_2(y)$ and using hMinv + hJadj,

$$DV(y)[{\mathbf{g}}_2(y)]=-⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩-⟨\breve{\mathbf{v}},\breve{\mathbf{D}}\breve{\mathbf{v}}⟩.$$

Route. $⟨\breve{\mathbf{v}},\breve{\mathbf{M}}({\mathbf{g}}_{2}y{)}_2⟩=-⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}+\breve{\mathbf{D}}\breve{\mathbf{v}}+{\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}⟩$ (map_neg, hMinv, inner_neg_right, inner_add_right), and $⟨\tilde{\mathbf{x}},\breve{\mathbf{K}}({\mathbf{J}}_{\tilde{x}}\breve{\mathbf{v}})⟩=⟨\breve{\mathbf{v}},{\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}⟩$ (hKsa, real_inner_comm, hJadj); the shared $⟨\breve{\mathbf{v}},{\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}⟩$ cancels and ring closes. This is the state-space partial the pin froze — not a stability claim: the surviving Coriolis term $-⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩$ is sign-indefinite.

5. Interfaces, honestly (ponytail)

Proved outright: the field, its equilibrium, the energy’s smoothness, and both derivative lemmas (§4). The following are named, never sorry — the ComLaSalle/IsSolutionTo precedent:

• The dissipation $\dot{V}=-⟨\breve{\mathbf{v}},\breve{\mathbf{D}}\breve{\mathbf{v}}⟩\le 0$ (eq 38) is the hdec lane’s, not this module’s. The field lemma gives the state-space partial $-⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩-⟨\breve{\mathbf{v}},\breve{\mathbf{D}}\breve{\mathbf{v}}⟩$. The total time derivative along a trajectory adds $\frac{1}{2}⟨\breve{\mathbf{v}},\dot{\breve{\mathbf{M}}}\breve{\mathbf{v}}⟩$ because $\breve{\mathbf{M}}=\breve{\mathbf{M}}(\mathbf{q}(t))$ is configuration-dependent. Giordano eq 23 passivity — the sealed Leanpunov.passivity_identity and Leanpunov.transported_passivity_identity (the latter producing the $\dot{\breve{\mathbf{M}}}-2\breve{\mathbf{C}}$ factorization by congruence transport) — gives $\frac{1}{2}⟨\breve{\mathbf{v}},\dot{\breve{\mathbf{M}}}\breve{\mathbf{v}}⟩=⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩$, exactly cancelling the surviving Coriolis term to leave $-⟨\breve{\mathbf{v}},\breve{\mathbf{D}}\breve{\mathbf{v}}⟩$. Both the time-varying-$\breve{\mathbf{M}}$ curve and this cancellation are the hdec lane’s work, named here, mathematically pinned in §3(1).
• hMinv, hJadj — ${\breve{\mathbf{M}}}^{-1}$ and ${\mathbf{J}}_{\tilde{x}}^{\top }$ as supplied operators with their defining identities. Discharged for a concrete SPD matrix on EuclideanSpace by Matrix.nonsingularInverse and the toEuclideanCLM adjoint fact.
• hMsa, hKsa — symmetry of $\breve{\mathbf{M}},\breve{\mathbf{K}}$. For concrete SPD blocks these are theorems (Matrix.PosDef.isHermitian), not assumptions; pinned load-bearing in §3(4).
• No flow / IsSolutionTo here. This module is a static vector field, so it needs no Flow/precompactness interface. Those enter only when the hdec and LaSalle lanes wire $g_2$ into the sealed lasalle engine — consuming coupledEnergy_fderiv_field (for the decrease), StiffnessResidual.stiffness_residual_injective' (for the collapse), and blockLyap_coercive (for boundedness).

6. Mathlib stones used

fderiv_inner_apply (derivative of an inner product), hasFDerivAt_fst/_snd, fderiv_add, fderiv_const_mul, ContinuousLinearMap.differentiableAt/.hasFDerivAt/.comp/.inner, ContinuousLinearMap.fst/snd/comp_apply/coe_fst'/coe_snd', real_inner_comm, inner_add_right, inner_neg_right, map_neg, map_zero. No sealed leanpunov stone is imported (this is upstream infrastructure); the §5 interfaces name the sealed stones that consume it (passivity_identity, transported_passivity_identity, stiffness_residual_injective', blockLyap_coercive) and the pattern it follows (ComLaSalle).

7. Cost feel

At the light end of an L2-scale push. Two of the five theorems (g2Field_origin, coupledEnergy_origin) are one-line simp; coupledEnergy_differentiable is a verbatim ComLaSalle transpose; coupledEnergy_fderiv is the direction-general lift of the com_dissipation computation; coupledEnergy_fderiv_field is a short corollary. One fix cycle (a single real_inner_comm argument order — the convention is $⟨b,a⟩=⟨a,b⟩$, so the LHS carries the second argument first). Well inside the stall gate; the SymPy pin’s caught malformed symmetry test (§3(4)) was the only real thinking beyond transcription.

8. The machine seal

#print axioms on the five theorems, verbatim from the full-integration lake build (2643 jobs, 2026-07-06):

info: Leanpunov/CoupledField.lean:178:0: 'Leanpunov.g2Field_origin' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/CoupledField.lean:179:0: 'Leanpunov.coupledEnergy_origin' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/CoupledField.lean:180:0: 'Leanpunov.coupledEnergy_differentiable' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/CoupledField.lean:181:0: 'Leanpunov.coupledEnergy_fderiv' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/CoupledField.lean:182:0: 'Leanpunov.coupledEnergy_fderiv_field' depends on axioms: [propext, Classical.choice, Quot.sound]

Nothing beyond {propext, Classical.choice, Quot.sound}; no sorryAx. The full project (L1–L4a + TARGET 1 + rung-1 + G2, 29 public theorems) builds clean.