gamma_invertible

$\mathbf{\Gamma }$ invertibility $⟺$ ${\mathbf{J}}_{{\nu }_e}^{\oplus }$ invertibility

Seal

Rung rung-1 · Status interfaced — each #print axioms reports exactly [propext, Classical.choice, Quot.sound], no sorryAx (recorded in The machine seal; full workspace build 2626 jobs). One named interface: hsvd, the singular-value criterion ${\sigma }_{\min }>0⟺\det \ne 0$ — see interfaces. The determinant and unit biconditionals carry no interface.
Links: module index · interface ledger · related det_gamma_identity · source giordano2019coordinated · pin tasks/streams/leanpunov/scratch/check_gamma_invertible.py · lesson lesson_01_error_floor_cascade

Sealed theorems

isUnit_coordinated_transform

Abstract commutative ring: the block transform is a unit iff its lower-right block is.

det_ne_zero_coordinated_transform

Abstract commutative ring: the two determinants vanish together.

gamma_nonsingular_iff

Thesis $12\times 12$ over $\mathbb{R}$: $\det \mathbf{\Gamma }\ne 0⟺\det {\mathbf{J}}_{{\nu }_e}^{\oplus }\ne 0$.

gamma_isUnit_iff

Thesis instance: $\mathbf{\Gamma }$ invertible $⟺{\mathbf{J}}_{{\nu }_e}^{\oplus }$ invertible.

gamma_isUnit_iff_sigmaMin_pos

The $\Omega$ bridge, given hsvd: the region $\Omega =\{{\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })>0\}$ is exactly where $\mathbf{\Gamma }$ is invertible.

Why this matters

Every downstream theorem of the coordinated architecture carries a standing side-condition: the coordinated transform $\mathbf{\Gamma }$ must be invertible at the current configuration. The controller inverts $\mathbf{\Gamma }$ once per step to recover the generalized velocities, and the singularity-handling layer refuses to enter — or slows the mission — near configurations where that inverse blows up. The singularity-free region is written

$$\Omega =\{q:{\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })(q)>0\}$$

(current_sota.md eq 2.4 §4.6, Giordano 2019 RA-L eq 19 / eq 36). Notice the region is defined by the small $6\times 6$ block ${\mathbf{J}}_{{\nu }_e}^{\oplus }$ — the circumcentroidal Jacobian — not by the full $12\times 12$ transform $\mathbf{\Gamma }$. That is a claim, and it is the claim this note seals: watching the small block is not a heuristic, it is exactly equivalent to $\mathbf{\Gamma }$ being invertible.

L1 already sealed the sharp algebraic fact behind this — the determinant identity $\det \mathbf{\Gamma }=\det {\mathbf{J}}_{{\nu }_e}^{\oplus }$ (det_gamma_identity.md, DetGamma.lean). This note (TARGET 3) turns that equality of scalars into the biconditional of invertibility the side-condition actually needs, and connects it to $\Omega$.

What we prove, and what we interface

Two grades of statement, both sealed:

1. The determinant / unit biconditionals — proved outright from L1:

   • $\det \mathbf{\Gamma }\ne 0⟺\det {\mathbf{J}}_{{\nu }_e}^{\oplus }\ne 0$ (gamma_nonsingular_iff)
   • $\mathbf{\Gamma }$ is a unit $⟺{\mathbf{J}}_{{\nu }_e}^{\oplus }$ is a unit (gamma_isUnit_iff), i.e. the matrices are invertible together, in the ring of matrices.

2. The $\Omega$-region bridge — gamma_isUnit_iff_sigmaMin_pos: the region $\Omega =\{{\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })>0\}$ is exactly where $\mathbf{\Gamma }$ is invertible.

The one fact grade 2 needs that grade 1 does not is the standard singular-value criterion for a square real matrix

$${\sigma }_{\min }(\mathbf{M})>0⟺\det \mathbf{M}\ne 0$$

This is left as a named interface hypothesis hsvd, not proved. See “The one interface” below for exactly why, and what it would take to discharge it. Everything downstream of hsvd — the reduction of the $\Omega$ condition on the small block to invertibility of the full transform — is machine-checked.

Sources and provenance

• Block structure of $\mathbf{\Gamma }$ and the $\Omega$ side-condition: (~/Code/Inspection/GNC/equations/current_sota.md) eq 2.4 and §4.6, transcribing Giordano, Ott & Albu-Schäffer, “Coordinated Control of Spacecraft’s Attitude and End-Effector for Space Robots” (IEEE RA-L 2019), bibkey giordano2019coordinated, eq 19 / eq 36.
• The determinant identity it stands on: det_gamma_identity.md and DetGamma.lean in this directory (L1, sealed).
• Matrix invertibility $⟺$ determinant invertibility: Matrix.isUnit_iff_isUnit_det (Mathlib, LinearAlgebra/Matrix/NonsingularInverse.lean), the formal form of Cramer’s rule / the adjugate identity.
• Unit $⟺$ nonzero in a field: isUnit_iff_ne_zero (Mathlib, Algebra/GroupWithZero/Units/Basic.lean).
• Machine pre-check (biconditional teeth): (~/Code/tasks/streams/leanpunov/scratch/check_gamma_invertible.py), five exact-rational trials 2026-07-06.

A notation note: this document writes ${\mathbf{p}}^{\times }$ for the $3\times 3$ skew-symmetric cross-product operator the source sheet writes $[\mathbf{p}{]}^{\wedge }$; and ${\mathbf{A}}^{\top }$ for the transpose.

The precise statement

As in L1, the arm is nonredundant ($n=6$ joints), so $\mathbf{\Gamma }\in {\mathbb{R}}^{12\times 12}$ is square and its determinant and inverse are defined. The transform, block rows and columns of sizes $3,3,6$, is

$$\mathbf{\Gamma }=\left[\begin{array}{ccc}{\mathbf{R}}_{cb}& -{\mathbf{R}}_{cb}{\mathbf{p}}_{bc}^{\times }& {\mathbf{R}}_{cb}{\bar{\mathbf{J}}}_v\\ 0& \mathbf{E}& 0\\ 0& {\mathbf{G}}_{{\omega }_b}& {\mathbf{J}}_{{\nu }_e}^{\oplus }\end{array}\right]$$

with ${\mathbf{R}}_{cb}\in SO(3)$ and $\mathbf{E}$ the $3\times 3$ identity.

Theorem (invertibility biconditional). At every configuration, $\mathbf{\Gamma }$ is invertible $⟺$ ${\mathbf{J}}_{{\nu }_e}^{\oplus }$ is invertible. Equivalently $\det \mathbf{\Gamma }\ne 0⟺\det {\mathbf{J}}_{{\nu }_e}^{\oplus }\ne 0$.

Corollary ($\Omega$ region). Given the singular-value criterion ${\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })>0⟺\det {\mathbf{J}}_{{\nu }_e}^{\oplus }\ne 0$, the region $\Omega =\{{\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })>0\}$ is exactly the set of configurations at which $\mathbf{\Gamma }$ is invertible.

Proof

The whole argument is a two-line composition — which is the point: once L1 pinned the determinant equality, the invertibility biconditional costs almost nothing, because invertibility of a square matrix is a property of its determinant alone.

Step 1 — the determinant biconditional. L1 gives, at every configuration, $\det \mathbf{\Gamma }=\det {\mathbf{J}}_{{\nu }_e}^{\oplus }$. Two scalars that are equal are zero together and nonzero together, so immediately

$$\det \mathbf{\Gamma }\ne 0⟺\det {\mathbf{J}}_{{\nu }_e}^{\oplus }\ne 0$$

No field structure is used here; it is pure substitution into the L1 identity. This is gamma_nonsingular_iff (and, at the abstract commutative-ring level, det_ne_zero_coordinated_transform).

Step 2 — from determinant to invertibility. For any square matrix over a commutative ring, $\mathbf{M}$ is invertible $⟺\det \mathbf{M}$ is a unit of the ring — this is Cramer’s rule made into an equivalence, Mathlib’s Matrix.isUnit_iff_isUnit_det. Applying it to both $\mathbf{\Gamma }$ and ${\mathbf{J}}_{{\nu }_e}^{\oplus }$ and substituting the L1 equality of determinants,

$$\mathbf{\Gamma }\text{ invertible}⟺\det \mathbf{\Gamma }\text{ a unit}⟺\det {\mathbf{J}}_{{\nu }_e}^{\oplus }\text{ a unit}⟺{\mathbf{J}}_{{\nu }_e}^{\oplus }\text{ invertible}$$

This is gamma_isUnit_iff (abstract level: isUnit_coordinated_transform). It holds over any commutative ring — the base-to-CoM rotation and the identity block do all the work through $\det {\mathbf{R}}_{cb}=1$, exactly as in L1.

Step 3 — the $\Omega$ bridge. Over the field $\mathbb{R}$, a scalar is a unit iff it is nonzero (isUnit_iff_ne_zero), so ”${\mathbf{J}}_{{\nu }_e}^{\oplus }$ invertible” is "$\det {\mathbf{J}}_{{\nu }_e}^{\oplus }\ne 0$". Feeding in the singular-value criterion ${\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })>0⟺\det {\mathbf{J}}_{{\nu }_e}^{\oplus }\ne 0$ (the interface hsvd) and chaining through Step 2,

$${\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })>0⟺\mathbf{\Gamma }\text{ invertible}$$

which is $\Omega =\{\mathbf{\Gamma }\text{ invertible}\}$, the standing side-condition. This is gamma_isUnit_iff_sigmaMin_pos. $\square$

The one interface

gamma_isUnit_iff_sigmaMin_pos takes two arguments that are not proved inside it:

• sigmaMin : Matrix (Fin 6) (Fin 6) ℝ → ℝ — an arbitrary candidate for the smallest-singular-value map. It is a bare function parameter, so the theorem cannot secretly assume anything about it: whatever "${\sigma }_{\min }$" means, the conclusion holds provided it satisfies the next hypothesis.
• hsvd : 0 < sigmaMin J ↔ J.det ≠ 0 — the standard SVD fact that a square real matrix is nonsingular iff its smallest singular value is positive.

Why interface hsvd rather than prove it? Mathlib’s pin (v4.31.0) does carry singular values — LinearMap.singularValues in Mathlib/Analysis/InnerProductSpace/SingularValues.lean — but they are defined on linear maps $T:E\to F$ as an $\mathbb{N}$-indexed Finsupp, with lemmas phrased through finrank and T.range (e.g. injective_iff_forall_lt_finrank_singularValues_pos). There is no library lemma of the form σ_min(matrix) > 0 ↔ det ≠ 0. Discharging hsvd would mean building the whole bridge: matrix $\to$ its toLin', "${\sigma }_{\min }>0$" (an $\inf$ over $i<n$ of an antitone Finsupp) $\to$ injectivity of that map $\to$ det ≠ 0 via the finite-dimensional rank-nullity route. That is precisely the new singular-value machinery TARGET 3 was scoped to avoid, and it is several lemmas past the S-difficulty content here (the determinant biconditional is a two-line composition). Per the campaign’s INTERFACE-don’t-fake rule, hsvd stays a named applier-side hypothesis: it is honest standard mathematics, not a weaker substitute and not a silent sorry. The upgrade path, if a later lane wants it, is exactly the LinearMap.singularValues route named above.

The determinant and unit biconditionals (gamma_nonsingular_iff, gamma_isUnit_iff) carry no interface — they are fully proved from L1.

Post-proof analysis

The moral. $\mathbf{\Gamma }$ adds no invertibility failures of its own. Its volume-preserving coordinates (a rotation, the base angular velocity passed through) can never make an invertible transform singular nor rescue a singular one; the entire loss of rank is inherited from the circumcentroidal block. The controller’s practice of gating on ${\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })$ is therefore exact: $\Omega$ is not an approximation of the invertible region, it is the invertible region.

What it still does not say. As L1 already noted, equal determinants do not mean equal conditioning: ${\sigma }_{\min }(\mathbf{\Gamma })\ne {\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })$ in general, and the empirical Spearman correlation ($\ge 0.9969$, sheet §6) is a separate, weaker statement. This note pins the singular set exactly; it says nothing new about how close to singular the two matrices are.

Cost. Difficulty S, and it felt like it: three theorems that are each a single rw chain over L1 plus two stock Mathlib lemmas, well under an L2-scale push. The only friction was elaboration order — under IsUnit (fromBlocks …) the middle identity block 1 needs an explicit (1 : Matrix (Fin 3) (Fin 3) ℝ) type ascription, because squareness (hence the identity’s row index) is only forced by the Monoid/.det instance that resolves after the block term elaborates. L1’s statement sat under .det, which pinned it earlier, so L1 did not need the ascription.

The machine seal

1. SymPy pre-check (~/Code/tasks/streams/leanpunov/scratch/check_gamma_invertible.py): builds the full $12\times 12$ eq 2.4 structure over exact rationals with a genuine rational $SO(3)$ rotation and the eq 2.2 form of ${\mathbf{G}}_{{\omega }_b}$, then exhibits the biconditional with teeth on both sides — a nonsingular ${\mathbf{J}}_{{\nu }_e}^{\oplus }$ ($\det \ne 0$) forces $\det \mathbf{\Gamma }\ne 0$, and a rank-deficient ${\mathbf{J}}_{{\nu }_e}^{\oplus }$ (last row an integer combination of the others, $\det =0$) forces $\det \mathbf{\Gamma }=0$ no matter what the arbitrary top-right blocks contain. Five trials, all passing 2026-07-06. (The determinant equality itself was already pinned in L1’s check_det_gamma.py; this pin targets the invertibility biconditional specifically.)
2. Lean 4 seal — GammaInvertible.lean in this directory. Five theorems: isUnit_coordinated_transform and det_ne_zero_coordinated_transform (abstract commutative ring), gamma_nonsingular_iff and gamma_isUnit_iff (thesis $12\times 12$ over $\mathbb{R}$, ${\mathbf{R}}_{cb}\in SO(3)$), and the $\Omega$ bridge gamma_isUnit_iff_sigmaMin_pos. Each #print axioms reports exactly [propext, Classical.choice, Quot.sound] — no sorryAx. Built green against the full Leanpunov workspace (2626 jobs) on the Mathlib v4.31.0 pin.