Linear algebra

Why graph dimension matters

A finite graph has distances defined by the lengths of its shortest paths. Representing those distances inside a normed vector space lets geometric language describe a combinatorial object, but the number of coordinates required can depend sharply on the graph. The isometric dimension asks for the smallest dimension of any real normed space that preserves every graph distance exactly. Linial, London, and Rabinovich study this invariant alongside metric embeddings and algorithmic uses of graph geometry in their 1995 paper. The cube is a useful test case: its vertices already have an obvious coordinate description, while the theorem must show that no different norm compresses those exact distances into fewer coordinates.

The paper's Section 5.3 relates isometric dimension to the rank of a matrix recording vertex distances in a maximum norm. It then computes the dimension of an even cycle and uses an isometric cycle inside the cube. These are known results of the paper, not an open conjecture. The mission isolates the rank characterization, the cycle calculation, and the cube calculation as reusable formal targets.

Graphs, norms, and the cube

For a finite connected simple graph $G=(V,E)$, let $d_G(x,y)$ be the minimum number of edges in a path from $x$ to $y$. A norm $N$ on $\mathbb R^d$ is nonnegative, vanishes only at zero, satisfies $N(av)=|a|N(v)$, and obeys $N(u+v)\leq N(u)+N(v)$. An isometric embedding is a map $\varphi:V\to\mathbb R^d$ such that $N(\varphi(x)-\varphi(y))=d_G(x,y)$ for every pair of vertices. The number $\dim(G)$ is the least $d$ for which some norm and some such map exist. The paper states the more general metric-space definition in Definition 2.1 and adopts connected graphs as the standing convention in Section 5.1 (pp. 218–219, 229).

The $m$-cube has binary strings $x=(x_1,\ldots,x_m)$ as vertices. Two strings are adjacent when exactly one coordinate differs. Its graph distance is the Hamming distance, the number of differing coordinates. For $m\geq2$, the even cycle $C_{2m}$ has $2m$ vertices in cyclic order, each adjacent to its two neighbors. A graph $J$ is an isometric subgraph of $G$ when its distances between its own vertices agree with their distances in $G$.

An $|V|\times r$ real matrix $M$ implements $G$ when the maximum absolute coordinate difference between rows $i$ and $j$ is $d_G(i,j)$, for every pair. The number of columns $r$ is allowed to vary; the matrix rank is its ordinary linear-algebraic rank. This is the matrix object in Theorem 5.7, p. 232.

Formalization targets

The first main intermediate target is the rank characterization

$$\dim(G)=\min_{M\text{ implements }G}\operatorname{rank}(M).$$

The next is the even-cycle result, stated for $m\geq2$:

$$\dim(C_{2m})=m.$$

The goal is Corollary 5.12, p. 233, for every positive integer $m$:

$$\boxed{\dim(m\text{-Cube})=m.}$$

The milestone list also records the isometric-subgraph lower bound, the nonsingularity of the distance matrix of a path, an isometric embedding of the cube into $\ell_1^m$, and an isometric $C_{2m}$ inside the cube. The paper's proof of the corollary names the last two facts in consecutive sentences (p. 233).

What the result establishes

The upper bound says the familiar $m$ binary coordinates suffice: the cube embeds in $\ell_1^m$ with all distances preserved. The lower bound is stronger than a claim about that particular norm or embedding. It rules out every real normed space of dimension below $m$, regardless of its norm. The even cycle provides a separate exact dimension calculation, while Theorem 5.7 gives a matrix-rank way to study other finite graph metrics. These statements separate the graph invariant from whichever embedding happens to be easiest to draw (Section 5.3, pp. 232–233).

The paper proves these claims mathematically. The remaining formalization work is to build machine-checked proofs of their precise statements, including the finite-dimensional norm interface, graph-distance calculations, implementing matrices, and the rank lower bound. The definitions of normed realization and implementing matrix can be reused for other graphs; the path-distance determinant can be used independently of graph embedding questions. The mission's theorem files are open proof targets, not claims that these proofs have already been checked in Lean.

Where the difficulty lies

Placing binary cube vertices in $\ell_1^m$ gives an immediate candidate for an upper bound, but it cannot by itself exclude embeddings into lower-dimensional spaces with a different norm. The lower bound has to control all norms. Theorem 5.7 converts that unrestricted geometric question into a rank statement for every implementing matrix, and Proposition 5.10 supplies the exact cycle dimension needed by the cube argument (pp. 232–233).

The paper's printed proof of Proposition 5.10 first obtains only $\operatorname{rank}(A)\geq m-1$, then says a more careful analysis yields $m$ without spelling it out. That final rank step is a genuine proof obligation for solvers; the stated proposition and its use in Corollary 5.12 are retained exactly (p. 233). The path-distance matrix cited in that proof is nonsingular when its size is at least two; size one would be a zero matrix.

Formalization scope

Lean represents an arbitrary $d$-dimensional real normed space by a norm function on Fin d → ℝ. This includes every finite-dimensional real normed space up to a choice of coordinates. The isoDim definition takes the least natural-number dimension admitting an isometric embedding, with equality of distances for every vertex pair. The graph metric comes from SimpleGraph.dist; connectedness is explicit where the paper assumes it. The cube is the graph on Fin m → Bool with Hamming-distance-one adjacency, and $C_{2m}$ is Mathlib's cycleGraph (2 * m). The goal assumes $m\geq1$; its $m=1$ case is direct, while the cycle milestones use $m\geq2$. A zero-dimensional cube consists of one vertex and is covered by the auxiliary upper-bound statement, though the goal follows the paper's positive-dimensional convention.

An implementing matrix has arbitrary finite column count. Instead of taking a maximum over an empty index set, the formal definition requires all column differences to be bounded by the graph distance and a column to attain that distance for distinct rows. This agrees with the paper's maximum formula whenever columns are present and handles a one-vertex graph with zero columns. Matrix rank is taken over $\mathbb R$; the path-distance matrix has entries $|r-s|$ for indices $0,\ldots,m-1$. The infimum over achievable dimensions or ranks is a minimum, since these are nonempty subsets of $\mathbb N$ for finite connected graphs. No asymptotic $O(\cdot)$ or $\Omega(\cdot)$ bound occurs in these targets, so there is no hidden constant to instantiate.

The statements require genuine norm axioms and exact graph distances. Allowing a seminorm, assuming the desired dimension bound, or replacing the cube by a path would empty the main claim. Useful contributions include the cube-distance calculation, the path determinant, an exact even-cycle lower bound, and the general rank characterization. The paper makes no running-time claim for these particular results; no algorithmic complexity assertion is included.

Selected references

• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2), 215–245, 1995. DOI: 10.1007/BF01200757.
• J. H. van Lint, R. M. Wilson, A Course in Combinatorics, Cambridge University Press, 1992, pp. 64–65, cited as [44] by Linial et al. for the path distance-matrix fact. Book record.

Motivation

Szemerédi's regularity lemma partitions the vertex set of any graph into a bounded number of parts between which edges are distributed almost randomly. It is a central tool of extremal graph theory, but the number of parts it needs is a tower of exponentials in $1/\epsilon$, which makes it unusable in algorithms. In 1996 and 1999 Frieze and Kannan introduced a weaker notion, now called weak regularity: a partition is good if, for every pair of disjoint vertex sets $S,T$, the number of edges between them is predicted, up to an additive error $\epsilon n^2$, by the densities between the parts. This weaker requirement is enough to approximate dense instances of Max-Cut and other problems, and it can be met with only $2^{O(1/\epsilon^2)}$ parts.

The paper Frieze and Kannan, Quick approximation to matrices and applications, Combinatorica 19 (1999) derives such partitions from a matrix decomposition. Section 5.1 shows that if the adjacency matrix of a graph is approximated by a sum of a few cut matrices with small error in the cut norm, then the atoms of the sets defining those cut matrices form a pseudo-regular partition. The weak regularity of this paper later became the basis of the cut-distance theory of graph limits (Lovász, Large networks and graph limits, AMS, 2012).

Setting

Let $G=(V,E)$ be a simple graph with $n=|V|$ vertices and adjacency matrix $\mathbf A$. For a real $V\times V$ matrix $\mathbf M$ and $S,T\subseteq V$ write $\mathbf M(S,T)=\sum_{i\in S}\sum_{j\in T}\mathbf M(i,j)$. A cut matrix $\mathrm{CUT}(R,C,d)$ has entry $d$ on $R\times C$ and $0$ elsewhere. A cut decomposition of width $s$ is a sum $\mathbf D=\mathbf D^{(1)}+\dots+\mathbf D^{(s)}$ of cut matrices $\mathbf D^{(t)}=\mathrm{CUT}(R_t,C_t,d_t)$; its error is $\mathbf W=\mathbf A-\mathbf D$.

Let $\mathcal P=V_1,\dots,V_k$ be a partition of $V$ with index set $K$, write $X_i=X\cap V_i$, let $e(S,T)$ be the number of edges between disjoint sets $S$ and $T$, and let $d_{i,j}=e(V_i,V_j)/(|V_i||V_j|)$ be the density between parts. The deviation from regularity is

$$\Delta_{\mathcal P}(S,T)=e(S,T)-\sum_{i\in K}\sum_{j\in K}d_{i,j}|S_i||T_j|,$$

and $\mathcal P$ is $\epsilon$-pseudo-regular if $|\Delta_{\mathcal P}(S,T)|\le\epsilon n^2$ for all disjoint $S,T\subseteq V$.

For a partition $\mathcal Q=W_1,\dots,W_q$, the block average $\mathbf M_{\mathcal Q}$ of $\mathbf M$ takes the value $\mathbf M(W_i,W_j)/(|W_i||W_j|)$ on $W_i\times W_j$, and $\mathbf M$ is compatible with $\mathcal Q$ if it is constant on every block $W_i\times W_j$. The atom partition of $R_1,\dots,R_s,C_1,\dots,C_s$ is the coarsest partition of $V$ in which every $R_t$ and $C_t$ is a union of parts; it has at most $4^s$ parts.

Formalization targets

Goal: claim (50), p. 204

If the cut decomposition has error at most $\epsilon n^2$, that is

$$|\mathbf A(S,T)-\mathbf D(S,T)|\le\epsilon n^2\quad\text{for all }S,T\subseteq V,$$

then the atom partition $V_1,\dots,V_k$ of the sets $R_t,C_t$ satisfies

$$|\Delta_{\mathcal P}(S,T)|\le 2\epsilon n^2\quad\text{for all disjoint }S,T\subseteq V,$$

i.e. it is $2\epsilon$-pseudo-regular. The width $s$ is unconstrained: the statement holds for decompositions of any width, and the width only enters through the bound $k\le 4^s$ on the number of parts.

Milestones

1. (47), p. 203. For disjoint $S,T$: $\mathbf A(S,T)=e(S,T)$, $\mathbf A_{\mathcal Q}(S,T)=\sum_{i,j}d_{i,j}|S_i||T_j|$, hence

$$\mathbf A(S,T)-\mathbf A_{\mathcal Q}(S,T)=\Delta_{\mathcal Q}(S,T).$$

2. D is compatible with $\mathcal P$, p. 204. The sum of the cut matrices is constant on every block of the atom partition.
3. Lemma 7(a), p. 203. If $\mathcal Q$ refines $\mathcal P$ and $\mathbf M$ is compatible with $\mathcal P$, then

$$\sup_{S,T\subseteq V}|\mathbf A(S,T)-\mathbf A_{\mathcal Q}(S,T)|\le 2\sup_{S,T\subseteq V}|\mathbf A(S,T)-\mathbf M(S,T)|.$$

Companions

• Lemma 7(b), p. 204. If $\mathbf M$ is compatible with $\mathcal P$, then $\|\mathbf A-\mathbf A_{\mathcal P}\|_F\le\|\mathbf A-\mathbf M\|_F$.
• $k\le 4^s$, p. 204. The atom partition of $2s$ sets has at most $4^s$ parts.

Significance

Claim (50) is the bridge from matrix approximation to graph partitions. Combined with Theorem 7 of the same paper (every matrix has a cut decomposition of width at most $1/\epsilon^2$ with cut-norm error $\epsilon\sqrt{mn}\|\mathbf A\|_F\le\epsilon n^2$ for a graph), it gives the weak regularity lemma: every graph has a $2\epsilon$-pseudo-regular partition into at most $4^{1/\epsilon^2}$ parts. Pseudo-regularity in turn means that $e(S,T)$ is determined up to $2\epsilon n^2$ by the numbers $|S_i|,|T_j|$, which reduces Max-Cut and related problems on dense graphs to a search over a bounded-dimensional space. Lemma 7(a) is of independent use: Section 5.1.1 of the paper applies it again to pass to an equitable refinement.

The results are proved in the paper. Mathlib contains Szemerédi's regularity lemma in its equipartition form, and the platform has a published statement of it; neither the Frieze–Kannan weak regularity statement, the deviation $\Delta_{\mathcal P}$, nor Lemma 7 has a machine-checked proof known to this mission. The mission produces a formal statement and proof of the partition half of the weak regularity lemma, reusable with any cut decomposition, including the existence result of the companion mission on cut decompositions.

Difficulty

The identity (47) and the compatibility of $\mathbf D$ are bookkeeping, but bookkeeping over Mathlib's Finpartition, atomise and the rational-valued edgeDensity, with sums over parts that must be regrouped into sums over vertices. The substance lies in Lemma 7(a). The obvious argument bounds $|\mathbf A-\mathbf A_{\mathcal Q}|$ by $|\mathbf A-\mathbf M|+|\mathbf M-\mathbf A_{\mathcal Q}|$, and the difficulty is the second term: $\mathbf M-\mathbf A_{\mathcal Q}$ is constant on the blocks of $\mathcal Q$, but its block sums on arbitrary $S,T$ have to be controlled by block sums of $\mathbf A-\mathbf M$, on which $\mathbf A$ and $\mathbf A_{\mathcal Q}$ need not agree. The printed argument handles only disjoint $S,T$, while the lemma is stated, and needed, for all pairs; a complete proof must cover pairs that overlap.

Formalization scope

All objects are defined in one definitions item in the namespace FriezeKannan.PseudoReg. The vertex set is a Fintype $V$ with decidable equality, the graph a SimpleGraph V with decidable adjacency, and its adjacency matrix Mathlib's adjMatrix over $\mathbb R$. A partition of $V$ is a Finpartition of Finset.univ, whose parts are the index set $K$; refinement is Mathlib's order $\mathcal Q\le\mathcal P$. Densities are SimpleGraph.edgeDensity, cast to $\mathbb R$, for all pairs of parts. For distinct parts this is the paper's $d(V_i,V_j)$. For a part with itself it is the block average $\mathbf A(V_i,V_i)/|V_i|^2$, not the value $e(A,A)/\binom{|A|}{2}$ printed in the §5 preamble: with the printed value the identity (47) fails on diagonal blocks, and the proof of (50) uses (47). The atom partition is Mathlib's Finpartition.atomise of the family $\{R_t\}\cup\{C_t\}$. The Frobenius norm is the square root of the sum of squared entries.

The paper takes the cut matrices from its Theorem 2, a randomized algorithm. The goal replaces this by the one property its proof uses: the hypothesis $|\mathbf A(S,T)-\mathbf D(S,T)|\le\epsilon n^2$ for all $S,T\subseteq V$ (Theorem 2 bounds the cut norm, a maximum over all pairs, by $\epsilon n\|\mathbf A\|_F\le\epsilon n^2$). The paper's symmetrised error $\bar{\mathbf W}$ is not needed. Lemma 7 is stated for an arbitrary real matrix $\mathbf A$, and the suprema of Lemma 7(a) are written as "every bound $c$ on the right-hand family gives the bound $2c$ on the left-hand family", over all pairs $S,T$. No hypothesis is added to any statement.

The partition in the goal is fixed as the atom partition. A formalization that let the partition vary would be trivial: the partition into singletons has $\Delta\equiv0$.

Needed infrastructure: regrouping sums over a Finpartition, and block sums of matrices constant on the blocks of a partition, on arbitrary and on block-compatible sets. These are reusable for any statement about cut norms of block-constant matrices. Proofs of the milestones, of the companions, and of the goal are all welcome.

Selected references

• A. Frieze and R. Kannan, Quick approximation to matrices and applications, Combinatorica 19(2):175–220, 1999. https://doi.org/10.1007/s004930050052
• A. Frieze and R. Kannan, The regularity lemma and approximation schemes for dense problems, Proc. 37th FOCS, 12–20, 1996. https://doi.org/10.1109/SFCS.1996.548459
• E. Szemerédi, Regular partitions of graphs, Problèmes combinatoires et théorie des graphes, Colloq. Internat. CNRS 260, 399–401, 1978.
• L. Lovász, Large networks and graph limits, AMS Colloquium Publications 60, 2012. https://doi.org/10.1090/coll/060

Motivation

Many problems in optimization and equilibrium modelling, among them linear and nonlinear complementarity problems, variational inequalities over polyhedra, and the Karush–Kuhn–Tucker conditions of nonlinear programs, can be written as a single generalized equation

$$0\in f(x)+\partial\psi_C(x),$$

where $\partial\psi_C$ is the normal-cone operator of a closed convex set $C$. S. M. Robinson introduced strong regularity of such an inclusion at a solution $x_0$ in Strongly regular generalized equations (1980) and proved an implicit-function theorem for it: when the linearised inclusion has a locally unique, Lipschitz inverse, solutions of the perturbed problem exist, are locally unique and depend Lipschitz-continuously on the perturbation. Strong regularity has since become the standard stability notion behind sensitivity analysis and the local convergence of Newton-type methods for variational problems; see Dontchev and Rockafellar, Implicit Functions and Solution Mappings (Springer, 2nd ed. 2014, doi:10.1007/978-1-4939-1037-3).

Strong regularity depends only on the linearisation, so deciding it means deciding it for a linear generalized equation. For a general polyhedral set $C$ the paper's appendix does this by a reduction: locally around $x_0$ the problem is equivalent to a homogeneous problem on a cone, the reduced form, and strong regularity is equivalent to unique solvability of that reduced form. This mission formalizes that appendix and the criterion it yields.

Setting

Work in $\mathbb R^n$ with the standard inner product, which identifies $\mathbb R^n$ with its dual. For $C\subseteq\mathbb R^n$ the normal cone at $x$ is

$$\partial\psi_C(x)=\{y:\langle y,c-x\rangle\le 0\ \text{for all } c\in C\}\ \text{if } x\in C,\qquad \partial\psi_C(x)=\emptyset\ \text{if } x\notin C.$$

A set is polyhedral convex if it is the intersection of finitely many closed half-spaces. Fix a nonempty polyhedral convex $C$, an $n\times n$ real matrix $A$ and $a\in\mathbb R^n$, and consider

$$0\in Ax+a+\partial\psi_C(x).\qquad\text{(A.1)}$$

It is strongly regular at a solution $x_0$ with constant $\lambda$ if there are neighbourhoods $U$ of $0$ and $V$ of $x_0$ such that for each $y\in U$ the perturbed inclusion

$$y\in Ax+a+\partial\psi_C(x)\qquad\text{(A.2)}$$

has exactly one solution $x=s(y)$ in $V$, and $\|s(y_1)-s(y_2)\|\le\lambda\|y_1-y_2\|$ on $U$.

The reduction uses the following objects, all built from the data:

• $y_0:=Ax_0+a$;
• the face $F:=\partial\psi_C^*(-y_0)$, the set of maximisers of $\langle -y_0,\cdot\rangle$ over $C$ (it contains $x_0$);
• the tangent cone $T:=T_F(x_0)=\partial\psi_F(x_0)^\circ$, the polar of the normal cone of $F$ at $x_0$;
• the subspace $L$ parallel to $F$ (the direction of its affine hull) and the orthogonal projector $P_L$;
• the lineality space $M$ of $T$, the subspace $L\cap M^\perp$, and the cone $K:=T\cap M^\perp$.

The reduced form of (A.1) at $x_0$ is the inclusion $z\in P_LAw+\partial\psi_T(w)$ for $z\in L$; in an orthonormal basis adapted to $M$, $L\cap M^\perp$ and $L^\perp$ it is $z\in Bw+\partial\psi_{\mathbb R^r\times K}(w)$ with an $(r+s)\times(r+s)$ matrix $B$. It is vacuous when $L=\{0\}$.

Formalization targets

Goal: Theorem A.4 (p. 60)

If $x_0$ solves (A.1), then (A.1) is strongly regular at $x_0$ if and only if

$$L=\{0\}\quad\text{or}\quad\forall z\in L\ \exists!\,w\in\mathbb R^n:\ z\in P_LAw+\partial\psi_T(w).$$

No Lipschitz constant is fixed: the left side is "strongly regular for some $\lambda$".

Milestones

1. Proposition A.1 (p. 58): for $x_0\in C$, $(C-x_0)\cap U=T_C(x_0)\cap U$ for some neighbourhood $U$ of $0$.
2. Proposition A.2 (p. 58): on $F=\partial\psi_C^*(-y_0)$, $\partial\psi_F(x)=\partial\psi_C(x)+y_0\mathbb R_+$, and $\partial\psi_C^*(-y)\subset F$ for $y$ near $y_0$.
3. Proposition A.3 (p. 58): for $x_0\in F$, near the origin, $0\in(y_0+k)+\partial\psi_C(x_0+h)$ iff $0\in P_Lk+\partial\psi_T(h)$.
4. The correspondence (A.4) (p. 60): for $x$ near $x_0$ and small $y$, (A.2) holds iff $0\in P_L(Ah-y)+\partial\psi_T(h)$ with $h=x-x_0$.

Companions

• Corollary 3.2 (p. 53), in two items. Sufficiency: the reduced form is vacuous, or $B_{11}$ is nonsingular and the Schur complement $B/B_{11}$ is positive definite. Characterisation when $K=\mathbb R^s_+$: strongly regular iff vacuous, or $B_{11}$ nonsingular and $B/B_{11}$ a P-matrix.
• The 3 × 3 linear complementarity example of §4 (p. 53): strongly regular at $x_0=(1,0,0)$, and not strongly regular once the entry $5$ of $A$ becomes $4$.

Significance

Theorem A.4 turns a local stability property, defined through neighbourhoods and an inverse map, into a finite-dimensional algebraic question about one homogeneous problem on a polyhedral cone. Combined with the Schur-complement criterion of Theorem 3.1, it gives checkable conditions (Corollary 3.2): nonsingularity of a block and positive definiteness, or the P-matrix property, of its Schur complement. Through the KKT reformulation of §4 this is the route by which strong second-order sufficiency and linear independence of binding constraint gradients imply strong regularity in nonlinear programming. The example of p. 53 shows the criterion deciding cases where $A$ itself is neither positive definite nor a P-matrix.

The results are classical and proved in the paper; to our knowledge none of them has a machine-checked proof. The formalization adds a coordinate-free statement of the reduced form, which the paper writes only in an adapted basis; a Lean account of exposed faces and tangent cones of polyhedra, with their local conic structure (Propositions A.1–A.2), which the paper lists "without proof" and cites to Rockafellar; and checked versions of the corollary and the example.

Difficulty

The definition of strong regularity is local, while condition (ii) is global on $L$. The obvious argument, "linearise and read off the inverse", does not apply, because $\partial\psi_C$ is a set-valued map whose graph changes shape from point to point. The step that carries the weight is Proposition A.3: a perturbation of $y_0$ may move the solution off the face $F$, and only polyhedrality, through the finitely many values of $\partial\psi_C$ on $F$ and the local conic structure of A.1–A.2, rules this out uniformly in a neighbourhood. The direction from strong regularity to (ii) needs positive homogeneity of the reduced form to pass from uniqueness near $0$ to uniqueness on all of $L$. The direction from (ii) to strong regularity needs the Lipschitz property of a single-valued inverse of a polyhedral multifunction (Robinson 1979, cited as [12, Proposition 2]), which is not elementary.

Formalization scope

• The space is EuclideanSpace ℝ (Fin n), with inclusions written as memberships: (A.2) is $y-(Ax+a)\in\partial\psi_C(x)$. A matrix acts through Matrix.toEuclideanLin. The normal cone carries the clause $x\in C$, so $\partial\psi_C(x)=\emptyset$ off $C$; without it every inclusion would be satisfiable at points outside $C$ and the statements would change meaning.
• $T_C(x_0)$ is the polar of the normal cone, as on p. 58, not the closure of the cone of feasible directions. $F$ is the set of maximisers of $\langle -y_0,\cdot\rangle$ (the sign matters: the opposite face would make the theorem false). $L$ is the direction of the affine span of $F$, and $P_L$ is Mathlib's Submodule.starProjection.
• The reduced form is stated basis-free on $L$; $\partial\psi_T$ is the normal cone of $T$ in all of $\mathbb R^n$. In Corollary 3.2, $B_{11}$ and $B/B_{11}$ are expressed through projectors onto $M$ and $L\cap M^\perp$. Only the case $K=\mathbb R^s_+$ is stated in a basis, an orthonormal basis of $L\cap M^\perp$ in which $K$ is the orthant.
• "Positive definite" does not require symmetry. "Strongly regular" without a constant is existential in $\lambda$, with $\lambda$ real.
• Corollary 3.2's second sentence refers on the page to "(3.8)", an evident slip for (3.9); it is formalized for (3.9).
• The standing assumption "C nonempty polyhedral convex" is a hypothesis of every item.
• A trivializing formalization is ruled out: strong regularity requires existence, uniqueness in $V$ and the Lipschitz bound together, and condition (ii) requires existence and uniqueness for every $z\in L$.
• Needed infrastructure: faces and tangent cones of polyhedra and their local structure (Minkowski–Weyl, finitely many faces), orthogonal decompositions, and Lipschitz continuity of single-valued polyhedral inverses. All of this is reusable beyond this mission. Proofs of the propositions, of the correspondence, and of the companions are welcome independently.

Selected references

• S. M. Robinson, Strongly regular generalized equations, Mathematics of Operations Research 5(1), 43–62, 1980. https://doi.org/10.1287/moor.5.1.43
• S. M. Robinson, Generalized equations and their solutions, Part I: Basic theory, Mathematical Programming Study 10, 128–141, 1979. https://doi.org/10.1007/BFb0120850
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• A. L. Dontchev and R. T. Rockafellar, Implicit Functions and Solution Mappings, 2nd ed., Springer, 2014. https://doi.org/10.1007/978-1-4939-1037-3
• R. W. Cottle, Manifestations of the Schur complement, Linear Algebra and its Applications 8, 189–211, 1974. https://doi.org/10.1016/0024-3795(74)90066-4

Motivation

A constrained system can be written as a generalized equation: a smooth or linear expression must balance the normal cone of a feasible set. This form includes variational inequalities and the first-order conditions of many optimization problems. It is useful to know whether a small change in the right-hand side determines one nearby solution and how far that solution moves. In the linear finite-dimensional case, Robinson's Theorem 3.1 gives matrix conditions that guarantee something stronger: a unique solution for every right-hand side, with one Lipschitz bound valid over the entire space. The theorem also identifies an exact matrix criterion when the feasible set is a product with a nonnegative orthant.

The question is relevant whenever some coordinates of a system are free and others are constrained by inequalities. Eliminating the free coordinates produces a smaller matrix, the Schur complement. The resulting condition can be checked on the reduced block, and in the orthant case it becomes the familiar P-matrix criterion from linear complementarity. Robinson states both claims in a single theorem and relates them to the behavior of a generalized equation rather than to an isolated matrix property Robinson, pp. 51–52.

Setting

Let $r,s$ be positive integers and give $\mathbb R^{r+s}$ its Euclidean norm. Write $w=(w_1,w_2)$, with $w_1\in\mathbb R^r$ and $w_2\in\mathbb R^s$. Let $K\subseteq\mathbb R^s$ be nonempty, closed, and convex, and put $D=\mathbb R^r\times K$. For $w\in D$, the normal cone is

$$N_D(w)=\{v\in\mathbb R^{r+s}:\langle v,c-w\rangle\leq0\text{ for every }c\in D\}.$$

For $w\notin D$, $N_D(w)$ is empty. Thus the inclusion $y\in Aw+N_D(w)$ itself enforces feasibility. This is Robinson's indicator-subdifferential convention Robinson, pp. 43 and 51.

Partition the real square matrix $A$ into blocks $A_{11}$, $A_{12}$, $A_{21}$, and $A_{22}$, where $A_{11}$ is $r\times r$. When $A_{11}$ is nonsingular, its Schur complement in $A$ is

$$A/A_{11}=A_{22}-A_{21}A_{11}^{-1}A_{12}.$$

A real matrix $M$ is positive definite in the theorem's sense when $v^\top Mv>0$ for every nonzero $v$. Symmetry is not assumed. A P-matrix has strictly positive determinants for every nonempty principal submatrix. Write $\mathbb R^s_+$ for the vectors with all components nonnegative. These conventions are stated or used in Theorem 3.1 and its proof.

Formalization targets

General closed convex set

For $T_K(w)=Aw+N_{\mathbb R^r\times K}(w)$, the first target is the sufficient condition

$$\det A_{11}\ne0\quad\text{and}\quad v^\top(A/A_{11})v>0\;(v\ne0) \quad\Longrightarrow\quad T_K^{-1}:\mathbb R^{r+s}\to\mathbb R^{r+s}\text{ is Lipschitz}.$$

Here “is Lipschitz” includes that exactly one inverse value exists at every $y$. The assertion holds for every nonempty closed convex $K$; it is not restricted to polyhedral sets.

Nonnegative orthant

When $K=\mathbb R^s_+$, the second target is an equivalence:

$$T_{\mathbb R^s_+}^{-1}\text{ is everywhere defined, single-valued and Lipschitz} \quad\Longleftrightarrow\quad \det A_{11}\ne0\text{ and }A/A_{11}\text{ is a P-matrix}.$$

The goal theorem is the conjunction of these two statements, matching Theorem 3.1. Its milestones record the paper's local upper Lipschitz assertion for polyhedral multifunctions, the block reduction, the reduced inverse result, the complementarity characterization, and the necessity of nonsingularity.

Significance

The first part gives a global sensitivity guarantee for a generalized equation with an arbitrary nonempty closed convex lower-block constraint. For any two right-hand sides, their unique solutions differ by at most a fixed multiple of the distance between those right-hand sides. The second part tells when this guarantee holds for the orthant model: the P-matrix condition is necessary as well as sufficient. These are the precise conclusions of Robinson's theorem; the mission concerns their machine-checked formalization, not an unresolved mathematical conjecture.

A complete development would provide reusable definitions of the normal-cone generalized equation, an explicitly nonsymmetric notion of positive definiteness, P-matrices, and the global inverse property. It would also formalize the linear complementarity characterization quoted in the paper. The current draft has Lean-checked statements with proof placeholders. No proof of Theorem 3.1 or of its milestones is claimed here.

Difficulty

Nonsingularity of the full matrix $A$ alone does not decide whether the constrained inverse exists uniquely: the normal cone can change as $w_2$ reaches different faces of $K$. A pointwise uniqueness argument also does not by itself supply one Lipschitz constant on all of $\mathbb R^{r+s}$. For the orthant case, checking only the full determinant or leading principal minors would miss the criterion Robinson invokes; every nonempty principal minor matters. The difficulty is to connect a global statement about all right-hand sides with the reduced matrix condition while preserving the normal cone's behavior at boundary points Robinson, pp. 51–52.

Formalization scope

Lean represents $\mathbb R^{r+s}$ as a Euclidean space indexed by the disjoint union of $\mathrm{Fin}(r)$ and $\mathrm{Fin}(s)$. This gives the paper's Euclidean norm rather than the sup norm of a product type. The normal cone is empty off its set, and the inverse property explicitly requires existence for every right-hand side, uniqueness, and one global real Lipschitz bound. The Schur complement appears only with a nonsingular $A_{11}$ in the substantive claims; matrix inversion on a singular input would otherwise be totalized by Lean. Positive definiteness does not add a symmetry hypothesis. The goal retains $r,s>0$ as printed; the paper's later remark about zero-dimensional blocks is outside this theorem.

The polyhedral milestones use finite intersections of closed half-spaces. The reduced-operator milestone uses a nonempty closed convex $K$, matching the theorem's setting. The LCP milestone allows any finite dimension; at dimension zero, both its universal uniqueness statement and its empty-minor P-matrix condition hold. A weaker encoding in which the inverse is merely single-valued where it happens to exist would erase the global conclusion and is excluded here.

Solvers can contribute the block-normal-cone equivalence, the global inverse statement for the reduced operator, the polyhedral Lipschitz result, the P-matrix characterization, and the final theorem. The normal-cone and matrix definitions can also serve later generalized-equation missions that use the same conventions.

Selected references

• S. M. Robinson, Strongly Regular Generalized Equations, Mathematics of Operations Research 5(1), 43–62, 1980. DOI 10.1287/moor.5.1.43.

Why closed-form ADMM updates for ℓ1 problems

Many estimation problems in statistics, machine learning and signal processing minimize a smooth loss plus a nonsmooth ℓ1-type regularizer: the lasso, basis pursuit, least absolute deviations, Huber fitting, the group lasso, and ℓ1-penalized maximum likelihood for Gaussian graphical models. Chapter 6 of Boyd, Parikh, Chu, Peleato and Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers (Found. Trends Mach. Learn. 3(1), 2011), shows that the alternating direction method of multipliers (ADMM) splits each of these problems into a step that touches only the loss and a step that touches only the regularizer, and that each step has a closed form. The practical value of ADMM on these problems rests entirely on those closed forms: an iteration is one cached linear solve, one projection, or one thresholding.

The capstone is sparse inverse covariance selection (§6.5), the ℓ1-penalized Gaussian maximum-likelihood problem of Banerjee, El Ghaoui and d'Aspremont (2008), also solved by the graphical lasso of Friedman, Hastie and Tibshirani (2008). Its ADMM X-update minimizes a log-determinant objective over positive definite matrices, and the book shows that it is solved exactly by one symmetric eigenvalue decomposition.

Setting

All vectors are real and $\|\cdot\|_2$ is the Euclidean norm. For $\kappa\in\mathbb R$ the soft thresholding operator is $S_\kappa(a)=a-\kappa$ if $a>\kappa$, $0$ if $|a|\le\kappa$, and $a+\kappa$ if $a<-\kappa$, applied componentwise to vectors and entrywise to matrices. The vector soft thresholding operator on $\mathbb R^m$ is $\mathcal S_\kappa(a)=(1-\kappa/\|a\|_2)_+a$, with $\mathcal S_\kappa(0)=0$. The Huber penalty is $g^{\mathrm{hub}}(a)=a^2/2$ for $|a|\le1$ and $|a|-1/2$ for $|a|>1$, summed over components for vectors.

In scaled-form ADMM for minimizing $f(x)+g(z)$ subject to $Ax+Bz=c$, with penalty $\rho>0$ and scaled dual variable $u$, the updates are

$$x^{k+1}=\operatorname*{argmin}_x\bigl(f(x)+\tfrac\rho2\|Ax+Bz^k-c+u^k\|_2^2\bigr),\quad z^{k+1}=\operatorname*{argmin}_z\bigl(g(z)+\tfrac\rho2\|Ax^{k+1}+Bz-c+u^k\|_2^2\bigr),$$

followed by $u^{k+1}=u^k+Ax^{k+1}+Bz^{k+1}-c$. "The update is given by formula $F$" means $F$ is the unique minimizer of the corresponding subproblem.

For sparse inverse covariance selection, $S\in\mathbb R^{n\times n}$ is symmetric (the empirical covariance), $\lambda>0$ is the regularization weight, $\|M\|_F^2=\sum_{ij}M_{ij}^2$, $\|M\|_1=\sum_{ij}|M_{ij}|$, and $\mathbb S^n_{++}$ is the set of symmetric positive definite matrices, the domain of $\log\det$. ADMM alternates

$$X^{k+1}=\operatorname*{argmin}_{X\in\mathbb S^n_{++}}\Bigl(\operatorname{Tr}(SX)-\log\det X+\tfrac\rho2\|X-Z^k+U^k\|_F^2\Bigr),\qquad Z^{k+1}=\operatorname*{argmin}_Z\Bigl(\lambda\|Z\|_1+\tfrac\rho2\|X^{k+1}-Z+U^k\|_F^2\Bigr),$$

and $U^{k+1}=U^k+X^{k+1}-Z^{k+1}$.

Formalization targets

Goal: the X-update in closed form (§6.5, p. 47)

Let $S$ and $Z-U$ be symmetric, $\rho>0$, and $\rho(Z-U)-S=Q\,\mathrm{diag}(\mu_1,\dots,\mu_n)\,Q^T$ with $Q^TQ=QQ^T=I$. Then

$$X=Q\,\mathrm{diag}\Bigl(\frac{\mu_i+\sqrt{\mu_i^2+4\rho}}{2\rho}\Bigr)Q^T$$

is positive definite and is the unique minimizer of $\operatorname{Tr}(SX')-\log\det X'+\frac\rho2\|X'-Z+U\|_F^2$ over $X'\in\mathbb S^n_{++}$.

Milestones

1. Scalar root (p. 47): for $\rho>0$, $t=(\mu+\sqrt{\mu^2+4\rho})/(2\rho)$ is positive and $\rho t-1/t=\mu$.
2. Equation (6.5) (p. 47): the matrix $X$ above is positive definite and $\rho X-X^{-1}=\rho(Z-U)-S$.
3. First-order condition (p. 47): a positive definite $X$ minimizes the X-objective over $\mathbb S^n_{++}$ if and only if $S-X^{-1}+\rho(X-Z+U)=0$.
4. Z-update (p. 47): $Z_{ij}=S_{\lambda/\rho}(X_{ij}+U_{ij})$ is the unique minimizer of $\lambda\|Z\|_1+\frac\rho2\|X-Z+U\|_F^2$.
5. Huber z-update (§6.1.1, p. 40): with $v=Ax-b+u$, $z=\frac{\rho}{1+\rho}v+\frac1{1+\rho}S_{1+1/\rho}(v)$ minimizes $g^{\mathrm{hub}}(z)+\frac\rho2\|Ax-z-b+u\|_2^2$.
6. Basis pursuit (§6.2, p. 41): if $AA^T$ is invertible, $(I-A^T(AA^T)^{-1}A)(z-u)+A^T(AA^T)^{-1}b$ is the projection of $z-u$ onto $\{x\mid Ax=b\}$.
7. Lasso (§6.4, p. 43): $(A^TA+\rho I)^{-1}(A^Tb+\rho(z-u))$ minimizes $\frac12\|Ax-b\|_2^2+\frac\rho2\|x-z+u\|_2^2$, and $S_{\lambda/\rho}(x+u)$ minimizes $\lambda\|z\|_1+\frac\rho2\|x-z+u\|_2^2$.
8. Group lasso (§6.4.2, p. 45): blockwise $\mathcal S_{\lambda/\rho}(x_i+u_i)$ minimizes $\lambda\sum_i\|z_i\|_2+\frac\rho2\sum_i\|x_i-z_i+u_i\|_2^2$.

Significance

The closed forms are what make ADMM competitive on these problems. For the lasso the x-update is a ridge regression whose factorization is computed once; for basis pursuit it is a cached projection; the ℓ1 step is a componentwise threshold. For covariance selection the X-update costs one eigenvalue decomposition, and the book (p. 46) cites Scheinberg, Ma and Goldfarb (2010) as showing that ADMM outperforms state-of-the-art methods on this problem. The goal also yields that $X^{k+1}$ is always positive definite, so the iterates remain in the domain of $\log\det$ without a line search.

All statements here are classical and their proofs are elementary convex analysis and linear algebra. A search of the platform found no machine-checked version of any of them. Formalizing them produces verified proximity operators (soft thresholding, vector soft thresholding, Huber, projection onto an affine set) and a verified matrix-function argument for $\log\det$ that later missions on ADMM, proximal methods and Gaussian graphical models can import.

Difficulty

The vector updates reduce to separable one-dimensional problems or to a normal equation, and the difficulty there is bookkeeping: uniqueness, the case $a=0$ of vector soft thresholding, and the three regimes of the Huber prox.

The goal is harder. The book's argument says that $X$ satisfies the gradient equation "and thus minimizes the X-minimization objective". Checking the equation is algebra; the claim to be proved is minimality over the open cone $\mathbb S^n_{++}$, which needs the convexity (indeed strict convexity, for uniqueness) of $-\log\det$ on positive definite matrices and the identification of its gradient with $-X^{-1}$ along symmetric directions. Mathlib has determinants and positive definiteness; a usable convexity statement for $\log\det$ on $\mathbb S^n_{++}$ is not among the platform's published results. Showing that $X$ satisfies (6.5) alone does not establish the goal.

Formalization scope

• Carriers. Vectors are EuclideanSpace ℝ (Fin n), matrices Matrix (Fin m) (Fin n) ℝ acting by Matrix.toEuclideanLin. The Frobenius norm and the entrywise ℓ1 norm are written as explicit sums, not through Mathlib's matrix norm instances. The vector ℓ1 norm is the platform definition HighDimStat.SparseLinear.l1Norm.
• Updates as unique minimizers. Each update is stated as: the book's formula is the unique minimizer of the subproblem (IsUniqueMinimizerOn). Iterates are not defined; the subproblem's data ($z^k$, $u^k$, $x^{k+1}$) are arbitrary.
• Domain of log det. The X-objective is minimized over Matrix.PosDef only. Singular or indefinite matrices are never competitors, so Real.log of a nonpositive determinant plays no role.
• Explicit hypotheses. $S$ and $Z-U$ are assumed symmetric in the goal and the first-order condition; $S$ need not be positive semidefinite. $\rho>0$ everywhere. Basis pursuit assumes $\det(AA^T)\ne0$, which the book uses without stating. The book's $\lambda>0$ is relaxed to $\lambda\ge0$ in the thresholding statements, which contain the book's case.
• Eigendecomposition. The goal holds for every orthogonal $Q$ and real $\mu$ with $\rho(Z-U)-S=Q\,\mathrm{diag}(\mu)Q^T$, not for one decomposition chosen by Mathlib.
• Names. The book uses $\lambda$ for both the regularization weight and the eigenvalues; Lean calls them lam and μ.
• Typo. The book prints $u^k$ in the group-lasso block update; the block $u_i^k$ is stated.
• Ruled out. A goal that only asserts that $X$ satisfies (6.5), or that minimizes over a set extended by Real.log of nonpositive determinants, is not the book's claim; the goal states unique minimality over $\mathbb S^n_{++}$.
• Not stated. Least absolute deviations and the generalized lasso updates (same pattern as milestones 5 and 7), the overlapping group lasso, and the two-step termination claim for Huber fitting on p. 40 (whose formula $x^{\mathrm{ls}}=(A^TA)^{-1}b$ is misprinted).

Contributions welcome: convexity and strict convexity of $-\log\det$ on $\mathbb S^n_{++}$ and its derivative; a general "prox of a separable function is componentwise" lemma; and the projection onto an affine set.

Selected references

• S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 2011, pp. 1–122. https://doi.org/10.1561/2200000016
• O. Banerjee, L. El Ghaoui, A. d'Aspremont, Model Selection Through Sparse Maximum Likelihood Estimation for Multivariate Gaussian or Binary Data, Journal of Machine Learning Research 9, 2008, pp. 485–516. https://jmlr.org/papers/v9/banerjee08a.html
• J. Friedman, T. Hastie, R. Tibshirani, Sparse Inverse Covariance Estimation with the Graphical Lasso, Biostatistics 9(3), 2008, pp. 432–441. https://doi.org/10.1093/biostatistics/kxm045
• K. Scheinberg, S. Ma, D. Goldfarb, Sparse Inverse Covariance Selection via Alternating Linearization Methods, Advances in Neural Information Processing Systems 23, 2010 (reference [148] of the book).
• R. Tibshirani, Regression Shrinkage and Selection via the Lasso, Journal of the Royal Statistical Society B 58(1), 1996, pp. 267–288. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
• M. Yuan, Y. Lin, Model Selection and Estimation in Regression with Grouped Variables, Journal of the Royal Statistical Society B 68(1), 2006, pp. 49–67. https://doi.org/10.1111/j.1467-9868.2005.00532.x

Motivation

Truncated-Newton methods minimize a smooth function $f:\mathbb{R}^n\to\mathbb{R}$ by taking, at each iterate $x_k$, a search direction obtained by solving the Newton equation $H(x_k)p=-g(x_k)$ only approximately, with the linear conjugate gradient (CG) method. Here $g$ is the gradient and $H$ the Hessian of $f$. The approach was analysed by Dembo and Steihaug (Math. Programming 26, 1983), building on the inexact Newton framework of Dembo, Eisenstat and Steihaug (SIAM J. Numer. Anal. 19, 1982), and Newton–CG with curvature tests remains a standard large-scale method (Nocedal and Wright, Numerical Optimization, Ch. 7).

Away from a minimizer the Hessian need not be positive definite, and CG on an indefinite system can produce directions along which $f$ curves downward. The Dembo–Steihaug method stops CG when it meets such a direction. A practical question follows: started at or near a stationary point that is not a local minimizer, will the method ever notice the nonpositive curvature? Theorem 2.4 of the paper answers it for exact CG: it does, except in a degenerate case described by the eigenspaces of $H$.

Setting

Fix a symmetric linear operator $H$ on $\mathbb{R}^n$, with the Euclidean inner product $u^{\mathsf T}v$ and norm $\|\cdot\|$, and a vector $g\in\mathbb{R}^n$. In the paper these are $H(x_k)$ and $g(x_k)$ at the current iterate.

The TNCG minor iteration (p. 194) runs CG on $Hp=-g$ from $p_0=0$. Its state at iteration $i$ is $(p_i,r_i,d_i,\delta_i)$:

$$p_0=0,\quad r_0=-g,\quad d_0=r_0,\quad \delta_0=r_0^{\mathsf T}r_0,$$

and, writing $q_i=Hd_i$,

$$\alpha_i=\frac{r_i^{\mathsf T}r_i}{d_i^{\mathsf T}q_i},\ \ p_{i+1}=p_i+\alpha_id_i,\ \ r_{i+1}=r_i-\alpha_iq_i,\ \ \beta_i=\frac{r_{i+1}^{\mathsf T}r_{i+1}}{r_i^{\mathsf T}r_i},\ \ d_{i+1}=r_{i+1}+\beta_id_i,\ \ \delta_{i+1}=r_{i+1}^{\mathsf T}r_{i+1}+\beta_i^2\delta_i .$$

At iteration $i$ the method first applies the curvature test (2.1), $d_i^{\mathsf T}Hd_i\le\varepsilon\,\delta_i$, and stops if it holds; otherwise it computes $r_{i+1}$ and applies the truncation test (2.2), $\|r_{i+1}\|/\|g\|\le\eta$, and stops if it holds. With $\varepsilon=\eta=0$, (2.1) reads $d_i^{\mathsf T}Hd_i\le0$ and (2.2) reads $r_{i+1}=0$. The method exits through (2.1) at $i$ when no test fired at any iteration $j<i$ and (2.1) holds at $i$.

For $\mu\in\mathbb{R}$ the eigenspace is $E(\mu,H)=\{v: Hv=\mu v\}$ (A.21). The span of vectors $v_1,\dots,v_m$ is written $[v_1,\dots,v_m]$; the Krylov space of $g$ is $[g,Hg,\dots,H^{m}g]$.

Formalization targets

Goal: Theorem 2.4 (p. 197)

Let $\eta_k=\varepsilon=0$. If $H$ is not positive definite, then either the minor iteration exits through (2.1) at some iteration $i$, so that

$$d_i^{\mathsf T}Hd_i\le 0 \quad\text{at an iteration } i \text{ the method reaches},$$

or

$$g^{\mathsf T}v=0\quad\text{for every } v \text{ with } Hv=\mu v,\ \mu\le0 .$$

Milestones

1. Theorem A.1, (A.2) and (A.5), at $\varepsilon=0$ (p. 206). If $d_i^{\mathsf T}Hd_i>0$ for $i=0,\dots,k$, then $d_i^{\mathsf T}Hd_j=0$ for $i\ne j\le k$, and $[d_0,\dots,d_k]=[g,Hg,\dots,H^kg]$.
2. Theorem A.5 (p. 210). If $g$ has a nonzero projection on each eigenspace of $H$, $k$ is the number of distinct eigenvalues, and vectors $d_0,\dots,d_{k-1}$ are $H$-conjugate with $(d_i,Hd_i)>0$ and span $[g,\dots,H^{k-1}g]$, then $H$ is positive definite.
3. The first sentence of the proof of Theorem 2.4 (p. 211). If $g$ is not orthogonal to any eigenspace of $H$, and exact CG passes the curvature test up to iteration $i$ and ends with $r_{i+1}=0$, then $H$ is positive definite.

Significance

The theorem is the theoretical justification, given in the paper on p. 197, for using the direction of negative curvature $d_i$ produced in case (ii) of the minor iteration: with exact arithmetic and no truncation, CG either produces a direction of nonpositive curvature or the gradient lies entirely in the span of eigenvectors with positive eigenvalues. The paper draws the consequence that if $x_k\to x^*$ and the method terminates through (2.2), then, outside this rare case, $x^*$ is a strong local minimizer. Theorem A.5 is a self-contained statement about conjugate families in Krylov spaces, usable in any analysis of CG on indefinite systems.

The result is proved in the paper (Appendix, pp. 206–211), with the CG relations of Theorem A.1 cited from Hestenes and Stiefel. No machine-checked proof of these statements is known to this mission. Formalizing them produces a Lean development of CG on a symmetric, possibly indefinite operator, with its conjugacy and Krylov-span relations, which classical treatments state only for positive definite systems.

Difficulty

The CG relations of Theorem A.1 are usually proved for positive definite $H$, where every denominator is positive. Here $H$ is indefinite, and the relations hold only as long as the curvature along the directions has stayed positive; the induction must carry that hypothesis and must also show the residuals do not vanish early. The passage from "CG ended with $r=0$" to a statement about all eigenspaces is the second obstacle: the CG run sees only the Krylov space of $g$, so one must relate that space to the eigenspaces that $g$ meets, using symmetry of $H$ and a count of distinct eigenvalues. A direct argument via "the directions span $\mathbb{R}^n$" fails, because when $g$ misses an eigenspace the Krylov space is a proper subspace.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n); $H$ is a continuous linear map that is self-adjoint (IsSelfAdjoint H), as the paper's $H$ is a Hessian. Positive definiteness is $v^{\mathsf T}Hv>0$ for all $v\ne0$. The CG recursion is total and carries no stopping test; division by zero returns $0$ in Lean, so states after a would-be stop are junk, and the statements read the iteration only through first-exit predicates. The test (2.2) is encoded in the product form $\|r_{i+1}\|\le\eta\|g\|$.

Theorem 2.4 is stated for an arbitrary symmetric $H$ and vector $g$ rather than at an iterate of a run of the full algorithm. It uses nothing else about $f$ or the run, and every such pair occurs as the Hessian and gradient of an admissible objective. The paper's (A.5) prints $H^{k-1}g$ as the last Krylov vector; the correct $H^kg$ is used.

A trivializing formalization exists and is ruled out: the first alternative is not "$d_i^{\mathsf T}Hd_i\le0$ for some $i$" over the unstopped recursion, which holds automatically once a residual vanishes (the recursion then continues with $d=0$); it requires that iteration $i$ is reached with no earlier exit. The goal does not assume conjugacy, the Krylov span identity, or the hypotheses of Theorem A.5.

A complete development needs the spectral theorem for self-adjoint operators on finite-dimensional spaces (in Mathlib), finiteness of the set of eigenvalues, and the CG invariants. The CG lemmas are reusable for any Newton–CG or trust-region CG analysis. Proofs of the milestones, and of auxiliary CG invariants such as (A.3)–(A.4), are welcome.

Selected references

• R. S. Dembo and T. Steihaug, Truncated-Newton algorithms for large-scale unconstrained optimization, Mathematical Programming 26 (1983) 190–212. https://doi.org/10.1007/BF02592055
• R. S. Dembo, S. C. Eisenstat and T. Steihaug, Inexact Newton methods, SIAM Journal on Numerical Analysis 19 (1982) 400–408. https://doi.org/10.1137/0719025
• M. R. Hestenes and E. Stiefel, Methods of conjugate gradients for solving linear systems, Journal of Research of the National Bureau of Standards 49 (1952) 409–436. https://doi.org/10.6028/jres.049.044
• T. Steihaug, The conjugate gradient method and trust regions in large scale optimization, SIAM Journal on Numerical Analysis 20 (1983) 626–637. https://doi.org/10.1137/0720042
• J. Nocedal and S. J. Wright, Numerical Optimization, 2nd ed., Springer, 2006. https://doi.org/10.1007/978-0-387-40065-5

Motivation

Sparse graphs with small nontrivial eigenvalues, expanders, are basic objects in combinatorics and theoretical computer science. They are used in error-correcting codes, derandomization, sorting networks, and the analysis of random walks. The Alon–Boppana bound says that a $d$-regular graph on $n$ vertices has a nontrivial eigenvalue of absolute value at least $2\sqrt{d-1}-o(1)$ (Alon 1986; Nilli 1991). Graphs that reach $2\sqrt{d-1}$ are Ramanujan graphs.

The classical explicit Ramanujan graphs of Lubotzky, Phillips and Sarnak (1988) and Margulis exist only for degrees $d = p+1$ with $p$ prime, and only for very sparse sequences of vertex counts. Constructions with $\lambda\le 2\sqrt{d-1}+\varepsilon$ for every degree came from Mohanty, O'Donnell and Paredes (STOC 2020, arXiv:1909.06988), but their graphs also do not have every number of vertices. Alon (arXiv:2003.11673, Combinatorica 41, 2021) asked for near-Ramanujan graphs of every degree and every large size. Theorem 1.3 of that paper answers this up to $\varepsilon$: for every $d$, every $\varepsilon>0$ and every large $n$ with $nd$ even there is an explicit $(n,d,\lambda)$-graph with $\lambda\le 2\sqrt{d-1}+\varepsilon$.

Setting

A $(n,d,\lambda)$-graph is a $d$-regular simple graph on $n$ vertices in which every nontrivial eigenvalue of the adjacency matrix $A$ has absolute value at most $\lambda$. The trivial eigenvalue is $d$, with the constant eigenvector $\mathbf 1$. Equivalently, every eigenvalue $\mu$ of $A$ with an eigenvector $f\ne0$, $\sum_v f(v)=0$, satisfies $|\mu|\le\lambda$.

Distances $\operatorname{dist}(v,w)$ are graph distances, and they are $\infty$ between components. The $k$-neighbourhood of a vertex $v$ is $B(v,k)=\{w:\operatorname{dist}(v,w)\le k\}$. The $k$-neighbourhood of an edge $uv$ is $B(u,k)\cup B(v,k)$, and $N_i$ is the set of vertices at distance exactly $i$ from $\{u,v\}$. A set contains no cycle if the subgraph induced on it is a forest. A ball contains at most one cycle if its induced subgraph has at most as many edges as vertices.

The construction starts from a $d$-regular graph $H$ on a vertex set $V$ and a set $U\subseteq V$. Write $N(U)$ for the set of neighbours of $U$, and let $m$ be a perfect matching on $N(U)$. Then $H'$ is the subgraph induced on $V\setminus U$, $M$ is the graph of matching edges $\{x,m(x)\}$, and $G=H'\cup M$.

Formalization targets

Goal: Theorem 1.3, relative to the input graph

Let $d\ge3$, $\varepsilon>0$, $r=\lceil 2/\varepsilon\rceil$. Suppose $H$ is an $(N,d,2\sqrt{d-1}+\varepsilon/2)$-graph in which the $(2r+4)$-neighbourhood of every vertex contains at most one cycle, and $r\le\log_{d-1}N$. Then for every $u$ with $ud$ even and $u\le N/(2d^{2r+3})$,

$$\exists\, G \text{ on } N-u \text{ vertices}:\quad G \text{ is an } \bigl(N-u,\ d,\ 2\sqrt{d-1}+\varepsilon\bigr)\text{-graph}.$$

The hypotheses on $H$ are what Theorem 3.3 (Mohanty–O'Donnell–Paredes) supplies, and that theorem is not formalized.

Milestones

• Lemma 3.1 (p. 10). A $d$-regular graph whose $(2r+4)$-balls contain at most one cycle has a set $U$ with $|U|\ge n/(2d^{2r+3})$, cycle-free $(r+1)$-balls, and pairwise distances $\ge 2r+3$.
• Lemma 3.2 (p. 11). If the $r$-neighbourhood of an edge $uv$ contains no cycle and $A f=\mu f$ with $\mu\ge2\sqrt{d-1}$, then

$$\sum_{w\in N_i}f^2(w)\ \ge\ \sum_{w\in N_{i-1}}f^2(w),\qquad 1\le i\le r .$$

• The variational characterization of nontrivial eigenvalues (§2.4, p. 8).
• In $G=H'\cup M$: $G$ is $d$-regular on $|V|-|U|$ vertices and $A_G=A_{H'}+A_M$. Matching edges have cycle-free $(r-1)$-neighbourhoods and pairwise disjoint $r$-neighbourhoods.
• Inequalities (9), (10), (11) (p. 13), and the spectral step: for every admissible $U$ and $m$, $G$ is an $(N-|U|,d,2\sqrt{d-1}+\varepsilon)$-graph.

Significance

Theorem 1.3 shows that the size restrictions of algebraic Ramanujan constructions cost nothing spectrally: up to an arbitrarily small $\varepsilon$, the Alon–Boppana bound is attained by explicit graphs on every admissible vertex count. The deletion method is local. It turns any near-Ramanujan graph whose short cycles are sparse into graphs of all nearby sizes, so it applies to future constructions as well. Lemma 3.2 is a self-contained delocalization statement in the tradition of Kahale 1995: eigenvectors of eigenvalues at least $2\sqrt{d-1}$ in absolute value cannot concentrate near tree-like edges.

The result is proved on paper. To our knowledge none of it is formalized; Mathlib has adjacency matrices, extended graph distance and acyclicity, but no theory of expanders. A complete development would give machine-checked versions of a delocalization lemma, of the greedy selection of far-apart vertices away from short cycles, and of the variational eigenvalue bound for induced subgraphs. It would also check two points the paper passes over. The proof of Theorem 1.3 treats only positive eigenvalues $\lambda\ge2\sqrt{d-1}$. And its claim that the $r$-neighbourhood of a matching edge is cycle-free fails when two deleted vertices are at distance exactly $2r+3$. This mission states the corrected forms (see Formalization scope).

Difficulty

The spectral bound for $G$ does not follow from interlacing alone. Deleting vertices is harmless, since by (9) the quadratic form of $H'$ is controlled by $H$. But the added matching contributes up to $\sum_{x\in N(U)}f(x)^2$ to $f^tA_Gf$, which can be as large as $\|f\|^2$ for an eigenvector concentrated on $N(U)$. The obvious estimate therefore gives only $\lambda\le 2\sqrt{d-1}+1+\varepsilon/2$. Closing the gap requires showing that an eigenvector of a large eigenvalue spreads its mass over the $r$ layers around each matching edge (Lemma 3.2). That in turn needs those neighbourhoods to be trees in $G$ and pairwise disjoint, which is where Lemma 3.1's choice of $U$ is used. The combinatorial part, tracking distances and cycles in $G$ when $G$ mixes edges of $H$ with matching edges, is the main formalization burden.

Formalization scope

• Representation. Vertex sets are finite types. Graphs are Mathlib SimpleGraphs with real adjacency matrices adjMatrix ℝ. The (n, d, λ) predicate requires IsRegularOfDegree d, symmetry, row sums $d$, and $|\mu|\le\lambda$ for every eigenpair $(\mu,f)$ with $f\ne0$, $\sum f=0$. Distances use the extended SimpleGraph.edist, never dist (which is $0$ across components). Cycle conditions are on induced subgraphs, and "at most one cycle" on a ball is $|E|\le|V|$. Deleted vertices are a Finset U; the new graph lives on the subtype {v // v ∉ U}. The matching is a fixed-point-free involution of $N(U)$.
• Explicit quantities replacing the paper's asymptotics. The paper writes "sufficiently large $n$" and $u=o(n)$. The goal instead takes any $u\le N/(2d^{2r+3})$ (the size Lemma 3.1 guarantees) with $ud$ even, plus Lemma 3.1's side condition $r\le\log_{d-1}N$. The equality $r=\lceil2/\varepsilon\rceil$ is used as $\lceil2/\varepsilon\rceil_+\in\mathbb N$. The paper's "every degree $d$" becomes $d\ge3$, the range of its proof.
• Corrections. (11) and Lemma 3.2's companion are stated for $|\mu|\ge2\sqrt{d-1}$, both signs. The matching-edge note is stated for the $(r-1)$-neighbourhood, which still yields the factor $1/r$ in (11). Lemma 3.2 itself is stated as printed.
• Out of scope. Theorem 3.3 ([18]) is a cited input: its graph is the hypothesis $H$. All claims of explicitness and polynomial running time are out of scope, as is §4's remark on applying the method to LPS graphs directly.
• No trivialization. The input hypotheses are exactly Theorem 3.3's conclusions plus Lemma 3.1's side condition, and they are met by high-girth Ramanujan graphs. No hypothesis mentions the spectrum or Rayleigh quotients of the constructed graph, and the goal's graph must be $d$-regular on exactly $N-u$ vertices.
• Reusable infrastructure. Welcome contributions include the variational characterization for symmetric matrices with constant row sums, a forest edge-count lemma for balls, BFS-layer structure of cycle-free balls in regular graphs, and the edge-disjoint decomposition $A_{G}=A_{H'}+A_M$. Each is useful beyond this mission.

Selected references

• N. Alon, Explicit expanders of every degree and size, arXiv:2003.11673v1, 2020; Combinatorica 41 (2021). https://arxiv.org/abs/2003.11673
• S. Mohanty, R. O'Donnell, P. Paredes, Explicit near-Ramanujan graphs of every degree, STOC 2020. https://arxiv.org/abs/1909.06988
• A. Lubotzky, R. Phillips, P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988). https://doi.org/10.1007/BF02126799
• N. Alon, Eigenvalues and expanders, Combinatorica 6 (1986). https://doi.org/10.1007/BF02579166
• A. Nilli, On the second eigenvalue of a graph, Discrete Mathematics 91 (1991). https://doi.org/10.1016/0012-365X(91)90112-F
• N. Kahale, Eigenvalues and expansion of regular graphs, J. ACM 42 (1995). https://doi.org/10.1145/210118.210136