The Smallest Singular Value as a Nonsingularity Criterion

At a glance

A square real matrix is nonsingular exactly when its smallest singular value is positive. This page proves that fact outright for the $6\times 6$ matrices the controller cares about, and uses it to close the one remaining assumption of the coordinated-transform invertibility result. That earlier module characterized the singularity-free region $\Omega =\{{\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })>0\}$ given the singular-value criterion as an explicit named hypothesis (hsvd), because Mathlib’s singular-value theory lives on linear maps between inner-product spaces, not on matrices, and no single library lemma packages ”${\sigma }_{\min }(\text{matrix})>0⟺\det \ne 0$.” Here that hypothesis becomes a theorem: with a genuine smallest singular value in hand, the region result gamma_isUnit_iff_sigmaMinEuclid_pos needs no assumption at all. Lean’s kernel has checked both results end-to-end on the three standard axioms [propext, Classical.choice, Quot.sound], with no sorry and no open assumption.
Links: module index · assumptions ledger · discharges the singular-value assumption of the invertibility result · source giordano2019coordinated · pin tasks/streams/ctrllib/scratch/pin_sigma_min_det.py

Motivation

The controller of the coordinated architecture protects a singularity-free region, the set of configurations where its $12\times 12$ change of coordinates — the coordinated transform $\mathbf{\Gamma }$ — stays invertible. The invertibility result pinned that region exactly: $\mathbf{\Gamma }$ is invertible precisely when its $6\times 6$ lower-right block, the circumcentroidal Jacobian ${\mathbf{J}}_{{\nu }_e}^{\oplus }$, is invertible. But the region the controller actually watches is written with a singular value, not a determinant,

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

and to connect that set to invertibility the earlier module needed one bridge: that a square real matrix is nonsingular exactly when its smallest singular value is positive. Rather than prove this on the spot, it took the criterion as an explicit hypothesis called hsvd and carried it in plain sight. The reason was pragmatic. Mathlib’s pin (v4.31.0) does carry singular values, but only for linear maps between inner-product spaces — LinearMap.singularValues, defined through the range and rank of the map — and there is no packaged lemma of the shape ”${\sigma }_{\min }$ of a matrix is positive iff its determinant is nonzero.” Discharging the criterion means building that bridge by hand.

This page builds it. The idea is not deep — over a field, “smallest singular value positive,” “injective,” and “determinant nonzero” are three names for the same condition on a square matrix — but the formalization has to cross from matrices into the inner-product-space world where singular values are defined, do the antitone bookkeeping that isolates the smallest value, and cross back to the determinant. The payoff is that the region result loses its last assumption: with a genuine smallest singular value substituted for the bare parameter, the characterization of $\Omega$ is proved in full.

The objects

Throughout, $\mathbf{J}$ is a $6\times 6$ real matrix (J : Matrix (Fin 6) (Fin 6) ℝ). Its singular values are the descending, nonnegative numbers $s_0\ge s_1\ge \dots$ obtained as the square roots of the eigenvalues of ${\mathbf{J}}^{\top }\mathbf{J}$. Mathlib supplies these not for the matrix directly but for the associated linear map on Euclidean space, reached through Matrix.toEuclideanLin — the same matrix read as an operator $\mathbf{J}:{\mathbb{R}}^6\to {\mathbb{R}}^6$ carrying the standard inner product, which is the setting in which “singular value” is even defined. On that operator, LinearMap.singularValues returns an $\mathbb{N}$-indexed, nonincreasing, zero-indexed sequence: the six genuine values sit at indices $0$ through $5$, and every index beyond $5$ holds a junk zero (there are only $\mathrm{finrank}=6$ dimensions to fill).

The smallest of the six genuine values therefore sits at index $5$. This is the object the module defines (sigmaMinEuclid):

${\sigma }_{\min }(\mathbf{J})=s_5(\mathbf{J})=\sqrt{{\lambda }_{\min }({\mathbf{J}}^{\top }\mathbf{J})}$

where ${\lambda }_{\min }$ denotes the smallest eigenvalue of the symmetric positive-semidefinite matrix ${\mathbf{J}}^{\top }\mathbf{J}$. This is a genuine smallest singular value, not a weaker stand-in: it is exactly what a numerical linear-algebra library returns as the last entry of a singular-value decomposition.

A word on what is concrete and what is generic. The earlier module’s corollary (gamma_isUnit_iff_sigmaMin_pos) took its smallest-singular-value map as a bare, unconstrained function sigmaMin : Matrix (Fin 6) (Fin 6) ℝ → ℝ, so that whatever "${\sigma }_{\min }$" a caller supplies, the conclusion holds provided that caller also proves the criterion. That generic version stays on the shelf for any consumer with its own notion of ${\sigma }_{\min }$. What this page adds is one concrete choice, sigmaMinEuclid, for which the criterion is discharged once and for all — the pattern already used to discharge the concrete symmetric-positive-definite operator hypotheses elsewhere in the library: define the concrete object, prove the borrowed fact for it as a theorem, and feed it in.

The two results are:

Theorem (the singular-value criterion). For every $6\times 6$ real matrix $\mathbf{J}$, the smallest singular value is positive if and only if the determinant is nonzero: ${\sigma }_{\min }(\mathbf{J})>0⟺\det \mathbf{J}\ne 0$.

Corollary (the region, with nothing assumed). With that criterion in hand at $\mathbf{J}={\mathbf{J}}_{{\nu }_e}^{\oplus }$, the region $\Omega =\{{\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })>0\}$ is exactly the set of configurations at which $\mathbf{\Gamma }$ is invertible — and this now rests on no named hypothesis.

The Singular-Value Criterion (sigmaMinEuclid_pos_iff_det_ne_zero)

Strategy

Work backward from the target ${\sigma }_{\min }(\mathbf{J})>0⟺\det \mathbf{J}\ne 0$. The two sides speak different languages: the left is about a singular value, an analytic object living on an inner-product-space operator; the right is about a determinant, an algebraic object living on the matrix. The classical bridge between them is injectivity. For a square matrix over a field, the following are one and the same condition: the determinant is nonzero, the matrix is invertible, the associated linear map is injective, its kernel is trivial, it has full rank — and its smallest singular value is positive. So the plan is to route from each end to injectivity of the operator $\mathbf{J}:{\mathbb{R}}^6\to {\mathbb{R}}^6$ and meet in the middle. The technique is a chain of biconditionals; there is no single Mathlib lemma spanning the gap, which is exactly why the criterion had to be assumed before and is proved by composition now.

Two subtleties deserve advance warning, because they are where the formal work concentrates.

Isolating the smallest value. Mathlib’s injectivity criterion for a linear map speaks of all the singular values below the dimension, not just the smallest. So we need to collapse the condition ”$s_0,\dots ,s_5$ all positive” down to the single condition ”$s_5$ positive.” This is where the sequence being nonincreasing (antitone) earns its keep, and we return to it in the proof.

Crossing between matrix and operator. The singular values live on toEuclideanLin J, an operator on ${\mathbb{R}}^6$-with-inner-product, whereas the determinant lives on the plain matrix. Passing “injective” from one side to the other is a relabeling of coordinates through the ofLp/toLp equivalence between Euclidean space and the plain function space — no mathematical content, but it must be carried out rigorously rather than waved away.

Proof

Let $\mathbf{J}$ be a $6\times 6$ real matrix, and write $\mathbf{T}=\mathrm{toEuclideanLin}\mathbf{J}$ for the operator it induces on Euclidean ${\mathbb{R}}^6$. We record at the outset that the dimension is fixed, ${\mathrm{finrank}}_{\mathbb{R}}({\mathbb{R}}^6)=6$ (finrank_euclideanSpace_fin); this number governs which indices carry genuine singular values.

Step 1 — from the smallest singular value to injectivity. Axler’s characterization, formalized as injective_iff_forall_lt_finrank_singularValues_pos (Axler, Linear Algebra Done Right, 7.68(a)), states that $\mathbf{T}$ is injective if and only if every singular value with index below the dimension is positive:

$\mathbf{T}\text{ injective}⟺\text{for every }i<6:s_i(\mathbf{J})>0$

We claim this whole family of conditions is equivalent to positivity of the single value at index $5$. One direction is immediate: if all six are positive then in particular $s_5$ is. For the other, suppose $s_5>0$ and let $i<6$. Because the singular-value sequence is nonincreasing — this is singularValues_antitone, the fact that $s_0\ge s_1\ge \dots$ — and $i\le 5$, we have $s_i\ge s_5>0$. So the smallest value dominates the argument: its positivity drags every earlier value along with it. This is the antitone collapse, and it is precisely why watching index $5$ alone suffices. Combining, we obtain

$s_5(\mathbf{J})>0⟺\mathbf{T}\text{ injective}$

that is, ${\sigma }_{\min }(\mathbf{J})>0⟺\mathbf{T}$ is injective.

Step 2 — injectivity as a kernel condition, transported to the matrix. A linear map is injective exactly when the only vector it sends to zero is zero itself (injective_iff_map_eq_zero). Reading this for $\mathbf{T}$ and transporting the statement back across the coordinate relabeling ofLp/toLp — which identifies the operator’s action with the matrix–vector product $\mathbf{J}\mathbf{v}$ — turns operator injectivity into a statement about the matrix:

$\mathbf{T}\text{ injective}⟺(\mathbf{J}\mathbf{v}=0\text{forces}\mathbf{v}=0)$

The transport is bookkeeping — toLp sends a plain vector into Euclidean space, ofLp brings it back, and toLpLin_apply says the operator applied to toLp v is toLp (J *ᵥ v) — so a kernel vector on one side is a kernel vector on the other. No inner-product geometry is used here; only that the two spaces are the same set wearing different labels.

Step 3 — the trivial-kernel condition is nonvanishing of the determinant. This is the classical fact that a square homogeneous system has only the zero solution exactly when its coefficient matrix is nonsingular. Mathlib records the contrapositive as exists_mulVec_eq_zero_iff, valid over any integral domain and in particular over $\mathbb{R}$: there exists a nonzero $\mathbf{v}$ with $\mathbf{J}\mathbf{v}=0$ if and only if $\det \mathbf{J}=0$. Negating both sides, the kernel is trivial if and only if $\det \mathbf{J}\ne 0$:

$(\mathbf{J}\mathbf{v}=0\text{forces}\mathbf{v}=0)⟺\det \mathbf{J}\ne 0$

Conclusion. Chaining the three equivalences — the smallest singular value positive (Step 1), operator injective and hence trivial kernel (Step 2), determinant nonzero (Step 3) — gives

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

which is sigmaMinEuclid_pos_iff_det_ne_zero. $■$

What this shows

The moral is that the smallest singular value is not a soft, approximate proxy for nonsingularity — it is an exact detector. A matrix with a positive smallest singular value is invertible; one with a vanishing smallest singular value is singular; there is no grey zone in between. The determinant and the smallest singular value cross zero at exactly the same configurations. What the antitone collapse adds is efficiency: to certify the whole matrix nonsingular one need only inspect a single number, the last singular value, because the sequence being nonincreasing lets that one number vouch for all the others.

The Region, With Nothing Assumed (gamma_isUnit_iff_sigmaMinEuclid_pos)

Strategy

The earlier module already proved, given the singular-value criterion, that positivity of ${\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })$ is equivalent to invertibility of $\mathbf{\Gamma }$. That proof took the criterion as the hypothesis hsvd attached to a bare parameter. We now have the criterion as a theorem for the concrete map ${\sigma }_{\min }=$ sigmaMinEuclid. So there is nothing left to discover: instantiate the earlier corollary at this concrete map and hand it the freshly proved criterion in place of the assumption.

Proof

Apply gamma_isUnit_iff_sigmaMin_pos — the earlier corollary — with the bare parameter chosen to be the concrete map sigmaMinEuclid, and supply for its hypothesis the theorem sigmaMinEuclid_pos_iff_det_ne_zero proved above. The corollary then reads, with no hypothesis remaining,

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

which is gamma_isUnit_iff_sigmaMinEuclid_pos. $■$

What this shows

The set the controller monitors, $\Omega =\{{\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })>0\}$, is now known — with no fact taken on trust — to be exactly the region where the coordinated transform is invertible. Every link in the chain has been checked by the kernel: from the smallest singular value of the $6\times 6$ circumcentroidal block, through the determinant of that block, through the determinant identity to the determinant of the full $12\times 12$ transform, and out to invertibility of $\mathbf{\Gamma }$. The singularity detector the controller relies on is, end to end, a theorem.

Scope and limitations

• This module assumes nothing. It carries no open named hypothesis; both results are proved in full. What it discharges is the hsvd assumption of the invertibility result, moving that fact from the assumed inputs into the checked interior.
• Concrete, not generic. The discharge is for one specific smallest-singular-value map, sigmaMinEuclid. The earlier bare-parameter corollary (gamma_isUnit_iff_sigmaMin_pos) is deliberately left in place for any consumer that arrives with a different notion of ${\sigma }_{\min }$ and its own proof of the criterion; this page does not remove it, it complements it. The generic statement stays maximally reusable; the concrete statement is the one the controller uses.
• Same singular set, not same conditioning. The criterion is about the sign of the smallest singular value, not its size. Nothing here claims that ${\sigma }_{\min }(\mathbf{\Gamma })$ equals ${\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })$; in general the two matrices are conditioned differently, and the strong empirical rank correlation between them is a separate, weaker statement. This page pins the singular set exactly and says nothing new about how close to singular either matrix is at a given configuration.

Provenance

• The region $\Omega$ and the coordinated transform $\mathbf{\Gamma }$: the house equation sheet (~/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 invertibility biconditional this page consumes is the coordinated-transform invertibility result.
• Singular values of a linear map, and the injectivity criterion: Mathlib’s LinearMap.singularValues and injective_iff_forall_lt_finrank_singularValues_pos (Analysis/InnerProductSpace/SingularValues.lean), formalizing Axler, Linear Algebra Done Right, 7.68(a); the nonincreasing ordering is singularValues_antitone.
• Matrix read as a Euclidean operator: Matrix.toEuclideanLin (Analysis/InnerProductSpace/PiL2.lean).
• Nontrivial kernel iff vanishing determinant: Matrix.exists_mulVec_eq_zero_iff over an integral domain (LinearAlgebra/Matrix/ToLinearEquiv.lean).
• Numerical pre-check of the criterion: (~/Code/tasks/streams/ctrllib/scratch/pin_sigma_min_det.py), 200 random $6\times 6$ trials, both directions.

Machine verification (#print axioms)

The criterion was pre-checked numerically before formalization. The pin (~/Code/tasks/streams/ctrllib/scratch/pin_sigma_min_det.py) draws 200 random $6\times 6$ real matrices and exhibits the biconditional with teeth on both sides: a full-rank draw has determinant well away from zero and smallest singular value well away from zero, while a rank-deficient construction — its last row an exact integer combination of the others — has both the determinant and the smallest singular value at zero. The smallest singular value in the pin is exactly NumPy’s last SVD entry, matching the index-$5$ definition proved here. All 200 trials pass.

The Lean module SigmaMinDet.lean then proves the two results. Each #print axioms query at the foot of the module reports the same three standard axioms and nothing more — no sorryAx:

Ctrllib.sigmaMinEuclid_pos_iff_det_ne_zero   depends on axioms: [propext, Classical.choice, Quot.sound]
Ctrllib.gamma_isUnit_iff_sigmaMinEuclid_pos  depends on axioms: [propext, Classical.choice, Quot.sound]

The module builds against the Mathlib v4.31.0 pin. Source: (~/Code/vault/lean/SigmaMinDet.lean).