Linear algebra

Combinatorics Graph Theory·Captain: mikedeng1

On a Conjecture of Spectral Extremal Problems: If the Extremal Graphs for F Are Turán Graphs Plus a Fixed Number of Edges, Every F-Free Graph of Maximum Spectral Radius Is ExtremalResearch Paper

Motivation

Extremal graph theory asks how many edges a graph on $n$ vertices can have without containing a fixed graph $F$ . The answer, the Turán number $\mathrm{ex}(n,F)$ , and the graphs attaining it, the set $\mathrm{Ex}(n,F)$ of extremal graphs, are known precisely only for special $F$ ; the Erdős–Stone–Simonovits theorem gives $\mathrm{ex}(n,F) = (1 - \frac{1}{\chi(F)-1} + o(1))\frac{n^2}{2}$ , where $\chi(F)$ is the chromatic number.

Spectral extremal graph theory asks the same question with the number of edges replaced by the spectral radius $\lambda(G)$ , the largest eigenvalue of the adjacency matrix. Since $\lambda(G) \ge 2e(G)/n$ , a spectral bound implies an edge bound, and spectral extremal results are usually stronger than their edge versions. Nikiforov (Linear Algebra Appl. 427, 2007) showed that the Turán graph $T_{n,r}$ maximises $\lambda$ among $K_{r+1}$ -free graphs, so for $F = K_{r+1}$ the spectral and the edge extremal graphs coincide. Whether this happens for other $F$ is the subject of the paper.

Timeline:

1941 Turán: $T_{n,r}$ is the unique extremal graph for $K_{r+1}$ .
2003 Chen, Gould, Pfender, Wei (J. Combin. Theory Ser. B 89): $\mathrm{ex}(n, F_{k,r+1}) = e(T_{n,r}) + O(1)$ for $k$ copies of $K_{r+1}$ sharing one vertex.
2007 Nikiforov (Linear Algebra Appl. 427): spectral Turán theorem for $K_{r+1}$ . 2009 Nikiforov (J. Graph Theory 62): spectral stability for large forbidden subgraphs, the source of Lemma 2.5.
2020 Cioabă, Feng, Tait, Zhang (Electron. J. Combin. 27): the spectral extremal graph for the friendship graph $F_k$ lies in $\mathrm{Ex}(n, F_k)$ .
2022 Cioabă, Desai, Tait (European J. Combin. 99) conjecture: if the graphs in $\mathrm{Ex}(n,F)$ are Turán graphs plus $O(1)$ edges, then the spectral extremal graphs lie in $\mathrm{Ex}(n,F)$ for large $n$ . Before the general proof it was known for $K_{r+1}$ , the friendship graphs $F_k$ , the graphs $H_{s,k}$ (Li, Peng) and the intersecting cliques $F_{k,r}$ (Desai, Kang, Li, Ni, Tait, Wang, arXiv:2108.03587).
2022/2023 Wang, Kang, Xue (arXiv:2203.10831; J. Combin. Theory Ser. B, 2023): the conjecture holds in general. This mission formalizes their Theorem 1.2.

Setting

All graphs are finite and simple. For a graph $G$ on $n$ vertices, $A(G)$ is its $0/1$ adjacency matrix and $\lambda(G)$ is the largest eigenvalue of $A(G)$ . A graph $G$ is $F$ -free if no subgraph of $G$ is isomorphic to $F$ . The Turán number $\mathrm{ex}(n,F)$ is the maximum number of edges $e(G)$ over $F$ -free graphs $G$ on $n$ vertices, and $\mathrm{Ex}(n,F)$ is the set of $F$ -free $n$ -vertex graphs with $\mathrm{ex}(n,F)$ edges. The Turán graph $T_{n,r}$ is the complete $r$ -partite graph on $n$ vertices with parts of sizes $\lfloor n/r\rfloor$ or $\lceil n/r\rceil$ .

The hypothesis on $F$ is: for fixed integers $r \ge 2$ and $a \ge 0$ and all large $n$ , $\mathrm{ex}(n,F) = e(T_{n,r}) + a$ and every graph in $\mathrm{Ex}(n,F)$ contains a spanning copy of $T_{n,r}$ , i.e. is $T_{n,r}$ plus $a$ edges. The paper states "adding $O(1)$ edges" and fixes the constant at the start of Section 3 (p. 4): "We may assume that the graphs in $\mathrm{Ex}(n,F)$ are obtained from $T_{n,r}$ by adding $a$ edges." The mission follows that reading. Examples: $K_{r+1}$ with $a = 0$ , the friendship graphs, and the intersecting cliques $F_{k,r+1}$ .

A graph $G$ is spectral extremal for $F$ if it is $F$ -free and $\lambda(G) \ge \lambda(G')$ for every $F$ -free $G'$ on the same $n$ vertices.

Formalization targets

Goal: Theorem 1.2

For $r \ge 2$ , $a \ge 0$ and $F$ satisfying the hypothesis, there is $N$ such that for all $n \ge N$ every spectral extremal graph $G$ for $F$ on $n$ vertices satisfies

e(G) = \mathrm{ex}(n,F), \qquad\text{i.e.}\qquad G \in \mathrm{Ex}(n,F).

The statement contains no numerical constant, and $N$ depends only on $F$ , $r$ , $a$ .

Milestones

The milestones follow the proof, in order: strict monotonicity of $\lambda$ under proper subgraphs of a connected graph (Lemma 2.3); connectivity of $G$ (Lemma 3.1); the bound $\lambda(G) \ge (1-\frac1r)n - \frac{r}{4n} + \frac{2a}{n}$ (Lemma 3.2); spectral stability for $\chi(F) = r+1$ (Corollary 2.6); for every maximum $r$ -cut $V_1 \cup \dots \cup V_r$ , $\sum_i e(V_i) \le \varepsilon n^2$ and $|V_i| = (\frac1r \pm 3\sqrt\varepsilon)n$ (Lemma 3.3); a counting inequality for intersections (Lemma 2.8); $e(G[V_i]) \le a$ and minimum degree above $(1 - \frac1r - 3r\varepsilon^{1/3})n$ (Lemma 3.6); at most $2a$ vertices of each part have a neighbour in that part, and all others see every other part completely (Lemma 3.7); Perron entries $x_u \ge 1 - 20a^2r^2/n$ for $a \ge 1$ (Lemma 3.8); $e(G_{in}) - e(G_{out}) \le a$ (Lemma 3.9); balancing two parts of a complete multipartite graph increases $\lambda$ (Lemma 2.7); and the maximum partition is balanced, $|n_i - n_j| \le 1$ (Lemma 3.10).

Significance

The theorem settles the Cioabă–Desai–Tait conjecture: for every $F$ whose extremal graphs are Turán graphs plus a bounded number of edges, the spectral extremal problem reduces to the edge extremal problem for large $n$ . This recovers the earlier cases (friendship graphs, the graphs $H_{s,k}$ , intersecting cliques) at once, and it turns any future determination of $\mathrm{Ex}(n,F)$ of this type into a spectral result with no further work.

The result is proved on paper; it has no machine-checked proof. Mathlib has Turán's theorem (extremalNumber_top, uniqueness of turanGraph) and the definition of extremalNumber, but no spectral extremal graph theory: no Perron–Frobenius theorem for graphs, no spectral Turán theorem, no stability theorem. The formalization would supply these, and the milestone statements are independently reusable: strict monotonicity of $\lambda$ (Lemma 2.3), the spectral comparison of complete multipartite graphs (Lemma 2.7) and spectral stability (Corollary 2.6) are standard tools of the area.

Difficulty

The natural first idea, comparing $G$ with an extremal graph $H$ by Rayleigh quotients, fails at the start: $\lambda(G) \ge \lambda(H)$ gives only $e(G) \ge e(T_{n,r}) - o(n^2)$ , far from $\mathrm{ex}(n,F)$ . Closing an additive gap of $O(1)$ edges requires control of the Perron vector to within $O(1/n)$ at every vertex and exact control of the part sizes. The second is the delicate step: an imbalance of one vertex between two parts costs $\Theta(1/n)$ in $\lambda$ , while the $a$ extra edges contribute only $O(1/n^2)$ beyond the Turán graph, so the two effects must be compared at different scales. Further, the proof needs the deep spectral stability theorem of Nikiforov (Lemma 2.5), whose own proof is long.

Formalization scope

Graphs on $n$ vertices are SimpleGraph (Fin n), matching Mathlib's extremalNumber n F; $F$ is a graph on any finite type. $\lambda(G)$ is the largest eigenvalue of G.adjMatrix ℝ (index $0$ of Mathlib's decreasingly sorted eigenvalues₀), not an absolute value and not a norm. " $F$ -free" is F.Free G (no copy of $F$ , not necessarily induced). "Sufficiently large $n$ " is ∃ N, ∀ n ≥ N with $N$ chosen after $F, r, a$ and before $G$ ; "sufficiently small $\varepsilon$ " is ∃ ε₀ > 0, ∀ ε ∈ (0, ε₀). Partitions $V_1 \cup \dots \cup V_r$ are labellings Fin n → Fin r whose parts may be empty; the Section 3 lemmas hold for every partition maximising the number of crossing edges. Lemma 3.8 carries the extra hypothesis $a \ge 1$ , because as printed it is false for $a = 0$ (for $F = K_{r+1}$ and $r \nmid n$ the Perron vector of $T_{n,r}$ has entries below $1$ ); the goal does not assume it.

Trivializing formalizations are ruled out: $\lambda$ is not defined from the edge count (which would make spectral and edge extremality the same), the hypothesis on $F$ does not contain the conclusion and is satisfiable (a sorry-free check for $F = K_{r+1}$ , $a = 0$ was compiled), the conclusion is $e(G) = \mathrm{ex}(n,F)$ and not a weaker bound, and the threshold is not chosen after $G$ .

A complete development needs the Perron–Frobenius theorem for irreducible nonnegative symmetric matrices, the Rayleigh quotient characterisation of $\lambda$ , the spectrum of complete multipartite graphs, Nikiforov's spectral stability lemma, and max-cut partition arguments. All of these are reusable beyond this mission, and proofs of any milestone, of the cited Lemmas 2.1, 2.2 and 2.5, or of Nikiforov's spectral Turán theorem are welcome.

Selected references

J. Wang, L. Kang, Y. Xue, On a conjecture of spectral extremal problems, J. Combin. Theory Ser. B, 2023; arXiv:2203.10831v1 (2022). https://arxiv.org/abs/2203.10831
S. Cioabă, D. N. Desai, M. Tait, The spectral radius of graphs with no odd wheels, European J. Combin. 99 (2022) 103420.
S. Cioabă, L. H. Feng, M. Tait, X. D. Zhang, The maximum spectral radius of graphs without friendship subgraphs, Electron. J. Combin. 27(4) (2020) P4.22.
G. Chen, R. J. Gould, F. Pfender, B. Wei, Extremal graphs for intersecting cliques, J. Combin. Theory Ser. B 89 (2003) 159–171.
V. Nikiforov, Bounds on graph eigenvalues II, Linear Algebra Appl. 427 (2007) 183–189.
V. Nikiforov, Stability for large forbidden subgraphs, J. Graph Theory 62(4) (2009) 362–368.
D. N. Desai, L. Kang, Y. Li, Z. Ni, M. Tait, J. Wang, Spectral extremal graphs for intersecting cliques, arXiv:2108.03587v2 (2021). https://arxiv.org/abs/2108.03587

18 thms2 active usersReviewed

Completed

Numerical Analysis Operations Research Optimization·Captain: mikedeng1

Conjugate Gradient Methods with Inexact Searches: The Self-Scaled Direction Is a Multiple of Beale's Restart DirectionResearch Paper

Motivation

Conjugate gradient methods minimize a smooth function $f:\mathbb R^n\to\mathbb R$ using only gradients and a handful of stored vectors. This makes them the standard choice when $n$ is too large for Newton or quasi-Newton methods, which store an $n\times n$ matrix. On a strictly convex quadratic with exact line searches the classical method of Hestenes and Stiefel terminates in at most $n$ steps. On general functions, and with the inexact line searches used in practice, its behaviour is much less clear.

D. F. Shanno's 1978 paper in Mathematics of Operations Research (doi:10.1287/moor.3.3.244) links conjugate gradient methods to quasi-Newton methods. It writes the search direction as $-\hat H g$ , where $\hat H$ is a positive definite approximation of the inverse Hessian that is never stored. The resulting "memoryless" BFGS directions give descent without exact line searches. The paper's new algorithm uses two BFGS updates: one from the last restart and one from the current step. Its first update is scaled by the Oren–Spedicato factor $\gamma_t$ . Shanno and Phua's CONMIN code implements the algorithm, and the memoryless BFGS direction is the one-pair case of the later limited-memory BFGS methods.

1952: Hestenes and Stiefel, linear conjugate gradients.
1964: Fletcher and Reeves, nonlinear conjugate gradients.
1969: Polak and Ribière, a second nonlinear variant.
1972: Beale, a restart procedure that keeps the computed direction $d_t$ .
1977: Powell's restart criterion (Powell 1977).
1978: Shanno's reformulation as memoryless and two-update quasi-Newton methods (this paper).

Setting

Vectors are columns in $\mathbb R^n$ . A prime denotes transpose: $u'v$ is the inner product and $uv'$ the outer product. An iterative method produces points $x_k$ , steps $p_k = x_{k+1}-x_k = \alpha_k d_k$ along search directions $d_k$ , gradients $g_k = \nabla f(x_k)$ , and gradient changes $y_k = g_{k+1}-g_k$ . A line search is exact when $p_k'g_{k+1} = 0$ .

The BFGS update of a matrix $H$ with the pair $(p,y)$ is

H^+ = H - \frac{p\,y'H + H y\,p'}{p'y} + \left(1+\frac{y'Hy}{p'y}\right)\frac{pp'}{p'y}.

A restart cycle begins at iteration $t$ . At a later iteration $k>t$ , Shanno's self-scaled restart matrix is

\hat H_k = \gamma_t\left(I - \frac{p_ty_t'+y_tp_t'}{p_t'y_t} + \frac{y_t'y_t}{p_t'y_t}\frac{p_tp_t'}{p_t'y_t}\right) + \frac{p_tp_t'}{p_t'y_t}, \qquad \gamma_t = \frac{p_t'y_t}{y_t'y_t}.

The matrix $\hat H_{k+1}$ is its BFGS update with $(p_k,y_k)$ , and the self-scaled two-update direction is $d_{k+1} = -\hat H_{k+1}g_{k+1}$ . The unscaled variant uses the BFGS update of $I$ in place of the first matrix.

Beale's direction is

d_{k+1} = -g_{k+1} + \frac{y_k'g_{k+1}}{d_k'y_k}d_k + \frac{y_t'g_{k+1}}{d_t'y_t}d_t.

The quadratic case has gradient $g(x) = Ax + c$ with $A$ symmetric positive definite.

Formalization targets

Goal: reduction of the self-scaled method to Beale's method

Let $A$ be symmetric positive definite, $g_i = Ax_i + c$ and $t<k$ . Assume that for $t\le i\le k$ we have $x_{i+1} = x_i + p_i$ , $p_i = \alpha_i d_i$ and $p_i'g_{i+1}=0$ , that $p_t'Ap_i = 0$ for $t<i\le k$ , and that $p_t, p_k \ne 0$ . Then

-\hat H_{k+1}g_{k+1} = \gamma_t\left(-g_{k+1} + \frac{y_k'g_{k+1}}{d_k'y_k}d_k + \frac{y_t'g_{k+1}}{d_t'y_t}d_t\right).

This is the paper's claim that "for $f(x)$ quadratic with exact searches each of the above methods reduces exactly to Beale's method defined by (28)", with the conclusion (44). The scale is exactly $\gamma_t$ .

Companion statements

The unscaled two-update direction equals Beale's direction exactly.
Both two-update directions are descent directions, $g_{k+1}'d_{k+1} < 0$ , whenever $p_t'y_t > 0$ and $p_k'y_k > 0$ . No exact search is needed.

Milestones on the path

(34): the expansion of $-\hat H_{k+1}g_{k+1}$ .
(40): its form under an exact search.
(41): gradients along a run on a quadratic.
$p_t'g_{k+1} = 0$ .
(38), corrected by a factor 2: the action of the self-scaled restart matrix.
(42): its form when $p_t'g_{k+1} = 0$ .
(43): the direction after substitution.

Significance

The result. The reduction says that the new algorithm reproduces Beale's restarted conjugate gradient directions on a quadratic with exact line searches. So it keeps the finite-termination and rate-of-convergence properties behind Beale's restart. Away from that setting it behaves as a quasi-Newton method, whose directions are descent directions under any line search with $p'y>0$ . The two regimes are what justify relaxing the line search, which the paper's computations exploit. The scale $\gamma_t$ changes only the length of the step, not its direction.

Formalizing it. The claim is proved in the paper by a short computation, and no machine-checked version is known. This mission produces:

a checked statement of the claim with every hypothesis explicit, including the conjugacy the proof takes as known;
a corrected version of display (38), which is misprinted;
reusable definitions of the additive BFGS update and of Beale's direction.

Difficulty

The obvious attempt is to expand both BFGS updates symbolically and compare with Beale's formula. This fails without two facts that are not algebraic identities. The first is that the restart step stays orthogonal to every later gradient, $p_t'g_{k+1}=0$ . It needs the affine gradient of a quadratic, the exact search at the restart step, and conjugacy of $p_t$ with all later steps. The second is $y_k'p_t = 0$ , which again comes from conjugacy. Beale's formula also has to be matched in its $d$ -form: the coefficient $\frac{y'g}{d'y}d$ equals $\frac{y'g}{p'y}p$ only when the step length is nonzero. The descent statements need a different argument: the BFGS update of a positive definite matrix with $p'y>0$ must be shown to remain positive definite, and this has to be done twice.

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ. The inner product $u'v$ is u ⬝ᵥ v, the outer product $uv'$ is vecMulVec u v, and $Hv$ is H *ᵥ v. The quadratic enters only through its gradient A *ᵥ x + c with A.PosDef. The paper's (4) is the case $c = -A\hat x$ . Iterates, steps, directions and gradients are sequences indexed by ℕ. Division is Lean's total division. Every statement that divides therefore carries hypotheses making its denominators nonzero: $p_t \ne 0$ and $p_k\ne0$ in the quadratic statements, and $p_t'y_t\ne 0$ or $p'y>0$ in the generic ones.

The conjugacy $p_t'Ap_i=0$ for $t<i\le k$ is a hypothesis, exactly as the paper's proof uses it. It is not derived from a full run of Beale's algorithm. The range $k\le t+n-1$ of Beale's formula is not assumed.

Several formalizations would make the claim easier than the paper's, and none of them is used:

defining the direction by the expanded formula (34), or the restart matrix by (38);
adding orthogonality or conjugacy hypotheses beyond those listed;
concluding only that the two directions are parallel;
dropping the restart term of Beale's direction;
allowing a zero denominator.

The generic milestones — (34), (40), (38), (42), (43) and the descent statements — are statements about arbitrary vectors and matrices and are reusable for any BFGS-based method. Proofs of any milestone, and alternative derivations of the goal, are welcome.

Selected references

D. F. Shanno, Conjugate Gradient Methods with Inexact Searches, Mathematics of Operations Research 3(3) (1978) 244–256. https://doi.org/10.1287/moor.3.3.244
E. M. L. Beale, A derivation of conjugate gradients, in F. A. Lootsma (ed.), Numerical Methods for Nonlinear Optimization, Academic Press, 1972, 39–43.
M. J. D. Powell, Restart procedures for the conjugate gradient method, Mathematical Programming 12 (1977) 241–254. https://doi.org/10.1007/BF01593790
M. R. Hestenes and E. Stiefel, Methods of conjugate gradients for solving linear systems, J. Res. Nat. Bur. Standards 49 (1952) 409–436. https://doi.org/10.6028/jres.049.044
S. S. Oren and E. Spedicato, Optimal conditioning of self-scaling variable metric algorithms, Mathematical Programming 10 (1976) 70–90. https://doi.org/10.1007/BF01580654

18 thms2 active usersReviewed

Control Theory Dynamical Systems·Captain: mikedeng1

Stabilization for a Perturbed Chain of Integrators in Prescribed Time I: Prescribed-Time Estimates for the Linear Time-Varying FeedbackResearch Paper

Motivation

Many control tasks have to settle at a given deadline, not merely eventually. Examples are missile guidance, where the interception time is fixed in advance, and rendezvous or consensus manoeuvres that must finish by a scheduled instant. Prescribed-time stabilization asks for a feedback that brings the state of a system to the origin at a time $T>0$ chosen by the designer, independently of the initial condition, and keeps this property under disturbances. It is stronger than finite-time stabilization, where the settling time depends on the initial state, and stronger than fixed-time stabilization, where it is only bounded uniformly.

Song, Wang, Holloway and Krstić (Automatica 2017) obtained prescribed-time regulation of normal-form systems with feedback gains that grow without bound as $t\to T$ . The computations required explicit time derivatives of the gain function. Chitour, Ushirobira and Bouhemou (SIAM J. Control Optim. 2020) recast this construction as time-varying homogeneity: a time-dependent dilation of the state combined with a change of time turns the prescribed-time problem into a standard exponential-stabilization problem on an infinite horizon. The analysis then reduces to linear matrix inequalities. This mission formalizes the linear-feedback part of that paper (§3.1, pp. 1026–1030).

Timeline:

2010: Chitour and Sigalotti (SIAM J. Control Optim. 48) prove a Lyapunov LMI for $J_n - b e_n K^T$ , uniform over a bounded range $\underline b\le b\le\bar b$ .
2017: Song, Wang, Holloway and Krstić give prescribed-time regulation with a time-varying feedback.
2020: Chitour, Ushirobira and Bouhemou remove the upper bound $\bar b$ (Proposition 10) and derive the prescribed-time estimate by time-varying homogeneity (Corollary 14).

Setting

Fix a positive integer $n$ and a prescribed time $T>0$ . Let $(e_i)_{1\le i\le n}$ be the canonical basis of $\mathbb R^n$ , and let $J_n$ be the $n$ -th Jordan block, $J_n e_i = e_{i-1}$ with $e_0=0$ . The perturbed chain of integrators is

\dot x(t) = J_n x(t) + \big(d(t) + b(t)u(t)\big) e_n, \qquad t\in[0,T),

with state $x(t)\in\mathbb R^n$ and control $u(t)\in\mathbb R$ . Here $d$ is a measurable matched disturbance, and $b$ is an uncertain control gain with $b(t)\ge\underline b>0$ and no upper bound.

With weights $r_i = n-i+1$ , the dilation is $D^{\mathbf r}_\mu = \operatorname{diag}(\mu^{r_1},\dots,\mu^{r_n})$ and $D_{\mathbf r} = \operatorname{diag}(r_1,\dots,r_n)$ . An admissible weight is a continuous function $a\ge0$ on $[0,T]$ with $\int_t^T a>0$ for $t<T$ . It defines

\lambda(t) = \frac{1}{\int_t^T a(\xi)\,d\xi},\qquad s(t) = \int_0^t\lambda(\xi)\,d\xi,\qquad 0\le t<T.

The parameter $\lambda$ blows up at $T$ , and $s$ maps $[0,T)$ onto $[0,\infty)$ . In the coordinates $y = D^{\mathbf r}_{\lambda(t)}x$ and the time $s$ , the system becomes

y' = \big(a D_{\mathbf r} + J_n\big)y + (b u + d)e_n .

The feedback studied is $u = -K^T D^{\mathbf r}_\eta y$ , that is $u(t) = -K^T D^{\mathbf r}_{\eta\lambda(t)}x(t)$ in the original variables, where $K\in\mathbb R^n$ and $\eta\ge1$ .

Formalization targets

Goal: Corollary 14 (corrected)

There is a rate $\mu>0$ depending only on $n$ and $\underline b$ such that, for every $T$ and admissible $a$ , there are $K$ and $C>0$ with

|x_i(t)| \le \frac{1}{(\eta\lambda(t))^{n-i+1}}\Big(C\eta\max(1,\eta^{n-1})e^{-\mu\eta s(t)}\|x(0)\| + C\max_{r\in[0,t]}|d(r)|\Big)

for every $\eta\ge1$ , every $b\ge\underline b$ , every disturbance $d$ , every closed-loop solution, every $t\in[0,T)$ and every $1\le i\le n$ . Since $\lambda(t)\to\infty$ , every coordinate reaches $0$ at the prescribed time $T$ .

Milestones

§3 (10): $\dot\lambda = a\lambda^2$ , $\lambda$ is nondecreasing and tends to $\infty$ at $T$ , and $s$ is an increasing $C^1$ bijection $[0,T)\to[0,\infty)$ .
§3 (7)–(11): the transformed dynamics.
Proposition 10: $\exists\rho,S,K$ such that $(J_n - be_nK^T)^TS + S(J_n-be_nK^T)\preceq-\rho\,\mathrm{Id}$ for all $b\ge\underline b$ .
Proposition 11: the same LMI with $aD_{\mathbf r}$ added, uniformly in $|a|\le C_0$ .
Proposition 12 (corrected): the ISS estimate (17) in the time $s$ .
Proposition 13: the $\eta$ -scaled LMI (20).

Significance

Corollary 14 says that a linear feedback with a time-varying gain drives the chain of integrators to the origin at the designer's deadline $T$ . The guarantee holds for every control gain $b\ge\underline b$ , however large, and gives an explicit input-to-state bound for the matched disturbance. The weight $a$ is free, so the blow-up profile of the gain can be chosen, for example to converge faster than polynomially. Proposition 10 removes the upper bound on $b$ from the classical LMI, and is of independent use for high-gain and persistently excited systems.

On formalization: the results are proved on paper; no formalization of them is known. The mission produces checked statements of the LMIs, the time change, and the prescribed-time estimate. Two printed estimates are false as stated, (17) and (23), and the mission states corrected versions (see Formalization scope). Formal proofs would certify the corrected constants.

Difficulty

The obvious approach is to take a Lyapunov function for the constant-coefficient closed loop and differentiate it along trajectories. This fails for two reasons. First, $b$ ranges over an unbounded interval, so no compactness argument yields a common Lyapunov matrix, and a single $S$ and $K$ must work for all $b\ge\underline b$ at once. Second, the transformed system carries the time-varying term $a(s)D_{\mathbf r}$ , and in the original time the feedback gain $\lambda(t)$ is unbounded. Estimates must survive both the rescaling by $D^{\mathbf r}_{\eta\lambda(t)}$ and the change of time. Constants that look harmless in the new time, such as the condition number of $S$ and the value $\lambda(0)$ , reappear in the original variables, and dropping them makes the printed estimates false.

Formalization scope

Lean representation: vectors of $\mathbb R^n$ are Fin n → ℝ, and coordinate i : Fin n is the paper's index i.val + 1, so $r_i$ = n - i.val. Matrices are Matrix (Fin n) (Fin n) ℝ, and $e_nK^T$ is vecMulVec (eN n) K. Matrix inequalities use the Loewner order (open scoped MatrixOrder), and "real symmetric positive definite" is PosDef. The norm $\|\cdot\|$ is Euclidean, written out as eucNorm. Solutions are Carathéodory solutions in integral form: for every $t$ in the interval, the right-hand side is integrable on $[0,t]$ and the integral identity holds. This matches the paper's measurable $b$ and $d$ . The standing assumptions are $n\ge1$ (§3), $T>0$ , $a$ continuous and nonnegative on $[0,T]$ with $\int_t^Ta>0$ on $[0,T)$ , and $b\ge\underline b>0$ . No upper bound on $b$ is assumed anywhere. $\max|d|$ is replaced by an arbitrary bound $D$ of $|d|$ on the interval.

Corrected statements, with milestone texts kept verbatim:

(17) as printed has no constant on the transient term and fails for $n\ge2$ : with $a\equiv1$ and $y(0)=e_1$ , $|y_1|$ first increases. Proposition 12 is stated with $C_S$ on that term.
(23) as printed fails at $t=0$ whenever $\int_0^Ta<1$ . The goal is stated with a constant $C$ on the transient term, and $K$ and $C$ may depend on $T$ and $a$ . The rate $\mu$ and the disturbance gain $C_S$ depend only on $n$ and $\underline b$ , as on the page.
Proposition 13's undefined $\mu_*$ is the $\rho$ of its statement.
" $\lambda$ increasing" is read as nondecreasing.
Corollary 14's " $t\ge0$ " is read as $t\in[0,T)$ .

Trivializing encodings are ruled out as follows. The integrability clause of IsIntegralSolution prevents a non-integrable right-hand side from integrating to $0$ . Every constant is quantified before the objects it must not depend on: the rate $\mu$ before $T$ and $a$ , $K$ before $\eta$ , and $\rho,S,K$ before $b$ . No statement weakens the estimates to mere convergence.

Needed infrastructure: Lyapunov estimates for absolutely continuous solutions, Loewner-order congruence, and interval-integral calculus for the time change. The LMI lemmas and the integral-form solution predicate are reusable in other control missions. Proofs of any milestone are welcome, and so are sharper constants.

Selected references

Y. Chitour, R. Ushirobira, H. Bouhemou, Stabilization for a Perturbed Chain of Integrators in Prescribed Time, SIAM J. Control Optim. 58(2):1022–1048, 2020. https://doi.org/10.1137/19M1285937
Y. Song, Y. Wang, J. Holloway, M. Krstić, Time-varying feedback for regulation of normal-form nonlinear systems in prescribed finite time, Automatica 83:243–251, 2017. https://doi.org/10.1016/j.automatica.2017.06.008
Y. Chitour, M. Sigalotti, On the stabilization of persistently excited linear systems, SIAM J. Control Optim. 48:4032–4055, 2010. https://doi.org/10.1137/080737812

10 thms2 active usersReviewed

Completed

Numerical Analysis Probability Random Matrix Theory·Captain: mikedeng1

Randomized Algorithms for Estimating the Trace of an Implicit Symmetric Positive Semi-Definite Matrix V: Sample Bound for the Mixed Unit Vector Trace EstimatorResearch Paper

Motivation

Many computations in numerical linear algebra, statistics and computational physics need the trace of a matrix $A$ that is never formed explicitly: $A$ may be an inverse, a matrix function $f(B)$ , or a product of large operators, and the only affordable access is a routine that returns $Av$ or $v^TAv$ for a given vector $v$ . Monte Carlo trace estimators handle this setting: draw random vectors $z$ and average the quadratic forms $z^TAz$ , each of which costs one matrix–vector product.

Avron and Toledo (J. ACM 2011) compare such estimators by the number of samples $M$ that guarantee relative error $\epsilon$ with probability $1-\delta$ , and by the number of random bits each sample consumes. Hutchinson's estimator (Hutchinson 1990) and the Gaussian estimator need $\Omega(n)$ random bits per sample. Section 8 of the paper studies two estimators that sample only from the $n$ standard basis vectors and so need about $\log_2 n$ bits per sample, which allows the samples to be generated in advance. The plain version has a sample bound that depends on how uneven the diagonal of $A$ is; the mixed version first multiplies $A$ on both sides by a random orthogonal mixing matrix of the kind introduced by Ailon and Chazelle (2006) for the fast Johnson–Lindenstrauss transform and used by Avron, Maymounkov and Toledo (2010) in least-squares solvers. This mission formalizes the resulting sample bound, Theorem 8.4.

Setting

Let $n \ge 1$ , let $A \in \mathbb{R}^{n\times n}$ be symmetric positive semi-definite, and let $e_1,\ldots,e_n$ be the standard basis of $\mathbb{R}^n$ .

A random variable $T$ is an $(\epsilon,\delta)$ -approximator of $\mathrm{trace}(A)$ if

\Pr\bigl(|T-\mathrm{trace}(A)| \le \epsilon\,\mathrm{trace}(A)\bigr) \ge 1-\delta

(Definition 4.1).

The unit vector estimator with $M$ samples is

U_M = \frac{n}{M}\sum_{i=1}^M z_i^TAz_i,

where $z_1,\ldots,z_M$ are independent uniform random samples from $\{e_1,\ldots,e_n\}$ (Definition 3.4). Each term $z_i^TAz_i$ is a diagonal entry of $A$ chosen uniformly at random. Its behaviour is governed by

r_D(A) = \frac{n\cdot\max_i A_{ii}}{\mathrm{trace}(A)},

which lies between $1$ and $n$ .

A random mixing matrix is $\mathcal F = FD$ , where the seed $F$ is a fixed orthogonal $n\times n$ matrix and $D$ is diagonal with i.i.d. Rademacher entries, $\Pr(D_{ii}=\pm1) = 1/2$ (Definition 3.5). The seed enters through

\eta = \max_{i,j}|F_{ij}|^2,

which satisfies $1/n \le \eta \le 1$ ; normalized DFT and Hadamard matrices attain $\eta = 1/n$ , DCT and DHT matrices have $\eta = 2/n$ (p. 8:5).

The mixed unit vector estimator is

T_M = \frac{n}{M}\sum_{i=1}^M z_i^T\mathcal F A\mathcal F^T z_i,

with $z_1,\ldots,z_M$ as above, independent of $D$ (Definition 3.6). It is the unit vector estimator applied to $\mathcal FA\mathcal F^T$ , whose trace equals $\mathrm{trace}(A)$ .

Formalization targets

Goal: Theorem 8.4

For every orthogonal seed $F$ , every symmetric positive semi-definite $A$ , every $\epsilon > 0$ , $\delta \in (0,1)$ and every $M \ge 1$ ,

M \ \ge\ 2n^2\eta^2\epsilon^{-2}\ln(4/\delta)\ln^2(4n^2/\delta) \quad\Longrightarrow\quad T_M \text{ is an } (\epsilon,\delta)\text{-approximator of } \mathrm{trace}(A).

Milestones

Lemma 8.1. For symmetric $A$ , $\mathrm{E}(U_1) = \mathrm{trace}(A)$ and $\mathrm{Var}(U_1) = n\sum_{i}A_{ii}^2 - \mathrm{trace}^2(A)$ .
Theorem 8.2. $U_M$ is an $(\epsilon,\delta)$ -approximator of $\mathrm{trace}(A)$ whenever

M \ge \tfrac12\epsilon^{-2}\ln(2/\delta)\,r_D^2(A).

Lemma 8.3. For $U \in \mathbb{R}^{n\times m}$ with orthonormal columns and $\delta > 0$ , with probability at least $1-\delta$ ,

|(\mathcal FU)_{ij}| \le \sqrt{2\eta\ln(2mn/\delta)} \quad\text{for all } i,j.

Proof of Theorem 8.4, p. 8:13. With probability at least $1-\delta/2$ over $D$ , $0 \le (\mathcal FA\mathcal F^T)_{jj} \le 2\eta\ln(4n^2/\delta)\,\mathrm{trace}(A)$ for all $j$ , and hence

r_D(\mathcal FA\mathcal F^T) \le 2n\eta\ln(4n^2/\delta).

Significance

Theorem 8.2 alone shows that the unit vector estimator can need order $n^2$ samples: when the trace is concentrated on one diagonal entry, $r_D(A) = n$ . Theorem 8.4 removes the dependence on $A$ entirely. For a Fourier-type seed with $\eta = \Theta(1/n)$ the bound becomes $O(\epsilon^{-2}\ln(1/\delta)\ln^2(n/\delta))$ samples for every positive semi-definite $A$ , while each sample still costs about $\log_2 n$ random bits, and the $n$ bits of $D$ are drawn once. Among the estimators of the paper this is the only one with both an $A$ -independent sample bound and logarithmic randomness per sample (Table I, p. 8:5). Lemma 8.3 is a standalone statement about randomized orthogonal transforms that is used well beyond trace estimation, in the analysis of subsampled randomized Hadamard transforms, sketching-based least squares, and fast Johnson–Lindenstrauss embeddings.

All results of the mission are proved in the literature: Lemma 8.3 in the cited works, the rest in the paper. As far as the platform's catalogue shows, none has a machine-checked proof. The mission produces checked statements of the paper's Section 8 with their exact constants, a probability model for random sign matrices and uniform basis-vector sampling that other randomized linear-algebra missions can reuse, and, once proved, a checked instance of Hoeffding's inequality applied to a concrete estimator.

Difficulty

The obvious argument for Theorem 8.4 applies Theorem 8.2 to $\mathcal FA\mathcal F^T$ . That matrix is random, so Theorem 8.2, which is a statement about a fixed matrix, cannot be applied directly: the proof must condition on $D$ , use that the samples $z_i$ are independent of $D$ , and combine a failure event over $D$ with a conditional failure event over the $z_i$ , each with probability at most $\delta/2$ . The second difficulty is Lemma 8.3: each entry $(\mathcal FU)_{ij} = \sum_k F_{ik}D_{kk}U_{kj}$ is a Rademacher sum whose coefficient vector has squared norm at most $\eta$ , and the bound needs a sub-Gaussian tail for such sums together with a union bound over all $mn$ entries. Bounding the diagonal of $\mathcal FA\mathcal F^T$ through the diagonal of $A$ alone does not work: each mixed diagonal entry depends on all entries of $A$ , including the off-diagonal ones.

Formalization scope

Everything is over $\mathbb{R}$ . The paper allows complex unitary seeds; since the estimator uses the transpose $\mathcal F^T$ , the mission takes $F$ real orthogonal ( $F^TF = I$ ). Matrices are Matrix (Fin n) (Fin n) ℝ, "symmetric positive semi-definite" is Matrix.PosSemidef, and $n \ge 1$ is assumed throughout. The sample spaces are explicit product measures: indices $k_1,\ldots,k_M$ uniform on Fin n with $z_i = e_{k_i}$ , the diagonal of $D$ with the $n$ -fold Rademacher product law, and, for $T_M$ , the product of the two, which makes $D$ and the $z_i$ independent as the paper assumes implicitly. Probabilities are Measure.real. $\eta$ and $\max_i A_{ii}$ are maxima over finite nonempty index sets; $r_D$ uses real division, whose value at $\mathrm{trace}(A) = 0$ is irrelevant because a positive semi-definite matrix with zero trace is $0$ . The sample-count thresholds are exactly the paper's constants.

Deviations from the page, all recorded in the items' Formalization Notes: Definition 3.4 and Theorem 8.2 are stated for positive semi-definite rather than positive definite $A$ (the proof uses only $A_{ii} \ge 0$ ); Table I's entry $8\epsilon^{-2}\ln(4n^2/\delta)\ln(4/\delta)$ for the mixed estimator, which disagrees with Theorem 8.4, is not used; the proof of Theorem 8.4 prints the conditional failure probability as " $\le 1-\delta/2$ " where $\delta/2$ is meant, and no statement copies it; Remark 8.5 ("for some small $C$ ") has no pinned constant and is not stated.

A formalization in which $D$ is an arbitrary orthogonal diagonal matrix, the $z_i$ are correlated with $D$ , or the law of the estimator is assumed rather than constructed would make the goal either false or a restatement of its hypotheses; the product-measure model rules this out.

Needed infrastructure: Hoeffding's inequality for bounded i.i.d. sums (in Mathlib as sub-Gaussian moment generating function bounds), a sub-Gaussian tail for Rademacher linear combinations, conditioning on one factor of a product measure, and the spectral theorem for real symmetric matrices. The Rademacher sign model and the random-mixing-matrix entry bound are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Lemma 8.3, are welcome.

Selected references

H. Avron and S. Toledo, Randomized algorithms for estimating the trace of an implicit symmetric positive semi-definite matrix, J. ACM 58(2), Article 8, 2011. https://doi.org/10.1145/1944345.1944349
N. Ailon and B. Chazelle, Approximate nearest neighbors and the fast Johnson–Lindenstrauss transform, STOC 2006. https://doi.org/10.1145/1132516.1132597
H. Avron, P. Maymounkov and S. Toledo, Blendenpik: Supercharging LAPACK's least-squares solver, SIAM J. Sci. Comput. 32(3), 2010. https://doi.org/10.1137/090767911
M. F. Hutchinson, A stochastic estimator of the trace of the influence matrix for Laplacian smoothing splines, Comm. Statist. Simulation Comput. 19(2), 1990. https://doi.org/10.1080/03610919008812866
W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58, 1963. https://doi.org/10.1080/01621459.1963.10500830

10 thms2 active usersReviewed

Completed

Numerical Analysis Probability Random Matrix Theory·Captain: mikedeng1

Randomized Algorithms for Estimating the Trace of an Implicit Symmetric Positive Semi-Definite Matrix III: Sample Bound for Normalized Rayleigh-Quotient Trace EstimatorsResearch Paper

Motivation

Many computations in numerical linear algebra, statistics and computational physics need the trace of a matrix $A$ that is never formed explicitly: $A$ may be an inverse, a matrix function $f(B)$ , or a product of large operators, and the only affordable access is a routine that returns $Av$ for a given vector $v$ . Examples include log-determinants and the generalized cross-validation criterion in statistics, counting eigenvalues in an interval, and charge densities in electronic-structure computations. Monte Carlo trace estimators handle this setting: draw random vectors $z$ , and average the quadratic forms $z^TAz$ , each of which costs one matrix–vector product.

Hutchinson (1990) introduced the estimator with Rademacher vectors and computed its variance. Avron and Toledo (J. ACM 2011) replaced variance statements with sample bounds: how many samples $M$ guarantee relative error $\epsilon$ with probability $1-\delta$ . Section 6 of their paper proves one such bound for an entire class of estimators at once, the normalized Rayleigh-quotient trace estimators, which contains Hutchinson's estimator and the unit vector estimator. This mission formalizes that bound (Theorem 6.1).

Setting

Let $A \in \mathbb{R}^{n\times n}$ be symmetric positive semi-definite, with eigenvalues $0 \le \lambda_1 \le \cdots \le \lambda_n$ and rank $\mathrm{rank}(A)$ . Write $\lambda_n$ for the largest eigenvalue and

\kappa_f(A) = \frac{\text{largest nonzero eigenvalue of }A}{\text{smallest nonzero eigenvalue of }A},

defined for $A \ne 0$ ; it is the condition number of $A$ on its range.

A normalized Rayleigh-quotient trace estimator of $A$ with $M$ samples is

R_M = \frac1M\sum_{i=1}^M z_i^TAz_i,

where $z_1,\ldots,z_M$ are independent random vectors in $\mathbb{R}^n$ with $z_i^Tz_i = n$ and $\mathrm{E}(z_i^TAz_i) = \mathrm{trace}(A)$ for each $i$ (Definition 3.2). The vectors need not be identically distributed. Hutchinson's vectors ( $\pm1$ entries, i.i.d. uniform) and the vectors $\sqrt n\,e_k$ with $k$ uniform are instances.

A random variable $T$ is an $(\epsilon,\delta)$ -approximator of $\mathrm{trace}(A)$ if

\Pr\bigl(|T-\mathrm{trace}(A)| \le \epsilon\,\mathrm{trace}(A)\bigr) \ge 1-\delta

(Definition 4.1).

Formalization targets

Goal: Theorem 6.1, in the form its proof establishes

For every nonzero symmetric positive semi-definite $A$ , every $\epsilon>0$ , $\delta\in(0,1)$ , and every normalized Rayleigh-quotient estimator $R_M$ of $A$ ,

M \ \ge\ \frac{\ln(2/\delta)\cdot n^2\,\kappa_f^2(A)}{2\,\mathrm{rank}^2(A)\,\epsilon^2} \quad\Longrightarrow\quad R_M \text{ is an } (\epsilon,\delta)\text{-approximator of } \mathrm{trace}(A).

Milestones (the displayed steps of the proof, p. 8:10)

$\mathrm{trace}(A)\,\kappa_f(A) \ge \mathrm{rank}(A)\,\lambda_n$ .
For every $z$ with $z^Tz = n$ : $\ 0 \le z^TAz \le \lambda_n z^Tz = n\lambda_n \le \frac{n}{\mathrm{rank}(A)}\mathrm{trace}(A)\,\kappa_f(A)$ .
For every $t>0$ :

\Pr(|R_M-\mathrm{trace}(A)| \ge t) \le 2\exp\left(-\frac{2M^2\mathrm{rank}^2(A)t^2}{M n^2\mathrm{trace}^2(A)\kappa_f^2(A)}\right).

For every $\epsilon>0$ :

\Pr(|R_M-\mathrm{trace}(A)| \ge \epsilon\,\mathrm{trace}(A)) \le 2\exp\left(-\frac{2M\mathrm{rank}^2(A)\epsilon^2}{n^2\kappa_f^2(A)}\right).

Significance

The result is distribution-free within the class: it needs only normalization and unbiasedness, so it covers Hutchinson's estimator, the unit vector estimator and any future normalized scheme with one argument. For well-conditioned matrices of full or nearly full rank the required number of samples is $O(\epsilon^{-2}\ln(1/\delta))$ , independent of $n$ . For ill-conditioned matrices the bound degrades with $\kappa_f^2(A)$ , which is the reason the paper proves sharper estimator-specific bounds in Sections 7 and 8; Theorem 6.1 is the baseline those results are compared against (Table I, p. 8:5).

The theorem is proved in the paper. No machine-checked version of it, or of any sample bound for trace estimators, is known to exist. The formalization adds a precise statement of the class of estimators on a general probability space, a corrected threshold (see below), and a Lean development that connects Mathlib's spectral theorem for symmetric matrices with its Hoeffding inequality for independent bounded variables.

Difficulty

Each step is short on paper; the work is in the interfaces. The eigenvalue inequality of milestone 1 requires relating the number of nonzero eigenvalues (with multiplicity) to $\mathrm{rank}(A)$ and handling the maximum and minimum over the nonzero spectrum. Milestone 2 is the Rayleigh-quotient bound $z^TAz \le \lambda_n z^Tz$ , which is a consequence of the spectral decomposition rather than a one-line identity. Milestone 3 applies Hoeffding's inequality to summands that are bounded only almost surely, are not identically distributed, and whose mean is fixed by hypothesis rather than computed; the two-sided bound must be assembled from two one-sided tails, and the event $|R_M - \mathrm{trace}(A)| \ge t$ must be rescaled to a statement about the sum $\sum_i z_i^TAz_i$ . A naive attempt that fixes a particular distribution for the $z_i$ (Rademacher, say) proves a different, narrower theorem and does not settle the goal.

Formalization scope

Matrices and spectrum. $A$ is Matrix (Fin n) (Fin n) ℝ with A.PosSemidef and A ≠ 0; eigenvalues are Mathlib's IsHermitian.eigenvalues. $\lambda_n$ is lambdaMax (the maximum eigenvalue) and $\kappa_f(A)$ is kappaF (maximum over minimum of the finite set of nonzero eigenvalues); both are Finset.max'/min'/sup' of nonempty finite sets. $\kappa_f(0)$ is a placeholder, and every statement assumes $A \ne 0$ .
Probability model. A general probability space $(\Omega, P)$ and random vectors z : Fin M → Ω → Fin n → ℝ satisfying IsNormalizedRayleighSample P A z: each $z_i$ measurable, the family mutually independent (iIndepFun), $z_i^Tz_i = n$ almost surely, and $\int z_i^TAz_i\,dP = \mathrm{trace}(A)$ . The estimator is universally quantified over this class. Unbiasedness is required for the given $A$ only, as on the page. Probabilities are P.real of events; $M \ge 1$ is a natural number and $1/M$ is (M : ℝ)⁻¹.
Correction of the printed statement. Theorem 6.1 and Table I print the threshold $\tfrac12\epsilon^{-2}n^{-2}\mathrm{rank}^2(A)\ln(2/\delta)\kappa_f^2(A)$ . The last display of the proof gives $\ln(2/\delta)\,n^2\kappa_f^2(A)/(2\,\mathrm{rank}^2(A)\epsilon^2)$ , with the exponents of $n$ and $\mathrm{rank}(A)$ swapped. The printed version is false: for $n=2$ , $A=e_1e_1^T$ , $z=\sqrt2\,e_k$ with $k$ uniform and $\epsilon=\delta=1/2$ it admits $M=1$ , while $R_1\in\{0,2\}$ . The goal states the proof's threshold.
Indexing slip. The proof writes $0=\lambda_1=\cdots=\lambda_k$ with $k=n-\mathrm{rank}(A)+1$ and $\kappa_f(A)=\lambda_n/\lambda_k$ , which would make $\lambda_k=0$ ; milestone 1 states the inequality with $\kappa_f$ as defined, not the indexing.
Non-trivialization. The hypotheses of the class are satisfiable (by the unit vector and Hutchinson estimators), $A\ne0$ excludes the degenerate $\kappa_f(0)$ , and all divisions in the statements have positive denominators, so no statement holds vacuously or through a junk value.
Reusable parts. A proof of milestone 2 is a general Rayleigh-quotient bound for symmetric matrices; milestone 3 is a two-sided Hoeffding bound for independent, almost surely bounded, non-identically distributed summands, useful well beyond this mission. Contributions welcome: proofs of any milestone, and a sorry-free instance showing a concrete estimator (e.g. $\sqrt n\,e_k$ ) satisfies IsNormalizedRayleighSample.

Selected references

H. Avron and S. Toledo, Randomized algorithms for estimating the trace of an implicit symmetric positive semi-definite matrix, Journal of the ACM 58(2), Article 8, 2011. https://doi.org/10.1145/1944345.1944349
M. F. Hutchinson, A stochastic estimator of the trace of the influence matrix for Laplacian smoothing splines, Communications in Statistics – Simulation and Computation 19(2), 433–450, 1990. https://doi.org/10.1080/03610919008812866
W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58(301), 13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830

8 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Probability+1·Captain: mikedeng1

Matching Is as Easy as Matrix Inversion: Steps 1–3 Find a Minimum Weight Perfect Matching with Probability at Least 1/2Research Paper

Motivation

Deciding whether a graph has a perfect matching, and finding one, are basic problems of combinatorial optimization; Edmonds' blossom algorithm solves them sequentially in polynomial time. The question behind this paper is whether they can also be solved in parallel, in polylogarithmic time on polynomially many processors (the class NC, or RNC when random bits are allowed).

The algebraic route to that question goes through the Tutte matrix. Tutte (1947) showed that a graph has a perfect matching if and only if its Tutte matrix, a skew-symmetric matrix of indeterminates, has a nonzero determinant. Substituting random numbers for the indeterminates turns this into a randomized parallel decision procedure, but it does not say which perfect matching exists, and a graph may have exponentially many.

Mulmuley, Vazirani and Vazirani (Combinatorica 7 (1987) 105–113) resolve this with the isolating lemma: random small integer weights make the minimum weight member of an arbitrary set family unique with probability at least one half. Once a single perfect matching is isolated, one determinant and one adjugate of an integer matrix reveal it. The isolating lemma has since become a standard tool in randomized algorithms and complexity theory, well beyond matchings.

Timeline:

1947, Tutte: a graph has a perfect matching iff the determinant of its Tutte matrix is a nonzero polynomial (doi:10.1112/jlms/s1-22.2.107).
1979, Lovász: random substitution into the Tutte matrix gives a randomized algorithm for deciding whether a perfect matching exists (Fundamentals of Computation Theory, LNCS 1979).
1986, Karp, Upfal and Wigderson: the first RNC algorithm that finds a perfect matching, with RNC³ running time (Combinatorica 6 (1986) 35–48).
1987, Mulmuley, Vazirani and Vazirani: the isolating lemma and an RNC² algorithm that inverts one integer matrix (this paper).
2016–2017, Fenner, Gurjar and Thierauf (arXiv:1601.06319) for bipartite graphs, and Svensson and Tarnawski (arXiv:1704.01929) for general graphs, partially derandomize the isolation step and place perfect matching in quasi-NC. Whether perfect matching is in NC remains open.

Setting

A set system $(S, F)$ is a finite set $S$ of elements together with a family $F$ of subsets of $S$ . Given a weight $w_x \in \mathbb{N}$ for each element $x$ , the weight of $T \subseteq S$ is $w(T) = \sum_{x \in T} w_x$ , and $F$ has a unique minimum weight set if one member of $F$ is strictly lighter than every other member.

A graph $G$ has vertices $v_1, \dots, v_n$ (in Lean, Fin n, in their natural order) and edge set $E$ , with $m = |E|$ . A perfect matching is a set $M \subseteq E$ such that every vertex lies in exactly one edge of $M$ . The edges and the perfect matchings of $G$ form a set system.

Given edge weights $w_{ij} \in \mathbb{N}$ , the integer matrix $B$ is obtained from the Tutte matrix by substituting $2^{w_{ij}}$ for its indeterminates:

b_{ij} = 2^{w_{ij}} \ \text{if } (v_i, v_j) \in E,\ i < j; \qquad b_{ij} = -2^{w_{ij}} \ \text{if } (v_i, v_j) \in E,\ i > j; \qquad b_{ij} = 0 \ \text{otherwise}.

$|B|$ is its determinant, $B_{ij}$ the submatrix with row $i$ and column $j$ removed, and $\operatorname{adj}(B)$ its adjugate, whose $(j, i)$ entry is $\pm|B_{ij}|$ .

The algorithm of §4 is:

Step 1. Compute $|B|$ and obtain $w$ , the exponent for which $2^{2w}$ is the highest power of 2 dividing $|B|$ .
Step 2. Compute $\operatorname{adj}(B)$ .
Step 3. Output every edge $(v_i, v_j)$ for which the integer $|B_{ij}|\,2^{w_{ij}}/2^{2w}$ is odd.

Formalization targets

Goal: Steps 1–3 find a minimum weight perfect matching with probability at least 1/2

For every graph $G$ that has a perfect matching, with edge weights drawn uniformly and independently from $\{1, \dots, 2m\}$ ,

\Pr\bigl[\text{the output of Steps 1–3 is a perfect matching of } G \text{ of minimum weight}\bigr] \ \ge\ \tfrac12 .

This is the correctness half of the paper's Theorem (p. 109). The probability is a fraction of the $(2m)^m$ weight functions.

Milestones

Lemma 1 (isolating lemma): for a nonempty family $F$ over an $n$ -element set, weights uniform in $[1, 2n]$ give a unique minimum weight set with probability $\ge 1/2$ .
Isolation for perfect matchings (§4): with edge weights uniform in $[1, 2m]$ , the minimum weight perfect matching is unique with probability $\ge 1/2$ .
Odd-cycle cancellation (proof of Lemma 2): for a skew-symmetric integer matrix, only permutations all of whose cycles have even length contribute to the determinant.
Lemma 2: if the minimum weight perfect matching is unique, of weight $w$ , then $|B| \neq 0$ and $2^{2w}$ is the highest power of 2 dividing $|B|$ .
Lemma 3: under the same hypothesis, $(v_i, v_j) \in M$ iff $|B_{ij}|\,2^{w_{ij}}/2^{2w}$ is odd.
Steps 1–3, deterministic core: under the same hypothesis, Step 1 obtains the weight of $M$ and Steps 2–3 output exactly $M$ .

Two companion items are included but are not on the goal's path: the maximum weight version of Lemma 1 (the remark after its proof, p. 107) and Lemma 4 (p. 110): the lexicographically largest matching set, for vertices sorted by decreasing weight, is a heaviest matching set.

Significance

The isolating lemma is a statement about arbitrary set families with no structure assumed, which is why it transfers: it is used for isolating satisfying assignments, for parallel algorithms for exact matching and minimum weight matchings with small weights, and in the derandomization program that led to the quasi-NC matching algorithms cited above. Lemmas 2 and 3 are the bridge from a combinatorial object (a unique minimum weight perfect matching) to arithmetic facts about one integer matrix (2-adic valuations of its determinant and adjugate entries), which is what makes the algorithm reducible to matrix inversion.

All results of this mission are proved in the paper. What the mission adds is machine-checked proofs: Mathlib at the pinned revision contains Tutte's barrier theorem but neither the isolating lemma nor the Tutte-matrix determinant arguments, and a search of Prove2Me (September 2026) found no formalization of them. A complete development yields a reusable isolating lemma for finite set systems and a reusable determinant expansion for skew-symmetric matrices.

Difficulty

The probabilistic step is a union bound over elements, but the event bounded for each element, "the element is ambiguous", is defined through a threshold that depends on all the other weights; the argument needs independence of that threshold from the element's own weight, which is a product-space (Fubini-type) counting statement rather than a one-line estimate. In a counting formalization over $\{1, \dots, 2n\}^S$ , each fibre must be handled separately.

The determinant steps require a genuine combinatorial involution on permutations: reversing an odd cycle must be well defined (a canonical choice of cycle) and self-inverse, preserve the sign, negate the value, and in Lemma 3 also preserve the constraint $\sigma(i) = j$ , which is where "since $n$ is even, there are at least two odd cycles" enters. Relating a permutation with only even cycles to a pair of perfect matchings whose union is its trail is the second nontrivial bijection. Divisibility must be tracked exactly: $2^{2w}$ divides every term, and every term other than the one of $M$ is divisible by $2^{2w+1}$ .

Formalization scope

Vertices are Fin n and the graph is G : SimpleGraph (Fin n) with decidable adjacency. Edge weights are functions G.edgeSet → ℕ; perfect matchings are Finset G.edgeSet in which every vertex lies in exactly one edge. The matrix is weightedTutteMatrix G w : Matrix (Fin n) (Fin n) ℤ, with the positive entry above the diagonal. Probabilities are ratios of counts over Fintype.piFinset (fun _ => Finset.Icc 1 (2m)), stated without division as $(2m)^m \le 2 \cdot \#\{\dots\}$ ; the weight range is exactly $[1, 2m]$ (resp. $[1, 2n]$ in Lemma 1). " $x/2^k$ is odd" means $2^k \mid x$ and $x/2^k$ is an odd integer. The minor $|B_{ij}|$ is taken as Mathlib's signed cofactor adjugate B j i; parity and divisibility do not see the sign. Step 1's $w$ is $\lfloor \nu_2(|B|)/2\rfloor$ .

Added hypotheses: Lemma 1 and its maximum version assume $F$ nonempty (the printed lemma omits it and is false for $F = \emptyset$ ); the goal and the isolation milestone assume $G$ has a perfect matching, which is the paper's own input assumption. Lemmas 2 and 3 allow arbitrary natural weights, as printed.

The algorithm's output is defined from $B$ , $|B|$ , $\operatorname{adj}(B)$ , the 2-adic valuation and parity only; a definition of the output that refers to perfect matchings or to minimality would trivialize the goal and is ruled out. The complexity half of the Theorem (RNC², $O(n^{3.5}m)$ processors), which rests on Pan's matrix-inversion algorithm, is not formalized, nor are §5a–b and §6.

Contributions welcome: proofs of the milestones in any order, general lemmas about the permutation expansion of skew-symmetric determinants, and a counting form of the union bound over product spaces, all of which are reusable outside this mission.

Selected references

K. Mulmuley, U. V. Vazirani, V. V. Vazirani, Matching is as easy as matrix inversion, Combinatorica 7(1) (1987) 105–113. https://doi.org/10.1007/BF02579206
W. T. Tutte, The factorization of linear graphs, J. London Math. Soc. 22 (1947) 107–111. https://doi.org/10.1112/jlms/s1-22.2.107
R. M. Karp, E. Upfal, A. Wigderson, Constructing a perfect matching is in random NC, Combinatorica 6(1) (1986) 35–48. https://doi.org/10.1007/BF02579407
L. Lovász, On determinants, matchings, and random algorithms, Fundamentals of Computation Theory (FCT '79), 1979, 565–574.
S. Fenner, R. Gurjar, T. Thierauf, Bipartite perfect matching is in quasi-NC, STOC 2016. https://arxiv.org/abs/1601.06319
O. Svensson, J. Tarnawski, The matching problem in general graphs is in quasi-NC, FOCS 2017. https://arxiv.org/abs/1704.01929

10 thms2 active usersReviewed

Completed

Numerical Analysis Optimization Theoretical Computer Science·Captain: mikedeng1

Sparse Approximate Solutions to Linear Systems 1: The Column Bound for Greedy SelectionResearch Paper

Motivation

Many problems in scientific computing and statistics ask for a solution of a linear system $Ax\approx b$ that uses as few unknowns as possible. In statistics this is subset selection (Golub and Van Loan, Matrix Computations, 1983). In coding theory over binary matrices it is the minimum weight solution problem (Gallager, 1968). Natarajan's own motivation was radial basis interpolation (Hardy, 1988). There the coefficients of the interpolant solve a square nonsingular linear system (Michelli, 1986). Few nonzero coefficients make the interpolant cheap to evaluate and, by Occam's razor, less prone to fitting noise.

Natarajan's paper (SIAM J. Comput. 24 (1995) 227–234) makes two contributions. First, finding the sparsest approximate solution over the reals is NP-hard (Theorem 1, the subject of the companion mission). Second, the obvious greedy heuristic, a QR factorization whose column pivots are chosen by their correlation with the right-hand side, is provably good (Theorem 2). This mission formalizes Theorem 2. The greedy method is known today as orthogonal least squares (OLS), a variant of orthogonal matching pursuit. Natarajan's bound is among the earliest worst-case guarantees for this family of algorithms and is widely cited in the sparse approximation and compressed sensing literature.

Setting

Let $A\in\mathbb R^{m\times n}$ have columns $a_1,\dots,a_n$ , let $b\in\mathbb R^m$ and $\varepsilon>0$ . Write $\|\cdot\|_2$ for the Euclidean norm and $\|x\|_0$ for the number of nonzero entries of $x$ . The sparse approximate solution problem asks for $x$ with $\|Ax-b\|_2\le\varepsilon$ and $\|x\|_0$ minimal. Define

\operatorname{Opt}(\delta)=\min\{\|x\|_0 : \|Ax-b\|_2\le\delta\}.

Let $\mathbf A$ be $A$ with every column divided by its Euclidean norm. Let $\mathbf A^+$ be its Moore–Penrose pseudo-inverse, the unique matrix $P$ with $\mathbf AP\mathbf A=\mathbf A$ , $P\mathbf AP=P$ and $\mathbf AP$ , $P\mathbf A$ symmetric. Let $\|\mathbf A^+\|_2$ be its spectral norm, the $\ell_2\to\ell_2$ operator norm.

Algorithm Greedy keeps a working matrix $A^{(r)}$ with columns $a^{(r)}_j$ , a working vector $b^{(r)}$ and a set $\tau$ of chosen indices. It starts from $A^{(0)}=\mathbf A$ , $b^{(0)}=b$ , $\tau=\emptyset$ . While $\|b^{(r)}\|_2>\varepsilon$ , it chooses an index $k\notin\tau$ that maximizes $|a_k^{(r)T}b^{(r)}|$ and replaces $b^{(r)}$ by its projection onto the orthogonal complement of $a^{(r)}_k$ . It adds $k$ to $\tau$ and replaces every column outside $\tau$ by its normalized projection onto that complement. If every correlation $a_j^{(r)T}b^{(r)}$ vanishes, the algorithm stops ("no solution exists"). A final solution phase solves the linear system $Bx=b^{(0)}-b^{(r)}$ in the chosen columns $B$ of $A$ . The number of nonzero entries of the output is therefore at most the number $t$ of selection iterations.

Formalization targets

Goal: Theorem 2, for $A$ with linearly independent columns

If the columns of $A$ are linearly independent and some $x$ satisfies $\|Ax-b\|_2\le\varepsilon/2$ , then every run of the selection phase, with any tie-breaking, performs

t\le\Big\lceil 18\,\operatorname{Opt}(\varepsilon/2)\,\|\mathbf A^+\|_2^2\,\ln\frac{\|b\|_2}{\varepsilon}\Big\rceil

iterations. The paper prints the theorem without the independence hypothesis. The hypothesis is needed (see Formalization scope).

Milestones

The proof on pp. 230–233 passes through the following statements, in order:

(12): some column satisfies $|a_j^{(r)T}b^{(r)}|\ge\|b^{(r)}\|_2^2/(2\sqrt{N^{(r)}}\|u^{(r)}\|_2)$ . Here $u^{(r)}$ is a sparsest vector with $\|A^{(r)}u^{(r)}-b^{(r)}\|_2\le\varepsilon/2$ and $N^{(r)}=\|u^{(r)}\|_0$ .
(18): $\|b^{(r+1)}\|_2^2\le(1-1/\rho)\|b^{(r)}\|_2^2$ whenever $\rho\ge 4N^{(r)}\|u^{(r)}\|_2^2/\|b^{(r)}\|_2^2$ .
Lemma 1: $t\le\lceil2\rho\ln(\|b\|_2/\varepsilon)\rceil$ for any such $\rho$ valid at every iteration.
Lemma 3: $N^{(r+1)}\le N^{(r)}\le N^{(0)}$ .
$N^{(0)}=\operatorname{Opt}(\varepsilon/2)$ .
The columns of $\mathbf A$ indexed by the support $\sigma$ of $u^{(r)}$ and by the chosen set $\tau$ are linearly independent, and $\sigma\cap\tau=\emptyset$ .
(31): $\|u^{(r)}\|_2\le\frac32\|Z^+\|_2\|b^{(r)}\|_2$ for the matrix $Z$ of those columns.
The singular-value comparison $\|Z^+\|_2\le\|M^+\|_2$ for a column submatrix $Z$ of a matrix $M$ with independent columns.
Lemma 2: $\|u^{(r)}\|_2\le\frac32\|\mathbf A^+\|_2\|b^{(r)}\|_2$ , for $A$ with independent columns.

Items 1–7 hold for every matrix $A$ . Items 8, 9 and the goal carry the independence hypothesis.

Significance

Theorem 2 is a bicriteria approximation guarantee for an NP-hard problem. The greedy output meets the error $\varepsilon$ with at most a factor $18\|\mathbf A^+\|_2^2\ln(\|b\|_2/\varepsilon)$ more nonzeros than the best solution at error $\varepsilon/2$ . The factor depends only on the conditioning of the normalized matrix and logarithmically on the required accuracy. Its structure follows Johnson's analysis of the greedy set cover algorithm (1974): a potential decreases by a constant factor per step, which gives a logarithmic number of steps. The intermediate facts (12), (18) and Lemma 1 are the template of many later analyses of matching pursuit and OLS.

The result is proved on paper, with a gap. The last step of the proof of Lemma 2 compares singular values of a submatrix with those of $\mathbf A$ , and this comparison holds only when $\mathbf A$ has full column rank. For general $A$ , Theorem 2 and Lemma 2 are false as printed. The formalization produces a machine-checked proof of the corrected theorem and pins down exactly where the hypothesis enters. The hypothesis-free statements (12), (18), Lemma 1, Lemma 3 and (31) form reusable infrastructure for greedy sparse approximation. No existing formalization of this algorithm or of its guarantee, in Lean or elsewhere, was found for this mission.

Difficulty

Each step of the proof is short, but the objects are defined by an iteration. The columns $a^{(r)}_j$ are repeatedly projected and renormalized, and the columns already chosen are left untouched. Every claim about iteration $r$ therefore needs invariants: chosen columns are orthonormal and orthogonal to $b^{(r)}$ , and the remaining columns are normalized projections of the original ones onto the orthogonal complement of the chosen ones. A proof has to establish these by induction before any lemma can be applied. The sparsest vector $u^{(r)}$ is defined by minimality, so Lemma 3 and the linear-independence claim are exchange arguments on supports rather than computations. Finally, the passage from (31) to Lemma 2 needs a quantitative fact about pseudo-inverses of column submatrices. Mathlib has neither the Moore–Penrose inverse of a rectangular matrix nor its norm as a reciprocal singular value.

A naive attempt to bound $\|u^{(r)}\|_2$ directly by $\|\mathbf A^+\|_2\|A^{(r)}u^{(r)}\|_2$ fails: $u^{(r)}$ multiplies the projected columns $A^{(r)}$ , not $\mathbf A$ , and different sparsest solutions can have different norms.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin m), so every $\|\cdot\|_2$ is the Euclidean norm. The only $\|\cdot\|_\infty$ is the maximum of $|a_j^{(r)T}b^{(r)}|$ , which is written out explicitly. The algorithm is a recursion greedyState A b k r in the sequence of choices k : ℕ → Fin n. A run of $t$ iterations (IsGreedyRun) requires, at each $r<t$ : the strict while-condition $\|b^{(r)}\|_2>\varepsilon$ , an unchosen index, a nonzero correlation, and maximality over the unchosen columns. The residual and the columns are computed, never assumed. Normalization sends $0$ to $0$ , so a column lying in the span of the chosen ones stays zero and is never chosen. $\operatorname{Opt}$ is an infimum over ℕ, and the goal assumes that some $x$ has $\|Ax-b\|_2\le\varepsilon/2$ , since otherwise the infimum would be $0$ . The ceiling is the natural-number ceiling. It agrees with the printed one whenever the loop runs at least once, because then $\|b\|_2>\varepsilon$ . The pseudo-inverse is any matrix satisfying the four Penrose equations. It is never defined as $(\mathbf A^T\mathbf A)^{-1}\mathbf A^T$ , which would hide the rank assumption.

Added hypothesis. The goal, Lemma 2 and the singular-value step assume that the columns of $A$ are linearly independent, which forces $n\le m$ . Without it, Theorem 2 fails. Take $m=2$ , $n=200$ , columns $(\cos\theta_j,\sin\theta_j)$ and $(\sin\theta_j,\cos\theta_j)$ for 100 distinct $\theta_j\in[0.001,0.01]$ , $b=\sqrt2(1,1)$ and $\varepsilon=1$ . Then $\operatorname{Opt}(1/2)=2$ and the bound evaluates to $1$ , but Greedy selects two columns. Lemma 2 fails for $\mathbf A=[e_1,e_2,(e_1+e_2)/\sqrt2]$ and $b=\beta(-1,1)/\sqrt2$ . The paper's motivating interpolation systems are square and nonsingular, so they satisfy the hypothesis. A hypothesis-free goal would replace $\|\mathbf A^+\|_2$ by the largest $\|Z^+\|_2$ over linearly independent column subsets $Z$ of $\mathbf A$ , which is what (31) gives. That quantity is not printed in the paper, so it is not the goal here.

A statement in which the iterates are free sequences constrained by hypotheses, the greedy choice is dropped, or $\operatorname{Opt}$ is taken over an empty set would be trivially true or would not describe this algorithm. The encoding above rules these out.

A complete development needs Gram–Schmidt-type invariants of the iteration, exchange arguments for sparsest solutions, and the Moore–Penrose inverse with its spectral norm. The last of these is reusable well beyond this mission. Contributions of any milestone, of the general Penrose-inverse facts, or of alternative proofs are welcome.

Selected references

B. K. Natarajan, Sparse Approximate Solutions to Linear Systems, SIAM J. Comput. 24(2):227–234, 1995. https://doi.org/10.1137/s0097539792240406
G. H. Golub and C. F. Van Loan, Matrix Computations, Johns Hopkins University Press, 1983.
D. S. Johnson, Approximation algorithms for combinatorial problems, J. Comput. System Sci. 9:256–278, 1974. https://doi.org/10.1016/S0022-0000(74)80044-9
R. Penrose, A generalized inverse for matrices, Proc. Cambridge Philos. Soc. 51:406–413, 1955. https://doi.org/10.1017/S0305004100030401

12 thms2 active usersReviewed

Control Theory Convex Optimization Numerical Analysis+2·Captain: mikedeng1

Robust Solutions to Least-Squares Problems with Uncertain Data IV: A Semidefinite Upper Bound on the Linear-Fractional Worst-Case Residual, Exact for Full PerturbationsResearch Paper

Motivation

Least-squares fitting is a standard tool in estimation, identification and data analysis, and its data $A$ , $b$ are rarely known exactly. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed to choose $x$ to minimize the worst-case residual over a set of admissible data perturbations. Earlier missions of this series treat unstructured perturbations of $[A\ b]$ and perturbations affine in a parameter vector. §5 of the paper covers a more general model, taken from robust identification (Doyle et al.): the perturbed data depend on an uncertain matrix $\Delta$ through a linear-fractional transformation. This form covers rational dependence of the data on uncertain parameters, max-norm bounds on independent parameters, and data matrices with some columns known exactly (pp. 1046–1047).

In this generality, deciding whether the worst-case residual is finite is NP-complete, and computing it is NP-hard even when the dependence is affine (§5.3, Lemma 5.1). Theorem 5.2 gives the tractable replacement: a semidefinite program whose value bounds the worst-case residual from above, and equals it when the perturbation is unstructured. The main tool is a structured form of the S-procedure. Robust control uses the same tool, with the scalings $S$ and $G$ below, to bound the real structured singular value (Fan, Tits and Doyle, 1991).

Setting

Vectors carry the Euclidean norm $\|v\|$ . For a matrix $X$ , $\|X\|$ is its largest singular value (operator norm between Euclidean spaces). Let $\mathcal D$ be a linear subspace of $\mathbb R^{N\times N}$ (the perturbation structure), and fix $A \in \mathbb R^{n\times m}$ , $b \in \mathbb R^n$ , $L \in \mathbb R^{n\times N}$ , $R_A \in \mathbb R^{N\times m}$ , $R_b \in \mathbb R^N$ , $D \in \mathbb R^{N\times N}$ . For $\Delta \in \mathcal D$ with $\det(I - D\Delta) \ne 0$ the perturbed data are

A(\Delta) = A + L\Delta(I - D\Delta)^{-1}R_A, \qquad b(\Delta) = b + L\Delta(I - D\Delta)^{-1}R_b .

With the normalization $\rho = 1$ (the paper's, with no loss of generality), the worst-case residual of $x \in \mathbb R^m$ is

r_{\mathcal D}(A,b,x) = \max_{\Delta \in \mathcal D,\ \|\Delta\| \le 1} \|A(\Delta)x - b(\Delta)\|

if $\det(I - D\Delta) \ne 0$ for every such $\Delta$ , and $+\infty$ otherwise (35). The commutant scalings are $\mathcal S = \{S = S^T : S\Delta = \Delta S\ \forall \Delta \in \mathcal D\}$ and $\mathcal G = \{G = -G^T : G\Delta = \Delta G\ \forall \Delta \in \mathcal D\}$ (37). The SDP constraint is

\mathcal F(\lambda,S,G,x) = \begin{bmatrix} \Theta & \begin{matrix} Ax - b \\ R_Ax - R_b\end{matrix} \\ \begin{matrix}(Ax-b)^T & (R_Ax - R_b)^T\end{matrix} & \lambda\end{bmatrix} \succ 0, \quad \Theta = \begin{bmatrix} \lambda I - LSL^T & -LSD^T + LG \\ -DSL^T + G^TL^T & S + DG - GD^T - DSD^T\end{bmatrix}. \qquad (38),(39)

Formalization targets

Goal: Theorem 5.2 (corrected)

For all $x$ and $\lambda$ :

\text{(a)}\quad S \in \mathcal S,\ G \in \mathcal G,\ S \succ 0,\ G\Delta \text{ skew } \forall \Delta \in \mathcal D,\ \mathcal F(\lambda,S,G,x) \succ 0 \ \Longrightarrow\ \lambda > r_{\mathcal D}(A,b,x);

\text{(b)}\quad \mathcal D = \mathbb R^{N\times N},\ \lambda > r_{\mathcal D}(A,b,x) \ \Longrightarrow\ \exists s > 0:\ \mathcal F(\lambda, sI, 0, x) \succ 0 .

Part (a) says the value of the SDP $\inf\{\lambda : (\lambda, S, G) \text{ feasible}\}$ (40) is an upper bound on $r_{\mathcal D}$ . Part (b) says this upper bound is exact for full perturbations, including the case $r_{\mathcal D} = \infty$ , where (40) is infeasible.

Milestones

Lemma 2.2, both directions: the full-block S-procedure. $\det(I - T_4\Delta) \ne 0$ and $T(\Delta) \succeq 0$ for all $\|\Delta\| \le 1$ if and only if $\|T_4\| < 1$ and a one-scalar LMI (10) holds (the "only if" under $T_2 \ne 0$ or $T_3 = 0$ ).
Lemma 2.3: sufficiency of the scaled LMI for a structured $\mathcal D$ , and its strict necessity for $\mathcal D = \mathbb R^{N\times N}$ .
§5.4, p. 1047: $\lambda > r_{\mathcal D}(A,b,x)$ if and only if a linear-fractional matrix function of $\Delta$ is positive definite on the structured unit ball.
§5.4, (38)–(39): the certificate (a) in the paper's own words.

Significance

The worst-case residual under linear-fractional uncertainty cannot be computed efficiently unless P = NP. Theorem 5.2 gives an SDP-computable upper bound with an explicit certificate $(S, G)$ . Since $x$ enters (38) linearly, the same constraint can also be optimized over $x$ (Theorem 5.3, not part of this mission). For $\mathcal D = \mathbb R^{N\times N}$ the bound is exact, which covers the model $[A(\Delta)\ b(\Delta)] = [A\ b] + L\Delta[R_A\ R_b]$ and, as a special case, the unstructured problem of §3.

The results are proved in the paper (the proof of Theorem 5.2 is only indicated, through Appendix C). No machine-checked version of these statements, of Lemma 2.2 or of the structured S-procedure with commutant scalings is known. The formalization also fixes the statements. As printed, Lemma 2.2's "only if", Lemma 2.3 and the upper bound of Theorem 5.2 are each false in a boundary or structural case (see Formalization scope). The corrected forms stated here are the ones the paper's proofs support.

Difficulty

Part (a) reduces to robust positivity of a linear-fractional matrix function, and the difficulty is the inverse $(I - D\Delta)^{-1}$ . The certificate is one LMI in which $\Delta$ does not appear, while the conclusion is about a rational function of $\Delta$ over a whole structured ball. The certificate also has to guarantee that $I - D\Delta$ is invertible everywhere on that ball, and not only that the residual is small where it is defined. Evaluating $\mathcal F$ at a single point does not show this. Part (b) needs a lossless S-procedure in its strict form. The standard (non-strict) S-lemma gives only $\succeq$ , and the gap between strict and non-strict inequalities is exactly where the printed statements fail. The degenerate case $T_2 = 0$ is not covered by the S-lemma's regularity condition and has to be handled separately.

Formalization scope

Dimensions are Fin n, Fin m, Fin N; $\mathcal D$ is a Submodule ℝ (Matrix (Fin N) (Fin N) ℝ), with $\mathcal D = \mathbb R^{N\times N}$ as ⊤. The Euclidean norm is written out, because ‖·‖ on Fin n → ℝ is the sup norm. $\|\Delta\|$ is the operator norm of Matrix.toEuclideanLin Δ, the largest singular value.
$\lambda > r_{\mathcal D}(A,b,x)$ is the predicate ResidualBelow: every $\Delta \in \mathcal D$ with $\|\Delta\| \le 1$ has $\det(I - D\Delta) \ne 0$ and residual $< \lambda$ . It is false for every $\lambda$ when $r_{\mathcal D} = \infty$ . No real-valued supremum is used, so the $\infty$ branch of (35) cannot turn into a default $0$ . Matrix inverses are Mathlib's Matrix.inv, and every use carries the determinant condition.
$\rho = 1$ throughout, as in the paper; general $\rho$ follows by scaling $\Delta$ .
Corrections of the printed statements. (i) (40) must require $S \succ 0$ . Without it, $N = n = m = 1$ , $D = 2$ , $L = 1$ , $A = b = R_A = R_b = 0$ , $x = 0$ , $S = -1$ , $G = 0$ satisfy (38) for every $\lambda > 1/3$ , while $r_{\mathcal D} = \infty$ . (ii) $G$ must make $G\Delta$ skew-symmetric for every $\Delta \in \mathcal D$ , which is the identity $p^TGq = 0$ used in the proof of Lemma 2.3. For $\mathcal D = \operatorname{span}\{I, J\}$ , $J = \begin{bmatrix}0&1\\-1&0\end{bmatrix}$ , the printed bound certifies $\lambda = 3/2$ for an instance with worst-case residual $2$ . The added condition holds automatically when every element of $\mathcal D$ is symmetric (e.g. the diagonal structures (36)) and when $G = 0$ (e.g. $\mathcal D = \mathbb R^{N\times N}$ ). (iii) Lemma 2.2's "only if" is stated under $T_2 \ne 0$ or $T_3 = 0$ . (iv) Lemma 2.3's necessity is stated in strict form, and its sufficiency concludes $T(\Delta) \succ 0$ .
Not stated: "If $\Theta > 0$ at the optimum, the upper bound is also exact". The infimum over the strict LMI (38) is not attained, and the paper does not say which limit is meant. Theorem 5.3, Lemma 2.4 and Lemma 5.1 are also not stated.
Trivializing encodings ruled out: the goal is not a statement about the value of an infimum (which a junk value could satisfy), and the added hypotheses are satisfiable (for instance $S = sI$ , $G = 0$ for full $\mathcal D$ , which part (b) produces).
Infrastructure needed: the Schur complement for block matrices (in Mathlib), a lossless S-lemma for two homogeneous quadratic forms in strict and non-strict form (the platform has ConvexOptimization.s_procedure, in a different sign convention), square roots of positive definite matrices that commute with $\mathcal D$ , and compactness of the structured unit ball. The S-procedure lemmas are reusable in robust control and trust-region analysis. Proofs of the milestones in any order are welcome.

Selected references

L. El Ghaoui and H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
S. Boyd, L. El Ghaoui, E. Feron and V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777
M. K. H. Fan, A. L. Tits and J. C. Doyle, Robustness in the presence of mixed parametric uncertainty and unmodeled dynamics, IEEE Trans. Automat. Control 36(1):25–38, 1991. https://doi.org/10.1109/9.62265
I. Pólik and T. Terlaky, A survey of the S-lemma, SIAM Review 49(3):371–418, 2007. https://doi.org/10.1137/S003614450444614X

8 thms2 active usersReviewed

Completed

Convex Optimization Numerical Analysis Operations Research+1·Captain: mikedeng1

Robust Solutions to Least-Squares Problems with Uncertain Data II: Robust Least Squares as Tikhonov RegularizationResearch Paper

Motivation

Least squares fits a linear model $Ax \simeq b$ by minimizing $\|Ax - b\|$ , and its solution can be extremely sensitive to errors in the data $(A, b)$ when $A$ is ill-conditioned. The standard remedy is Tikhonov regularization (ridge regression): minimize $\|Ax - b\|^2 + \mu\|x\|^2$ , whose solution $x = (A^\top A + \mu I)^{-1}A^\top b$ is stable but depends on a parameter $\mu > 0$ that must be chosen by some external rule.

El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed instead to take the uncertainty in $(A, b)$ seriously: the robust least-squares (RLS) solution minimizes the worst-case residual over all perturbations $[\Delta A\ \Delta b]$ of Frobenius norm at most $\rho$ . Their Theorem 3.1 shows that for $\rho = 1$ this worst-case residual equals $\|Ax - b\| + \sqrt{\|x\|^2 + 1}$ and that its minimization is the second-order cone program (15). Theorem 3.2, the subject of this mission, reads off the optimal solution: it is a Tikhonov-regularized solution, and the regularization parameter is not a free choice but is fixed by the data. This gives a principled answer to the question of how to choose $\mu$ , and it is the reason the paper describes RLS as "a Tikhonov regularization procedure" with "a rigorous way to compute the regularization parameter" (abstract, p. 1035).

A closely related model for least squares with bounded data uncertainty was developed at the same time by Chandrasekaran, Golub, Gu and Sayed; the paper notes that their preliminary draft (its reference [5]) gives a solution to the unstructured RLS problem similar to that of §3.2 (pp. 1036–1037).

Setting

Throughout, $A \in \mathbb R^{n\times m}$ , $b \in \mathbb R^n$ , $x \in \mathbb R^m$ , and every vector norm is Euclidean, $\|v\| = \sqrt{\sum_i v_i^2}$ . For $x \in \mathbb R^m$ , $[x; 1] \in \mathbb R^{m+1}$ is $x$ with a coordinate $1$ appended, so $\|[x;1]\| = \sqrt{\|x\|^2 + 1}$ .

The SOCP (15) is the problem, in the variables $x \in \mathbb R^m$ and $\lambda, \tau \in \mathbb R$ ,

\text{minimize } \lambda \quad\text{subject to}\quad \|Ax - b\| \le \lambda - \tau,\qquad \|[x;1]\| \le \tau.

A triple $(x, \lambda, \tau)$ is optimal for (15) if it is feasible and $\lambda \le \lambda'$ for every feasible $(x', \lambda', \tau')$ . Its dual, derived in the paper from the general second-order cone duality of §2.1, is the problem in $z \in \mathbb R^n$ , $u \in \mathbb R^m$ , $v \in \mathbb R$

\text{maximize } b^\top z - v \quad\text{subject to}\quad A^\top z + u = 0,\quad \|z\| \le 1,\quad \|[u; v]\| \le 1.

The minimum-norm solution of $Ax = b$ is a solution $x$ with $\|x\| \le \|y\|$ for every other solution $y$ ; when $Ax = b$ is consistent it is $A^\dagger b$ , with $A^\dagger$ the Moore–Penrose pseudoinverse.

In the Lean development these objects are IsSOCPFeasible, IsSOCPOptimal, IsDualFeasible, dualObjective, IsDualOptimal and IsMinNormSolution, in the namespace RobustLS.Tikhonov, with the Euclidean norm eucNorm.

Formalization targets

Goal: Theorem 3.2 with the identity for $\mu$

Let $(x, \lambda, \tau)$ be optimal for (15) and set $\mu = (\lambda - \tau)/\tau$ . Then

x = \begin{cases} (\mu I + A^\top A)^{-1}A^\top b & \text{if } \mu > 0,\\ A^\dagger b & \text{else,}\end{cases}\qquad\text{and}\qquad \mu = \frac{\|Ax - b\|}{\sqrt{\|x\|^2 + 1}}.

By Theorem 3.1 (the subject of the companion mission I of this series), the $x$ -part of an optimal point of (15) is the RLS solution for $\rho = 1$ , so this is formula (17) of the paper. The identity for $\mu$ is the final display of the paper's proof and is the claim in the mission's title.

Milestones (in the order of the paper's proof, p. 1041)

Both (15) and its dual have optimal points.
If $\lambda = \tau$ at the optimum, then $Ax = b$ and $\lambda = \tau = \sqrt{\|x\|^2 + 1}$ .
In that case $x$ is the minimum-norm solution of $Ax = b$ , $x = A^\dagger b$ .
Eq. (18): for $\lambda > \tau$ , primal and dual optimal values coincide,

\|Ax - b\| + \|[x;1]\| = \lambda = b^\top z - v = -(Ax-b)^\top z - [x^\top\ 1]\begin{bmatrix} -A^\top z\\ v\end{bmatrix}.

The dual optimal point is $z = -(Ax - b)/\|Ax - b\|$ , $[u; v] = -[x; 1]/\sqrt{\|x\|^2 + 1}$ .
Substituting into $A^\top z + u = 0$ : $x = (A^\top A + \mu I)^{-1}A^\top b$ with $\mu = (\lambda - \tau)/\tau = \|Ax - b\|/\sqrt{\|x\|^2 + 1}$ .

A further item states Remark 3.1: for $\lambda > \tau$ , $x$ is the unique minimizer of the weighted residual $\big\|[A; I; 0]y - [b; 0; 1]\big\|_\Theta$ with $\Theta = \mathbf{diag}((\lambda-\tau)I, \tau I, \tau)$ and $\|r\|_\Theta = \|\Theta^{-1/2} r\|$ .

Significance

The result. Theorem 3.2 turns a robust optimization problem into a familiar linear-algebra object. It says that the robust solution always lies on the Tikhonov path $\{(A^\top A + \mu I)^{-1}A^\top b : \mu > 0\}$ or at its endpoint $A^\dagger b$ , and it identifies the point on the path through a fixed-point equation relating $\mu$ to the residual and the size of the solution. The paper builds on this in §3.3 (a one-dimensional search for $\mu$ via the SVD) and in §6 (continuity of the RLS solution in the data), and Remark 3.1 is the template for the weighted least-squares interpretation of the structured and linear-fractional problems in §5.

Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal account of second-order cone duality for a concrete program, the characterization of the optimal dual point by equality in the Cauchy–Schwarz inequality, and the minimum-norm characterization of $A^\dagger b$ , all in terms of explicit Euclidean norms on Fin k → ℝ.

Difficulty

The paper's proof rests on strong duality for (15) ("both primal and dual problems are strictly feasible"), which it cites from the SOCP literature rather than proving; Mathlib has no second-order cone duality, so this step is the main gap. The degenerate case $\lambda = \tau$ also needs care: there $\|Ax - b\| = 0$ , the residual term is not differentiable at the optimum, and the conclusion changes from a regularized inverse to a pseudoinverse. A statement that only handles the case $Ax \ne b$ , or that assumes the matrix $A^\top A + \mu I$ invertible without deriving it from $\mu > 0$ , misses part of the theorem.

Formalization scope

Normalization. The paper states Theorem 3.2 for $\rho = 1$ ("we take $\rho = 1$ in what follows", p. 1039) and obtains general $\rho$ by the scaling $\varphi(A, b, \rho) = \rho\,\varphi(A/\rho, b/\rho, 1)$ . Only the $\rho = 1$ statement is formalized.
The RLS solution. The perturbation model is not used here: all statements are about optimal points of (15). That the $x$ -part of such a point is the RLS solution is Theorem 3.1 (mission I), and it is recalled in prose only.
Norms. Vectors are Fin k → ℝ; the Euclidean norm is the explicit eucNorm v = √(∑ vᵢ²) (Mathlib's ‖·‖ on Fin k → ℝ is the sup norm). Stacked vectors $[x;1]$ and $[u;v]$ are indexed by Fin m ⊕ Unit.
Optimality. "Optimal point" means feasible with objective no worse than every feasible point; the minimum and maximum are therefore attained by definition, and milestone 1 guarantees they exist.
Pseudoinverse. Mathlib has no matrix pseudoinverse, so $A^\dagger b$ is stated as the minimum-norm solution of $Ax = b$ , which is how the proof uses it. The branch "else" is $\neg(\mu > 0)$ .
Inverse. $(\mu I + A^\top A)^{-1}$ is Mathlib's Matrix.inv; it is used only where $\mu > 0$ , where the matrix is positive definite. $\tau \ge 1$ at every feasible point, so $\mu$ is well defined without an extra hypothesis.
No trivialization. The goal quantifies over optimal points of (15) over the whole feasible set, not over feasible points, and milestone 1 shows the hypothesis is satisfiable for every $(A, b)$ , including $n = 0$ or $m = 0$ .
Weighted norm. For Remark 3.1, $\|r\|_\Theta$ for the diagonal $\Theta$ is written as $\sqrt{\sum_i r_i^2/\theta_i}$ , which equals $\|\Theta^{-1/2}r\|$ for positive weights.

Contributions welcome: second-order cone (or general conic) weak and strong duality for finite-dimensional programs, the equality case of Cauchy–Schwarz in the explicit-norm form used here, and a Moore–Penrose pseudoinverse for real matrices with its minimum-norm property. The platform's ConvexOptimization.conic_slater_strong_duality may help with the duality step.

Selected references

L. El Ghaoui and H. Lebret, Robust Solutions to Least-Squares Problems with Uncertain Data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
S. Chandrasekaran, G. H. Golub, M. Gu and A. H. Sayed, A new linear least-squares type model for parameter estimation in the presence of data uncertainties, cited as submitted to SIAM J. Matrix Anal. Appl. (reference [5] of the paper).
A. N. Tikhonov and V. Y. Arsenin, Solutions of Ill-Posed Problems, Wiley, New York, 1977 (reference [43] of the paper).
Y. Nesterov and A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
M. S. Lobo, L. Vandenberghe, S. Boyd and H. Lebret, Applications of Second-Order Cone Programming, Linear Algebra Appl. 284:193–228, 1998. https://doi.org/10.1016/S0024-3795(98)10032-0

9 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

A Singular Value Thresholding Algorithm for Matrix Completion 3: Convergence to the Minimum Nuclear Norm SolutionResearch Paper

Motivation

Nuclear norm minimization is the standard convex surrogate for rank minimization: to recover a low-rank matrix from a few linear measurements, or from a subset of its entries, one minimizes the sum of the singular values subject to the data constraints. For matrix completion, Candès and Recht (Found. Comput. Math. 2009) showed that this convex program recovers a low-rank matrix exactly from sufficiently many random entries. Solving it at scale is another matter: interior-point methods for the equivalent semidefinite program become impractical beyond matrices of a few hundred rows and columns.

Cai, Candès and Shen (SIAM J. Optim. 2010) proposed the singular value thresholding (SVT) algorithm, whose iterates are cheap and typically of low rank. SVT does not solve the nuclear norm problem itself. It solves a proximal problem, in which the nuclear norm is replaced by $\tau\|X\|_* + \tfrac12\|X\|_F^2$ for a fixed parameter $\tau>0$ . Section 3.4 of the paper justifies this substitution: as $\tau\to\infty$ , the solutions of the proximal problem converge to a specific solution of the nuclear norm problem, the one of least Frobenius norm. This mission formalizes that result, Theorem 3.1 of the paper, under general convex constraints.

Setting

Let $n_1, n_2$ be natural numbers and $\mathbb R^{n_1\times n_2}$ the space of real $n_1\times n_2$ matrices, with the inner product $\langle X, Y\rangle = \operatorname{trace}(X^*Y) = \sum_{i,j}X_{ij}Y_{ij}$ . Three functions of a matrix $X$ are used:

the Frobenius norm $\|X\|_F = \sqrt{\langle X, X\rangle}$ ;
the nuclear norm $\|X\|_*$ , the sum of the singular values of $X$ ;
for a parameter $\tau$ , the proximal objective $f_\tau(X) = \tau\|X\|_* + \tfrac12\|X\|_F^2$ .

Let $f_1,\dots,f_m:\mathbb R^{n_1\times n_2}\to\mathbb R$ be constraint functions and $\mathcal C = \{X : f_i(X)\le 0,\ i = 1,\dots,m\}$ the feasible set. The nuclear norm problem is

\text{(1.6)}\qquad \text{minimize } \|X\|_* \quad \text{subject to } f_i(X)\le 0,\ i=1,\dots,m,

and, for $\tau>0$ , the proximal problem is

\text{(3.4)}\qquad \text{minimize } f_\tau(X) \quad \text{subject to } f_i(X)\le 0,\ i=1,\dots,m.

When the $f_i$ are convex and $\mathcal C$ is nonempty, (3.4) has exactly one solution, written $X^\star_\tau$ , because $f_\tau$ is strongly convex. Problem (1.6) may have many solutions. Among them, the paper singles out the minimum Frobenius norm solution

\text{(3.14)}\qquad X_\infty := \arg\min_X\{\|X\|_F^2 : X \text{ is a solution of (1.6)}\}.

Linear equality constraints, and in particular the matrix completion constraints $X_{ij} = M_{ij}$ for sampled entries $(i,j)$ , are covered by taking pairs of affine functionals.

Formalization targets

Goal: Theorem 3.1

Assume that the $f_i$ are convex and lower semicontinuous. Then

\text{(3.15)}\qquad \lim_{\tau\to\infty}\|X^\star_\tau - X_\infty\|_F = 0.

Milestones

In the order in which the paper's proof uses them (all on p. 1967):

Eq. (3.16), for every $\tau>0$ :

\|X^\star_\tau\|_* + \frac{1}{2\tau}\|X^\star_\tau\|_F^2 \le \|X_\infty\|_* + \frac{1}{2\tau}\|X_\infty\|_F^2 \quad\text{and}\quad \|X_\infty\|_*\le\|X^\star_\tau\|_*.

Eq. (3.17), for every $\tau>0$ : $\|X^\star_\tau\|_F^2 \le \|X_\infty\|_F^2$ .
Convergence of the nuclear norms: $\lim_{\tau\to\infty}\|X^\star_\tau\|_* = \|X_\infty\|_*$ .
Uniqueness of $X_\infty$ : two minimum Frobenius norm solutions of (1.6) coincide when the $f_i$ are convex.
Cluster points: if $\tau_k\to\infty$ and $X^\star_{\tau_k}\to X_c$ , then $X_c = X_\infty$ .

Significance

The result itself. Theorem 3.1 is the link between the problem SVT actually solves and the problem one wants solved. The companion missions of this series prove that the SVT iteration, and its variant for general convex constraints, converges to $X^\star_\tau$ . Theorem 3.1 says what $X^\star_\tau$ is worth: for large $\tau$ it is close to a nuclear norm minimizer, and the minimizer it approaches is identified exactly, namely the one of least Frobenius norm. The statement is not specific to matrix completion. It covers every finite family of convex, lower semicontinuous constraints, and hence noisy variants such as the inequality-constrained problems of §3.3 of the paper.

Formalizing it. The theorem is proved in the paper, in about half a page. It has not, to our knowledge, been machine-checked. A formal proof pins down the hypotheses: the argument needs the minimizers to exist, and it uses continuity and convexity of the nuclear norm, closedness of the feasible set, and uniqueness of $X_\infty$ . It also produces a reusable fact about the nuclear norm in Lean, namely that the sum of singular values is a continuous convex function of the matrix.

Difficulty

The first steps are elementary consequences of the definitions of $X^\star_\tau$ and $X_\infty$ : (3.16) compares objective values, and (3.17) and the convergence of the nuclear norms follow by algebra and a squeeze. The difficulty lies elsewhere.

Identifying the limit. Boundedness gives cluster points of $X^\star_\tau$ , not convergence. Each cluster point must be shown to be feasible, to be optimal for (1.6), and to have the least Frobenius norm among the optimal points. Feasibility uses lower semicontinuity of the constraints. Optimality uses continuity of the nuclear norm. Minimality uses (3.17) passed to the limit.
Uniqueness of $X_\infty$ . The last step concludes $X_c = X_\infty$ from $\|X_c\|_F = \|X_\infty\|_F$ , which needs uniqueness of the minimum Frobenius norm solution. That in turn needs convexity of the solution set of (1.6), hence convexity of the nuclear norm, together with strict convexity of $\|\cdot\|_F^2$ .
Nuclear norm in Lean. The nuclear norm is defined from singular values, and its convexity (the triangle inequality for the sum of singular values) and continuity are not currently available as ready-made statements. They are the main groundwork.

A tempting shortcut, reading the family $X^\star_\tau$ as a sequence indexed by integers, proves a weaker statement: the limit in (3.15) is over real $\tau\to\infty$ .

Formalization scope

Matrices. Matrices are Matrix (Fin n₁) (Fin n₂) ℝ, abbreviated Mat n₁ n₂, over the reals as in the paper. $\langle X,Y\rangle = \sum_{i,j}X_{ij}Y_{ij}$ and $\|X\|_F = \sqrt{\langle X,X\rangle}$ .
Nuclear norm. $\|X\|_*$ is the sum of Mathlib's LinearMap.singularValues of Matrix.toEuclideanLin X. It is the genuine sum of singular values, not an abstract norm or the Frobenius norm.
Constraints. The constraints are a family f : Fin m → Mat n₁ n₂ → ℝ of real-valued functions. $m = 0$ (no constraints) is allowed.
Hypotheses of Theorem 3.1. The hypotheses are ConvexOn ℝ Set.univ (f i) and LowerSemicontinuous (f i) for every $i$ . Lower semicontinuity is redundant for real-valued convex functions on a finite-dimensional space, but it is kept because the theorem states it.
$X^\star_\tau$ and $X_\infty$ . $X^\star_\tau$ is a family Xτ : ℝ → Mat n₁ n₂ assumed to solve (3.4) for every $\tau>0$ , and its values at $\tau\le 0$ play no role. $X_\infty$ is a matrix assumed to satisfy the defining property (3.14): it solves (1.6) and has the least $\|\cdot\|_F^2$ among its solutions. Uniqueness of $X_\infty$ is a milestone to prove, not an assumption.
Vacuous case. These hypotheses presuppose, as the paper does, that (1.6) has a solution. They can be met exactly when the feasible set is nonempty. When it is empty the statement is vacuous, which matches the paper, where $X_\infty$ is then undefined.
Limits and topology. Limits in $\tau$ are along Filter.atTop on $\mathbb R$ . Convergence of matrices uses Mathlib's entrywise topology, which is the topology of $\|\cdot\|_F$ . The goal states (3.15) literally, with the Frobenius norm of the difference tending to $0$ .
Excluded shortcuts. A formalization that replaces the nuclear norm by the Frobenius norm or by an arbitrary norm, indexes $\tau$ by $\mathbb N$ , or assumes uniqueness or convergence as a hypothesis would not be Theorem 3.1. It is ruled out.

Infrastructure. The needed facts, all reusable beyond this mission:

nonnegativity, convexity and continuity of the nuclear norm on real matrices;
closedness and convexity of sublevel sets of convex lower semicontinuous functions;
uniqueness of the minimizer of a strictly convex function over a convex set;
a cluster-point argument for bounded families in finite-dimensional spaces.

Contributions of these general lemmas as separate theorems are welcome.

Selected references

J.-F. Cai, E. J. Candès, Z. Shen, A Singular Value Thresholding Algorithm for Matrix Completion, SIAM J. Optim. 20(4):1956–1982, 2010. https://doi.org/10.1137/080738970
E. J. Candès, B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9:717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
B. Recht, M. Fazel, P. A. Parrilo, Guaranteed Minimum-Rank Solutions of Linear Matrix Equations via Nuclear Norm Minimization, SIAM Rev. 52(3):471–501, 2010. https://doi.org/10.1137/070697835

8 thms2 active usersReviewed

Completed

Convex Optimization Numerical Analysis Optimization·Captain: mikedeng1

A Singular Value Thresholding Algorithm for Matrix Completion 2: Convergence of the SVT Iteration under General Convex ConstraintsResearch Paper

Motivation

Singular value thresholding (SVT) is a first-order method introduced by Cai, Candès and Shen (SIAM J. Optim. 20 (2010)) for recovering a low-rank matrix from incomplete or indirect information. Its basic form, for matrix completion, alternates a soft-thresholding of singular values with a gradient step on a dual variable, and needs only one sparse singular value decomposition per iteration. That is what made nuclear-norm heuristics usable on matrices with tens of thousands of rows and columns, where interior-point methods for the equivalent semidefinite program do not fit in memory.

Matrix completion is only one constraint set. In applications the data are noisy linear measurements $b = \mathcal A(M) + z$ , and the constraint takes the form of componentwise error bounds or norm balls around the data (§3.3 of the paper). Section 3.2 of the paper extends the method to a general finite family of convex constraints, and §4.2 proves that the extended iteration converges. This mission formalizes that extension and its convergence theorem, Theorem 4.4.

Setting

Let $n_1, n_2, m$ be natural numbers and $\mathbb R^{n_1\times n_2}$ the real $n_1\times n_2$ matrices, with the Frobenius inner product $\langle X, Y\rangle = \sum_{i,j} X_{ij}Y_{ij}$ and norm $\|X\|_F = \sqrt{\langle X, X\rangle}$ . The nuclear norm $\|X\|_*$ is the sum of the singular values of $X$ . For a fixed $\tau > 0$ the objective is

f_\tau(X) = \tau\|X\|_* + \tfrac12\|X\|_F^2 .

A matrix $Z$ is a subgradient of a function $g$ at $X_0$ , written $Z\in\partial g(X_0)$ , if $g(X)\ge g(X_0) + \langle Z, X - X_0\rangle$ for all $X$ .

Let $f_1,\dots,f_m:\mathbb R^{n_1\times n_2}\to\mathbb R$ be convex and put $\mathcal F(X) = (f_1(X),\dots,f_m(X))\in\mathbb R^m$ . On $\mathbb R^m$ , $\langle u, v\rangle = \sum_i u_iv_i$ and $\|v\|$ is the Euclidean norm. The constrained problem is

\text{(3.4)}\qquad \text{minimize } f_\tau(X)\quad\text{subject to } f_i(X)\le 0,\ i=1,\dots,m,

with Lagrangian $\mathcal L(X, y) = f_\tau(X) + \langle y, \mathcal F(X)\rangle$ for $y\ge 0$ . A pair $(X^\star, y^\star)$ with $y^\star\ge0$ is primal-dual optimal if it is a saddle point:

\mathcal L(X^\star, y)\le \mathcal L(X^\star, y^\star)\le \mathcal L(X, y^\star)\qquad\text{for all } y\ge 0,\ X .

The paper's standing assumption "strong duality holds" is the existence of such a pair.

The iteration (3.5) starts from $y^0 = 0$ and, for step sizes $\delta_k$ , sets for $k = 1, 2, \dots$

X^k = \arg\min_X\{f_\tau(X) + \langle y^{k-1}, \mathcal F(X)\rangle\},\qquad y^k = [\,y^{k-1} + \delta_k\mathcal F(X^k)\,]_+ ,

where $x_+$ has entries $\max(x_i, 0)$ . It is Uzawa's method for (3.4): an exact minimization in the primal variable followed by a projected ascent step on the dual. When $\mathcal F(X) = b - \mathcal A(X)$ is affine, the minimization is a singular value thresholding step, which gives the algorithm its name.

The analysis of §4.2 assumes $\mathcal F$ is Lipschitz in the sense

\text{(4.2)}\qquad \|\mathcal F(X) - \mathcal F(Y)\|\le L\,\|X - Y\|_F\quad\text{for all } X, Y,

for a constant $L\ge 0$ .

Formalization targets

Goal: Theorem 4.4 (p. 1969)

If $0 < \inf_k\delta_k\le\sup_k\delta_k < 2/L^2$ and strong duality holds, then the sequence $X^k$ of (3.5) converges to the unique solution of (3.4):

\exists!\,X^\star\ \text{solving (3.4)},\qquad \lim_{k\to\infty} X^k = X^\star .

Milestones, in the order the proof uses them

Lemma 4.1 (p. 1968): $\langle Z - Z', X - X'\rangle\ge\|X - X'\|_F^2$ for $Z\in\partial f_\tau(X)$ , $Z'\in\partial f_\tau(X')$ .
Lemma 4.3 (p. 1969): for a primal-dual optimal pair and each $\delta > 0$ , $y^\star = [y^\star + \delta\mathcal F(X^\star)]_+$ .
Eq. (4.4) (p. 1969): there are $Z^k\in\partial f_\tau(X^k)$ and $Z^\star\in\partial f_\tau(X^\star)$ with $\langle Z^k, X - X^k\rangle + \langle y^{k-1}, \mathcal F(X) - \mathcal F(X^k)\rangle\ge 0$ and $\langle Z^\star, X - X^\star\rangle + \langle y^\star, \mathcal F(X) - \mathcal F(X^\star)\rangle\ge 0$ for all $X$ .
Eq. (4.5) (p. 1969): $\langle y^{k-1} - y^\star, \mathcal F(X^k) - \mathcal F(X^\star)\rangle\le -\|X^k - X^\star\|_F^2$ .
Contraction step (p. 1969): $\|y^k - y^\star\|\le\|y^{k-1} - y^\star + \delta_k(\mathcal F(X^k) - \mathcal F(X^\star))\|$ .
Eq. (4.6) (p. 1970): if $2\delta_k - \delta_k^2L^2\ge\beta > 0$ for $k\ge1$ , then $\|y^k - y^\star\|^2\le\|y^{k-1} - y^\star\|^2 - \beta\|X^k - X^\star\|_F^2$ .

Significance

The result. Theorem 4.4 is the convergence guarantee for SVT beyond matrix completion. The componentwise error bounds of (3.8), whose SVT iteration is (3.9), are finitely many affine constraints and fall under it directly, as does any finite family of Lipschitz convex constraints, for instance a Frobenius-norm ball around the data. The conic variants of §3.3 ((3.11)–(3.13)) project the dual variable onto a cone rather than onto the nonnegative orthant and are not covered by the theorem as stated. Together with Theorem 3.1 of the same paper, which says that the solution of (3.4) tends to the minimum-nuclear-norm solution as $\tau\to\infty$ , it justifies using SVT as a solver for nuclear-norm minimization under general convex constraints.

Formalizing it. The theorem is proved in the paper, with two steps delegated to the literature: Lemma 4.3 cites [31], and the concluding step reads "the conclusion is as before". Its proof is short but relies on convex-analytic facts that are standard on paper and missing, in this form, from Mathlib: subgradients of the nuclear norm, the subdifferential sum rule for finite convex functions, and nonexpansiveness of the projection onto the nonnegative orthant. No machine-checked proof of this theorem or of Uzawa-type convergence for nuclear-norm objectives is known to exist. The mission produces a complete, checked version of the argument, including the omitted closing step.

Difficulty

The obvious approach is to view (3.5) as projected gradient ascent on the dual function $g(y) = \min_X\mathcal L(X, y)$ and quote the standard convergence theorem for gradient methods with Lipschitz gradients. That does not apply directly: for general convex $f_i$ the dual function need not be differentiable, $\mathcal F(X^k)$ is only a supergradient, and the Lipschitz hypothesis (4.2) is on $\mathcal F$ , not on a dual gradient. The proof instead works with the primal-dual pair: it needs first-order optimality conditions (4.4), which require a subdifferential sum rule for $f_\tau + \sum_i y_i f_i$ with nonsmooth $f_i$ , and it needs the strong monotonicity of $\partial f_\tau$ (Lemma 4.1), which depends on the description of subgradients of the nuclear norm. A second subtlety is that the theorem asserts convergence of the whole primal sequence to the unique solution, not to some solution along a subsequence, while nothing is claimed about convergence of the dual sequence.

Formalization scope

Matrices are Matrix (Fin n₁) (Fin n₂) ℝ, vectors in $\mathbb R^m$ are Fin m → ℝ, and convergence of matrices is in Mathlib's product topology, which coincides with the Frobenius topology. The nuclear norm is the sum of Mathlib's LinearMap.singularValues of the matrix viewed as a map between Euclidean spaces. Each $f_i$ is a real-valued function with ConvexOn ℝ Set.univ. The iteration is a predicate on sequences indexed by ℕ: the paper's step $k$ produces X (k+1) and y (k+1) from y k with step size δ (k+1), and y 0 = 0. $X^k$ is required to minimize $\mathcal L(\cdot, y^{k-1})$ ; for $\tau>0$ and convex $f_i$ this minimizer exists and is unique, so the predicate is satisfiable and determines the sequence. The step-size condition is stated as $a\le\delta_k\le C$ for $k\ge1$ with $a>0$ and $C L^2 < 2$ , which avoids the division $2/L^2$ (evaluated as $0$ in Lean when $L=0$ ); for $L=0$ it requires only bounded steps, matching the convention $2/0 = \infty$ . Strong duality is the hypothesis that a saddle point exists; Slater's condition is not assumed. The paper's standing assumptions ( $\tau>0$ , convex $f_i$ , and (4.2) where $L$ enters) appear as explicit hypotheses in every statement.

A formalization that assumes convergence or boundedness of the dual iterates, replaces the primal minimization by a closed-form thresholding step (valid only for affine $\mathcal F$ ), or states only subsequential convergence would not be this theorem; each of these is excluded by the statements above.

A complete development needs: subgradients of the nuclear norm and strong monotonicity of $\partial f_\tau$ ; existence and characterization of minimizers of strongly convex continuous functions on a finite-dimensional space; the subdifferential sum rule for finite convex functions; complementary slackness from the saddle-point inequalities; and nonexpansiveness of the entrywise positive part. These are reusable beyond this mission, especially for other Uzawa and augmented Lagrangian analyses. Contributions of any of these pieces as separate lemmas are welcome.

Selected references

J.-F. Cai, E. J. Candès, Z. Shen, A Singular Value Thresholding Algorithm for Matrix Completion, SIAM J. Optim. 20(4):1956–1982, 2010. https://doi.org/10.1137/080738970
E. J. Candès, B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9:717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
K. J. Arrow, L. Hurwicz, H. Uzawa, Studies in Linear and Nonlinear Programming, Stanford University Press, 1958.
S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441

9 thms2 active usersReviewed

Completed

Convex Optimization Numerical Analysis Optimization·Captain: mikedeng1

A Singular Value Thresholding Algorithm for Matrix Completion 1: The SVT Iteration Converges to the Unique Solution of the Proximal ProblemResearch Paper

Motivation

Matrix completion asks to recover an $n_1\times n_2$ matrix $M$ from a subset $\Omega$ of its entries. When $M$ has low rank, a standard convex surrogate is to minimize the nuclear norm $\|X\|_*$ (the sum of the singular values) subject to agreeing with $M$ on $\Omega$ ; Candès and Recht showed that this recovers $M$ exactly under incoherence and sampling conditions (Candès–Recht 2009). Generic interior-point solvers for this semidefinite program do not scale beyond matrices of a few hundred rows.

Cai, Candès and Shen (SIAM J. Optim. 2010) proposed the singular value thresholding (SVT) algorithm: a first-order iteration whose only nonlinear step is a soft-thresholding of singular values, and whose other iterate is a sparse matrix supported on $\Omega$ . The algorithm has become a standard baseline in low-rank matrix recovery and a model example of dual (Uzawa-type) methods for nuclear-norm problems. This mission formalizes its convergence theorem.

Setting

All matrices are real. For $X,Y\in\mathbb R^{n_1\times n_2}$ write $\langle X,Y\rangle=\operatorname{trace}(X^*Y)=\sum_{i,j}X_{ij}Y_{ij}$ and $\|X\|_F^2=\langle X,X\rangle$ . The nuclear norm $\|X\|_*$ is the sum of the singular values of $X$ .

For an index set $\Omega$ , the sampling projector $P_\Omega$ keeps the entries with indices in $\Omega$ and sets the others to zero.

A reduced singular value decomposition of a matrix $Y$ of rank $r$ is $Y=U\Sigma V^*$ with $U$ ( $n_1\times r$ ) and $V$ ( $n_2\times r$ ) having orthonormal columns and $\Sigma=\operatorname{diag}(\sigma_1,\dots,\sigma_r)$ with $\sigma_i>0$ . For $\tau\ge0$ the singular value shrinkage operator is

\mathcal D_\tau(Y)=U\operatorname{diag}\big((\sigma_i-\tau)_+\big)V^*,\qquad t_+=\max(0,t).

Fix $\tau>0$ , a sequence of step sizes $\{\delta_k\}_{k\ge1}$ and data $M$ . The SVT iteration (2.7) starts from $Y^0=0$ and sets, for $k=1,2,\dots$ ,

X^k=\mathcal D_\tau(Y^{k-1}),\qquad Y^k=Y^{k-1}+\delta_k P_\Omega(M-X^k).

The proximal problem (2.8) is

\text{minimize}\ \ f_\tau(X)=\tau\|X\|_*+\tfrac12\|X\|_F^2\quad\text{subject to}\ \ P_\Omega(X)=P_\Omega(M).

More generally, for a linear map $\mathcal A:\mathbb R^{n_1\times n_2}\to\mathbb R^m$ with adjoint $\mathcal A^*$ and spectral norm $\|\mathcal A\|=\sup\{\|\mathcal A(X)\|_{\ell_2}:\|X\|_F=1\}$ , and $b\in\mathbb R^m$ , problem (3.1) is to minimize $f_\tau(X)$ subject to $\mathcal A(X)=b$ , and Uzawa's iteration (3.3) starts from $y^0=0$ and sets $X^k=\mathcal D_\tau(\mathcal A^*(y^{k-1}))$ , $y^k=y^{k-1}+\delta_k(b-\mathcal A(X^k))$ .

Formalization targets

Goal: Theorem 4.2, second sentence (p. 1968)

If $0<\inf_k\delta_k\le\sup_k\delta_k<2$ , then (2.8) has a unique solution $X^\star$ and the SVT iterates satisfy

\lim_{k\to\infty}X^k=X^\star .

Theorem 4.2, first sentence (p. 1968)

If (3.1) is feasible and $0<\inf_k\delta_k\le\sup_k\delta_k<2/\|\mathcal A\|^2$ , then (3.1) has a unique solution and the iterates $X^k$ of (3.3) converge to it.

Supporting results (milestones, in attack order)

Well-definedness of $\mathcal D_\tau$ (§2.1, p. 1960): the output does not depend on the chosen SVD.
Theorem 2.1 (p. 1960): $\mathcal D_\tau(Y)=\arg\min_X \tfrac12\|X-Y\|_F^2+\tau\|X\|_*$ .
Sparsity of the iterates (§2.2, p. 1961): since $Y^0=0$ , every $Y^k$ vanishes outside $\Omega$ .
Eq. (2.14) (p. 1964): the minimizers of the Lagrangian $f_\tau(X)+\langle Y,P_\Omega(M-X)\rangle$ are those of $\tau\|X\|_*+\tfrac12\|X-P_\Omega Y\|_F^2$ .
Lemma 4.1 (p. 1968): for $Z\in\partial f_\tau(X)$ , $Z'\in\partial f_\tau(X')$ , $\langle Z-Z',X-X'\rangle\ge\|X-X'\|_F^2$ .
The §3.1 reduction (p. 1964): for a sampling operator, $\mathcal A^*\mathcal A=P_\Omega$ and (3.3) becomes (2.7) under $Y^k=\mathcal A^*(y^k)$ .
Theorem 4.2, first sentence, as above.

Significance

The theorem certifies that SVT, run with any step sizes in a fixed interval $(0,2)$ , computes the unique minimizer of the strongly convex surrogate (2.8). Together with the separate fact that the solution of (2.8) tends to the minimum nuclear norm completion as $\tau\to\infty$ (the paper's Theorem 3.1, a companion mission), this is what justifies using SVT as a solver for nuclear-norm matrix completion. Theorem 2.1, the proximal characterization of singular value soft-thresholding, is used throughout the literature on proximal methods for low-rank problems.

The paper's proof of Theorem 4.2 consists of the reduction to Uzawa's method and a citation of a general convergence theorem for projected gradient methods on the dual. The formalization produces a self-contained, machine-checked chain: the proximal characterization of $\mathcal D_\tau$ , the Lagrangian identity, strong monotonicity of $\partial f_\tau$ , and the convergence argument itself. To our knowledge none of these results has a machine-checked proof; Mathlib at the pinned revision has singular values of linear maps but no SVD structure, no nuclear norm and no subgradient calculus.

Difficulty

Nothing in the iteration is a gradient step of a smooth function in $X$ : the $X$ -update is a nonsmooth proximal map, and the convergence of $X^k$ is not visible from the recursion itself. The paper's argument cites a general theorem on projected gradient methods ([25, Theorem 2.1]) and takes for granted that "strong duality holds" for (2.8) (p. 1963), so the existence of a Lagrange multiplier is part of what must be formalized. Theorem 2.1 depends on the subdifferential of the nuclear norm, which Mathlib does not provide, and therefore on the singular value decomposition and the duality between the nuclear and spectral norms. Convergence of objective values or of a subsequence would not suffice: the target is convergence of the whole sequence $X^k$ to the unique solution.

Formalization scope

Matrices are Matrix (Fin n₁) (Fin n₂) ℝ; convergence is Mathlib's topology on matrices, which coincides with the Frobenius-norm topology. $\langle\cdot,\cdot\rangle$ and $\|\cdot\|_F$ are defined entrywise; $\|X\|_*$ is the sum of Mathlib's LinearMap.singularValues of $X$ viewed as a map $\mathbb R^{n_2}\to\mathbb R^{n_1}$ . The shrinkage operator is a relation IsShrink τ Y X defined, as in (2.1)–(2.2), through some reduced SVD of $Y$ ; well-definedness is a milestone. It is not defined as the minimizer of (2.3), which would make Theorem 2.1 definitional. Linear maps $\mathcal A$ are given by matrices $A_1,\dots,A_m$ with $\mathcal A(X)_i=\langle A_i,X\rangle$ , and a sampling operator by an injective enumeration of $\Omega$ . Subgradients are those of (2.4).

Sequences are indexed by $\mathbb N$ : Lean's step $k+1$ is the paper's step $k$ , so $X^0$ and $\delta_0$ are unused. Committed conventions:

$Y^0=0$ and $y^0=0$ are hypotheses; with a start that is nonzero outside $\Omega$ the iterates converge to a different matrix.
The standing $\tau>0$ is kept, except in Theorem 2.1 and the well-definedness statement, which are printed for $\tau\ge0$ .
The step-size conditions are explicit bounds $a>0$ , $C$ with $a\le\delta_k\le C$ for $k\ge1$ , together with $C<2$ , respectively $C\|\mathcal A\|^2<2$ . The multiplicative form avoids Lean's $x/0=0$ : for $\mathcal A=0$ the condition does not become unsatisfiable.
Feasibility of (3.1) is an added hypothesis of Theorem 4.2's first sentence, since "the unique solution" presupposes it.
"Converges to the unique solution" is stated as existence and uniqueness of the solution together with convergence of the whole sequence to it.

A small unprinted helper, $\|\mathcal A\|\le1$ for sampling operators, is included to pass from the first sentence of Theorem 4.2 to the second; it is not a milestone. The subdifferential formula (2.6) of the nuclear norm and the Fejér-type condition of §5.1.2 are not stated. Reusable infrastructure welcome from solvers: existence and uniqueness properties of the reduced SVD, the nuclear/spectral norm duality, the subdifferential of the nuclear norm, and a general convergence theorem for Uzawa's method with a strongly convex objective.

Selected references

J.-F. Cai, E. J. Candès, Z. Shen, A Singular Value Thresholding Algorithm for Matrix Completion, SIAM J. Optim. 20(4):1956–1982, 2010. https://doi.org/10.1137/080738970
E. J. Candès, B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9:717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
K. J. Arrow, L. Hurwicz, H. Uzawa, Studies in Linear and Non-Linear Programming, Stanford University Press, 1958.

12 thms2 active usersReviewed

Convex Optimization Linear Optimization Operations Research+1·Captain: mikedeng1

Path-Finding Methods for Linear Programming II: Properties of the Regularized D-Optimal-Design Weight FunctionResearch Paper

Motivation

Interior point methods for a linear program $\min\{c^\top x : Ax\ge b\}$ with $A\in\mathbb R^{m\times n}$ follow the central path of the logarithmic barrier $-\sum_i\log s_i$ , where $s=Ax-b$ is the slack vector. Renegar's path-following analysis (1988) gives $O(\sqrt m\,L)$ iterations, and for decades this was the best bound for methods whose iterations cost a linear system solve. Vaidya's volumetric barrier $-\log\det(A^\top S^{-2}A)$ and the hybrid volumetric barriers of Vaidya and of Anstreicher (references [45] and [2] of the paper) reached $O((m\,\mathrm{rank}(A))^{1/4}L)$ iterations at the price of more expensive linear algebra. Nesterov and Nemirovski showed that a universal barrier gives $O(\sqrt n\,L)$ iterations, but that barrier cannot be evaluated efficiently.

Lee and Sidford (FOCS 2014; full version arXiv:1312.6677) obtained $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ iterations, each costing $\tilde O(1)$ linear system solves, by following a weighted central path whose weights are recomputed from the slacks. The weights come from a weight function $g$ , defined as the minimizer of a regularized D-optimal-design problem. This mission is about that weight function and the theorem (Theorem 1 of the paper) certifying its properties. The companion mission, Path-Finding Methods for Linear Programming I, formalizes the path-following framework (Theorem 5 of §IV.C) that consumes these properties.

Setting

Fix $A\in\mathbb R^{m\times n}$ with full column rank, $\mathrm{rank}(A)=n$ , and $1\le n<m$ . For vectors $s,w\in\mathbb R^m_{>0}$ write $S=\mathrm{diag}(s)$ , $W=\mathrm{diag}(w)$ , $W^\alpha=\mathrm{diag}(w_i^\alpha)$ , and $A_s=S^{-1}A$ . For a matrix $M$ let $\|v\|_M=\sqrt{v^\top Mv}$ .

Projection matrix and slack sensitivity (Definition 2, p. 428). The projection matrix is $P_{S^{-1}A}(w)=W^{1/2}S^{-1}A\,(A^\top S^{-1}WS^{-1}A)^{-1}A^\top S^{-1}W^{1/2}$ , and the slack sensitivity is

\gamma(s,w)=\max_{i\in[m]}\big\|W^{-1/2}\mathbb 1_i\big\|_{P_{S^{-1}A}(w)} .

Weight function (Definition 4, p. 428). A map $g:\mathbb R^m_{>0}\to\mathbb R^m_{>0}$ is a weight function with constants $c_1,c_\gamma,c_r$ if it is differentiable and, for every $s>0$ , with $G(s)=\mathrm{diag}(g(s))$ , $G'(s)$ the Jacobian of $g$ at $s$ , and $\|y\|_{G(s)}=\sqrt{\sum_ig_i(s)y_i^2}$ :

Size: $\|g(s)\|_1\le c_1$ ;
Slack sensitivity: $c_\gamma\ge1$ and $\gamma(s,g(s))\le c_\gamma$ ;
Step consistency: $c_r\ge1$ and for all $r\ge c_r$ , $y\in\mathbb R^m$ : $\|(I+r^{-1}G^{-1}G'S)y\|_{G(s)}\le\|y\|_{G(s)}$ and $\|y+r^{-1}G^{-1}G'Sy\|_\infty\le\|y\|_\infty+c_r\|y\|_{G(s)}$ ;
Uniformity: $\|g(s)\|_\infty\le2$ .

The regularized objective (6), p. 429. For $\alpha,\beta\in\mathbb R$ ,

\hat f(s,w)=\mathbb 1^\top w-\frac1\alpha\log\det\big(A_s^\top W^\alpha A_s\big)-\beta\sum_{i\in[m]}\log w_i ,\qquad g(s)=\arg\min_{w\in\mathbb R^m_{>0}}\hat f(s,w).

At $\alpha=1,\beta=0$ this is the D-optimal design problem, dual to computing the John ellipsoid of the polytope $\{y:|[A(y-x)]_i|\le s_i\}$ (§V.B).

Formalization targets

Goal: Theorem 1 (Properties of Weight Function), §V.A, p. 429

With

\alpha=1-\Big(\log_2\frac{2m}{\mathrm{rank}(A)}\Big)^{-1},\qquad \beta=\frac{\mathrm{rank}(A)}{2m},

the objective $\hat f(s,\cdot)$ has a unique minimizer over $\mathbb R^m_{>0}$ for every $s>0$ , and the resulting $g$ is a weight function with

c_1(g)=2\,\mathrm{rank}(A),\qquad c_\gamma(g)=2,\qquad c_r(g)=2\log_2\frac{2m}{\mathrm{rank}(A)} .

Milestones: the three bullets of Theorem 1

Size: every minimizer $w$ of $\hat f(s,\cdot)$ satisfies $\|w\|_1\le2\,\mathrm{rank}(A)$ .
Slack sensitivity: every minimizer $w$ satisfies $\gamma(s,w)\le2$ .
Step consistency: any map $g$ selecting a minimizer at every $s>0$ is differentiable on $\mathbb R^m_{>0}$ and satisfies the two step-consistency inequalities for every $r\ge2\log_2\frac{2m}{\mathrm{rank}(A)}$ .

A supporting (non-milestone) item states the existence and uniqueness of the minimizer on its own.

Significance

The result. Theorem 1 is the input that turns the weighted path-following framework into an $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ -iteration method: the framework needs $O(c_\gamma^{-1}c_r^{-3}c_1^{-1/2})$ -sized steps in $t$ (p. 428), and Theorem 1 makes that $\tilde\Omega(1/\sqrt{\mathrm{rank}(A)})$ . The step consistency bound is what allows the weights to be recomputed after each Newton step without losing centrality. The same construction underlies later work on Lewis-weight barriers and on fast approximate John ellipsoids and maximum flow (§VIII of the paper).

Formalizing it. The theorem is proved in the full version of the paper (arXiv:1312.6677); the FOCS extended abstract contains no proofs. No part of it has a machine-checked proof. A complete formalization would give a verified account of leverage-score calculus (sums of leverage scores equal the rank; derivatives of projection matrices), of the convexity of $w\mapsto-\log\det(A^\top W^\alpha A)$ for $\alpha\in(0,1)$ , and of differentiability of an argmin via the implicit function theorem, none of which is currently packaged in Mathlib in this form.

Difficulty

Size and slack sensitivity are statements about the minimizer, which is only characterized implicitly; they require precise matrix calculus for $\log\det(A_s^\top W^\alpha A_s)$ and a comparison between the matrices $A^\top WA$ (which defines $\gamma$ ) and $A^\top W^\alpha A$ (which defines $g$ ). The specific values of $\alpha$ and $\beta$ matter here: the unregularized choice $\alpha=1$ , $\beta=0$ makes the problem degenerate (p. 429).

The hard part is step consistency. The Jacobian $G'$ of an argmin is available only implicitly, as the solution of a linear system obtained by differentiating the optimality condition. A bound on $\|G'\|$ that depends on $m$ is easy to get and useless: the theorem needs the operator norm of $I+r^{-1}G^{-1}G'S$ in the $G(s)$ -norm to be at most $1$ as soon as $r$ exceeds $2\log_2(2m/\mathrm{rank}(A))$ , and an $\ell_\infty$ bound with only an additive $c_r\|y\|_{G(s)}$ loss.

Existence and differentiability of the minimizer are conclusions, not hypotheses. The minimization is over an open orthant on which the objective is not obviously coercive or strictly convex for $\alpha<1$ , and differentiability of $g$ requires the Hessian of $\hat f$ at the minimizer to be invertible.

Formalization scope

Vectors are Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; inverses are Matrix.inv, $\log\det$ is Real.log (Matrix.det …), $w_i^\alpha$ is Real.rpow, $\log_2$ is Real.logb 2, the Jacobian is fderiv ℝ g s, and $\|\cdot\|_\infty$ is Mathlib's sup norm on Fin m → ℝ.

Conventions and pinned hypotheses:

Full column rank A.rank = n is assumed in every theorem. The paper never states it, but without it $A_s^\top W^\alpha A_s$ is singular and every formula is undefined (in Lean, Matrix.inv and Real.log would return junk $0$ ).
$1\le n<m$ . $\beta=\mathrm{rank}(A)/(2m)$ and $\log_2(2m/\mathrm{rank}(A))$ need $\mathrm{rank}(A)\ge1$ ; at $m=\mathrm{rank}(A)$ the page's $\alpha$ is $0$ and $1/\alpha$ in (6) is undefined.
Reading of $\alpha$ : the exponent $-1$ is the reciprocal of $\log_2\frac{2m}{\mathrm{rank}(A)}$ , giving $\alpha\in(0,1)$ .
Size is an upper bound $\|g(s)\|_1\le c_1$ (the paper's weight function has $\|g(s)\|_1=\tfrac32\mathrm{rank}(A)$ , while Theorem 1 reports $c_1=2\,\mathrm{rank}(A)$ ).
The first step-consistency bullet (an operator-norm bound) is stated for every vector $y$ .
$g$ is any map $\mathbb R^m\to\mathbb R^m$ whose value at each positive $s$ minimizes $\hat f(s,\cdot)$ over $\mathbb R^m_{>0}$ . Only its values on the open orthant matter. The goal also asserts that such minimizers exist and are unique, so it is not vacuous.

Ruling out trivializations: the goal does not assume $g$ to be a weight function or to be differentiable, and it does not replace $g$ by an arbitrary weight function; differentiability is a conclusion (a predicate using fderiv without it would make step consistency hold vacuously wherever $g$ fails to be differentiable).

Useful infrastructure, reusable beyond this mission: leverage scores and their sum; derivatives of $w\mapsto\log\det(A^\top WA)$ and of projection matrices; convexity of $-\log\det(A^\top W^\alpha A)$ in $w$ (related to the published ConvexOptimization.log_det_concaveOn); differentiability of the argmin of a strictly convex smooth function. Contributions of these as separate theorems are welcome, as is a proof of any single bullet of Theorem 1.

Selected references

Y. T. Lee, A. Sidford, Path Finding Methods for Linear Programming: Solving Linear Programs in Õ(√rank) Iterations and Faster Algorithms for Maximum Flow, FOCS 2014, pp. 424–433. https://doi.org/10.1109/FOCS.2014.52
Y. T. Lee, A. Sidford, Path Finding I: Solving Linear Programs with Õ(√rank) Linear System Solves, arXiv, 2013. https://arxiv.org/abs/1312.6677
J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Mathematical Programming 40 (1988). https://doi.org/10.1007/BF01580724

7 thms2 active usersReviewed

Completed

Mathematical Physics·Captain: ShapeZero

The passivity-admissible couplings have dimension n² = dim u(n)Textbook

Motivation

The Shape Zero model (Shape Zero LLC, unpublished) aims to obtain all three factors of the Standard Model gauge structure — $U(1)$ , $SU(2)$ and $SU(3)$ — from a single linear-algebra statement applied at three node sizes. A node carrying $n$ oscillator pairs has a $2n$ -dimensional real state space with a complex structure $J$ . Within the model, the couplings that do no net work (passive couplings) are the symmetric matrices, and those that respect $J$ are the ones commuting with it. The claim is that the couplings satisfying both conditions form a real vector space of dimension exactly $n^2$ , which is the dimension of the unitary Lie algebra $\mathfrak{u}(n)$ (Unitary group):

node size $n$	admissible dimension	Lie algebra
1	1	$\mathfrak{u}(1)$
2	4	$\mathfrak{u}(2) = \mathfrak{u}(1) \oplus \mathfrak{su}(2)$
3	9	$\mathfrak{u}(3) = \mathfrak{u}(1) \oplus \mathfrak{su}(3)$

The dimension count has so far been checked numerically for $n = 1, \dots, 5$ only, giving $1, 4, 9, 16, 25$ . A machine-checked proof covers every $n$ , and it is the claim a physicist examining the model would check first.

What this mission does NOT prove. This mission proves the linear algebra: symmetric matrices commuting with $J$ form a space of dimension $n^2$ . It does not prove the physics step that passivity forces a coupling to be symmetric. That step is a separate premise of the model, and a completed mission must not be read as establishing it.

Setting

Fix a natural number $n$ . Consider real $2n \times 2n$ matrices, with rows and columns indexed by two copies of $\{0, \dots, n-1\}$ , so that each matrix is written in $2 \times 2$ block form with $n \times n$ blocks:

W = \begin{pmatrix} A & B \\ C & D \end{pmatrix}.

Let $I$ be the $n \times n$ identity matrix and define the standard complex structure

J = \begin{pmatrix} 0 & -I \\ I & 0 \end{pmatrix},

which satisfies $J^2 = -1$ . In the Lean development this matrix is PassivityUn.stdJ n, and the index type is PassivityUn.Blk n, the disjoint union of two copies of Fin n.

Two real linear subspaces of the $4n^2$ -dimensional space of such matrices are defined:

symm n: the symmetric matrices, $W^{\mathsf T} = W$ ;
commJ n: the matrices commuting with $J$ , $WJ = JW$ .

The admissible coupling class admissible n is their intersection:

\mathcal{A}_n = \{\, W \in \mathbb{R}^{2n \times 2n} : W^{\mathsf T} = W \ \text{and}\ WJ = JW \,\}.

Formalization targets

Goal: the admissible class has dimension $n^2$

\dim_{\mathbb{R}} \mathcal{A}_n = n^2 \qquad \text{for every } n \in \mathbb{N}.

This is PassivityUn.admissible_finrank. It asserts the exact dimension for all $n$ at once, not for a particular node size.

Milestones

M1. $J \cdot J = -1$ , so $J$ is a complex structure.
M2. A block matrix $\begin{pmatrix} A & B \\ C & D \end{pmatrix}$ commutes with $J$ exactly when $D = A$ and $B = -C$ .
M3. A block matrix $\begin{pmatrix} A & -B \\ B & A \end{pmatrix}$ is symmetric exactly when $A^{\mathsf T} = A$ and $B^{\mathsf T} = -B$ .
M4. The dimension counts of symmetric and antisymmetric $n \times n$ matrices add to $n^2$ : $\tfrac{n(n+1)}{2} + \tfrac{n(n-1)}{2} = n^2$ .

Significance

The result itself. The goal identifies the admissible coupling class with the real form of the $n \times n$ Hermitian matrices, the space whose dimension is that of $\mathfrak{u}(n)$ (Hermitian matrix). Applied at $n = 1, 2, 3$ it gives the dimensions $1$ , $4$ and $9$ , which the Shape Zero model matches with $\mathfrak{u}(1)$ , $\mathfrak{u}(2) = \mathfrak{u}(1) \oplus \mathfrak{su}(2)$ and $\mathfrak{u}(3) = \mathfrak{u}(1) \oplus \mathfrak{su}(3)$ . Without a proof for general $n$ , the model rests on a finite numerical check.

Formalizing it. The underlying fact is standard linear algebra, a special case of the correspondence between real matrices commuting with a complex structure and complex-linear maps (Linear complex structure). No machine-checked statement of this exact dimension count was found in the platform library. The mission produces a verified, general- $n$ statement whose hypotheses are fully explicit, and it separates the verified linear algebra from the unverified physical premise.

Difficulty

Every step is standard linear algebra, so the difficulty is in the formal bookkeeping rather than the mathematics. The dimension of a subspace defined by equations is not computed by any Mathlib tactic. It has to be obtained by exhibiting an explicit linear equivalence with spaces of known dimension, and that requires moving between the $2n \times 2n$ matrix indexed by a disjoint union and its four $n \times n$ blocks. Checking small cases numerically, as has already been done, does not extend to a statement about every $n$ .

Formalization scope

Matrices are real (ℝ), not complex. The complex structure enters only through the fixed real matrix $J$ .
Matrices are indexed by Fin n ⊕ Fin n (PassivityUn.Blk n) rather than Fin (2n), so that block decomposition via Mathlib's Matrix.fromBlocks is direct. The first copy of Fin n indexes the upper/left blocks.
Each condition is defined as the kernel of a linear map: symmetry as the kernel of $W \mapsto W^{\mathsf T} - W$ , and commuting with $J$ as the kernel of $W \mapsto WJ - JW$ . Both are therefore subspaces by construction, with no hand-written closure proofs.
Dimension is Module.finrank ℝ. The ambient space is finite-dimensional, so the convention that finrank of an infinite-dimensional space is $0$ never applies.
The case $n = 0$ is included, and there the statement reads $0 = 0$ . This is not a trivialization: the claim is quantified over all $n$ , and every $n \ge 1$ is a nontrivial instance.
M4 is stated with natural-number division and truncated subtraction. Both are exact here, because $n(n \pm 1)$ is always even and $n \cdot (n - 1) = 0$ when $n = 0$ .

The development needs only Mathlib's block matrices, transpose, linear maps and finrank. The block-characterization lemmas (M2, M3) are reusable for any statement relating real matrices commuting with $J$ to complex matrices. Contributions are welcome on the milestones and on the assembling isomorphism.

Selected references

B. C. Hall, Lie Groups, Lie Algebras, and Representations: An Elementary Introduction, 2nd ed., Graduate Texts in Mathematics 222, Springer, 2015. https://doi.org/10.1007/978-3-319-13467-3
Wikipedia, Unitary group. https://en.wikipedia.org/wiki/Unitary_group
Wikipedia, Linear complex structure. https://en.wikipedia.org/wiki/Linear_complex_structure
Wikipedia, Hermitian matrix. https://en.wikipedia.org/wiki/Hermitian_matrix
Mathlib, Mathlib.Data.Matrix.Block (block matrices, Matrix.fromBlocks). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Block.html

7 thms2 active usersReviewed

Combinatorics Graph Theory Theoretical Computer Science·Captain: mikedeng1

Explicit Expanders of Every Degree and Size 3: Deleting Far-Apart Tree-Like Vertices of a Near-Ramanujan Graph and Matching Their Neighbours Keeps λ ≤ 2√(d−1) + εResearch Paper

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

13 thms1 active userReviewed

Combinatorics Graph Theory Theoretical Computer Science·Captain: mikedeng1

Explicit Expanders of Every Degree and Size 2: Attaching New Vertices to a (p+1)-Regular Ramanujan Graph and Adding Loops Keeps Every Nontrivial Eigenvalue at Most √(2(p+1)) + √p + o(1)Research Paper

Motivation

Sparse graphs whose adjacency spectrum is concentrated near zero, expanders, are used throughout theoretical computer science: in error-correcting codes, derandomization, sorting and routing networks, and the construction of pseudorandom objects (Hoory, Linial and Wigderson, survey). The best possible spectral expansion for a $d$ -regular graph is governed by the Alon–Boppana bound $2\sqrt{d-1}$ , and graphs attaining it, Ramanujan graphs, were constructed explicitly by Lubotzky, Phillips and Sarnak (LPS 1988) and by Margulis. These constructions exist only for special degrees ( $d = p+1$ with $p$ prime) and special numbers of vertices (orders of $PSL(2,\mathbb F_q)$ or $SL(2,\mathbb F_q)$ ). Applications often need a graph of a prescribed size $n$ .

N. Alon's paper Explicit expanders of every degree and size (arXiv:2003.11673v1; Combinatorica 41, 2021) shows how to obtain explicit near-Ramanujan graphs on exactly $n$ vertices. This mission formalizes the spectral core of its Theorem 1.2: a Ramanujan graph on $m$ vertices can be enlarged to $n = m + r$ vertices, with degree raised by one, while the nontrivial eigenvalues stay within a constant factor of optimal.

Setting

Let $V$ be a finite set of $m \ge 1$ vertices. A $(n,d,\lambda)$ -graph is a $d$ -regular graph on $n$ vertices whose adjacency matrix $A$ satisfies $|\mu| \le \lambda$ for every nontrivial eigenvalue $\mu$ , that is, every eigenvalue other than the top eigenvalue $d$ of the constant vector $\mathbf 1$ . For a symmetric $A$ with $A\mathbf 1 = d\,\mathbf 1$ , the nontrivial eigenvalues are those with an eigenvector $f \ne 0$ satisfying $\sum_v f(v) = 0$ . Graphs may carry loops, at most one per vertex, and a loop adds one to the degree: it is a diagonal entry $1$ of $A$ .

Fix an integer $p \ge 0$ and let $H$ be an $(m, p+1, 2\sqrt p)$ -graph on $V$ , a $(p+1)$ -regular Ramanujan graph. Let $R = \{u_1, \dots, u_r\}$ be $r$ new vertices and let $W_1, \dots, W_r \subseteq V$ be pairwise disjoint sets of $p+2$ vertices each. Put $W = \bigcup_i W_i$ and $L = V \setminus W$ . The graph $G$ on $U = V \cup R$ is obtained from $H$ by joining each $u_i$ to every vertex of $W_i$ and adding one loop at each vertex of $L$ . Its adjacency matrix is

A_G = A_H + A_R + A_L,

where $A_H$ is the adjacency matrix of $H$ (zero on $R$ ), $A_R$ that of the stars joining $u_i$ to $W_i$ , and $A_L$ the diagonal matrix of the loops. Every vertex of $G$ has degree $p+2$ .

Formalization targets

Goal: Theorem 1.2, spectral core

A_G \text{ is an } \Big(m+r,\; p+2,\; \sqrt{2(p+1)} + \sqrt p + \frac{(p+1)\,r}{m}\Big)\text{ matrix.}

The paper states $\lambda \le \sqrt{2(d-1)} + \sqrt{d-1} + o(1)$ for $d = p+2$ ; its proof gives $\sqrt{2(p+1)} + \sqrt p + o(1)$ , which is stronger, and the error term it produces is $(p+1)r/m$ . The goal is parametrised by $H$ , $r$ and the sets $W_i$ , so it does not depend on how $m$ and $r$ are chosen.

Milestones

The variational characterization of the nontrivial eigenvalues: for a symmetric matrix with constant row sums and $\lambda \ge 0$ , $|\mu| \le \lambda$ for every nontrivial eigenvalue if and only if $|f^tAf| \le \lambda\|f\|^2$ whenever $\sum f = 0$ .
The Cauchy–Schwarz display: $\sum_U f = 0$ implies $|\sum_V f|^2 = |\sum_R f|^2 \le |R| \sum_R f^2$ .
Inequality (3): $|f^tA_Hf| \le b^2(p+1) + c^2\, 2\sqrt p$ with $b^2 = (\sum_V f)^2/m$ and $c^2 = \sum_V f^2 - b^2$ .
Display (4): $f^tA_Lf = \sum_{v\in L} f^2(v)$ .
Inequality (5): $|f^tA_Rf| \le \frac{p+2}{x}\sum_R f^2 + x\sum_W f^2$ for every $x > 0$ .
Inequality (6): for $\sum_U f = 0$ and $x > 0$ ,

|f^tA_Gf| \le (2\sqrt p+1)\sum_L f^2 + (2\sqrt p+x)\sum_W f^2 + \frac{p+2}{x}\sum_R f^2 + (p+1)\frac rm \sum_R f^2.

Significance

With $H$ the Lubotzky–Phillips–Sarnak graph on $m = |SL(2,\mathbb F_q)|$ vertices for the largest suitable prime $q$ with $m \le n$ , and $r = n - m$ , the distribution of primes in arithmetic progressions gives $r = o(m)$ , and the goal yields an explicit $(n, p+2, \lambda)$ -graph with $\lambda \le (1+\sqrt2)\sqrt{d-1} + o(1)$ for every sufficiently large $n$ . This is within a factor of about $1.21$ of the Ramanujan bound $2\sqrt{d-1}$ , for every number of vertices, by an elementary modification of an existing graph. The statement is useful independently of LPS: any Ramanujan graph, or any graph with a bound on its nontrivial eigenvalues, can be padded to a nearby size in the same way.

The result is proved in the paper. No formalization of it, of the $(n,d,\lambda)$ notion, or of the variational characterization of nontrivial eigenvalues for regular graphs exists on the platform. The mission produces a checked version of the spectral argument, and the variational characterization (milestone 1) is a general fact about symmetric matrices with constant row sums that applies to any spectral expander argument.

Difficulty

The vertices of $W$ and $L$ lie in the old graph $H$ , whose spectrum is controlled, but the new vertices of $R$ are not; and a vector orthogonal to $\mathbf 1$ on $U$ need not be orthogonal to the constant vector on $V$ . Bounding $f^tA_Gf$ by applying the Ramanujan bound for $H$ to $f$ restricted to $V$ therefore fails: the restriction has a component along the trivial eigenvector of $H$ , whose eigenvalue $p+1$ is large. The argument must show that this component is small, of order $r/m$ , and must balance the star edges between $R$ and $W$ against the loops on $L$ so that every vertex class gets the same coefficient. The naive bound $|f^tA_Rf| \le \|A_R\|\,\|f\|^2 = \sqrt{p+2}\,\|f\|^2$ added to $2\sqrt p$ for $H$ and $1$ for $L$ gives a constant larger than $\sqrt{2(p+1)}+\sqrt p$ ; the stated constant needs the weighted estimate.

On the Lean side, milestone 1 concerns the spectrum of a symmetric matrix on the invariant subspace $\mathbf 1^\perp$ , while Mathlib states the spectral theorem for the whole space.

Formalization scope

Vertices of $G$ are the disjoint union $V \oplus \mathrm{Fin}\, r$ . $G$ is represented by its real adjacency matrix, since it has loops; $H$ is a Mathlib SimpleGraph with adjMatrix.
The $(n,d,\lambda)$ predicate is stated for matrices: $|V| = n$ , symmetry, $A\mathbf 1 = d\,\mathbf 1$ , and $|\mu| \le \lambda$ for every eigenpair $(\mu, f)$ with $f \ne 0$ and $\sum f = 0$ . For simple graphs, $d$ -regularity is added.
The paper's $o(1)$ terms are replaced by the explicit quantities its proof produces: $(p+1)r/m$ in the goal, and $(p+1)\frac rm\sum_R f^2$ in (6). Inequality (3) is stated with the corrected relation $b^2 + c^2 = \sum_V f^2$ ; the paper's " $b^2 + c^2 = 1$ " holds only for unit restrictions.
The bound uses $\sqrt p = \sqrt{d-2}$ , as in the proof and the abstract, which implies the printed $\sqrt{d-1}$ .
$p$ is any natural number. The hypothesis " $p$ prime, $p \equiv 1 \pmod 4$ " serves only to obtain $H$ from LPS, and $H$ is a hypothesis here. The sets $W_i$ are arbitrary pairwise disjoint sets of size $p+2$ , not the paper's consecutive blocks of a numbering of $SL(2,\mathbb F_q)$ .
Out of scope: the existence of the prime $q$ and the estimate $n - m = o(m)$ ; the numbering of $SL(2,\mathbb F_q)$ ; the "strongly explicit" and polynomial-time claims; the LPS construction (Theorem 2.1, cited); the variant that replaces loops by a matching for even $n$ .
The goal cannot be satisfied trivially: dropping the condition $\sum f = 0$ makes it false, since $p+2$ is always an eigenvalue, and for $p \ge 2$ and small $r/m$ the bound is below $p + 2$ (for $p = 5$ it is about $5.70 + 6r/m$ ). At $p = 1$ the bound $3 + 2r/m$ is at least the degree $3$ , so that case holds trivially; it is the paper's statement there as well.
Contributions welcome: proofs of each milestone, especially the variational characterization, which is reusable for mission 3 of this series and for any regular-graph spectral argument.

Selected references

N. Alon, Explicit expanders of every degree and size, arXiv:2003.11673v1, 2020; Combinatorica 41 (2021). https://arxiv.org/abs/2003.11673
A. Lubotzky, R. Phillips, P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988) 261–277. https://doi.org/10.1007/BF02126799
S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bull. AMS 43 (2006) 439–561. https://doi.org/10.1090/S0273-0979-06-01126-8

9 thms1 active userReviewed

Combinatorics Operations Research·Captain: mikedeng1

On the Abstract Properties of Linear Dependence 5: The Seven-Element Fano Matroid Corresponds to No Real MatrixResearch Paper

Motivation

Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets equipped with a rank function, or equivalently a family of independent sets, obeying a few postulates abstracted from the linear dependence of the columns of a matrix. The obvious first question about such an abstraction is whether it is genuinely more general than its model, that is, whether there are matroids that do not arise from any matrix. Section 16 of the paper answers it with a seven-element example, now called the Fano matroid $F_7$ , and proves that no real matrix corresponds to it.

The question has had a long life. Representability of matroids over a given field is a central theme of matroid theory: Tutte (1958) characterized the matroids representable over the field with two elements by a single excluded minor, the four-point line $U_{2,4}$ , and the regular matroids by three excluded minors, $U_{2,4}$ , $F_7$ and its dual; and Seymour's decomposition of regular matroids (1980) rests on the same objects. Whitney's §16 is the starting point of this line: the first proof that the abstract postulates admit matroids outside linear algebra over $\mathbb R$ .

Timeline:

1935. Whitney defines matroids, the circuit matrix of a matrix, and proves (§16) that the seven-element matroid $M'$ corresponds to no real matrix; in a footnote he credits Saunders MacLane with finding that $M'$ corresponds to no matrix and identifying it with a finite projective geometry. On p. 533 he exhibits a matrix of integers mod 2 for $M'$ .
1958. Tutte characterizes binary and regular matroids by excluded minors; $F_7$ appears as an excluded minor for regularity (Tutte 1958).

Setting

Let $\mathbf M=(a_{ij})$ be an $m\times n$ matrix with columns $C_1,\dots,C_n$ . For a set $N$ of columns, let $r(N)$ be the rank of the submatrix formed by those columns. Regarding the columns as abstract elements gives a matroid $M$ on $\{C_1,\dots,C_n\}$ with rank function $r$ : the matroid of $\mathbf M$ . A matroid corresponds to $\mathbf M$ if it is the matroid of $\mathbf M$ , with elements matched to columns.

A circuit of a matroid is a minimal dependent set. For a circuit $P=\{i_1,\dots,i_p\}$ of the matroid of $\mathbf M$ , there are numbers $b_1,\dots,b_n$ with $\sum_j a_{ij}b_j=0$ for every row $i$ , and $b_j\neq 0$ exactly for $j\in P$ ; the set of such vectors is written $Z_{i_1\cdots i_p}$ when only the support condition is meant. Stacking one such row per circuit gives the circuit matrix $\mathbf M'$ of $\mathbf M$ , determined up to nonzero factors on its rows.

A fundamental set of circuits of a matroid $M$ with nullity $n(M)=\rho(M)-r(M)$ ( $\rho$ the number of elements) is a family of circuits $P_1,\dots,P_q$ with $q=n(M)$ such that the elements can be ordered $e_1,\dots,e_n$ with $e_{n-q+i}\in P_i$ and $e_{n-q+j}\notin P_i$ for $j>i$ ; it is strict if $e_{n-q+j}\notin P_i$ for every $j\neq i$ .

The matroid $M'$ of §16 has elements $1,\dots,7$ ; its bases (maximal independent sets) are all three-element sets except

124,\quad 135,\quad 167,\quad 236,\quad 257,\quad 347,\quad 456. \qquad (16.1)

Formalization targets

Goal: §16, pp. 529–530

\exists\,M' \quad\text{and}\quad \forall m\ \forall\,\mathbf M\in\mathbb R^{m\times 7}:\ M' \text{ is not the matroid of } \mathbf M .

The number of rows is arbitrary; the existence clause makes the non-existence statement non-vacuous.

Milestones

§12. Every real matrix has a matroid: the ranks of column submatrices satisfy the rank postulates.
§14, (14.1). Every real matrix has a circuit matrix.
Theorem 29. The rows of a fundamental set of circuits form a base for the rows of the circuit matrix, so $r(\mathbf M')=q=n(\mathbf M)$ .
Lemma 10. The support of a vector in the row space $H$ of a circuit matrix is a union of circuits.
Lemma 11. Two vectors of $H$ with the same circuit as support are proportional.
Theorem 32. For a circuit matrix normalised along a strict fundamental set, a minor $D$ vanishes iff an associated $q\times q$ minor $D'$ vanishes, iff some circuit avoids a prescribed set of columns.
§16, rank of $M'$ . The rank of a $k$ -set is $k$ for $k\le 2$ , $3$ for $k\ge 4$ , and for $k=3$ it is $2$ on (16.1) and $3$ otherwise.
p. 533. $M'$ is the matroid of an explicit $3\times 7$ matrix of integers mod 2.

Significance

The result. The theorem separates the abstract notion of matroid from linear dependence over $\mathbb R$ : some matroids are not real-representable. It also exhibits that representability depends on the field, because the same matroid is the matroid of a matrix over the integers mod 2 (milestone 8). Everything later written about representability over particular fields, excluded-minor characterizations, and the gap between abstract and linear matroids starts from this distinction. Theorem 32 is of independent interest: it translates statements about circuits of a represented matroid into the vanishing of minors of a normalised circuit matrix.

Formalizing it. The result is classical and its proof is short on paper, but it is not formalized in Mathlib, which has matroids (Matroid, circuits, ranks) but no column matroid of a matrix with a rank-of-submatrix characterization, no circuit matrix, and no Fano matroid. The mission produces those objects and the bridge lemmas (Theorem 29, Lemmas 10–11, Theorem 32) that connect matroid circuits with linear algebra of the circuit matrix. No machine-checked proof of the non-representability of the Fano matroid over $\mathbb R$ in Lean is known to the curators.

Difficulty

The obvious attempt is a direct search: suppose a real $m\times 7$ matrix has $M'$ as its matroid and derive a contradiction from the seven dependent triples. This does not work as stated. Each rank condition is a determinantal (nonlinear) condition on the entries, the number of rows $m$ is unbounded, and a representation is determined only up to row operations and column scalings, so there is no finite case check and no single linear computation that settles the question. The contradiction has to come from an argument that is invariant under these symmetries, and the milestones (circuit vectors determined up to scaling, fundamental sets spanning, circuits detected by minors) are what such an argument needs to be stated in. The field also matters: the argument must use that $2\neq 0$ in $\mathbb R$ , since over a field of characteristic 2 the statement is false (milestone 8).

Formalization scope

Elements and matrices. Matroids are Mathlib Matroids whose ground set is the whole (finite) type. The Fano matroid lives on Fin 7, Whitney's element $k$ being k - 1; the seven triples are written out literally. Matrices are Matrix (Fin m) ι K; "the matroid of $\mathbf M$ " means: ground set everything, and the rank M.eRk N of every finite set $N$ of columns equals Matrix.rank of the column submatrix.
Field. The goal and Lemmas 10–11, Theorems 29 and 32 are stated over $\mathbb R$ , as in the paper; the predicate "matroid of a matrix" is stated over any field so that the mod-2 milestone uses the same notion.
Circuit matrix. Rows are determined up to nonzero factors, so "circuit matrix" is a predicate on a matrix together with a bijection between its rows and the circuits; every theorem holds for every such choice.
Nullity and indices. $q=n(M)$ is written $q+r(M)=\rho(M)$ in extended naturals, with no truncated subtraction. In Theorem 32, $n=p+q$ , the complement of $i_1,\dots,i_s$ is given as an order embedding of Fin t with $s+t=q$ , and determinants are of square submatrices in the paper's row and column order.
Ruling out trivial readings. The goal includes the existence of $M'$ ; without it "every matroid with these bases has no real matrix" could hold vacuously. The goal quantifies over every number of rows; fixing $m=3$ would be a weaker statement.

Reusable beyond this mission: the matroid of a matrix over a field, the circuit matrix, fundamental sets of circuits, and the Fano matroid. Contributions welcome: proofs of the milestones, and a proof of the goal by any route, including one that does not go through Theorem 32.

Selected references

H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182
W. T. Tutte, A homotopy theorem for matroids, I, II, Transactions of the American Mathematical Society 88 (1958), 144–174. https://doi.org/10.2307/1993244
J. Oxley, Matroid Theory, 2nd ed., Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001
O. Veblen and J. W. Young, Projective Geometry, Vol. I, Ginn, 1910 (cited by Whitney for the finite projective geometry).

13 thms1 active userReviewed

Combinatorics Operations Research·Captain: mikedeng1

On the Abstract Properties of Linear Dependence 6: Every Matroid Satisfying (C*) Is Represented by a Matrix of Integers Mod 2Research Paper

Motivation

Whitney's 1935 paper introduced matroids as an abstraction of linear dependence among the columns of a matrix. Most of the paper works over the real numbers; its appendix asks which matroids arise from matrices of integers mod 2, that is, matrices with entries 0 and 1 in which rank and dependence are computed over the two-element field. These are today's binary matroids. They include the cycle matroids of graphs (Whitney closes the paper by noting that graphs correspond to mod-2 matrices with exactly two ones in each column) and they are the setting of several later structure theorems: Tutte's excluded-minor characterization of binary matroids (Tutte 1958), Seymour's decomposition of regular matroids (Seymour 1980) and Seymour's theory of binary clutters and max-flow min-cut (Seymour 1977), which underlies parts of combinatorial optimization.

Whitney's answer is an intrinsic postulate, (C*), on the circuits of the matroid, stated without reference to any matrix, and a constructive representation theorem (Theorem 37): a matroid satisfying (C*) is the matroid of a mod-2 matrix, and the matrix is unique once the columns of one base are fixed.

Setting

A matroid $M$ on elements $e_1, \dots, e_n$ is given by its independent sets; its circuits are its minimal dependent sets, its rank $r(M)$ is the size of a base, and its nullity is $n(M) = n - r(M)$ . Here $M$ is a Mathlib Matroid (Fin n) whose ground set is all of Fin n.

Subsets of the elements are added mod 2: a sum of finitely many sets is the set of elements lying in an odd number of them (for two sets, the symmetric difference). A cycle is a sum mod 2 of circuits; the empty sum is the null cycle $\emptyset$ . A set is a true sum of sets that have no common elements and whose union it is. Postulate (C*) requires that each cycle be a true sum of circuits.

With $n = r + q$ , a family $P_1, \dots, P_q$ is a strict fundamental set of circuits with respect to $e_{n-q+1}, \dots, e_n$ if $q = n(M)$ , each $P_i$ is a circuit, and $P_i$ contains $e_{n-q+i}$ but no other $e_{n-q+j}$ .

For a matrix $\mathbf M$ over the integers mod 2 with columns $C_1, \dots, C_n$ , columns are independent (mod 2) if no non-null subset of them sums to the zero column. The matroid corresponding to $\mathbf M$ has the column indices as elements and these independent sets.

Formalization targets

Goal: Theorem 37 (p. 533)

Let $M$ satisfy (C*), with elements $e_1, \dots, e_n$ and base $\{e_1, \dots, e_{n-q}\}$ . For every matrix $\mathbf M_1$ mod 2 (any number of rows) whose $n - q$ columns are independent mod 2,

\exists!\ \mathbf M = (\mathbf M_1 \mid C_{n-q+1} \cdots C_n) \ \text{ whose corresponding matroid is } M.

Milestones

Theorem 9 (p. 517): if $e_1, \dots, e_{n-q}$ is a base, there is a unique strict fundamental set of circuits with respect to $e_{n-q+1}, \dots, e_n$ .
Appendix, p. 531: (C*) implies the circuit postulate (C₂), for any family of sets.
Theorem 33: under (C*), the circuits are exactly the minimal non-null cycles.
Theorem 34: under (C*), the cycles are exactly the $2^q$ sums mod 2 of a strict fundamental set.
Theorem 35: two (C*)-matroids with a common strict fundamental set have the same circuits.
Theorem 36: any $P_1, \dots, P_q$ with $e_{n-q+i} \in P_i \subseteq \{e_1, \dots, e_{n-q}, e_{n-q+i}\}$ is the strict fundamental set of exactly one (C*)-matroid.
Appendix, p. 532: the matroid of a matrix mod 2 exists, satisfies (C*), and its cycles are the supports of the mod-2 dependencies among the columns.

Milestone 7 and the goal together characterize binary matroids as the matroids satisfying (C*).

Significance

The result. Theorem 37 and the p. 532 claim give an intrinsic, matrix-free description of the matroids representable over the two-element field, and Theorem 36 parametrizes all of them by $q$ arbitrary subsets of a base. Uniqueness in Theorem 37 says that a binary representation is determined by the columns of one base; in modern terms, binary matroids are uniquely representable over GF(2) up to row operations. Every later theory of binary matroids, including graphic and cographic matroids, Tutte's excluded-minor theorem and Seymour's decomposition, starts from this equivalence.

Formalizing it. The results are proved in the paper and in textbooks (e.g. Oxley, Matroid Theory, Ch. 9) but, at the Mathlib revision used here, there is no notion of a matroid represented by a matrix over a field, and no binary-matroid theory. On Prove2Me, the existing binary objects (SeymourMFMC.Binary.*) are binary clutters defined through blockers, not matroids represented by mod-2 matrices. This mission produces the representation predicate for mod-2 matrices, the cycle space of a matroid, and the equivalence between (C*) and binary representability.

Difficulty

Writing down candidate columns is not the hard part; showing that the matroid of the completed matrix is $M$ itself, and not merely a matroid sharing some of its circuits, is. Whitney's example at the end of §9 exhibits two different matroids with a common strict fundamental set, so agreement on fundamental circuits does not by itself identify a matroid; any argument must use (C*) on both the given matroid and the matroid of the matrix. A naive comparison of independent sets column by column does not close this gap. Uniqueness likewise depends on the independence mod 2 of the prescribed columns: without it, different completions can give the same matroid.

Formalization scope

Matroids are Mathlib Matroid (Fin (r + q)) with ground set Set.univ; Whitney's $e_k$ is k - 1, his $e_1, \dots, e_{n-q}$ is the range of Fin.castAdd q, and $e_{n-q+i}$ is Fin.natAdd r (i - 1). Writing $n = r + q$ removes natural-number subtraction; $q$ is not a free parameter, since $\{e_1, \dots, e_r\}$ is required to be a base.
Sums mod 2 count parity of membership (sumMod2); cycles are sums over finite sets of circuits; true sums are unions over finite pairwise-disjoint sets of circuits; (C*) is SatisfiesCStar on the circuit family {C | M.IsCircuit C}. These definitions take the circuit family as a parameter, so that the (C₂) milestone is posed for an arbitrary family of sets, as Whitney poses it.
A strict fundamental set includes the nullity condition $r(M) + q = \rho(M)$ , stated in $\mathbb N_\infty$ .
Matrices are Matrix (Fin m) (Fin n) (ZMod 2) with any $m$ ; independence mod 2 of columns is LinearIndepOn (ZMod 2) of the columns (the rows of the transpose). IsMatroidOf M A compares all independent sets, not only bases.
Ruled out: the goal is not satisfied by any statement that compares only the bases of one size, by an existence-only statement without uniqueness, or by real (instead of mod-2) independence.
Tacit hypotheses made explicit: the matroid's ground set is exactly $e_1, \dots, e_n$ ( $\rho(M) = n$ ); the elements and matroids are finite.

Contributions welcome: the general fact that the matroid of a vector family over a field exists (a reusable Matroid.ofFun-style construction over any field), the cycle-space lemmas, and proofs of the milestones in any order.

Selected references

H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182
W. T. Tutte, A homotopy theorem for matroids, I, II, Transactions of the AMS 88 (1958), 144–174. https://doi.org/10.2307/1993244
P. D. Seymour, The matroids with the max-flow min-cut property, Journal of Combinatorial Theory Ser. B 23 (1977), 189–222. https://doi.org/10.1016/0095-8956(77)90031-4
P. D. Seymour, Decomposition of regular matroids, Journal of Combinatorial Theory Ser. B 28 (1980), 305–359. https://doi.org/10.1016/0095-8956(80)90075-1
J. Oxley, Matroid Theory, 2nd ed., Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001

11 thms1 active userReviewed

Numerical Analysis Optimization·Captain: mikedeng1

Projection-like Retractions on Matrix Manifolds IV: Within σ_r(X̄)/2 of a Rank-r Matrix, the Truncated SVD Is the Unique Nearest Matrix of Rank Exactly rResearch Paper

Motivation

Optimization over sets of matrices of fixed rank comes up in low-rank matrix completion, model reduction, and the low-rank approximation of solutions of large matrix equations. A standard approach treats the constraint set as a Riemannian manifold and runs gradient or Newton-type methods on it (Absil, Mahony & Sepulchre 2008). Each iteration takes a step in the tangent space and then has to return to the manifold. A map that does this to first order is called a retraction, and its cost is often what decides whether a manifold method is practical.

Absil and Malick (2012) study retractions defined by projection: step to $X+Z$ in the ambient space, then take the nearest point of the manifold. Their Proposition 3.2 shows that for any $C^k$ submanifold ( $k\ge2$ ) this projective retraction is a retraction. Section 3.2 makes it explicit for the manifold of fixed-rank matrices: near any matrix of rank $r$ , the nearest matrix of rank exactly $r$ is the truncated singular value decomposition (Proposition 3.3). Section 4.4 also gives a closed form for a second retraction on the same manifold, the orthographic retraction (Proposition 4.11).

Setting

Fix natural numbers $n$ , $m$ and $r\ge1$ . The space $\mathbb R^{n\times m}$ of real $n\times m$ matrices carries the Frobenius norm $\|X\|^2=\sum_{i,j}X_{ij}^2=\operatorname{trace}(X^\top X)$ (3.6). The fixed-rank set is

\mathcal R_r=\{X\in\mathbb R^{n\times m}:\ \operatorname{rank}(X)=r\},

a smooth submanifold of $\mathbb R^{n\times m}$ . It is not closed: its closure is the set of matrices of rank at most $r$ .

A singular value decomposition (3.5) of $X$ is a factorization $X=U\Sigma V^\top$ in which $U=[u_1,\dots,u_n]\in\mathbb R^{n\times n}$ and $V=[v_1,\dots,v_m]\in\mathbb R^{m\times m}$ are orthogonal and $\Sigma\in\mathbb R^{n\times m}$ is zero off its diagonal. The diagonal of $\Sigma$ holds the singular values of $X$ in nonincreasing order,

\sigma_1(X)\ge\sigma_2(X)\ge\cdots\ge\sigma_{\min\{n,m\}}(X)\ge0,

and $\sigma_i(X)=0$ for $i>\min\{n,m\}$ . A matrix has rank $r$ exactly when $\sigma_r(X)>0=\sigma_{r+1}(X)$ . The truncated SVD of rank $r$ is $\hat X=\sum_{i=1}^r\sigma_i(X)u_iv_i^\top$ (3.7).

For a set $Q$ and a point $X$ , the projection $P_Q(X)$ is the set of nearest points: the $Y\in Q$ with $\|X-Y\|\le\|X-W\|$ for all $W\in Q$ . For a set that is not closed, $P_Q(X)$ may be empty or contain several points.

Formalization targets

Goal: Proposition 3.3

Let $\bar X\in\mathcal R_r$ . For every $X$ with $\|X-\bar X\|<\sigma_r(\bar X)/2$ and every singular value decomposition $X=U\Sigma V^\top$ ,

P_{\mathcal R_r}(X)=\Bigl\{\sum_{i=1}^r\sigma_i(X)\,u_iv_i^\top\Bigr\}.

The projection exists, is unique, and is the truncated SVD. The radius $\sigma_r(\bar X)/2$ and the strict inequality are those of the paper.

Milestones

The paper's proof goes through four claims, which are the milestones in attack order:

Weyl's bound (§3.2, proof of Proposition 3.3, citing Horn–Johnson 7.3.8): $|\sigma_i(\bar X)-\sigma_i(X)|\le\|X-\bar X\|$ for every $i\ge1$ .
Eckart–Young (3.7): for every singular value decomposition of $X$ , $\hat X$ is a nearest matrix to $X$ of rank at most $r$ .
The gap (3.8): if $\operatorname{rank}\bar X=r$ and $\|X-\bar X\|<\sigma_r(\bar X)/2$ , then $\sigma_{r+1}(X)<\sigma_r(\bar X)/2<\sigma_r(X)$ .
Uniqueness under a gap (§3.2, proof of Proposition 3.3, citing Helmke–Moore): if $\sigma_r(X)>\sigma_{r+1}(X)$ , then $\hat X$ is the only nearest matrix of rank at most $r$ .

Further result: Proposition 4.11

Write $X=U\left[\begin{smallmatrix}\Sigma_0&0\\0&0\end{smallmatrix}\right]V^\top$ (4.7), with $\Sigma_0$ the positive diagonal of nonzero singular values, and a tangent vector $Z=U\left[\begin{smallmatrix}A&C\\B&0\end{smallmatrix}\right]V^\top$ (4.8). If $\Sigma_0+A$ is invertible, the orthographic retraction is

R(X,Z)=U\begin{bmatrix}\Sigma_0+A&C\\B&B(\Sigma_0+A)^{-1}C\end{bmatrix}V^\top .

Here $R(X,Z)$ is the nearest point to $X+Z$ of $\mathcal R_r\cap(X+Z+N_{\mathcal R_r}(X))$ .

Significance

The result. Proposition 3.3 reduces the projective retraction on $\mathcal R_r$ to one truncated singular value decomposition. With Proposition 3.2 this gives an explicit, computable retraction for Riemannian optimization on fixed-rank matrices. It is used, for instance, in low-rank matrix completion algorithms. The point is local: $\mathcal R_r$ is not closed, so far from $\mathcal R_r$ the nearest matrix of rank exactly $r$ need not exist, and the proposition gives an explicit radius on which it does exist and is unique. Proposition 4.11 gives a second retraction that needs only products of matrices and one $r\times r$ inverse.

Formalizing it. All results here are proved, on paper. To the best of a search of Mathlib and the Prove2Me catalog, none is machine-checked. Mathlib has singular values of linear maps between finite-dimensional inner product spaces (LinearMap.singularValues), but no singular value decomposition in matrix form, no Weyl perturbation inequality for singular values, and no Eckart–Young theorem. A complete development would add these, and the Eckart–Young theorem with its uniqueness case is a standard result of numerical linear algebra in its own right.

Difficulty

The proof in the paper is short only because it cites three facts, and each of them is a real piece of matrix analysis.

Weyl's bound needs the variational (min–max) description of singular values, which Mathlib does not have for singular values.
Eckart–Young requires comparing $\|X-Y\|$ with the singular values of $X$ for every $Y$ of rank at most $r$ , not only for those diagonal in the same bases. The obvious approach, writing $Y$ in the singular bases of $X$ , fails because $Y$ need not be diagonal there.
Uniqueness under the gap requires showing that every minimizer is diagonal in some singular bases of $X$ and then using the gap to fix its support. Without the gap uniqueness fails: for $X=I_2$ and $r=1$ every $uu^\top$ with $\|u\|=1$ is a nearest point.

A further subtlety: Proposition 3.3 must hold for any singular value decomposition of $X$ . Singular vectors are not unique, so the proof has to show that the truncation does not depend on the choice under the gap (3.8).

Formalization scope

Matrices are Matrix (Fin n) (Fin m) ℝ with Mathlib's Frobenius norm (open scoped Matrix.Norms.Frobenius). The projection is the published platform predicate RandomGradFree.Nonsmooth.IsMetricProjection, and $P_{\mathcal R_r}(X)$ is the set {Y | IsMetricProjection (rankSet r) X Y}. The set equality with a singleton states existence, uniqueness and the formula together.

Conventions committed to:

sv X i is $\sigma_i(X)$ , 1-based as on the page. It is Mathlib's 0-based singularValues of Matrix.toEuclideanLin X at i - 1, so the index $0$ is meaningless and every statement uses indices $\ge1$ .
IsSVD X U S V is the predicate of (3.5). The singular value decomposition is a hypothesis of the theorems, never a choice made inside them, so the theorems hold for every singular value decomposition.
truncSVD r U S V is $\sum_{i\le r}\Sigma_{ii}u_iv_i^\top$ , written with the diagonal of S. That these entries are the singular values $\sigma_i(X)$ is a fact to be proved, not part of the definition.
The hypothesis $r\ge1$ is added, because $\sigma_r$ needs it (and $\mathcal R_0=\{0\}$ ). It is the only hypothesis of Proposition 3.3 not printed on the page.
In Proposition 4.11, matrices use the block index types Fin r ⊕ Fin p and Fin r ⊕ Fin q. The tangent vector and the normal space are taken in the form the page gives, and invertibility of $\Sigma_0+A$ is an explicit hypothesis. In the paper's proof it comes from " $Z$ in a neighborhood of the origin".

A formalization in which the radius is replaced by a smaller one, the projection is taken onto the matrices of rank at most $r$ , or the singular value decomposition is chosen inside the statement is a different theorem and is ruled out.

Wanted contributions, all reusable beyond this mission:

existence of a singular value decomposition in matrix form, and the identification of its diagonal with singularValues;
Weyl's inequality for singular values;
the Eckart–Young theorem and its uniqueness case;
the Schur-complement rank formula for $2\times2$ block matrices, used for Proposition 4.11.

Selected references

P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds, SIAM J. Optim. 22(1):135–158, 2012. https://doi.org/10.1137/100802529 (authors' version HAL hal-00651608v2: https://hal.science/hal-00651608v2)
P.-A. Absil, R. Mahony and R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://press.princeton.edu/absil
C. Eckart and G. Young, The approximation of one matrix by another of lower rank, Psychometrika 1(3):211–218, 1936. https://doi.org/10.1007/BF02288367
R. A. Horn and C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985 (§7.3, §7.4). https://doi.org/10.1017/CBO9780511810817
U. Helmke and J. B. Moore, Optimization and Dynamical Systems, Springer, 1994 (Ch. 5). https://doi.org/10.1007/978-1-4471-3467-1

8 thms1 active userReviewed

Differential Geometry Optimization·Captain: mikedeng1

Projection-like Retractions on Matrix Manifolds III: Near a Locally Symmetric Point, the Projection onto a Spectral Manifold Is U Diag(P_M(λ(X))) UᵀResearch Paper

Motivation

Riemannian optimization algorithms move along a manifold by taking a step in a tangent direction and then coming back to the manifold. The map that does the coming back is a retraction, and the most natural candidate on a submanifold of a Euclidean space is the projective retraction: add the tangent step, then take the nearest point of the manifold. Its practical value depends on whether that nearest point can be computed.

For many manifolds of symmetric matrices the defining property is a property of the eigenvalues: matrices whose largest eigenvalue has multiplicity $p$ , matrices with prescribed spectrum, and similar sets that arise in eigenvalue optimization and in alternating projection methods (Lewis and Malick 2008). Daniilidis, Malick and Sendov (reference [8] of the paper) showed that such a spectral set is a smooth manifold when the underlying set of eigenvalue vectors is a smooth, locally symmetric manifold. P.-A. Absil and J. Malick (SIAM J. Optim. 2012; authors' version hal-00651608v2) then showed that, close to such a manifold, the metric projection onto it has a closed form: one eigendecomposition and one projection in $\mathbb R^n$ . This mission formalizes that result, Theorem 3.9 of the paper.

Setting

Write $\mathbf S_n$ for the real symmetric $n \times n$ matrices with the Frobenius norm $\|X\|^2 = \sum_{i,j} X_{ij}^2$ , $\mathbf O_n$ for the orthogonal matrices, and $\mathbf \Sigma_n$ for the permutation matrices, which act on $\mathbb R^n$ (with the Euclidean norm) by permuting coordinates. Let

\mathbb R^n_\downarrow = \{x \in \mathbb R^n : x_1 \ge x_2 \ge \cdots \ge x_n\}.

For $X \in \mathbf S_n$ , $\lambda(X) \in \mathbb R^n_\downarrow$ is the vector of its eigenvalues, with multiplicity, in nonincreasing order; every $X$ has an eigendecomposition $X = U \operatorname{Diag}(\lambda(X)) U^\top$ with $U \in \mathbf O_n$ . For $M \subseteq \mathbb R^n$ the spectral set of $M$ is

\lambda^{-1}(M) = \{X \in \mathbf S_n : \lambda(X) \in M\}.

For a set $Q$ and a point $y$ , $P_Q(y)$ is the set of nearest points of $Q$ to $y$ (it may be empty or contain several points).

Let $\mathcal M$ be a $C^2$ submanifold of $\mathbb R^n$ : around each of its points it is a coordinate slice of a $C^2$ chart with $C^2$ inverse. Let $\mathcal S = \lambda^{-1}(\mathcal M \cap \mathbb R^n_\downarrow)$ , let $\bar X \in \mathcal S$ and $\bar x = \lambda(\bar X)$ . The set $\mathcal M \cap B(\bar x, \delta)$ (open ball) is strongly locally symmetric if for every $x \in \mathcal M \cap B(\bar x, \delta)$ and every $P \in \mathbf \Sigma_n$ with $Px = x$ ,

P\big(\mathcal M \cap B(\bar x, \delta)\big) = \mathcal M \cap B(\bar x, \delta). \qquad (3.15)

Formalization targets

Goal: Theorem 3.9 (projection onto spectral manifolds)

Assume $\mathcal M$ is a $C^2$ submanifold of $\mathbb R^n$ , $\bar X \in \mathcal S$ , $\delta > 0$ and (3.15). Then there is $\delta_0 \in (0, \delta]$ such that for every $X \in \mathbf S_n$ with $\|X - \bar X\| \le \delta_0/2$ , the set $P_{\mathcal M}(\lambda(X))$ is a single point $p$ , and for every $U \in \mathbf O_n$ with $X = U \operatorname{Diag}(\lambda(X)) U^\top$ ,

P_{\mathcal S}(X) = \{\, U \operatorname{Diag}(p)\, U^\top \,\}.

The goal fixes no constant: $\delta_0$ is only asserted to exist, as the paper's proof restricts $\delta$ to make the local uniqueness of $P_{\mathcal M}$ and Lemma 3.8 apply.

Milestones

(3.11): $\|\lambda(X) - \lambda(Y)\| \le \|X - Y\|$ for $X, Y \in \mathbf S_n$ .
Lemma 3.7: for closed $M \subseteq \mathbb R^n_\downarrow$ , an eigendecomposition $X = U\operatorname{Diag}(\lambda(X))U^\top$ and sorted $z$ , $U \operatorname{Diag}(z) U^\top \in P_{\lambda^{-1}(M)}(X) \iff z \in P_M(\lambda(X))$ .
Lemma 3.8: for $\bar x \in \mathbb R^n_\downarrow$ and all small $\delta > 0$ , for $y \in B(\bar x, \delta)$ and sorted $x \in B(\bar x, \delta)$ , the maximum of $x^\top P y$ over permutations fixing $\bar x$ is attained at some $P$ with $Py$ sorted.
(3.20): under (3.15) and for small $\delta$ , the distance from a sorted $x \in B(\bar x, \delta)$ to $\mathcal M \cap B(\bar x, \delta)$ is attained up to equality on sorted points.

Significance

The theorem turns the projective retraction on a spectral manifold, an optimization problem over $n \times n$ matrices, into a projection in $\mathbb R^n$ onto $\mathcal M$ plus one eigendecomposition. For the matrices whose largest eigenvalue has multiplicity $p$ , the projection onto $\mathcal M_p$ is an explicit averaging of the top $p$ eigenvalues (Example 3.10 of the paper), which completes a partial result of Oustry (reference [29, Th. 13] of the paper). Together with Theorem 3.5, it is what makes the projective retraction a practical alternative on manifolds where the Riemannian exponential has no known efficient formula.

The result is proved in the paper; to our knowledge none of it is formalized. The mission produces a machine-checked version of the theorem and of the spectral-set toolkit beneath it: the Lipschitz property of sorted eigenvalues, the reduction of projections onto spectral sets to projections onto sets of vectors, and the permutation rearrangement lemma. The formalization also corrects a misstatement: Lemma 3.7 as printed quantifies over all $z \in \mathbb R^n$ , and its direction " $\Rightarrow$ " fails for unsorted $z$ (for $n = 2$ , $M = \{(2, 0)\}$ , $X = U = I$ , $z = (0, 2)$ ). The mission states it for $z \in \mathbb R^n_\downarrow$ , which is the only case Theorem 3.9 uses.

Difficulty

The obvious argument shows only half of the goal. Lemma 3.7 characterizes the nearest points of $\mathcal S$ that share the eigenvectors $U$ of $X$ ; it does not exclude a nearest point with other eigenvectors, and the goal asserts that $P_{\mathcal S}(X)$ is a single point. Excluding the others needs the equality case of the trace inequality $\operatorname{trace}(XY) \le \lambda(X)^\top \lambda(Y)$ (3.10), which the paper quotes from the literature without proof, and the fact that the projection $p$ inherits the ties of $\lambda(X)$ , which comes from strong local symmetry and uniqueness of $P_{\mathcal M}$ .

The local uniqueness of $P_{\mathcal M}$ near a point of a $C^2$ submanifold (Lemma 3.1 of the paper) is itself a tubular-neighbourhood argument through the inverse function theorem. Mathlib has no metric projection onto embedded submanifolds, no von Neumann trace inequality for sorted eigenvalues, and no Hoffman–Wielandt inequality. Finally, the radii interact: the restriction $\delta_0$ must make Lemma 3.1, Lemma 3.8 and the ball inclusion $P_{\mathcal M}(x) \in B(\bar x, \delta)$ all hold at once.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n), with the Euclidean norm (not the sup norm of Fin n → ℝ). Matrices are Matrix (Fin n) (Fin n) ℝ with Mathlib's Frobenius norm (open scoped Matrix.Norms.Frobenius); $\mathbf S_n$ is IsHermitian (symmetry over $\mathbb R$ ) and $\mathbf O_n$ is Matrix.orthogonalGroup.
$\lambda(X)$ is eig X, built from Mathlib's sorted IsHermitian.eigenvalues₀; on a non-symmetric matrix it returns $0$ , and every statement assumes symmetry. $\mathbb R^n_\downarrow$ is sortedDesc n, spectral sets are specSet, permutations act by permAct (an isometry), and (3.15) is IsStronglyLocallySymmetric on the open ball.
Nearest points are the platform predicate RandomGradFree.Nonsmooth.IsMetricProjection; $P_Q(y)$ is {z | IsMetricProjection Q y z}.
The submanifold hypothesis is a local slice-chart predicate IsSubmanifold 2 d M. The paper allows $k = 2$ or $\infty$ ; $k = 2$ covers both. Only the hypotheses of Theorem 3.5 (cited from Daniilidis–Malick–Sendov without proof) are assumed, not its conclusion that $\mathcal S$ is a manifold.
"For $\delta$ small enough" is $\exists \delta_1 > 0, \forall \delta \in (0, \delta_1]$ ; the radius of Theorem 3.9 is an existential $\delta_0 \le \delta$ , with the paper's non-strict $\|X - \bar X\| \le \delta_0/2$ .
Both singleton claims of Theorem 3.9 are part of the conclusion. A version proving only $\subseteq$ would be satisfied by the empty set, and a version that assumes $P_{\mathcal M}(\lambda(X))$ is a singleton would delete the theorem's local-uniqueness content; neither is the target.

Infrastructure that a full development needs and that is reusable beyond this mission: the von Neumann/Fan trace inequality and its equality case for real symmetric matrices, the Hoffman–Wielandt inequality (3.11), the rearrangement inequality over permutations fixing a vector, and the local existence and uniqueness of metric projections onto $C^2$ submanifolds. Useful platform items: RHLinalg.vonNeumann_trace_ineq (the trace inequality for Hermitian matrices), RHLinalg.bilinear_doublyStochastic_le_of_monovary (the rearrangement step), and Bhatia.trace_mul_perm_bounds (trace pairings between permutation pairings of unsorted spectra). Contributions of these lemmas, of alternative proofs of (3.11), and of the equality case of (3.10) are welcome.

Selected references

P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds, SIAM J. Optim. 22(1):135–158, 2012. https://doi.org/10.1137/100802529; authors' version https://hal.science/hal-00651608v2
A. Daniilidis, J. Malick and H. Sendov, Locally symmetric submanifolds lift up to spectral manifolds, preprint, 2009 (reference [8] of the paper; the source of Theorem 3.5).
A. S. Lewis and J. Malick, Alternating projections on manifolds, Math. Oper. Res. 33(1):216–234, 2008. https://doi.org/10.1287/moor.1070.0291
F. Oustry, A second-order bundle method to minimize the maximum eigenvalue function, Math. Program. 89:1–34, 2000 (reference [29] of the paper).
A. S. Lewis, Convex analysis on the Hermitian matrices, SIAM J. Optim. 6(1):164–177, 1996. https://doi.org/10.1137/0806009

8 thms1 active userReviewed

Control Theory Dynamic Programming Markov Chain+2·Captain: mikedeng1

Bellman's Dynamic Programming IX: Markovian Decision Processes and the Maximal Perron RootTextbook

Motivation

Chapter XI of Richard Bellman's Dynamic Programming (Princeton University Press, 1957; DOI 10.2307/j.ctv1nxcw0f) studies decision processes whose state is a vector of nonnegative quantities, for example the probabilities that a system is in each of $N$ states, or the stocks of $N$ commodities, and whose transitions are linear maps chosen stage by stage by a controller. Maximizing a linear functional of the state at every stage leads to the nonlinear difference equation

x_i(n+1) = \max_q \sum_{j=1}^N a_{ij}(q)\, x_j(n), \qquad x_i(0) = c_i,

and, in the limit of small time steps, to differential equations of the form $dx/dt = \max_q [A(q,t)x + b(q,t)]$ and, when two opposing controllers act, $dx/dt = \max_p \min_q[\dots]$ .

These equations are the multiplicative counterpart of the additive Bellman equation. Their growth rate is the natural object for controlled population models, controlled Markov chains observed through their unnormalized state vectors, and economic growth models with a choice of technology. Bellman announced the discrete results in "A Markovian decision process" (J. Math. Mech. 6, 1957) the same year as the book, and R. A. Howard's Dynamic Programming and Markov Processes (MIT Press, 1960) developed policy iteration for the related average-reward problem. The central discrete result of the chapter, Theorem 2, is an early instance of what is now called nonlinear Perron–Frobenius theory (Lemmens and Nussbaum, 2012).

Setting

Fix $N \ge 1$ . Row $i$ of the matrix carries its own control $q_i$ , ranging over a set $S_i$ ; the joint control is $q = (q_1, \dots, q_N)$ in $S = S_1 \times \dots \times S_N$ , and $A(q) = (a_{ij}(q_i))$ . Bellman insists on this row-wise structure (§ 3): "the set of q's for each row is distinct from the corresponding set for any other row ... so that there is no interaction between the various maximizations". The maximum of a vector over $q$ is then taken row by row.

The Perron root $\varphi(q)$ is the characteristic root of $A(q)$ of largest absolute value, the spectral radius of $A(q)$ as a complex matrix. The conditions (10.3) of the chapter are:

for every $y$ and every row the maximum of $\sum_j a_{ij}(q_i) y_j$ over $S_i$ is attained;
$0 < a_{ij}(q) \le m < \infty$ on $S$ ;
$\varphi$ attains its maximum on $S$ .

For the continuous processes, $\|x\| = \sum_i |x_i|$ and $\|A\| = \sum_{i,j}|a_{ij}|$ , and a solution of $dx/dt = F(t,x)$ , $x(0)=c$ , on $[0,T]$ is a continuous $x$ with $x(t) = c + \int_0^t F(s, x(s))\,ds$ , which is the book's "satisfying the equation almost everywhere". The successive approximations are $x_0 = c$ , $x_{n+1}(t) = c + \int_0^t F(s, x_n(s))\,ds$ .

Formalization targets

Goal: Chapter XI, Theorem 2

Under (10.3) there is exactly one $\lambda > 0$ for which

\lambda y_i = \max_q \sum_{j=1}^N a_{ij}(q)\, y_j, \qquad i = 1,\dots,N,

has a solution with all $y_i > 0$ . That solution is unique up to a positive factor, and

\lambda = \max_{q \in S} \varphi(q).

Milestones

§ 4, Lemma. For row-wise maximized operators $T_1(x) = \max_q[b_1(q,t) + \int_0^t A(q,s)x\,ds]$ and $T_2(y)$ likewise, $\|T_1(x) - T_2(y)\| \le \max_q[\|b_1 - b_2\| + \int_0^t \|A(q,s)\|\,\|x-y\|\,ds]$ .
Theorem 1. If $\|A(q,t)\|, \|b(q,t)\| \le f(t)$ with $f$ locally integrable and the maximum is attained, then $dx/dt = \max_q[A(q,t)x + b(q,t)]$ , $x(0) = c$ , has a unique solution, the uniform limit of the successive approximations.
Theorem 3 (corrected). If moreover $\varphi$ has a unique maximizer on $S$ and $c \ge 0$ , $c \ne 0$ , then the recurrence satisfies $x_i(n) \sim a\,y_i\,\lambda^n$ with $a = a(c) > 0$ .
Theorem 4. The same well-posedness for $dx/dt = \max_p\min_q[A(p,q,t)x + b(p,q,t)] = \min_q\max_p[\dots]$ on $[0,T]$ .
Theorem 5. If $(Bp,q) \ge d > 0$ on probability vectors, the solution of $du/dt = \max_p\min_q[(Ap,q) - (Bp,q)u]$ satisfies

\lim_{t\to\infty} u(t) = \max_p \min_q \frac{(Ap,q)}{(Bp,q)} = \min_q \max_p \frac{(Ap,q)}{(Bp,q)} .

Significance

Theorem 2 identifies the optimal long-run growth rate of a controlled multiplicative process with the largest Perron root among the admissible matrices, and shows that the optimal process has a single positive stationary direction. Theorem 3 turns this into the asymptotics of the value iteration $x(n+1) = \max_q A(q)x(n)$ : after normalization by $\lambda^n$ the iterates converge to a multiple of the eigenvector. Theorems 1 and 4 are the existence and uniqueness results that justify defining continuous-time controlled processes and differential games by these equations. Theorem 5 recovers the min-max theorem for ratios of bilinear forms (Chapter X) as the long-run limit of a scalar differential game.

The results are classical, and none of them is formalized. Mathlib has the spectral radius and irreducible matrices but no Perron–Frobenius theorem and no Brouwer fixed point theorem; the platform has a statement of the Perron theorem for a single positive matrix (ClassicalGaps.perron_positive_matrix). A formal proof of the goal therefore also produces a reusable monotone, positively homogeneous eigenvector theorem on the positive orthant.

Difficulty

The map $y \mapsto \max_q A(q)y$ is not linear, so the linear-algebra proof of the Perron theorem through the characteristic polynomial does not apply. Existence of a positive eigenvector needs a fixed point argument for a nonlinear map of the simplex (Bellman uses Brouwer's theorem). The identification $\lambda = \max_q \varphi(q)$ must connect the nonlinear eigenvalue with the spectra of the individual matrices, which requires the Perron theory of each $A(q)$ , including the fact that the Perron root dominates every complex eigenvalue in modulus. For Theorem 3, the iterates may switch controls infinitely often when $S$ is infinite, so an argument that the optimal control is eventually constant does not settle convergence. For Theorems 1 and 4, the right-hand side is only measurable in $t$ and Lipschitz in $x$ with an integrable constant, so the classical Picard–Lindelöf theorem with a continuous right-hand side does not apply directly.

Formalization scope

Everything lives in the namespace BellmanDP.Markovian. Vectors are Fin N → ℝ and matrices are Matrix (Fin N) (Fin N) ℝ. Row $i$ 's control type is Q i with admissible set S i, and the joint admissible set is Set.pi Set.univ S. The Perron root is (spectralRadius ℂ (A.map (algebraMap ℝ ℂ))).toReal, the largest modulus of a complex eigenvalue; it is not defined as a positive eigenvalue with a positive eigenvector, which would make the Perron–Frobenius content of the goal definitional. The maximized eigen-equation is stated with IsGreatest, so the maxima are attained. The goal and Theorem 3 assume $N \ge 1$ ; for $N = 0$ every $\lambda$ would qualify.

Conventions and repairs:

Theorem 3 prints "a unique q for which the maximum value of q is assumed". A control has no maximum value; the proof uses " $q^*$ ... the value of $q$ for which $\lambda = \varphi(q^*)$ ", so the hypothesis is uniqueness of the maximizer of $\varphi$ . For $c = 0$ the iterates vanish and $x_i(n) \sim a y_i\lambda^n$ fails, so $c \ne 0$ is assumed (the proof takes $c > 0$ "without loss of generality"). The asymptotic is stated as $x_i(n)/\lambda^n \to a y_i$ with $a > 0$ .
Theorems 1 and 4: the book's controls are functions of $t$ with the maximum outside the integral; since the maximization is pointwise (§ 4), the statements use pointwise sets and the integral of the pointwise maximum. Measurability of $t \mapsto F(t,x)$ is not stated in the book and is assumed. In Theorem 4 the max-min is taken row by row, and (2a) is encoded as the existence of a saddle point in each row.
§ 4 Lemma: " $\le \max_q[\dots]$ " is stated as " $\le [\dots]$ at some admissible joint $q$ ".
Theorem 5: the right-hand side is the max-min form; the equality of the two ratio values is part of the conclusion.

Degenerate readings are ruled out: the maxima are attained or taken over nonempty compact sets, never Lean's junk sSup of an unbounded set, and the Perron root is spectral rather than defined through the conclusion. Contributions welcome: a proof of the single-matrix Perron theorem in the form needed here, a Brouwer or Kakutani fixed point theorem for the simplex, and a Carathéodory existence theorem for $dx/dt = F(t,x)$ with an integrable Lipschitz constant, each reusable well beyond this mission.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter XI. https://doi.org/10.2307/j.ctv1nxcw0f
R. Bellman, "A Markovian decision process", Journal of Mathematics and Mechanics 6 (1957), 679–684.
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
O. Perron, "Zur Theorie der Matrices", Mathematische Annalen 64 (1907), 248–263. https://doi.org/10.1007/BF01449896
B. Lemmens and R. Nussbaum, Nonlinear Perron–Frobenius Theory, Cambridge University Press, 2012. https://doi.org/10.1017/CBO9781139026079

9 thms1 active userReviewed

Completed

Machine Learning Probability·Captain: Minghui

Fine-Tuning Can Distort Pretrained Features: Perfect-Feature LP-FT SeparationResearch Paper

Why initialization matters for transfer learning

Transfer learning starts with a representation learned on an earlier task and adapts it to a new one. Two common choices are linear probing, which changes only the final linear predictor, and fine-tuning, which changes the representation as well. These procedures optimize related training objectives, but their behavior away from the training data can differ. Kumar and coauthors study this distinction through two-layer linear networks, alongside experiments with nonlinear networks. This mission formalizes their perfect-feature LP-FT result, rather than the empirical claims or the general imperfect-feature comparison. See Section 3.4, Proposition 3.7, PDF p. 10.

LP-FT first learns a head by linear probing and then uses that head to initialize full fine-tuning. The perfect-feature setting isolates the effect of head initialization: the representation already contains exactly the features needed to predict the labels, but the head initially need not use them correctly. The mathematical question is whether joint training preserves or loses the representation's ability to predict outside the observed training subspace.

Linear predictors, training data, and OOD loss

An input is a vector $x\in\mathbb R^d$ . A feature extractor is a matrix $B\in\mathbb R^{k\times d}$ , and a head is a vector $v\in\mathbb R^k$ . Together they predict $v^\top Bx$ , with effective weight vector $B^\top v$ . The fixed matrix $X\in\mathbb R^{n\times d}$ contains the $n$ training inputs as rows. Their span is $S=\operatorname{rowspace}(X)$ , with dimension $m$ .

The ground truth has orthonormal-row features $B_\star$ and a nonzero head $v_\star$ . Write $w_\star=B_\star^\top v_\star$ and $Y=Xw_\star$ . Perfect pretrained features mean $B_0=UB_\star$ for an orthogonal matrix $U$ . The corresponding aligned head is $u=Uv_\star$ . The dimensions satisfy $1\le k\le m$ and $m+k<d$ .

The two geometric assumptions require the orthogonal projections from $R_0=\operatorname{rowspace}(B_0)$ into $S$ and into $S^\perp$ to be injective. In this dimension regime these are exactly the positive largest-principal-angle cosine conditions used by the paper. They demand more than two subspaces having some nonorthogonal directions. The Lean definition spells out injectivity of $v\mapsto\Pi_T B_0^\top v$ for each $T\in\{S,S^\perp\}$ . See Definition 3.2 and Appendix A.1, PDF pp. 7 and 22-23.

An out-of-distribution law $\mu$ is any probability measure on $\mathbb R^d$ with a finite second moment and positive-definite uncentered second-moment matrix $\Sigma=\mathbb E_\mu[xx^\top]$ . Its mean need not be zero. Define

L_{\rm OOD}(v,B)=\mathbb E_{x\sim\mu} [(v^\top Bx-w_\star^\top x)^2].

Both training methods use the unnormalized loss $\widehat L(v,B)=\|XB^\top v-Y\|_2^2$ . Fine-tuning follows its gradient flow in both parameters; linear probing keeps $B=B_0$ . Time is real and nonnegative. These are the paper's equations (3.2)-(3.3), PDF p. 6.

Formalization targets

The goal is Proposition 3.7 in an explicit nonzero-signal regime. For $\sigma>0$ , initialize an FT head with independent Gaussian coordinates, $v_0\sim\mathcal N(0,\sigma^2I_k)$ . Establish

\Pr\!\left[\forall t\ge0,\quad L_{\rm OOD}(v_{\rm FT}(t),B_{\rm FT}(t))>0\right]=1.

Linear probing, from any initial head, must converge to $u$ . Fine-tuning initialized at its limit must satisfy

v_{\rm LP}(t)\longrightarrow u,\qquad \forall t\ge0,\quad L_{\rm OOD}(v_{\rm LP\text{-}FT}(t),B_{\rm LP\text{-}FT}(t))=0.

The probability-one event applies to all times simultaneously. The goal also asserts existence of the relevant global flows; a conditional claim about a possibly nonexistent trajectory would not suffice. The statement does not assert a numerical error lower bound or a positive time-infimum.

Seven milestones supply the supporting results: global flow existence and FT uniqueness; unchanged features orthogonal to the training span; the balancedness invariant; the second-moment identity for OOD risk; almost-sure Gaussian head misalignment; exact LP recovery; and stationarity after LP initialization. The principal source is Appendices A.2 and A.7, PDF pp. 23-31 and 45-47.

What the result establishes

The result distinguishes two initializations of the same joint-training procedure. In this idealized setting, a head obtained by linear probing gives zero OOD loss throughout subsequent fine-tuning, while a Gaussian head almost surely has positive OOD loss at every finite time. The conclusion concerns population squared prediction error, not classification accuracy or a finite test-set estimate.

The paper establishes the mathematical claim; this mission asks for a Lean proof of the stated model and result. The scope is deliberately limited to perfect pretrained features. It does not claim an LP-FT upper bound for imperfect features, which the authors identify as a further challenge in Section 3.4, PDF p. 10. A completed development would also provide reusable components for finite dimensional gradient flows, factorized linear models, and population risk.

Why the proof needs the training dynamics

The training loss alone does not select a unique effective predictor in an overparameterized problem. Knowing that a predictor fits the observed examples therefore does not determine its OOD loss. Formalization must track the head and feature extractor together, and it must distinguish parameter stationarity from a claim that a derivative happens to vanish at one time. The Gaussian conclusion also requires one event controlling an uncountable set of times; separate probability-one statements for individual times would be weaker.

Formalization scope and conventions

Vectors use Mathlib's finite dimensional real Euclidean spaces. Matrices are represented as continuous linear maps, with Euclidean adjoints and operator norms. The feature update is written explicitly as the Frobenius-gradient equation; it is not a gradient with respect to the operator norm. Differentiability is imposed within $[0,\infty)$ , including the right derivative at zero.

The dimensions, nonzero target, positive Gaussian scale, finite second moments, and projection injectivity are explicit. The nonzero target restricts the formalization to the regime of the Gaussian alignment argument in Lemma A.12; $k\le m$ makes the identifiability condition used in Proposition A.20 precise. The random-head law is the scaled standard Gaussian measure. No randomness of the fixed training matrix or independence from an additional data draw is assumed.

The model contains no assumed convergence, invariant, or desired risk bound. Each of those is a theorem obligation. The well-posedness milestone makes explicit an analytic prerequisite of the source's flow notation. The risk milestone uses the identity in (A.29)-(A.32), avoiding the reversed inequality printed in (A.28). The quantitative constant in Theorem 3.3 is outside this mission. Source-aligned proofs and the supporting analysis infrastructure are welcome; changing the learning rule or assuming a milestone inside the model would change the task.

Selected references

Ananya Kumar, Aditi Raghunathan, Robbie Jones, Tengyu Ma, and Percy Liang, Fine-Tuning can Distort Pretrained Features and Underperform Out-of-Distribution, ICLR 2022, arXiv:2202.10054v1. Main target: Section 3.4, Proposition 3.7, PDF p. 10, equations (3.10)-(3.11); proof: Appendix A.7, PDF pp. 45-47, Proposition A.20 and (A.208)-(A.218). Supporting invariants: Appendix A.2, PDF p. 24, Lemmas A.3-A.4, equations (A.15)-(A.20). Gaussian alignment: Appendix A.3, PDF pp. 34-35, Lemmas A.11-A.12.

9 thms1 active userReviewed

Completed

Mathematical Physics·Captain: ShapeZero

The spectrum of the octonionic two-generator flowTextbook

Motivation

This mission is pure mathematics about objects it defines itself: an octonion multiplication built from the Fano plane of the companion mission The role postulates force exactly seven points, and the matrix of the linear map

p \;\mapsto\; p\,a + b\,p

for two unit imaginary octonions $a, b$ . It is motivated by the two-generator D8 flow $\dot\psi = \psi a + b\psi$ in the Shape Zero derivation (00_START_HERE/MODEL_SPEC.md §1b; 02_synthesis/D8_SYNTHESIS.md). The statements below do not depend on that motivation.

Result. For $a = e_1$ and $b = c\,e_1 + s\,e_2$ with $c^2 + s^2 = 1$ , the characteristic polynomial of $M = R_a + L_b$ is

X^2\,(X^2 + 4)\,\bigl(X^2 + (2 - 2c)\bigr)^2 .

With $c = \cos\theta$ , $2 - 2c = 4\sin^2(\theta/2)$ , so the eigenvalues are $0, 0, \pm 2i$ and $\pm 2i\sin(\theta/2)$ (each twice), and the ratio of the two nonzero frequencies is $1/\sin(\theta/2)$ .

What this mission does NOT prove.

Only the canonical pair. It proves the result for $a = e_1$ , $b = \cos\theta\, e_1 + \sin\theta\, e_2$ . That every pair of unit imaginary octonions at angle $\theta$ gives the same spectrum follows from the classical fact that $G_2$ acts transitively on such pairs — not formalized here.
Nothing about any model. It says nothing about which angle, if any, a physical model selects, or whether the D8 flow plays a role in one.
One orientation. The octonion table uses one orientation of the Fano lines; all valid orientations give isomorphic algebras, and the spectrum is basis-independent, but only this table is formalized.

Setting

Write $e_0 = 1, e_1, \dots, e_7$ for the standard basis of $\mathbb{R}^8$ . The imaginary unit $e_u$ ( $u = 1, \dots, 7$ ) is labelled by the Fano point $u - 1$ . For each line $\{l, l+1, l+3\}$ (mod $7$ ) of the companion mission's Fano plane RolesForceSeven.fanoLine, the product is oriented cyclically along the ordered triple $(l, l+1, l+3)$ :

e_{l+1}\,e_{l+2} = e_{l+4}, \qquad e_{l+2}\,e_{l+4} = e_{l+1}, \qquad e_{l+4}\,e_{l+1} = e_{l+2}

(unit indices mod $7$ , shifted into $1, \dots, 7$ ), with the reversed products negative, $e_u^2 = -1$ , and $e_0$ the identity. This defines OctonionD8.octTable and the bilinear product OctonionD8.omul on $\mathbb{R}^8$ .

For $a, b \in \mathbb{R}^8$ , Rmat a is the matrix of $p \mapsto p\,a$ and Lmat b the matrix of $p \mapsto b\,p$ (column $j$ is the image of $e_j$ ). The flow matrix is

M = \texttt{flowMat}\;c\;s = R_{e_1} + L_{c e_1 + s e_2}.

The Fano plane is imported from the companion mission, not restated. The reordering blockEquiv and the two blocks blockA c s, blockB c s are defined explicitly for the milestones.

Formalization targets

Goal: the characteristic polynomial

c^2 + s^2 = 1 \;\Longrightarrow\; \chi_M(X) = X^2\,(X^2 + 4)\,\bigl(X^2 + (2 - 2c)\bigr)^2 .

This is OctonionD8.flow_charpoly. The hypothesis $c^2 + s^2 = 1$ is the only one, and it is needed: without it the characteristic polynomial differs.

Milestones — the proof outline

The proof goes through an invariant-subspace decomposition. Reorder the basis as $(e_0, e_1, e_2, e_4 \mid e_3, e_5, e_6, e_7)$ (OctonionD8.blockEquiv).

M1 (block-diagonal form). For all real $c, s$ , in the reordered basis $M$ is block diagonal: $M = \begin{pmatrix} A & 0 \\ 0 & B \end{pmatrix}$ , with explicit $4\times4$ blocks $A$ on $(e_0, e_1, e_2, e_4)$ and $B$ on $(e_3, e_5, e_6, e_7)$ (OctonionD8.blockA, OctonionD8.blockB).
M2 (block $A$ ). If $c^2 + s^2 = 1$ , then $\chi_A(X) = X^2\,(X^2 + 4)$ .
M3 (block $B$ ). If $c^2 + s^2 = 1$ , then $\chi_B(X) = \bigl(X^2 + (2 - 2c)\bigr)^2$ .

The goal follows: the characteristic polynomial is unchanged by reordering the basis, and that of a block-diagonal matrix is the product of the blocks' characteristic polynomials.

Further results (after the goal)

It is the octonions: the norm is multiplicative. For all $p, q \in \mathbb{R}^8$ , $\sum_k (pq)_k^2 = \bigl(\sum_i p_i^2\bigr)\bigl(\sum_j q_j^2\bigr)$ — the eight-square identity, which certifies that the table defines a normed (composition) algebra, the octonions, rather than some other algebra.
The flow conserves the norm. $M^{\mathsf T} = -M$ .
An annihilating polynomial. If $c^2 + s^2 = 1$ , then $M\,(M^2 + 4)\,\bigl(M^2 + (2 - 2c)\bigr) = 0$ .

Corollary: the frequencies

For $0 < \theta < \pi$ , with $c = \cos\theta$ and $s = \sin\theta$ , the roots over $\mathbb{C}$ of the characteristic polynomial, with multiplicity, are exactly

0,\ 0,\ \pm 2i,\ \pm 2i\sin(\theta/2),\ \pm 2i\sin(\theta/2),

and $0 < \sin(\theta/2) < 1$ . So the two nonzero frequencies $2$ and $2\sin(\theta/2)$ are distinct, and their ratio is $1/\sin(\theta/2)$ . Uses $2 - 2\cos\theta = 4\sin^2(\theta/2)$ .

Significance

The result itself. It gives the spectrum of the two-generator flow for the canonical pair in closed form, for every angle, from an octonion table built on the formalized Fano plane.

Formalizing it. The spectrum had been checked numerically and symbolically only.

Numerical and symbolic cross-check (independent code)

check	result
table from the companion mission's Fano lines is a normed algebra (200 random pairs)	true
eigenvalue magnitudes $\{0 \times 2,\ 2\sin(\theta/2) \times 4,\ 2 \times 2\}$ at 5°, 30°, 60°, 76.3°, 90°, 120°, 150°	max error $1.8\times10^{-15}$
symbolic characteristic polynomial (sympy, $s^2 = 1 - c^2$ )	$X^2(X^2 + 4)(X^2 + 2 - 2c)^2$

These agree with the repository's shape_zero_tests/d8_closed_form.py (frequencies $\{0, 2\sin(\theta/2), 2\}$ to $5\times10^{-11}$ ), which uses a different octonion table.

Difficulty

Moderate. The goal needs the characteristic polynomial of an $8\times8$ matrix with symbolic entries; a direct determinant expansion is expensive. The milestones take the invariant-subspace route: the block-diagonal form (M1) is an entrywise computation from the octonion table, and each $4\times4$ block's characteristic polynomial (M2, M3) is a small determinant, reduced with $c^2 + s^2 = 1$ . The further results are large but mechanical polynomial identities (the eight-square identity; the annihilating polynomial), where the risk is performance, not ideas.

Formalization scope

Vectors are Fin 8 → ℝ; matrices are Matrix (Fin 8) (Fin 8) ℝ, with column $j$ the image of the basis vector $e_j$ .
The characteristic polynomial is Mathlib's Matrix.charpoly over $\mathbb{R}$ ; the corollary maps it to $\mathbb{C}$ and uses Polynomial.roots, a multiset, so multiplicities are part of the statement.
The table is one fixed orientation of the Fano lines; $G_2$ -invariance and other orientations are out of scope.

Selected references

Wikipedia, Octonion. https://en.wikipedia.org/wiki/Octonion
Wikipedia, Fano plane. https://en.wikipedia.org/wiki/Fano_plane
Shape Zero repository (motivation only). https://github.com/ShapeZeroSZ/shape-zero

11 thms1 active userReviewed

Completed

Mathematical Physics·Captain: ShapeZero

Zero net power forces every link coupling to be symmetric, in any dimensionTextbook

Motivation

The Shape Zero model (Shape Zero LLC, unpublished) couples neighbouring nodes through a velocity-dependent force, one coupling matrix per link. The companion mission Zero net power forces every link coupling to be symmetric (rings of ≥ 3 sites) proves that a coupling doing no net work (a passive coupling) must have every link matrix symmetric — but only on a one-dimensional ring. The model's base is three-dimensional. This mission extends the result to a periodic cubic lattice with any number q of spatial axes, so it covers q = 3 directly and reduces exactly to the ring result at q = 1.

What this mission does NOT prove. As with the companion missions, commuting with the complex structure $J$ is not derived here; it remains a modelling premise. This mission shows only that passivity forces symmetry on every link in every direction.

Setting

Fix natural numbers $q$ (number of axes), $L$ (sites along each axis) and $d$ . A site is a point $x \in (\mathbb{Z}/L\mathbb{Z})^q$ of the periodic cubic lattice; $x \pm e_a$ is the site one step forward or back along axis $a$ , wrapping around. Each link — a site $x$ together with an axis $a$ — carries its own real $d\times d$ matrix $W(x,a)$ , and each site carries a velocity $v(x) \in \mathbb{R}^d$ . The force on site $x$ is

F(x) = \sum_{a} \Bigl( W(x,a)\, v(x+e_a) - W(x-e_a,a)\, v(x-e_a) \Bigr),

where the second term uses the matrix of the link behind $x$ . The total power is

P_W(v) = \sum_{x} v(x) \cdot F(x).

In Lean, sites are Site q L = Fin q → Fin L, the step is shift x a s (update coordinate $a$ by $s$ in Fin L), and the power is PassivityTorus.power q L d W v. The coupling is passive when $P_W(v) = 0$ for every $v$ .

Formalization targets

Goal: passive if and only if every link is symmetric ( $L \ge 3$ )

L \ge 3 \;\Longrightarrow\; \Bigl(\forall v,\; P_W(v) = 0\Bigr) \iff \Bigl(\forall x, a,\; W(x,a)^{\mathsf T} = W(x,a)\Bigr).

This is PassivityTorus.passive_iff_symm, for every $q$ and $d$ .

Milestones

M1. Stepping back then forward along an axis returns to the start.
M2 (power identity, every $q$ , $L$ ). $P_W(v) = \sum_x \sum_a v(x) \cdot \bigl((W(x,a) - W(x,a)^{\mathsf T})\, v(x+e_a)\bigr)$ .
M3 (symmetric links are passive, every $L$ ).
M4 (passive forces symmetric, $L \ge 3$ ).

Significance

The result itself. It is the dimension-independent form of the passivity theorem: whatever the number of spatial axes, a per-link coupling does no net work for every motion exactly when every link matrix is symmetric. It removes the one-dimensional restriction from the step that justifies restricting the model's coupling class to symmetric matrices.

Formalizing it. The ring result has been machine-checked; the lattice extension had been checked numerically only (identity error $\le 3.6\times10^{-14}$ at $(q,L) = (1,3), (2,3), (3,3), (3,4)$ ). A proof covers every $q$ , $L \ge 3$ and $d$ .

Difficulty

The algebra is the ring argument; the difficulty is bookkeeping. The incoming term must be reindexed by the one-step shift, which is a bijection of the torus, and the converse needs a test motion supported on two neighbouring sites $x$ and $x+e_a$ together with a proof that no other link joins them.

The hypothesis $L \ge 3$ is necessary. At $L = 2$ the step forward and the step back along an axis reach the same site. This is proved (in Lean, locally): for every $q \ge 1$ , putting the same non-symmetric matrix $\begin{pmatrix} 0 & 1 \\ 0 & 0 \end{pmatrix}$ on every link of the $L = 2$ lattice gives exactly zero power for every velocity field, so passivity does not force symmetry there. Weakening the hypothesis makes the goal false.

Formalization scope

The lattice is periodic in every axis, with the same $L$ along each; [NeZero L] is needed for the literal $1$ in Fin L and is implied by $L \ge 3$ in the goal.
There is one matrix per site per axis, with no relation assumed between links.
Passivity is quantified over all velocity fields; everything is real.
$q = 0$ (a single site, no links) and $d = 0$ are included; both sides of the goal hold trivially there, and this is not a trivialization since the statement is quantified over all $q$ and $d$ .

Selected references

Wikipedia, Symmetric matrix. https://en.wikipedia.org/wiki/Symmetric_matrix
Wikipedia, Passivity (engineering). https://en.wikipedia.org/wiki/Passivity_(engineering)
Mathlib, Mathlib.Data.Matrix.Mul (dot product ⬝ᵥ, matrix–vector product *ᵥ). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Mul.html

6 thms1 active userReviewed

Completed

Mathematical Physics·Captain: ShapeZero

Zero net power forces every link coupling to be symmetric (rings of ≥ 3 sites)Textbook

Motivation

The Shape Zero model (Shape Zero LLC, unpublished) couples neighbouring nodes on a ring through a velocity-dependent force, with one coupling matrix per link. A companion mission, The passivity-admissible couplings have dimension n² = dim u(n), shows that real matrices which are symmetric and commute with a complex structure $J$ form a space of dimension $n^2 = \dim \mathfrak{u}(n)$ . That mission deliberately takes symmetry as given. This mission supplies the reason for it: a coupling that never does net work (a passive coupling) must have every link matrix symmetric, provided the ring has at least three sites.

Together the two missions give the chain

\text{passive} \;\Longrightarrow\; \text{every } W_i \text{ symmetric} \qquad\text{(this mission)},

\text{symmetric} + \text{commutes with } J \;\Longrightarrow\; \dim = n^2 \qquad\text{(companion mission)}.

What these two missions do NOT prove. Commuting with $J$ is not derived here. It is the requirement that the coupling respect each node's complex structure, and in the model it is imposed, not forced by passivity. After both missions the proved content is: passivity forces symmetry, and symmetric $J$ -compatible couplings have the dimension of $\mathfrak{u}(n)$ . The $J$ -compatibility step remains a modelling premise. In addition, the coupling space consists of the Hermitian matrices, which match $\mathfrak{u}(n)$ in dimension; the Lie algebra $\mathfrak{u}(n)$ itself appears only after multiplying by $i$ (Unitary group).

Setting

Let $N$ and $d$ be natural numbers with $N \ge 1$ . A ring has $N$ sites labelled by $\mathbb{Z}/N\mathbb{Z} = \{0, \dots, N-1\}$ , so site $N-1$ is next to site $0$ ; indices $i + 1$ and $i - 1$ are taken modulo $N$ . Each site carries a velocity vector $v_i \in \mathbb{R}^d$ , and each link $i \to i+1$ carries a real $d \times d$ link matrix $W_i$ . The force on site $i$ is

F_i = W_i\, v_{i+1} - W_{i-1}\, v_{i-1},

where the second term uses the previous link's matrix $W_{i-1}$ . The total power delivered by the coupling is

P_W(v) = \sum_{i \in \mathbb{Z}/N\mathbb{Z}} v_i \cdot \bigl( W_i\, v_{i+1} - W_{i-1}\, v_{i-1} \bigr).

In the Lean development this is PassivityRing.power N d W v, with sites indexed by Fin N (whose addition and subtraction wrap around modulo $N$ ), vectors in Fin d → ℝ, and $\cdot$ the dot product ⬝ᵥ. The coupling is passive when $P_W(v) = 0$ for every choice of velocities $v$ .

Formalization targets

Goal: passive if and only if every link is symmetric (rings of at least 3 sites)

N \ge 3 \;\Longrightarrow\; \Bigl( \forall v,\; P_W(v) = 0 \Bigr) \iff \Bigl( \forall i,\; W_i^{\mathsf T} = W_i \Bigr).

This is PassivityRing.passive_iff_symm. It holds for every $d$ and every family of link matrices, with no assumption relating different links.

Milestones

M1 (power identity, every $N$ ). $P_W(v) = \sum_i v_i \cdot \bigl((W_i - W_i^{\mathsf T})\, v_{i+1}\bigr)$ .
M2 (symmetric links are passive, every $N$ ). If every $W_i$ is symmetric, then $P_W(v) = 0$ for all $v$ .
M3 (passive forces symmetric, $N \ge 3$ ). If $P_W(v) = 0$ for all $v$ , then every $W_i$ is symmetric.

Significance

The result itself. The goal turns a physical requirement — no net work for any motion — into an exact algebraic condition on each link separately. It is the step that justifies restricting the companion mission's coupling class to symmetric matrices, so that the dimension count $n^2$ applies to the passive couplings of the model rather than to an assumed class.

Formalizing it. The model's claim has so far been checked numerically at ring sizes $1, 2, 3, 4, 7$ . A machine-checked proof covers every $N \ge 3$ and every $d$ , makes the role of the hypothesis $N \ge 3$ explicit, and separates what is proved (passivity forces symmetry) from what remains a modelling premise ( $J$ -compatibility).

Difficulty

The forward direction and the power identity are finite-sum bookkeeping. The central difficulty is the converse: the hypothesis constrains a single scalar quantity summed around the ring, and it must be shown to constrain each link matrix individually. On small rings this fails because distinct terms of the sum coincide, so the argument depends on the ring being large enough that neighbouring sites are genuinely distinct, and in Lean that is modular arithmetic on Fin N.

The hypothesis $N \ge 3$ is necessary, not a convenience:

$N = 1$ : the site is its own neighbour on both sides, so the force is $W_0 v_0 - W_0 v_0 = 0$ and the power vanishes for every $W_0$ , symmetric or not.
$N = 2$ : the power reduces to $v_0 \cdot (D - D^{\mathsf T})\, v_1$ with $D = W_0 - W_1$ , so it depends only on the difference of the two link matrices. Taking both links equal to the same non-symmetric matrix, for example $\begin{pmatrix} 0 & 1 \\ 0 & 0 \end{pmatrix}$ , gives zero power for all velocities.

Weakening the hypothesis to $2 \le N$ , or dropping it, makes the goal false.

Formalization scope

Sites are Fin N with its wrap-around arithmetic, so $i + 1$ and $i - 1$ go around the ring; [NeZero N] is required for the literal $1$ in Fin N and is implied by $N \ge 3$ in the goal.
There is one matrix per link, W : Fin N → Matrix (Fin d) (Fin d) ℝ, not a single shared matrix, and no relation between different links is assumed.
Passivity is quantified over all velocity configurations v : Fin N → (Fin d → ℝ).
Everything is real (ℝ); symmetry is (W i)ᵀ = W i.
$d = 0$ is included; there both sides of the goal hold trivially. This is not a trivialization, since the statement is quantified over all $d$ .

M1 and M2 hold for every $N \ge 1$ and carry no ring-size hypothesis; M3 and the goal require $N \ge 3$ . The development needs only Mathlib's finite sums, dot products, matrix–vector products and Fin arithmetic.

Selected references

B. C. Hall, Lie Groups, Lie Algebras, and Representations: An Elementary Introduction, 2nd ed., Graduate Texts in Mathematics 222, Springer, 2015. https://doi.org/10.1007/978-3-319-13467-3
Wikipedia, Unitary group. https://en.wikipedia.org/wiki/Unitary_group
Wikipedia, Symmetric matrix. https://en.wikipedia.org/wiki/Symmetric_matrix
Mathlib, Mathlib.Data.Matrix.Mul (dot product ⬝ᵥ, matrix–vector product *ᵥ). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Mul.html

5 thms1 active userReviewed

Missions

On a Conjecture of Spectral Extremal Problems: If the Extremal Graphs for F Are Turán Graphs Plus a Fixed Number of Edges, Every F-Free Graph of Maximum Spectral Radius Is ExtremalResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Conjugate Gradient Methods with Inexact Searches: The Self-Scaled Direction Is a Multiple of Beale's Restart DirectionResearch Paper

Motivation

Setting

Formalization targets

Goal: reduction of the self-scaled method to Beale's method

Companion statements

Milestones on the path

Significance

Difficulty

Formalization scope

Selected references

Stabilization for a Perturbed Chain of Integrators in Prescribed Time I: Prescribed-Time Estimates for the Linear Time-Varying FeedbackResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary 14 (corrected)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Randomized Algorithms for Estimating the Trace of an Implicit Symmetric Positive Semi-Definite Matrix V: Sample Bound for the Mixed Unit Vector Trace EstimatorResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Randomized Algorithms for Estimating the Trace of an Implicit Symmetric Positive Semi-Definite Matrix III: Sample Bound for Normalized Rayleigh-Quotient Trace EstimatorsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.1, in the form its proof establishes

Milestones (the displayed steps of the proof, p. 8:10)

Significance

Difficulty

Formalization scope

Selected references

Matching Is as Easy as Matrix Inversion: Steps 1–3 Find a Minimum Weight Perfect Matching with Probability at Least 1/2Research Paper

Motivation

Setting

Formalization targets

Goal: Steps 1–3 find a minimum weight perfect matching with probability at least 1/2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Sparse Approximate Solutions to Linear Systems 1: The Column Bound for Greedy SelectionResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2, for AAA with linearly independent columns

Milestones

Significance

Difficulty

Formalization scope

Selected references

Robust Solutions to Least-Squares Problems with Uncertain Data IV: A Semidefinite Upper Bound on the Linear-Fractional Worst-Case Residual, Exact for Full PerturbationsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.2 (corrected)

Milestones

Significance

Goal: Theorem 2, for $A$ with linearly independent columns

Goal: Theorem 3.2 with the identity for $\mu$

Goal: the admissible class has dimension $n^2$