Linear algebra

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

Completed

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

Dynamic Programming Operations Research·Captain: mikedeng1

Analytical Solution to a Discrete-Time Model for Dynamic Learning and Decision Making: the two-action frontier difference equations have a unique closed-form solution with explicit det YResearch Paper

Learning while doing, and the frontier of continuation values

Many sequential decisions trade off immediate reward against information: a firm prices without knowing which demand regime it faces, a clinician treats without knowing a patient's type, a bandit player pulls a risky arm to learn its mean. Formally these are partially observed Markov decision problems (POMDPs) with a hidden but fixed state. Their value function is the upper envelope of a set of linear functions of the belief, one continuation-value vector per policy. The efficient frontier of these vectors describes the optimal policy for every prior at once. Except for special cases, the frontier of a POMDP has to be computed numerically.

Hao Zhang (Management Science, 2021; accepted version SSRN 3847049) treats the case of two states, two actions and two signals. Under a commensurability condition on the signals, the extreme points of the frontier satisfy linear difference equations with constant coefficients (Theorems 2 and 4 of the paper). The paper solves these equations in closed form. Theorem 3 covers the case where the second action reveals nothing, so that it acts as a stopping action. Theorem 6 covers the case where both actions are informative. This mission formalizes the solution of the difference equations, including the explicit determinant of the coupling matrix that Appendix B states as Theorem 6 (Complete).

Setting

The hidden state is $\theta \in \{1, 2\}$ , the actions are $A$ and $B$ , and the signals are $\gamma$ and $\bar\gamma$ . In each period, action $a$ in state $\theta$ produces signal $\gamma$ with probability $p_\theta(a, \gamma)$ and an expected reward $r_\theta(a)$ , and rewards are discounted by $\delta \in (0, 1)$ . The anchor points $\hat u^a_\theta = (1-\delta)^{-1} r_\theta(a)$ are the values of always playing $a$ . Write $p^A_\theta = p_\theta(A,\gamma)$ and $p^B_\theta = p_\theta(B,\gamma)$ .

The signal quality indices are integers $n(A,\gamma) = n^A > 0$ , $n(A,\bar\gamma) = -\bar n^A < 0$ , $n(B,\gamma) = n^B > 0$ and $n(B,\bar\gamma) = -\bar n^B < 0$ . Their absolute values are relatively prime, and for some $\mu > 1$ each log-likelihood ratio $\ln(p_1(a,s)/p_2(a,s))$ equals $n(a,s) \ln\mu$ (Definition 3).

For each $\theta$ the paper's boundary-value problem (28)–(31) asks for real sequences $v^A, v^B$ on $k = 0, 1, 2, \dots$ satisfying four conditions:

v^A(k+n^A) - \delta^{-1}(p^A_\theta)^{-1} v^A(k) + (p^A_\theta)^{-1}(1-p^A_\theta)\, v^A(k-\bar n^A) = 0 \quad (k \ge \bar n^A),

v^B(k+\bar n^B) - \delta^{-1}(1-p^B_\theta)^{-1} v^B(k) + (1-p^B_\theta)^{-1} p^B_\theta\, v^B(k-n^B) = 0 \quad (k \ge n^B),

the coupling condition $v^A(k) + \hat u^A_\theta = v^B(\bar n^A + n^B - 1 - k) + \hat u^B_\theta$ for $k = 0, \dots, \bar n^A + n^B - 1$ , and decay, $v^A(k), v^B(k) \to 0$ .

The characteristic polynomials are

f^A_\theta(z) = z^{n^A+\bar n^A} - \delta^{-1}(p^A_\theta)^{-1} z^{\bar n^A} + (p^A_\theta)^{-1}(1-p^A_\theta), \qquad f^B_\theta(z) = z^{n^B+\bar n^B} - \delta^{-1}(1-p^B_\theta)^{-1} z^{n^B} + (1-p^B_\theta)^{-1}p^B_\theta.

$Z^a_{unit}$ is the set of their roots with $|z| < 1$ , and $m^a_z$ is the multiplicity of the root $z$ . From these roots the paper builds a square matrix $Y = (Y^A, Y^B)$ . Its A-columns are $\binom{k}{\tau}z^{k-\tau}$ and its B-columns are $\binom{\bar n^A+n^B-1-k}{\tau}z^{\bar n^A+n^B-1-k-\tau}$ , in a fixed column order.

Formalization targets

Goal: Theorem 6 (Complete), EC p. 11

For each $\theta$ , under the standing assumptions of §5, the goal asserts four things:

$\sum_{z\in Z^A_{unit}} m^A_z = \bar n^A$ and $\sum_{z\in Z^B_{unit}} m^B_z = n^B$ .
For every enumeration of the roots,

\det Y = \prod_{i<l}(z^A_l - z^A_i)^{m^A_i m^A_l}\prod_{i,l}(1 - z^A_i z^B_l)^{m^A_i m^B_l}\prod_{i<l}(z^B_i - z^B_l)^{m^B_i m^B_l}.

$\det Y \ne 0$ .
The problem (28)–(31) has exactly one real solution. That solution is the root expansion $v^a_\theta(k) = \sum_{z \in Z^a_{unit}}\sum_{\tau<m^a_z}\alpha^a_{z,\tau}\binom{k}{\tau}z^{k-\tau}$ , whose coefficients are given by $(\boldsymbol\alpha^A; -\boldsymbol\alpha^B) = (\hat u^B_\theta - \hat u^A_\theta)Y^{-1}\mathbf 1$ .

Milestones

Eq. (18): the general solution of a constant-coefficient linear recurrence with repeated characteristic roots.
Eq. (19): the determinant of the generalized (confluent) Vandermonde matrix.
From the proof of Theorem 3: $z^{n+\bar n} - \delta^{-1}p^{-1}z^{\bar n} + p^{-1}(1-p)$ has exactly $\bar n$ roots in the open unit disk, counted with multiplicity.
From the proof of Theorem 3: decay of an exponential polynomial forces zero coefficients on every root with $|z| \ge 1$ .
Theorem 3: the one-sided problem (13)–(15), when action $B$ is uninformative.
The base case and the inductive step of the determinant computation in the proof of Theorem 6 (Complete).

Significance

The result turns the efficient frontier of this class of POMDPs into explicit algebra. Each extreme point is a finite sum over the roots of two trinomials in the unit disk, and the coefficients come from one linear solve. The paper uses this to explain the shape of the frontier: how many extreme points the two actions contribute, and how quickly they accumulate at the anchor points. It also shows that the coupled two-sided problem is always well posed, because $Y$ is nonsingular.

The paper proves the results in prose; none of them is machine-checked. The mission contributes a checked proof of the solution formula and of the determinant identity. The identity is a confluent Vandermonde-type evaluation with a reflected second block. Several pieces are general mathematics that Mathlib lacks: the solution space of a linear recurrence with repeated roots in binomial form, the confluent Vandermonde determinant, root counting in the unit disk, and the decay lemma for exponential polynomials.

Difficulty

The obvious argument is to write down the general solution, discard the growing modes and match the boundary data. It runs into three problems. First, the count of roots in the disk is what makes $Y$ square. It comes from Rouché's theorem, which Mathlib does not have, so it must be proved or replaced by a polynomial argument. Second, roots on the unit circle are not excluded a priori, so the decay argument has to handle polynomially weighted unimodular terms. Third, and hardest, is $\det Y \ne 0$ . $Y$ is not a confluent Vandermonde matrix: its B-block is reflected ( $N-1-k$ in place of $k$ ). The paper reduces the simple-root case to a Vandermonde matrix in the inverted points $1/z^B_j$ , and then handles each repeated B-root by differentiating with respect to a "nominal root". Making that induction precise requires care with column orders and signs.

Formalization scope

The Lean development lives in the namespace LearnDoFrontier.TwoAction. A Model carries $\delta$ , $p^A_\theta$ , $p^B_\theta$ , the rewards $r_\theta(a,s)$ and the four indices, with the negative indices stored as the positive naturals $\bar n^A, \bar n^B$ . States, actions and signals are Fin 2, and index 0 stands for $\theta = 1$ , $A$ and $\gamma$ . Model.Standing collects the assumptions of §5: $0<\delta<1$ , General Position, Informative Actions A and B, and Definition 3, with "relatively prime" read as a joint gcd of $1$ . Sequences are real and indexed by $\mathbb N$ , while the roots, coefficients and $Y$ are complex. The solution formula is an equality in $\mathbb C$ . Root enumerations are arbitrary bijections onto $Z^a_{unit}$ , universally quantified, and the columns of $Y$ follow the paper's order: A-columns first, roots first, then $\tau$ ascending for A and descending for B. Exponents use natural-number subtraction, which is harmless because the binomial factor vanishes whenever $k<\tau$ . The determinant milestones are stated for arbitrary distinct points rather than roots, as the paper's induction uses them.

No formalization may make the targets hold by definition. $Z_{unit}$ and $m_z$ are the actual roots and multiplicities, never "the first $\bar n^A$ roots". Uniqueness ranges over all real sequences satisfying (28)–(31), not only over root expansions. The coefficients are given by $Y^{-1}$ , not chosen to fit the boundary.

The link from the POMDP's efficient frontier to (13)–(15) and (28)–(31) (Theorems 2 and 4) is not formalized. Its proofs are geometric sketches, and Theorem 4 assumes a two-segment frontier structure that the paper itself calls a conjecture. The mission is about the difference equations exactly as the paper poses them. Proofs of any milestone are welcome, and the recurrence, Vandermonde and root-count lemmas are reusable well beyond this mission.

Selected references

Hao Zhang, Analytical Solution to a Discrete-Time Model for Dynamic Learning and Decision Making, Management Science, 2021. https://doi.org/10.1287/mnsc.2021.4194 ; accepted version with E-Companion: https://ssrn.com/abstract=3847049
Saber Elaydi, An Introduction to Difference Equations, 3rd ed., Springer, 2005. https://doi.org/10.1007/0-387-27602-5
Richard D. Smallwood and Edward J. Sondik, The Optimal Control of Partially Observable Markov Processes over a Finite Horizon, Operations Research 21(5), 1973. https://doi.org/10.1287/opre.21.5.1071

10 thms1 active userReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Equilibria and Systemic Risk in Saturated Networks: necessary and sufficient conditions for uniqueness of saturated network equilibria, class by class, when the spectral radius is at most oneResearch Paper

Motivation

Many models of contagion in networks reduce to the same fixed-point equation: each node receives a linear combination of the states of its in-neighbours plus an exogenous term, and its own state is that inflow clipped to an interval. In the interbank clearing model of Eisenberg and Noe (Management Science, 2001) the states are payments capped by liabilities; in network games with strategic complementarities and bounded actions the states are best responses; in flow networks with finite capacities the states are flows. Massai, Como and Fagnani (arXiv:1912.04815, Mathematics of Operations Research) study this equation in a common form, with no sign restriction on the exogenous term and no normalisation of the interaction matrix. For a regulator or a modeller, the first question about such an equation is whether its solution is unique: when it is not, the outcome of a default cascade, or the play of a game, is not determined by the data.

Earlier uniqueness results covered special cases: Eisenberg and Noe proved uniqueness of the clearing vector under a regularity condition on the liability network, and contraction arguments give uniqueness when the interaction matrix has spectral radius below one. The paper treats every nonnegative interaction matrix with spectral radius at most one.

Setting

The nodes form a finite set $\mathcal V$ . A network is a pair $(P, w)$ with $P$ an entrywise nonnegative $\mathcal V \times \mathcal V$ matrix and $w$ a nonnegative vector; an exogenous flow is an arbitrary $c \in \mathbb R^{\mathcal V}$ . Writing $S_0^{w}$ for the coordinatewise clipping $(S_0^w(y))_i = \min\{\max\{y_i, 0\}, w_i\}$ , a network equilibrium is a solution of

x = S_0^w(P^\top x + c), \qquad\text{i.e.}\qquad x_i = \min\Big\{\max\Big\{\sum_j x_j P_{ji} + c_i,\ 0\Big\},\ w_i\Big\}.

The set of equilibria is $\mathcal X$ . The spectral radius $\rho(A)$ of a square matrix is the largest modulus of its complex eigenvalues. The digraph $\mathcal G_P$ has a link $i \to j$ when $P_{ij} \neq 0$ ; its strongly connected components are the classes of $P$ , and $P^{(ll)}$ denotes the principal block of $P$ on the class $\mathcal V_l$ . After a permutation of the nodes, $P$ is block upper triangular with these blocks on the diagonal. A class is basic if $\rho(P^{(ll)}) = \rho(P)$ and final if no link leaves it. A network is non-expansive if $\rho(P) < 1$ , or $\rho(P) = 1$ and every basic class is final. For an equilibrium $x$ , a node is surplus, exposed or deficit according as its inflow $c_i + \sum_k P_{ki}x_k$ lies above $w_i$ , in $[0, w_i]$ , or below $0$ .

Formalization targets

Goal: Theorem 2 (p. 16)

Assume $\rho(P) \le 1$ , let $\mathcal V_l$ be a class and fix the equilibrium on the nodes upstream of $\mathcal V_l$ . Put $u^{(l)} = c^{(l)} + \sum_{i<l} P^{(il)\top}x^{(i)}$ . Then the projection $x^{(l)}$ of the equilibria on $\mathcal V_l$ is

unique when $\rho(P^{(ll)}) < 1$ ;
when $\rho(P^{(ll)}) = 1$ , with right and left dominant eigenvectors $p^{(l)}$ , $\pi^{(l)}$ of $P^{(ll)}$ , non-unique if and only if

p^{(l)\top}u^{(l)} = 0, \qquad \min_{i \in \mathcal V_l}\frac{\nu^{(l)}_i}{\pi^{(l)}_i} + \min_{i \in \mathcal V_l}\frac{w_i - \nu^{(l)}_i}{\pi^{(l)}_i} > 0,

where $\nu^{(l)} = P^{(ll)\top}\nu^{(l)} + u^{(l)}$ ; and in that case the projections form the segment $\{\nu^{(l)} + \alpha\pi^{(l)}\}$ with $\alpha$ between minus the first minimum and the second.

The goal is a statement about $\mathcal X$ , the equilibria of the whole network, not about an isolated block.

Milestones

The milestones follow the paper's own chain of results:

Proposition 1 (i): $\mathcal X$ is a complete lattice.
Proposition 2: Perron–Frobenius facts for nonnegative and irreducible matrices.
Lemma 1 and Proposition 3: a positive vector $v$ with $Pv \le v$ exists if and only if the network is non-expansive.
Theorem 1 and Corollary 1: for non-expansive networks the surplus/exposed/deficit partition is the same for every equilibrium, and on it all equilibria solve one linear system.
Proposition 4: $\rho(P) < 1$ gives a unique equilibrium.
Proposition 5: the irreducible case with $\rho(P) = 1$ , where the equilibria are non-unique exactly when $p^\top c = 0$ and the segment condition (29) holds, and then form the segment (30).

Significance

Theorem 2 answers the uniqueness question completely for $\rho(P) \le 1$ , a range that contains every stochastic and sub-stochastic matrix and hence the standard interbank and flow-network models. It reduces uniqueness to finitely many checks, one per class, each a linear equation and two finite minima. It also shows that when uniqueness fails there is a continuum of equilibria (a segment on each critical class) rather than isolated ones, which is false for $\rho(P) > 1$ (Remark 9 of the paper). Theorem 1 says that, for non-expansive networks, which nodes are defaulting, solvent-but-exposed, or in surplus does not depend on the equilibrium selected; this is the robustness property the paper uses for systemic-risk measures.

None of these results has a machine-checked proof that we know of. The mission also produces reusable linear algebra: the Perron–Frobenius theorem for nonnegative matrices with the complex spectral radius (absent from Mathlib), its irreducible refinements, and the characterisation of matrices admitting a positive subinvariant vector.

Difficulty

The obvious argument is the contraction one: when $\rho(P) < 1$ the map $x \mapsto S_0^w(P^\top x + c)$ is a contraction in a suitable norm. At $\rho(P) = 1$ that argument fails, and non-uniqueness genuinely occurs. Even non-expansiveness in some norm is not enough: Example 1 of the paper has $\rho(P) = 1$ , a simple eigenvalue, and still an equilibrium-dependent partition, because a basic class is not final. The difficulty is to localise the critical behaviour to the classes of spectral radius one. It also needs the projection of the equilibrium set on a class, with its upstream values fixed, to be exactly the equilibrium set of a smaller irreducible network. Then the whole of $\mathcal X$ has to be identified with a segment of the kernel line of $I - P^{(ll)\top}$ intersected with a box.

Formalization scope

Nodes are a finite type with decidable equality. $P$ is a real matrix with nonnegative entries and $w$ a nonnegative vector, so $w_i = 0$ is allowed. The exogenous flow $c$ is unrestricted in sign. $\rho$ is Mathlib's spectralRadius ℂ of the complexified matrix (in $[0,\infty]$ ), never the real spectral radius. Equilibria are the solutions of (1) with $\min$ / $\max$ exactly as in (3). Classes are strongly connected components of $\mathcal G_P$ with reachability by paths of length at least zero, so a node on no cycle forms a class with block $[0]$ . Instead of assuming $P$ in block triangular form, the goal quantifies over a class and fixes the equilibrium on the nodes upstream of it. "Non-unique" is Set.Nontrivial. Minima over a class are Finset.inf' over a nonempty index set. Dominant eigenvectors are nonnegative, nonzero eigenvectors for the eigenvalue $1$ ; positivity of $\pi$ is not assumed.

Four printed slips are read as intended and disclosed in the items:

the sums $\sum_{k \ne i}$ in the partition (19) are the full sums of (1);
"connected components" on p. 10 are strongly connected components;
the third bullet of Theorem 2 sums over $i < l$ ;
Proposition 2 (iv) is stated as $\rho(P)x = P^\top x + c$ , which agrees with the printed equation when $\rho(P) = 1$ .

Several formalizations would trivialise the goal and are ruled out:

a block-only reading, in which the class projection is replaced by solutions of the block equation, is Proposition 5 again;
the real spectral radius makes the hypotheses depend silently on Perron–Frobenius;
assuming $c \ge 0$ , $w > 0$ , $P$ sub-stochastic or irreducible removes the cases the theorem is about.

A complete development needs the Perron–Frobenius theory of nonnegative and irreducible matrices, the Tarski fixed-point theorem (in Mathlib), and the condensation of a digraph into its strongly connected components. The Perron–Frobenius milestones are reusable well beyond this mission and are welcome as independent contributions. The continuity results of §5 (Theorem 3, Corollaries 2–3) are out of scope.

Selected references

L. Massai, G. Como, F. Fagnani, Equilibria and Systemic Risk in Saturated Networks, Mathematics of Operations Research; arXiv:1912.04815v2, 2021. https://arxiv.org/abs/1912.04815
L. Eisenberg, T. H. Noe, Systemic Risk in Financial Networks, Management Science 47(2), 2001. https://doi.org/10.1287/mnsc.47.2.236.9835
A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM, 1994. https://doi.org/10.1137/1.9781611971262

11 thms1 active userReviewed

Differential Geometry Optimization·Captain: mikedeng1

On Geometric Connections of Embedded and Quotient Geometries in Riemannian Fixed-rank Matrix Optimization: Gradient and Hessian Connections for Fixed-rank PSD Matrices via YYᵀResearch Paper

Motivation

Many estimation problems in statistics, signal processing and machine learning ask for a low-rank positive semidefinite matrix: phase retrieval, matrix sensing, PCA-type problems and the Burer–Monteiro approach to semidefinite programs. A standard formulation is

\min_{X\in\mathbb S^{p\times p},\ X\succeq0,\ \operatorname{rank}(X)=r} f(X),\qquad 0<r\le p, \tag{1}

and Riemannian optimization solves it by treating the feasible set as a smooth manifold. Two geometries are in common use. In the embedded geometry the set of rank- $r$ PSD matrices is a submanifold of $\mathbb R^{p\times p}$ with the Euclidean metric. In the quotient geometry one writes $X=YY^\top$ with a full-column-rank factor $Y$ and optimizes over equivalence classes $[Y]=\{YO:O\text{ orthogonal}\}$ . Algorithms built on the two geometries behave similarly in experiments, and landscape results (absence of spurious local minima, strict saddles) have been proved separately for each. Luo, Li and Zhang (arXiv:2110.12121, Mathematics of Operations Research 2024) explain this by an explicit dictionary between the Riemannian gradients and Hessians of the two geometries. This mission formalizes their first main result, Theorem 3, for the full-rank factorization of PSD matrices.

Setting

Matrices carry the Frobenius inner product $\langle A,B\rangle=\operatorname{tr}(A^\top B)$ . The objective $f:\mathbb R^{p\times p}\to\mathbb R$ is twice continuously differentiable and symmetric, $f(X)=f(X^\top)$ (the paper's standing assumptions); $\nabla f$ and $\nabla^2f$ are its Euclidean gradient and Hessian.

Embedded geometry. $\mathcal M_{r+}=\{X\in\mathbb S^{p\times p}:X\succeq0,\ \operatorname{rank}X=r\}$ , viewed as $\mathcal M^e_{r+}\subset\mathbb R^{p\times p}$ . Its tangent space $T_X\mathcal M^e_{r+}$ is the span of the tangent cone. The Riemannian gradient $\operatorname{grad}f(X)$ is the orthogonal projection of $\nabla f(X)$ onto $T_X\mathcal M^e_{r+}$ , and the Riemannian Hessian quadratic form $\operatorname{Hess}f(X)[\xi,\xi]$ is the derivative $\frac{d}{dt}\langle\operatorname{grad}f(c(t)),\xi\rangle$ at $t=0$ along any $C^1$ curve $c$ in $\mathcal M_{r+}$ with $c(0)=X$ , $c'(0)=\xi$ .

Quotient geometry. The total space is $\mathbb R_*^{p\times r}$ , the $p\times r$ matrices of full column rank, with the objective $\bar h_{r+}(Y)=f(YY^\top)$ (18a). A weight $Y\mapsto W_Y$ , smooth and symmetric positive definite, defines the metric $\bar g_Y(\eta,\theta)=\operatorname{tr}(W_Y\eta^\top\theta)$ . The vertical space $\mathcal V_Y=\{Y\Omega:\Omega^\top=-\Omega\}$ is tangent to the orbit $[Y]$ , and the horizontal space $\mathcal H_Y$ is its $\bar g_Y$ -orthogonal complement. Tangent vectors of the quotient $\mathcal M^{q_1}_{r+}=\mathbb R_*^{p\times r}/\mathbb O_r$ are represented by horizontal vectors: $\overline{\operatorname{grad}h_{r+}([Y])}$ is the horizontal part of the total-space gradient $\nabla\bar h_{r+}(Y)W_Y^{-1}$ , and $\overline{\operatorname{Hess}h_{r+}([Y])}[\theta,\theta]=\bar g_Y(\bar\nabla_\theta\operatorname{grad}\bar h,\theta)$ for horizontal $\theta$ , where $\bar\nabla$ is the Levi-Civita connection of $\bar g$ (Koszul formula).

Comparison data. $\mathcal L^{r+}_Y(\theta)=Y\theta^\top+\theta Y^\top$ ; $U\in\mathrm{St}(r,p)$ spans the top $r$ eigenspace of $X=YY^\top$ , $P=U^\top Y$ , $Y^\dagger=(Y^\top Y)^{-1}Y^\top$ . For a quadratic form on a $d$ -dimensional space with inner product $g$ , $\lambda_k$ is its $k$ -th largest eigenvalue relative to $g$ ( $1\le k\le d$ ). $\sigma_1,\sigma_r$ are the extreme singular values of an $r\times r$ matrix.

Formalization targets

Goal: Theorem 3 (p. 21)

If in addition $W_Y=OW_{YO}O^\top$ for all orthogonal $O$ , then for every $Y\in\mathbb R_*^{p\times r}$ and $X=YY^\top$ ,

\operatorname{grad}f(X)=\Big(\overline{\operatorname{grad}h_{r+}([Y])}W_YY^\dagger+\big(\overline{\operatorname{grad}h_{r+}([Y])}W_YY^\dagger\big)^\top(I_p-YY^\dagger)\Big)/2,\qquad\overline{\operatorname{grad}h_{r+}([Y])}=2\operatorname{grad}f(X)YW_Y^{-1},

and if $[Y]$ is a Riemannian first-order stationary point of (18a),

\overline{\operatorname{Hess}h_{r+}([Y])}[\theta,\theta]=\operatorname{Hess}f(X)[\mathcal L^{r+}_Y(\theta),\mathcal L^{r+}_Y(\theta)]\quad\forall\theta\in\mathcal H_Y,

both Hessians have $d=pr-(r^2-r)/2$ eigenvalues, and $\lambda_i(\overline{\operatorname{Hess}h_{r+}([Y])})$ lies between $2\sigma_r(PW_Y^{-1}P^\top)\lambda_i(\operatorname{Hess}f(X))$ and $4\sigma_1(PW_Y^{-1}P^\top)\lambda_i(\operatorname{Hess}f(X))$ .

Milestones

Lemma 6: $Y_1Y_1^\top=Y_2Y_2^\top$ iff $Y_2=Y_1O$ ; $U_1B_1U_1^\top=U_2B_2U_2^\top$ iff $U_2=U_1O$ , $B_2=O^\top B_1O$ ; $\mathcal M_{r+}=\{YY^\top\}=\{UBU^\top\}$ .
Lemma 3: $\mathcal M^e_{r+}$ is a smooth embedded submanifold of dimension $pr-r(r-1)/2$ , with tangent space in the block form (14).
Lemma 4 (i): explicit $\mathcal V_Y$ , $\mathcal H_Y$ and their dimensions.
Lemma 1 on $\mathbb R_*^{p\times r}$ : the total-space gradient is already horizontal.
Proposition 1, embedded bullet: the formulas (19) for $\operatorname{grad}f$ and $\operatorname{Hess}f$ .
Proposition 1, quotient bullet: the formulas (20) for the lifted gradient and Hessian.
Proposition 2: $\mathcal L^{r+}_Y$ is a bijection $\mathcal H_Y\to T_X\mathcal M^e_{r+}$ .
Proposition 2, (23): $2\sigma_r(PW_Y^{-1}P^\top)\bar g_Y(\theta,\theta)\le\|\mathcal L^{r+}_Y\theta\|_F^2\le4\sigma_1(PW_Y^{-1}P^\top)\bar g_Y(\theta,\theta)$ .
Theorem 2: the abstract sandwich inequality for spectra of two quadratic forms related by a bijection with bounded metric distortion.

Significance

Theorem 3 says that at stationary points the two geometries see the same second-order landscape: the Hessians are congruent through $\mathcal L^{r+}_Y$ , so their eigenvalues have the same signs and comparable magnitudes, with explicit factors depending on $W_Y$ and the spectrum of $X$ . The paper derives from it (Corollary 1) that first-order stationary points, second-order stationary points and strict saddles correspond between the embedded and quotient formulations, so a landscape result proved in one geometry transfers to the other. The choice of weight $W_Y$ (flat $I_r$ , right-invariant $(Y^\top Y)^{-1}$ , or $Y^\top Y$ ) changes the comparison constants, which is how the paper relates the conditioning of the two approaches.

The result is proved in the paper; it is not formalized anywhere. A formal development adds machine-checked Riemannian gradients and Hessians on a concrete embedded submanifold and on a concrete quotient, a checked horizontal-space computation, and a reusable abstract sandwich theorem for max–min eigenvalues. Corollary 1 and the parallel results for the polar factorization and for general rank- $r$ matrices (Theorems 4–7) are natural follow-up missions on the same definitions.

Difficulty

The identities (19), (20) and (34) are matrix calculus once the geometric objects are pinned down; the difficulty is that the definitions are intrinsic. The embedded Hessian requires differentiating the tangent projection $P_{T_X\mathcal M^e_{r+}}$ along the manifold, which produces the curvature term $2\langle\nabla f(X),U_\perp D\Sigma^{-1}D^\top U_\perp^\top\rangle$ ; the obvious computation that ignores the moving tangent space gives the wrong Hessian. The quotient Hessian involves the derivative of the weight $W_Y$ and needs the horizontal-space description of Lemma 4 to see that the projection in (5) can be dropped. Identifying $\operatorname{span}$ of the tangent cone with the block form (14) needs an explicit chart of the rank- $r$ PSD set. The final sandwich requires a max–min (Courant–Fischer) argument relative to two different inner products, and the order of the bounds flips for negative eigenvalues.

Formalization scope

$\mathbb R^{a\times b}$ is EuclideanSpace ℝ (Fin a × Fin b) (Frobenius inner product) with matrix views toMat/ofMat. The weight $W$ takes values in $\mathbb R^{r\times r}$ in the same form so that $\mathrm DW_Y$ is defined.
The embedded tangent space and Riemannian gradient are the published platform definitions ProjLikeRetr.Retractor.tangentSpace (span of the tangent cone) and ZORiem.RGD.rgrad (projected Euclidean gradient); "smooth embedded submanifold of dimension $d$ " is the published coordinate-slice predicate ProjLikeRetr.Retractor.IsSubmanifold k d, for every $k$ .
The embedded Hessian is a curve-defined predicate on a quadratic form; the quotient Hessian is the Koszul-formula form $\bar g_Y(\mathrm DG[\theta],\theta)+\tfrac12\mathrm D\bar g(\theta,\theta)[G]$ . Neither is defined by the paper's formulas (19), (20) or (34): those are theorems, and a formalization that defined the Hessians or gradients by them would make the mission trivial.
$\lambda_k$ is the max–min value over $k$ -dimensional subspaces (the paper's Lemma 13); "sandwiched between $a$ and $b$ " means $\min(a,b)\le\mu\le\max(a,b)$ ; $\sigma_1,\sigma_r$ of the symmetric positive definite $PW_Y^{-1}P^\top$ are its extreme Rayleigh quotients.
Conventions: $0<r\le p$ ; $f$ is $C^2$ and symmetric; $W_Y$ is positive definite on $\mathbb R_*^{p\times r}$ and $W$ is smooth there (the meaning of "Riemannian metric"); " $U$ spans the top $r$ eigenspace of $YY^\top$ " is $U^\top U=I_r$ , $UU^\top Y=Y$ ; $Y^\dagger=(Y^\top Y)^{-1}Y^\top$ ; $\mathcal L^{r+}_Y$ is defined as $Y\theta^\top+\theta Y^\top$ rather than by the block formula (22).
In Theorem 2 the map $\mathcal L$ is assumed linear, as in every application in the paper, and the printed domain $\mathcal H_X$ in (12)–(13) is read as $\mathcal H_Z$ .
Not encoded: the half of Lemma 3 about general rank- $r$ matrices, Lemma 4 (ii) (no quotient-manifold structure in Mathlib), the polar factorization geometry and Theorems 4–7, Corollaries 1–2.

Useful contributions include Mathlib-level lemmas on the tangent cone of the rank- $r$ PSD set, Courant–Fischer for a form relative to a non-standard inner product, and matrix-calculus lemmas for $\mathrm D(W^{-1})$ .

Selected references

Y. Luo, X. Li, A. R. Zhang, On Geometric Connections of Embedded and Quotient Geometries in Riemannian Fixed-rank Matrix Optimization, Mathematics of Operations Research, 2024; arXiv:2110.12121v2. https://arxiv.org/abs/2110.12121
P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244
M. Journée, F. Bach, P.-A. Absil, R. Sepulchre, Low-rank optimization on the cone of positive semidefinite matrices, SIAM Journal on Optimization 20(5), 2010. https://doi.org/10.1137/080731359
B. Vandereycken, S. Vandewalle, A Riemannian optimization approach for computing low-rank solutions of Lyapunov equations, SIAM J. Matrix Anal. Appl. 31(5), 2010. https://doi.org/10.1137/090764566
R. Bhatia, Matrix Analysis, Springer GTM 169, 1997. https://doi.org/10.1007/978-1-4612-0653-8

14 thms1 active userReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Technical Note—Global Robust Stability in a General Price and Assortment Competition Model: Robust Best-Response Price Dynamics Contract Geometrically to the Special Equilibrium from Any StartResearch Paper

Motivation

Retailers that sell many products set prices against one another, and the demand for each product depends on the prices of all of them. Affine demand models, $q(p)=a-Rp$ , are the standard starting point for this kind of multi-product price competition in operations management and industrial organization. Two questions follow once an equilibrium is known to exist. Can the firms reach it, and does it matter where they start? A Nash equilibrium that the firms cannot find by adjusting their prices tells little about what prices will actually be observed.

Federgruen and Hu (Operations Research 69(1), 2021; submitted manuscript at SSRN 3010503) answer this for a general multi-firm, multi-product model with an arbitrary number of firms and arbitrary product assortments. The game has features that defeat the usual tools. Once the affine demands are extended so that no demand turns negative, the game is in general not supermodular. Example 1 of the paper, after McGuire and Staelin (1983/2008), is a duopoly that is not supermodular and has a continuum of equilibria. Earlier work (Federgruen and Hu, Operations Research 63(3), 2015) characterized the equilibria. One of them, the special equilibrium $(p^*|w)$ , has a closed form. The 2021 paper shows that this equilibrium is reached from any starting price vector when every firm repeatedly plays a robust best response.

Setting

A finite set $\mathcal N$ of products is partitioned among firms. Firm $i$ sells the products $\mathcal N(i)$ . The foundational demands are

q(p)=a-Rp,\qquad a\ge 0,

where $R$ is an $\mathcal N\times\mathcal N$ price-sensitivity matrix subject to three assumptions:

(P) $R$ is positive definite in the quadratic-form sense: $x^\top Rx>0$ for all $x\ne 0$ . $R$ need not be symmetric.
(Z) $R$ is a Z-matrix: $R_{lm}\le 0$ for $l\ne m$ , so the products are substitutes.
(IS) $R$ is symmetric within each firm: $R_{lm}=R_{ml}$ when $l,m\in\mathcal N(i)$ .

Each firm has a cost vector, $w\in\mathbb R^{\mathcal N}_{++}$ . Let $T(R)$ be the block-diagonal matrix of the transposed firm blocks $R^\top_{\mathcal N(i),\mathcal N(i)}$ , and let $\Psi(R)=T(R)[R+T(R)]^{-1}$ and $Q(w')=\Psi(R)a-\Psi(R)Rw'$ . The cost projection $w'=\Theta(w)$ solves the linear complementarity problem

w'\le w,\qquad Q(w')^\top(w-w')=0,\qquad Q(w')\ge 0,

and the special equilibrium is

(p^*|w)=w'+[R+T(R)]^{-1}(a-Rw').

Given the other firms' prices $p_{-\mathcal N(i)}$ , firm $i$ sees the residual intercept $\alpha=a_{\mathcal N(i)}-R_{\mathcal N(i),-\mathcal N(i)}p_{-\mathcal N(i)}$ . Its robust best response maximizes

(x-w_{\mathcal N(i)})^\top(\alpha-R_{\mathcal N(i),\mathcal N(i)}x)\quad\text{over } x\ge 0,\ \alpha-R_{\mathcal N(i),\mathcal N(i)}x\ge 0.

Prices are restricted to keep the firm's own affine demands nonnegative, so the firm needs only its own demand and cost data. Collecting all firms gives the map $RB$ , and $RB^{(n)}$ is its $n$ -fold iterate. Finally, $\Lambda(R)=I-[T(R)]^{-1}R$ .

Formalization targets

Goal: Theorem 3 (global robust stability)

There exist a norm $\|\cdot\|$ on $\mathbb R^{\mathcal N}$ and a constant $0<\gamma<1$ such that

\|RB(\hat p)-RB(\tilde p)\|\le\gamma\|\hat p-\tilde p\|\quad(\hat p,\tilde p\ge 0),

\|RB^{(n)}(p)-(p^*|w)\|\le\gamma^n\|p-(p^*|w)\|,\qquad \lim_{n\to\infty}RB^{(n)}(p)=(p^*|w)\quad(p\ge 0).

Neither the norm nor $\gamma$ is fixed, because the paper asserts only that they exist.

Milestones

The milestones follow the paper's own proof:

Lemma 1: $RB$ is well defined.
The proof of Theorem 2: the projection LCP has a unique, nonnegative solution.
Theorem 2: $(p^*|w)$ is a fixed point of $RB$ .
Lemma B.1(a), (c), (e), (f), (g): the M-matrix lemmas.
Lemma 2: the per-firm comparison of robust best responses.
Three claims from the proof of Theorem 3(a):
- the componentwise bound $|RB(\hat p)-RB(\tilde p)|\le\Lambda(R)|\hat p-\tilde p|$ ;
- $\Lambda(R)\ge 0$ with spectral radius $\rho(\Lambda(R))<1$ ;
- for every $\varepsilon>0$ , an absolute norm whose induced norm satisfies $\|\Lambda(R)\|\le\rho(\Lambda(R))+\varepsilon$ .

Significance

Theorem 3 makes the special equilibrium an operational prediction. Firms that adjust prices myopically, each using only its own demand and cost information, converge to $(p^*|w)$ from any start. The convergence is geometric, so the number of rounds needed to come within $\epsilon$ grows only logarithmically in the initial distance. This holds although the game is not supermodular and can have infinitely many equilibria, so the lattice-theoretic stability results that cover supermodular games do not apply. Theorem 2 also identifies which of the possibly many equilibria the dynamics select.

The result is proved in the paper, but it has not been formalized. A machine-checked version has two parts: a model layer (affine multi-product demand, the cost projection, robust best responses), and an M-matrix layer (Lemma B.1: inverse-positivity, Schur complements of inverse M-matrices, spectral radius bounds). Mathlib has neither. The proof also rests on results that the paper cites without proof: Propositions 2 and 3 of Federgruen and Hu (2015), and Theorem 4(b) and Lemma B.2(d) of Federgruen and Hu (2016). A formalization has to supply them. In one place the proof cites Horn and Johnson (1985, Lemma 5.6.10) for an absolute norm close to the spectral radius. As stated there, that lemma does not give absoluteness for general matrices: $\begin{pmatrix}1&1\\-1&-1\end{pmatrix}$ has spectral radius $0$ , but every absolute norm gives it induced norm at least $1$ . The claim holds for the nonnegative matrix $\Lambda(R)$ , and the corresponding milestone is stated for that matrix only.

Difficulty

The obvious route is to show that $RB$ is a contraction in the sup norm and invoke Banach's fixed-point theorem. This fails: $\|\Lambda(R)\|_\infty$ can exceed $1$ even though $\rho(\Lambda(R))<1$ , and the bound $|RB(\hat p)-RB(\tilde p)|\le\Lambda(R)|\hat p-\tilde p|$ is all the structure gives. The norm must be adapted to $\Lambda(R)$ and must also be absolute, so that the componentwise bound transfers. The per-firm estimate behind that bound (Lemma 2) is itself not a Lipschitz estimate for an explicit formula. The robust best response is the solution of a constrained quadratic program whose active set changes with the competitors' prices, and the comparison goes through a componentwise minimum $\check p=\min\{\hat p,\tilde p\}$ and monotonicity in the intercept. Separately, the fixed-point property needs the cost projection $\Theta(w)$ , an LCP whose unique solvability and nonnegativity depend on (IS).

Formalization scope

Products form a finite type ι and firms a type F, with firm : ι → F assigning each product to its firm. Vectors are ι → ℝ with the pointwise order. Matrices are Matrix ι ι ℝ, and every matrix inequality is entrywise. The commitments are:

(P) is ∀ x ≠ 0, 0 < x ⬝ᵥ R *ᵥ x, not Mathlib's Matrix.PosDef, which would add global symmetry.
The special equilibrium $(p^*|w)$ is written through any solution $w'$ of the LCP (12)–(14). The paper says this form is valid for all $w>0$ . A milestone proves that the solution exists, is unique, and is nonnegative.
The robust best response is a relation, " $q$ is a robust best response to $p$ ", with the feasibility constraint of (8) built in. Lemma 1 makes it single-valued. Part (b) of the goal is stated for every robust best-response sequence started at $p^0\ge 0$ .
"A norm on $\mathbb R^{\mathcal N}$ " is a seminorm that vanishes only at $0$ .
The spectral radius is that of the matrix viewed over $\mathbb C$ , so complex eigenvalues count.
Matrix inverses use Mathlib's ⁻¹. Every inverted matrix is invertible under the hypotheses.

No trivializing reading is available. The norm must be definite, the robust best response keeps its feasibility constraint and is never defined by a closed form, and the convergence statement holds for every iterate. A sorry-free sanity check confirms that the standing assumptions, the cost projection and the fixed-point relation are all satisfiable on a two-firm example.

The following results are not formalized here:

Theorem 1 and Proposition 1, which characterize the set of Nash equilibria and the existence of $(p^*|w)$ under the full LCP-extended demand. They are independent of the goal.
Example 1, Lemma B.2, Lemma C.1 and Proposition 2 of Appendix D.

Contributions that would be reusable beyond this mission include:

a general M-matrix library (inverse-positivity, Schur complements, Perron–Frobenius bounds);
uniqueness for P-matrix LCPs;
the existence of absolute norms close to the spectral radius for nonnegative matrices.

Selected references

A. Federgruen, M. Hu, Technical Note—Global Robust Stability in a General Price and Assortment Competition Model, Operations Research 69(1) 164–174, 2021. https://doi.org/10.1287/opre.2020.2001 (submitted manuscript: https://ssrn.com/abstract=3010503)
A. Federgruen, M. Hu, Multi-Product Price and Assortment Competition, Operations Research 63(3) 572–584, 2015.
A. Federgruen, M. Hu, Sequential Multiproduct Price Competition in Supply Chain Networks, Operations Research 64(1) 135–149, 2016.
R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985; Topics in Matrix Analysis, Cambridge University Press, 1991.
I. N. Imam, The Schur complement and the inverse M-matrix problem, Linear Algebra and its Applications 62 235–240, 1984.
T. W. McGuire, R. Staelin, An industry equilibrium analysis of downstream vertical integration, Marketing Science 27(1) 115–130, 2008 (reprint of Marketing Science 2(2), 1983).

15 thms1 active userReviewed

Mathematical Physics Quantum Information·Captain: mikedeng1

Quantum computation, quantum state engineering, and quantum phase transitions driven by dissipation: The DQC Liouvillian Has a Unique Steady State Encoding the Circuit and a Gap Above 1/T²Research Paper

Motivation

A quantum circuit normally applies a sequence of gates to a prepared state. Verstraete, Wolf and Cirac proposed a different physical route: couple a quantum system to a memoryless environment so that dissipation drives it toward a state recording the circuit's computation. Their dissipative quantum computation construction places a clock beside the computational qubits and makes the circuit history a stationary state of a time independent master equation. A useful process must have a well identified stationary state and a rate of relaxation that does not collapse with the number of qubits or with the chosen gates. The paper argues for these properties in its DQC section and its efficiency appendix (Verstraete, Wolf and Cirac, 2008, pp. 1–2, 4–5).

The printed spectral gap formula and part of its supporting clock block do not describe the slowest decay of the stated generator. Direct finite dimensional calculations reveal a slower coherence sector. This mission therefore targets the stated stationary state and a corrected, explicitly ranged version of the paper's lower bound. The discrepancies and boundary cases are recorded in the formalization scope so that the target is a mathematical claim about the displayed Lindblad operators rather than an unchecked transcription.

Setting

Fix $N\geq 0$ qubits and $T\geq 0$ circuit steps. A computational basis string is a function from the $N$ qubit positions to $\{0,1\}$ . The clock register has basis $|t\rangle$ for $t=0,\ldots,T$ . A family of unitary gates $U_1,\ldots,U_T$ acts on the qubit register. Its history vectors are $|\psi_0\rangle=|0\cdots0\rangle$ and $|\psi_t\rangle=U_t\cdots U_1|0\cdots0\rangle$ .

A jump operator resets qubit $i$ only when the clock is at zero: $L_i=|0\rangle_i\langle1|\otimes|0\rangle\langle0|$ . For each neighboring clock pair, another jump operator moves in both directions, applying the relevant gate on the forward move and its adjoint on the reverse move. The Lindblad generator is the linear map on matrices

\mathcal L(\rho)=\sum_k\left(L_k\rho L_k^\dagger-\frac12(L_k^\dagger L_k\rho+\rho L_k^\dagger L_k)\right).

There is no Hamiltonian term. The proposed history state is the normalized density matrix

\rho_0=\frac1{T+1}\sum_{t=0}^{T}|\psi_t\rangle\langle\psi_t|\otimes|t\rangle\langle t|.

These are equations (1)–(4) of the paper, with the clock step index repaired as described below. The appendix introduces a gate removal unitary $W$ , a connected clock path matrix $L_{00}$ , and clock blocks with a penalty at time zero. Their spectra lead to the uniqueness and decay claims (paper, pp. 2, 4–5).

Formalization targets

Main goal

For every $N\geq0$ , $T\geq2$ , and family of unitary gates, prove that $\mathcal L(\rho_0)=0$ , that $\rho_0$ is positive semidefinite with trace one, and that the full kernel of $\mathcal L$ consists of scalar multiples of $\rho_0$ . For $T\geq5$ , prove additionally that every nonzero eigenvalue $\mu$ satisfies

\operatorname{Re}(\mu)<-\frac1{T^2}.

The bound applies uniformly across the number of qubits and the circuit gates. It is the corrected form of the efficiency conclusion on p. 5. The goal does not assert the printed formula $\Delta=\pi^2/(2T+3)^2$ , which is contradicted by the slowest coherence sector (paper, pp. 2, 5).

Supporting targets

The milestones first establish stationarity and removal of the circuit gates by $W$ . They then target the one dimensional fixed space for identity gates, the first nonzero eigenvalue of the connected clock path, the penalized clock blocks, and the full generator's bound for identity gates. This follows the sequence of reductions described in the efficiency appendix while retaining the paper's exact clock constants where they are valid (paper, pp. 4–5).

Significance

The kernel statement identifies every stationary matrix, a stronger assertion than merely finding one stationary density matrix. The eigenvalue bound supplies a uniform spectral scale for the finite dimensional generator, independent of the circuit content. Together these make precise the part of dissipative computation that says the intended history is singled out and spectrally separated from other modes. A convergence time theorem would also have to control Jordan blocks or the operator semigroup and is outside this target; the paper itself notes this separate issue on p. 5 (paper, p. 5).

Formalizing the corrected claim creates a reusable finite matrix representation of a Lindblad generator and a circuit clock, plus independently usable path and boundary penalty spectral statements. The paper result is known in physics prose; these exact Lean statements are open proof goals in this proposal. The correction also prevents later arguments from importing a spectral equality that does not hold for the displayed process.

Difficulty

The gate operators couple the qubit register to the clock, so diagonalizing a clock matrix alone does not describe the generator. Even after the gates are removed, the Liouvillian acts on matrices, including coherences between two qubit states and two clock times. The decay of a one sided coherence at clock zero carries half the penalty of a population term. Reading every nonzero sector as if it had the population penalty produces the printed gap value and misses the slowest mode. The clock path also has to retain the first edge and its endpoint diagonal entries; omitting that edge changes the spectrum.

Formalization scope

Lean uses matrices indexed by $N$ bit strings paired with the finite clock $\{0,\ldots,T\}$ , and a complex linear endomorphism on those matrices. Gates are quantified as unitary matrices; they may act on all qubits, whereas the paper starts with nearest neighbor gates. The appendix's spectral argument is independent of that locality, so this is a disclosed generalization. The model also permits $N=0$ . Gates use zero based indexing: Lean's $U(t)$ is the paper's $U_{t+1}$ and acts on the step $t\to t+1$ . This repairs equation (3), which otherwise calls for both an undefined $U_0$ and an out of range clock state $|T+1\rangle$ .

Uniqueness is restricted to $T\geq2$ : at $T=1$ an additional clock coherence is stationary. The strict $1/T^2$ bound is restricted to $T\geq5$ : direct diagonalization shows it fails for $T=1,2,3,4$ . The paper's printed corner coefficient $-2$ is correct for a population sector, but a one sided coherence has coefficient $-3/2$ . A milestone states the valid printed matrix fact and the corrected bound for all clock zero penalties $a\geq1/2$ . The connected path matrix follows the displayed spectral formula rather than the printed tridiagonal sum whose range omits the first edge.

The generator is defined from the jump operators by equation (1). It is not defined from the desired block decomposition or eigenvalues. The spectral assertion quantifies over actual nonzero complex eigenvalues and compares their real parts directly; no default valued infimum defines a gap. Work toward the mission may supply matrix identities, unitary covariance, tridiagonal spectra, or a direct finite dimensional analysis of the generator. The generic finite matrix Lindblad definition can be reused independently of this circuit model.

Selected references

Frank Verstraete, Michael M. Wolf, and J. Ignacio Cirac, Quantum computation, quantum state engineering, and quantum phase transitions driven by dissipation, arXiv:0803.1447v2, 2008; later Nature Physics 5, 633–636 (2009). Pinned preprint.

9 thms1 active userReviewed

Algebra Category Theory·Captain: mikedeng1

Higher-Dimensional Algebra VI: Lie 2-Algebras: The Category of Semistrict Lie 2-Algebras Is Equivalent to the Category of 2-Term L∞-AlgebrasResearch Paper

Motivation

An ordinary Lie algebra has a vector space and an antisymmetric bracket satisfying the Jacobi identity. In a Lie 2-algebra, the vectors become the objects of a linear category, and the Jacobi identity is witnessed by a morphism called the Jacobiator. This lets the Jacobi identity hold coherently rather than as a strict equation. Baez and Crans developed this notion to make the relation between categorified Lie algebra structures and short chain complexes precise (Baez–Crans, §§3–4). The result of interest here is their equivalence between semistrict Lie 2-algebras and two-term $L_\infty$ -algebras, Theorem 36.

Setting

A 2-vector space is a category internal to vector spaces over a field $k$ : its objects $V_0$ and morphisms $V_1$ are vector spaces; source $s$ , target $t$ , identity $i$ , and composition are linear. Composition is read in diagrammatic order, so $fg$ means first $f$ , then $g$ . The identity laws require $s(i(x))=t(i(x))=x$ . Lemma 6 shows that linearity forces the composition of composable $f$ and $g$ to be

fg=f+g-i(t(f)).

The arrow part of $f$ is $\vec f=f-i(s(f))\in\ker s$ . It remembers the displacement of $f$ after its source is translated to zero. A 2-vector space can therefore be compared with the two-term complex $\ker s\xrightarrow{t}V_0$ . Conversely, a complex $C_1\xrightarrow{d}C_0$ gives arrows $(x,h)\in C_0\oplus C_1$ with source $x$ , target $x+d h$ , and identity $(x,0)$ (Baez–Crans, Proposition 8).

A semistrict Lie 2-algebra is a 2-vector space with a skew-symmetric bilinear bracket functor and a completely antisymmetric trilinear natural isomorphism

J_{x,y,z}: [[x,y],z]\longrightarrow[x,[y,z]]+[[x,z],y].

The Jacobiator obeys the Jacobiator identity, an equality between two composites of morphisms through the octagon in Definition 22. A homomorphism $F$ is a linear functor equipped with a bilinear natural transformation $F_2(x,y):[F_0x,F_0y]\to F_0[x,y]$ satisfying Definition 23’s square. The resulting one-cell category is $\mathrm{Lie2Alg}$ (Baez–Crans, pp. 18–21).

A 2-term $L_\infty$ -algebra has vector spaces $V_1,V_0$ , a differential $d:V_1\to V_0$ , brackets $l_2$ of degrees adding to at most one, and a trilinear map $l_3:V_0^3\to V_1$ . Its equations are precisely (a)–(i) of Lemma 33. In particular, $d(l_3)$ measures the failure of the ordinary Jacobi identity, and equation (i) is its four-input coherence law. Homomorphisms $\varphi=(\varphi_0,\varphi_1,\varphi_2)$ are chain maps with a skew bilinear comparison map satisfying all three equations of Definition 34. They form $\mathrm{2Term}L_\infty$ (Baez–Crans, pp. 28–30).

Formalization targets

The goal is Theorem 36, an equivalence of the two one-cell categories:

\mathrm{Lie2Alg}\simeq\mathrm{2Term}L_\infty.

The milestone path begins with Lemma 6’s forced composition law. Proposition 8 states the underlying linear equivalence $\mathrm{2Vect}\simeq\mathrm{2Term}$ , and the 2-cell part of Theorem 12 identifies linear natural transformations between linear functors with chain homotopies between the corresponding chain maps, through their arrow parts. Propositions 25 and 35 establish identity, composition, and associativity for the homomorphisms on each side. Equation (3) reconciles the two expressions for the bracket of morphisms under the construction $T$ . The proof of Theorem 36 then supplies $T$ on objects and morphisms and the reverse construction $S$ . The goal additionally requires functoriality and natural isomorphisms, which the paper asks the reader to check or construct (Baez–Crans, pp. 30–36).

Significance

The equivalence says that the categorical and chain-complex descriptions carry the same one-cell algebraic information. It permits constructions expressed with morphisms, functors, and a Jacobiator to be studied with a differential and higher brackets, and conversely. Later classifications of skeletal Lie 2-algebras in the paper use the two-term viewpoint (Baez–Crans, §§5–6).

Theorem 36 is proved in the cited paper; the machine-checked proof is the work this mission seeks. The local files compile the definitions and open theorem statements, and a sorry-free check exhibits nonzero carriers satisfying the principal structures. The milestones expose the individual obligations that a complete Lean proof must discharge. This mission does not claim a formal proof of the result or of the stronger 2-categorical statement.

Difficulty

A bilinear bracket on objects and morphisms is not enough to define a bracket functor: it must preserve source, target, identity, and simultaneous composition. In the $T$ direction, two ways of decomposing a pair of morphisms suggest different bracket formulas. Their equality is equation (3), using Lemma 33(f). In the $S$ direction, the interaction of two degree-one elements comes from the bracket functor’s preservation of a commuting square. The Jacobiator’s naturality and octagon must then correspond to the remaining $L_\infty$ identities. Finally, the constructions must act on homomorphisms and yield natural isomorphisms of functors (Baez–Crans, pp. 31–36).

Formalization scope

The field $k$ has characteristic different from two in Theorem 36 and its §4.3 milestones, matching the standing assumption on p. 27. The §3 and §4.1 results retain the paper’s broader field convention. All vector spaces are unrestricted in dimension. A 2-vector space stores $V_0,V_1,s,t,i$ and defines its composition by Lemma 6. A 2-term $L_\infty$ -algebra is represented directly by Lemma 33(a)–(i), with $[h,x]=-[x,h]$ and $[h,k]=0$ ; the general graded Definition 32 is outside scope.

The two categories are represented by raw object and morphism data with explicit predicates for lawful homomorphisms. An equivalence consists of functors preserving lawful morphisms, identities, and composites, together with natural isomorphisms in both directions. This representation keeps Propositions 25 and 35 as proof obligations and expresses the one-categorical content of Theorem 36. The stronger Theorem 39 asserts a 2-equivalence, but its 2-cell work is left without proof in the source and is not the goal here.

The Lie 2-algebra side retains the bracket’s functoriality on composable morphisms, the full naturality square, and the Jacobiator octagon. Its coherence is not replaced by Lemma 33’s equations: doing so would collapse the goal into a comparison of two copies of the same definition. The infrastructure for two-term complexes, 2-vector spaces, raw categories, curried multilinear maps, and their homomorphisms is reusable. Of Theorem 12 only the 2-cell correspondence is stated; the 2-functoriality of $S,T$ and the 2-naturality of the comparison isomorphisms are not. Of Proposition 25 only the one-cell category laws are stated; the 2-homomorphisms of Definition 24 are not. A formalization in which the Lie 2-algebra side is defined by arrow-part equations, or in which the equivalence omits the natural isomorphisms or the category laws, would trivialize the goal and is excluded. Contributions proving the displayed category laws, the $S$ and $T$ constructions, their functoriality, and the two natural isomorphisms are welcome.

Selected references

John C. Baez and Alissa S. Crans, Higher-Dimensional Algebra VI: Lie 2-Algebras, arXiv:math/0307263v6, 2010 preprint. arXiv
John C. Baez and Alissa S. Crans, Higher-Dimensional Algebra VI: Lie 2-Algebras, Theory and Applications of Categories 12 (2004), 492–538 (journal version; theorem numbers in this mission follow the arXiv v6). TAC

12 thms1 active userReviewed

Differential Geometry Mathematical Physics·Captain: mikedeng1

Geometrization of Quantum Mechanics: The Unitary Momentum Map Pulls Back the Lie and Jordan Tensors of the Observables to the Kähler Structure of Hilbert SpaceResearch Paper

Motivation

Quantum mechanics is usually written in linear-algebraic terms: states are vectors of a complex Hilbert space, observables are Hermitian operators, and expectation values pair the two. Classical mechanics is written geometrically: states form a symplectic manifold, observables are functions on it, and dynamics is a Hamiltonian flow. A line of work starting with Kibble (1979) and continued by Cirelli, Lanzavecchia, Heslot, Ashtekar–Schilling (arXiv:gr-qc/9706069) and Brody–Hughston (arXiv:quant-ph/9906086) recasts quantum mechanics in the classical language: the Hilbert space, seen as a real manifold, carries a Kähler structure (a symplectic form, a Euclidean metric and a compatible complex structure), and observables become real quadratic functions on it.

Cariñena, Clemente-Gallardo and Marmo (arXiv:math-ph/0701053v2) organise this correspondence around one map, the momentum map of the unitary group acting on Hilbert space. The algebra of observables carries two products, a Lie product (the commutator) and a Jordan product (the anticommutator). The paper's Proposition 5 states that the momentum map carries both products, read as tensors on the dual of the unitary Lie algebra, to the symplectic and Euclidean parts of the Kähler structure of Hilbert space. This mission formalizes that statement in finite dimension.

Setting

Fix $n\in\mathbb N$ and let $\mathcal H=\mathbb C^n$ , with $\langle\psi|\phi\rangle=\sum_k\overline{\psi_k}\phi_k$ . The space of observables $\mathcal O$ is the real vector space of Hermitian $n\times n$ complex matrices. On it the paper defines:

the isomorphism $\alpha(A)=iA$ onto the Lie algebra $\mathfrak u(n)$ of anti-Hermitian matrices, eq. (2);
the Lie product $[A,B]_-=\alpha^{-1}(\alpha(A)\alpha(B)-\alpha(B)\alpha(A))=i(AB-BA)$ , eq. (3);
the scalar product $\langle A,B\rangle=\tfrac12\operatorname{Tr}(AB)$ , eq. (4);
the Jordan product $A\circ B=\tfrac12(AB+BA)$ , eq. (6).

Through (4), the dual $\mathfrak u^*(n)$ is identified with Hermitian matrices $\xi$ . Each observable $A$ gives a linear function $\widehat A(\xi)=\tfrac12\operatorname{Tr}(\xi A)$ . On $\mathfrak u^*(n)$ the paper defines the Lie–Poisson tensor (11), $\Lambda(d\widehat A,d\widehat B)(\xi)=\tfrac i2\operatorname{Tr}\,\xi(\alpha(A)\alpha(B)-\alpha(B)\alpha(A))$ , and the Jordan tensor (12), $\mathcal R(\xi)(d\widehat A,d\widehat B)=\tfrac12\operatorname{Tr}\,\xi(AB+BA)$ .

On the Hilbert space side, use real coordinates $z_k=q_k+ip_k$ . Every complex matrix $A$ defines the quadratic function $f_A(\psi)=\tfrac12\langle\psi|A\psi\rangle$ . The canonical Poisson bracket is $\{f,g\}=\sum_k(\partial_{q_k}f\,\partial_{p_k}g-\partial_{p_k}f\,\partial_{q_k}g)$ , and the contravariant Euclidean structure is $G=\sum_k(\partial_{q_k}\otimes\partial_{q_k}+\partial_{p_k}\otimes\partial_{p_k})$ . The momentum map is

\mu:\mathbb C^n\to\mathfrak u^*(n),\qquad \mu(\psi)=\rho_\psi=|\psi\rangle\langle\psi| .

Formalization targets

Goal: Proposition 5 (p. 12)

For Hermitian $A,B$ and every $\psi\in\mathbb C^n$ :

\widehat A(\mu(\psi))=f_A(\psi),\qquad \{f_A,f_B\}(\psi)=\Lambda(d\widehat A,d\widehat B)(\mu(\psi)),\qquad G(df_A,df_B)(\psi)=\mathcal R(\mu(\psi))(d\widehat A,d\widehat B).

In the paper's notation: $\mu^*(\widehat A)=f_A$ , $\mu^*(\{\widehat A,\widehat B\})=\{f_A,f_B\}$ and $\mu^*(\mathcal R(d\widehat A,d\widehat B))=G(\mu^*(d\widehat A),\mu^*(d\widehat B))$ .

Milestones

In attack order:

Lemma 5 (p. 12): $f_A$ is real-valued for all $\psi$ if and only if $A$ is Hermitian.
Lemma 1 (p. 4), in two parts:
- $[\cdot,\cdot]_-$ makes $\mathcal O$ a real Lie algebra, isomorphic to $\mathfrak u(n)$ through $\alpha$ ;
- $\tfrac12\operatorname{Tr}(AB)$ is a real, symmetric, positive definite scalar product, invariant under $A\mapsto UAU^\dagger$ .
Lemma 2 (p. 5): $(\mathcal O,\circ)$ is a Jordan algebra.
Proposition 1 (p. 5): the scalar product is invariant for both products (7), and $\mathrm{ad}_-$ is a derivation of $\circ$ (8).
Lemma 3 (p. 5): $\mathcal O$ is a Jordan–Lie algebra. This means the Lie and Jordan algebra axioms hold, (8) holds together with the associator identity (9), $(A\circ B)\circ C-A\circ(B\circ C)=\tfrac14\hbar[[A,C]_-,B]_-$ , here with $\hbar=1$ .
Equivariance (§3.1.1, p. 11): $\mu$ takes values in $\mathfrak u^*(n)$ and $\mu(U\psi)=U\mu(\psi)U^\dagger$ for unitary $U$ .

Significance

Proposition 5 says that the algebra of observables can be read off Hilbert space geometrically:

commutators of observables become Poisson brackets of their expectation-value functions;
anticommutators become the metric pairing of their gradients.

This is the dictionary behind geometric treatments of the Schrödinger equation as a Hamiltonian flow. It also underlies variance and uncertainty relations written through the metric, and the reduction to projective space and density states that the paper discusses in §§2.5 and 4. The paper presents it as an alternative to the GNS construction for pure states.

The paper's proof is "Direct verification", and Lemmas 1–3 and Proposition 1 are classical facts about Hermitian matrices. No step is open. What the mission adds is a machine-checked version with every normalisation pinned, as listed in Formalization scope:

the factors ½ in (4), (6) and $f_A$ ;
the factor $i/2$ in (11);
$\hbar=1$ in (9).

The paper uses both the Hermitian picture (3), (4), (6) and the anti-Hermitian picture (5), (11). The formal statement fixes the signs and factors needed to read their relation precisely. The prior-art search for this mission found no published Prove2Me statement with the same finite-dimensional objects and conclusion.

Difficulty

The algebraic milestones are short computations once the definitions are unfolded. The work concentrates in the goal, whose two sides live in different worlds.

The left side is built from real partial derivatives of real-valued functions on $\mathbb C^n$ , viewed as $\mathbb R^{2n}$ . Its derivatives must be computed in the directions $e_k$ and $ie_k$ and then recombined into complex inner products.

The right side is a trace of a product of matrices with the rank-one matrix $|\psi\rangle\langle\psi|$ .

The difficulty is that the derivative formulas use real coordinates while the tensor formulas use complex matrix products and traces. Their normalizations and sign conventions must agree at the level of the full identity, including the $i$ in $\alpha(A)$ and the factors of $\tfrac12$ in the quadratic functions.

Replacing the derivative-defined brackets by their closed forms would make the goal trivial and is not permitted, see below.

Formalization scope

All objects are defined in one definitions module in the namespace GeomQM.MomentumMap, over Mathlib's Matrix (Fin n) (Fin n) ℂ and vectors Fin n → ℂ.

Committed conventions.

Observables carry an explicit IsHermitian hypothesis. Lemma 5 is about an arbitrary complex matrix, and equivariance needs no hypothesis. $n=0$ is allowed, since every statement then holds trivially, as in the paper.
$\partial/\partial q_k$ and $\partial/\partial p_k$ are fderiv ℝ applied to Pi.single k 1 and Pi.single k I. This is the paper's $z_k=q_k+ip_k$ .
$f_A$ is defined as the complex number $\tfrac12\langle\psi|A\psi\rangle$ , and the real function used in the goal is its real part. Lemma 5 is stated on the complex value, so that it is not vacuous.
$\mathfrak u^*(n)$ is the space of Hermitian matrices. $\widehat A$ uses the pairing (4), $\tfrac12\operatorname{Tr}(\xi A)$ , not the pairing (5), which differs by a factor $i$ on $\alpha(A)$ and would change the sign.
$\Lambda$ is (11) applied literally to $\alpha(A),\alpha(B)$ . The shortcut $\widehat{[A,B]_-}$ has the opposite sign.
$\mathcal R$ is the right-most expression of (12).
The real-valued tensors take the real part of trace expressions that are real for Hermitian arguments.
The second bracket $\{f_1,f_2\}_+$ displayed on p. 12 is not used, because Proposition 5 names $G$ .

Ruled out. The brackets on $\mathbb C^n$ are defined through real derivatives of arbitrary functions, never as $f_{-i[A,B]}$ or $f_{AB+BA}$ . The tensors on $\mathfrak u^*(n)$ are trace formulas, never rewritten as quadratic functions of $\psi$ . Either shortcut would make bullets 2 and 3 hold by definition.

Not in scope. The following are not formalized:

Propositions 2–4: the Poisson structure on all of $\mathcal O^*$ , Lie derivatives of $\mathcal R$ , and generalized distributions;
Lemma 4: linear dynamics preserving both products;
the Rayleigh-quotient statements of §3.4;
the projective-space material of §4.

Welcome contributions. Proofs of the milestones and of the goal, and general lemmas that would be reusable beyond this mission:

derivative formulas for real quadratic forms on Fin n → ℂ;
the identity $\operatorname{Tr}(|\psi\rangle\langle\psi|M)=\langle\psi|M\psi\rangle$ .

Selected references

J. F. Cariñena, J. Clemente-Gallardo, G. Marmo, Geometrization of Quantum Mechanics, arXiv preprint, 2007 (v2). https://arxiv.org/abs/math-ph/0701053v2
T. W. B. Kibble, Geometrization of quantum mechanics, Communications in Mathematical Physics 65, 189–201, 1979. https://doi.org/10.1007/BF01225149
A. Ashtekar, T. A. Schilling, Geometrical formulation of quantum mechanics, in On Einstein's Path, Springer, 1998. https://arxiv.org/abs/gr-qc/9706069
D. C. Brody, L. P. Hughston, Geometric quantum mechanics, Journal of Geometry and Physics 38, 19–53, 2001. https://arxiv.org/abs/quant-ph/9906086
J. Grabowski, M. Kuś, G. Marmo, Geometry of quantum systems: density states and entanglement, Journal of Physics A 38, 10217–10244, 2005. https://arxiv.org/abs/math-ph/0507045
N. P. Landsman, Mathematical Topics Between Classical and Quantum Mechanics, Springer Monographs in Mathematics, 1998. https://doi.org/10.1007/978-1-4612-1680-3

9 thms1 active userReviewed

Information Theory Quantum Information·Captain: mikedeng1

Classical capacity of fermionic product channels: An Explicit Formula for the Gaussian Capacity, Which Equals the One-Shot Capacity for n ≤ 2Research Paper

Motivation

Sending classical messages through a quantum device requires choosing input states that remain distinguishable after noise. The one-shot classical capacity measures the best information rate when each channel use is signaled with a separate input state. For many channels the optimization is difficult because it ranges over all ensembles of quantum states. Fermionic systems provide a finite-dimensional setting in which the noise has a direct description on elementary operators, but the optimal signaling states still need not be obvious. Bravyi's 2005 paper isolates a family of fermionic product channels, computes the best rate from Gaussian input states for any number of qubits, and proves that this restricted rate is the full one-shot rate for one or two qubits.

Setting

The system has $n$ qubits, with computational basis indexed by bit strings $x\in\{0,1\}^n$ . The Jordan–Wigner Majorana operators $c_1,\ldots,c_{2n}$ are tensor products of Pauli matrices: $c_{2j-1}$ has $Z$ on qubits before $j$ , $X$ on qubit $j$ , and identity afterwards; $c_{2j}$ replaces $X$ with $Y$ . Their ordered monomials $c(x)=c_1^{x_1}\cdots c_{2n}^{x_{2n}}$ , $x\in\{0,1\}^{2n}$ , form a basis of all operators on the qubits. The paper gives these operators and their monomials in Eq. (3).

A fermionic product channel $\Phi_b$ is determined by attenuation coefficients $b_p\in[0,1]$ . On each monomial it acts by $\Phi_b(c(x))=(\prod_{p:x_p=1}b_p)c(x)$ , and linearity defines it on every operator. A state is a positive semidefinite matrix of trace one. For a finite ensemble of output states $\{(p_a,\rho_a)\}$ , with nonnegative weights summing to one, its Holevo quantity in bits is

\chi= S\!\left(\sum_a p_a\rho_a\right)-\sum_a p_aS(\rho_a), \qquad S(\rho)=-\operatorname{Tr}(\rho\log_2\rho).

The supremum of $\chi$ over all finite ensembles of outputs of $\Phi_b$ is $C_1(\Phi_b)$ . A Gaussian state has the specific form $U\rho_\lambda U^\dagger$ of Definition 1: $\rho_\lambda=2^{-n}\prod_j(I+\lambda_j Z_j)$ , each $\lambda_j\in[-1,1]$ , and $U=\exp(iH_2+iH_1)$ for Hermitian quadratic and linear combinations of Majorana operators. Requiring Gaussian input states gives $C_1^g(\Phi_b)$ . Setting $H_1=0$ gives an even Gaussian state. These are separate classes; the even class supplies an intermediate entropy minimum. Definition 1 and Eq. (13) are on page 4.

Formalization targets

Gaussian capacity

Write $b_1^\downarrow\ge\cdots\ge b_{2n}^\downarrow$ for the coefficients in decreasing order, and let $H(t)=-t\log_2t-(1-t)\log_2(1-t)$ . The main formula, Theorem 1 and Eq. (6), is

C_1^g(\Phi_b)=n-H\!\left(\frac{1+b_1^\downarrow}{2}\right) -\sum_{j=1}^{n-1}H\!\left(\frac{1+b_{2j}^\downarrow b_{2j+1}^\downarrow}{2}\right).

It holds for every $n\ge1$ and every unsorted $b\in[0,1]^{2n}$ . The milestones identify the covariance and Gaussian-preservation facts, the exact even and general Gaussian minimum-output entropies, and an ensemble attaining the capacity.

Full one-shot capacity for at most two qubits

The second clause of Theorem 1 states

C_1(\Phi_b)=C_1^g(\Phi_b)\qquad(n\le2).

Thus restricting the input ensemble to Gaussian states loses no one-shot capacity in these dimensions. The paper does not prove this equality for arbitrary $n$ .

Significance

The formula replaces an optimization over arbitrary finite Gaussian ensembles with binary entropies of sorted attenuation coefficients. In the one- and two-qubit cases it also settles the unrestricted one-shot optimization for this channel family. The intermediate result $C_1=n-S_{\min}$ relates signaling directly to minimum output entropy; the even-Gaussian and Gaussian minima make the distinction between the two state classes explicit. These relationships are established in Sections II–IV of the paper.

The mathematical results are proved in the 2005 paper. This mission asks for machine-checked proofs of their exact finite-dimensional statements. The definitions of bit-valued von Neumann entropy, finite output ensembles, ordered Majorana monomials, Gaussian-state predicates, and covariance matrices can support later work on fermionic channels. The submitted goal and milestones are presently proof obligations rather than claims of existing Lean proofs.

Difficulty

The channel is simple on each Majorana monomial, but the entropy of a general output state is not determined by its one- and two-point correlations. Even within the Gaussian class, optimizing only the even Gaussian states gives a different formula from optimizing all Gaussian states: linear Majorana terms change the optimum. A direct search over density matrices therefore does not expose the closed expression in Theorem 1. For the unrestricted two-qubit clause, one must also relate arbitrary states to the Gaussian class; the paper invokes a three-qubit parity result for that step. The distinctions and parity result appear in Sections III–IV.

Formalization scope

Lean represents qubit basis vectors by Fin n → Fin 2 and operators by complex matrices on that finite type. Majorana indices start at zero in Lean, so the paper's $c_{2j-1},c_{2j}$ correspond to consecutive indices $2j-2,2j-1$ . The Jordan–Wigner tensor factor at coordinate $j$ acts on qubit $j$ ; the monomial product follows increasing Majorana index. The channel is defined on all matrices by the trace-orthogonal monomial expansion of Eq. (4), not merely on covariance matrices. Attenuations may equal zero or one. Entropies use logarithms to base two, with $0\log_2 0=0$ .

Every capacity uses a real supremum over all finite normalized ensembles, with arbitrary ensemble size. The inputs are density matrices, and their channel outputs must be density matrices. The Gaussian capacity requires every input to satisfy Definition 1; Lemma 2 ensures these outputs are Gaussian too. The minimum-output quantities are real infima over their stated input classes, and the corresponding milestone theorems assert attainment. For the actual channels the relevant sets are nonempty and bounded: the maximally mixed state supplies an output state, while every Holevo quantity lies between zero and $n$ . This representation rules out restricting the Gaussian ensemble to the displayed optimizing family, assuming the goal's coefficients are initially sorted, or replacing bit entropy with natural-log entropy.

The development needs finite-matrix functional calculus, positivity, matrix exponentials, permutation and singular-value reasoning, and finite ensemble entropy bounds. Contributions to those reusable layers and to the paper's covariance, Gaussian-preservation, and minimum-output results are within scope. Lemma 3 is stated in its even-Gaussian form, which its proof establishes; the displayed lemma says only “Gaussian.”

Selected references

Sergey Bravyi, Classical capacity of fermionic product channels, arXiv preprint quant-ph/0507282v1, 2005. arXiv

13 thms1 active userReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Shapley–Snow Kernels, Multiparameter Eigenvalue Problems, and Stochastic Games: Every Discounted Value Is a Rank-Drop Root of a Kernel-Reduced Pencil, Algebraic of Degree at Most Its RankResearch Paper

Motivation

Zero-sum stochastic games model two opponents who interact over a finite set of states, each state being a matrix game whose outcome also decides the next state. Since Shapley (1953), every such game with discount factor $\lambda\in(0,1]$ has a value $v_\lambda^k$ at each initial state $k$ , characterised as the fixed point of a contraction. The value is the basic quantity of the theory, both for the discounted game and for its limits as $\lambda\to0$ , and computing it, or describing what kind of number it is, is a long-standing question in game theory and operations research.

A short history of the algebraic side of the question:

1950: Shapley and Snow describe the extreme optimal strategies of a matrix game through square sub-matrices and their cofactors.
1953: Shapley proves existence of $v_\lambda$ as the unique fixed point of the Shapley operator.
1976: Bewley and Kohlberg use Tarski–Seidenberg to show that $\lambda\mapsto v_\lambda$ is semi-algebraic and admits a Puiseux expansion near $0$ ; the degree of the algebraic equation is not controlled.
2018: Attia and Oliu-Barton (A solution for stochastic games, arXiv e-print, reference [2] of the paper) characterise $v^k_\lambda$ as the unique zero of $w\mapsto\mathrm{val}((-1)^n(\Delta^k-w\Delta^0))$ , with $n+1$ auxiliary matrices built from a Kronecker determinant.
2021: the present paper (arXiv:1810.08798v2, Mathematics of Operations Research 46(3)) refines this with Shapley–Snow kernels and the theory of multiparameter eigenvalue problems, and obtains an explicit univariate polynomial with $v^k_\lambda$ as a root, of degree bounded by a rank.

Setting

A stochastic game has states $K=\{1,\dots,n\}$ , finite nonempty action sets $I_k$ , $J_k$ at state $k$ , a payoff $g(k,i,j)\in\mathbb R$ , transition probabilities $q(\ell\mid k,i,j)\ge0$ with $\sum_\ell q(\ell\mid k,i,j)=1$ , and a discount factor $\lambda\in(0,1]$ .

A real matrix $A$ is a matrix game: the row player picks a mixed strategy $x$ , the column player a mixed strategy $y$ , and the row player receives ${}^txAy$ . Its value $\mathrm{val}(A)$ is the number that each player can guarantee. For $z\in\mathbb R^n$ , the local game $\mathcal G^k(\lambda,z)$ has entries $\lambda g(k,i,j)+(1-\lambda)\sum_\ell q(\ell\mid k,i,j)z^\ell$ , and the discounted value $v_\lambda\in\mathbb R^n$ is the unique solution of $\mathrm{val}(\mathcal G^k(\lambda,v_\lambda))=v^k_\lambda$ for all $k$ .

The data array $D(\lambda)$ is the $n\times(n+1)$ array of matrices $M^k_0=\lambda G^k$ , $M^k_k=(1-\lambda)Q^k_k-U$ and $M^k_\ell=(1-\lambda)Q^k_\ell$ for $\ell\neq k$ , where $G^k=(g(k,i,j))$ , $Q^k_\ell=(q(\ell\mid k,i,j))$ and $U$ is a matrix of ones. The Kronecker determinant of an $n\times n$ array of matrices replaces products of scalars by Kronecker products; entrywise, its entry at rows $(i_1,\dots,i_n)$ and columns $(j_1,\dots,j_n)$ is $\det\big(A_{k\ell}^{i_kj_k}\big)_{k,\ell}$ . The auxiliary matrices are $\Delta^\ell=(-1)^\ell\det_\otimes D^{(\ell)}(\lambda)$ , where $D^{(\ell)}$ deletes column $\ell$ , for $0\le\ell\le n$ .

A Shapley–Snow kernel of a matrix game $G$ is a square sub-matrix $\dot G$ with $S(\mathrm{co}(\dot G))\neq0$ whose cofactor strategies $\mathrm{co}(\dot G)\mathbf 1/S(\mathrm{co}(\dot G))$ and ${}^t\mathrm{co}(\dot G)\mathbf 1/S(\mathrm{co}(\dot G))$ , completed by zeros, are optimal in $G$ ; $\mathrm{co}$ is the cofactor matrix and $S$ the sum of entries. Choosing a kernel $\dot I_k\times\dot J_k$ of every local game $\mathcal G^k(\lambda,v_\lambda)$ and restricting each $M^k_\ell$ to it gives the reduced array $\dot D(\lambda)$ , with square auxiliary matrices $\dot\Delta^0,\dots,\dot\Delta^n$ .

Formalization targets

Goal: Theorem 3.4.2

For every state $k$ and every choice of kernels:

\text{(i) } v^k_\lambda \text{ is the unique } w\in\mathbb R \text{ with } \mathrm{val}(\dot\Delta^k-w\dot\Delta^0)=0;\qquad \text{(ii) } \mathrm{rank}(\dot\Delta^k-v^k_\lambda\dot\Delta^0)<\max_{w\in\mathbb R}\mathrm{rank}(\dot\Delta^k-w\dot\Delta^0);

(iii) some nonzero polynomial $P^k$ of degree at most $\mathrm{rank}(\dot\Delta^0)$ , the determinant of a square sub-matrix of $\Delta^k-w\Delta^0$ , vanishes at $v^k_\lambda$ ; (iv) if all entries of $D(\lambda)$ are rational, then

[\mathbb Q(v^k_\lambda):\mathbb Q]\le\mathrm{rank}(\dot\Delta^0).

Milestones

In attack order: Shapley's fixed-point theorem (§2.1); the sign of $\Delta^0$ (Lemma 2.2.3) and unique solvability of $\mathrm{val}(A-wB)=0$ (Remark 2.2.4); the Shapley–Snow theorem (Theorem 2.3.1) and existence of kernels (§3.1); the cofactor lemmas B1–B3 and Proposition 2.3.4 on the kernel of $\dot G-v\dot U$ ; the rank-drop criterion (Lemma C1), the tensor kernel vector (Lemma C2) and Proposition 2.4.4; Proposition 3.2.1 placing $v_\lambda$ in the reduced solution sets; Proposition 3.4.1, the characterising polynomial.

Significance

The result. Theorem 3.4.2 turns the computation of a discounted value into univariate root finding: $v^k_\lambda$ is a root of one of finitely many explicit polynomials, read off from $D(\lambda)$ , of degree bounded by $\mathrm{rank}(\dot\Delta^0)\le\prod_k\min(|I_k|,|J_k|)$ . Part (iv) gives an explicit bound on the algebraic degree of the value of a rational game, a quantity that the semi-algebraic approach leaves uncontrolled. The same polynomials yield, in §4 of the paper, the convergence of $v_\lambda$ as $\lambda\to0$ and a bound on its rate. These are not part of this mission.

Formalizing it. The theorem is proved in the paper; no part of it is machine-checked. A complete development formalizes the value of a matrix game on arbitrary finite action sets, Shapley's fixed point, the Shapley–Snow description of extreme optimal strategies, Kronecker determinants of arrays of matrices, and the singular multiparameter-eigenvalue lemmas of Muhič–Plestenjak and Atkinson. Each of these is reusable outside stochastic games.

Difficulty

The obvious route is Cramer's rule for the multiparameter system $\det(M^k_0+z^1M^k_1+\dots+z^nM^k_n)=0$ : when $\Delta^0$ is invertible, the solutions are the eigenvalues of $\Delta^k(\Delta^0)^{-1}$ . Here $\Delta^0$ , and still more $\dot\Delta^0$ , is in general singular, and the polynomials $\det(\dot\Delta^k-w\dot\Delta^0)$ may vanish identically, so the determinant equation carries no information. The value must instead be located through a rank drop of the pencil. Proving the rank drop requires nonzero left and right kernel vectors with ${}^tx\dot\Delta^0y\neq0$ , which come from the sign of $\Delta^0$ (Lemma 2.2.3) and from nonnegative kernel strategies of the Shapley–Snow kernels transported through Kronecker products. Neither ingredient is available off the shelf.

A second obstacle is the paper's degree argument: it quotes the degree of $\det(A+wB)$ as equal to $\mathrm{rank}(B)$ , which is false in general; only the inequality holds and is posed.

Formalization scope

Model. States are Fin n with $n\ge1$ . The action sets I k, J k are finite, nonempty and may depend on the state, as in §4, p. 20, where the paper extends its results "word for word" to that case. The transition probabilities are nonnegative and sum to one, and 0 < lam ≤ 1.
Value. The value of a matrix game is the relation IsMatVal A w: optimal strategies of both players guarantee $w$ . No supremum or infimum over strategy sets is taken. $v_\lambda$ is any $v$ with IsShapleyFixed g q lam v; the milestone shapley_fixed_point gives existence and uniqueness, so the goal is not vacuous.
Kernels. A kernel is given by embeddings Fin s ↪ I, Fin s ↪ J. IsSSK requires $S(\mathrm{co}(\dot G))\neq0$ and optimality of the completed cofactor strategies. The paper also requires the pair to be basic, but by Theorem 2.3.1 this is equivalent.
Linear algebra. co M is the transposed adjugate. The Kronecker determinant is defined through its entry formula (K5), and rows and columns of $\Delta^\ell$ are indexed by tuples instead of lexicographic integers. Column $0$ of the array is the paper's $\ell=0$ , and the paper's $\Delta^k$ is Delta … k.succ. " $\max_w\mathrm{rank}$ " means "some real $w$ gives larger rank". The sets $S^M,S^\Delta$ accept complex vectors in Lemma C2, as in §2.4; $S^R,T^M$ are used over $\mathbb R^n$ in the game results. Proposition 3.4.1 takes its polynomial from a determinant of a reduced-pencil submatrix, as the proof constructs.
Conventions. Part (i) is the printed form, without the $(-1)^n$ of Result 1 (i); both hold for the square reduced matrices. Part (iv) is IsAlgebraic ℚ v ∧ (minpoly ℚ v).natDegree ≤ rank.

The goal ranges over Shapley–Snow kernels, not over arbitrary square sub-matrices, and $E^k$ is built from the full $\Delta^k-w\Delta^0$ with only its degree cap taken from $\dot\Delta^0$ . A formalization in which kernels are arbitrary square sub-matrices, or in which $E^k$ is built from $\dot\Delta$ , states a different theorem.

Contributions are welcome at every level. In particular: the value of a matrix game on Fintype index types with existence and uniqueness, Shapley's contraction, the Shapley–Snow theorem, the Kronecker determinant and its column-alternation property (K3), and the bound $\deg\det(A+wB)\le\mathrm{rank}(B)$ .

Selected references

L. Attia, M. Oliu-Barton, Shapley–Snow kernels, multiparameter eigenvalue problems and stochastic games, Mathematics of Operations Research 46(3), 2021; arXiv:1810.08798v2. https://arxiv.org/abs/1810.08798v2
L. Attia, M. Oliu-Barton, A solution for stochastic games, arXiv e-print, 2018 (reference [2] of the paper).
L. S. Shapley, Stochastic games, PNAS 39(10), 1953. https://doi.org/10.1073/pnas.39.10.1095
L. S. Shapley, R. N. Snow, Basic solutions of discrete games, Contributions to the Theory of Games I (Annals of Mathematics Studies 24), 1950, pp. 27–35.
T. Bewley, E. Kohlberg, The asymptotic theory of stochastic games, Mathematics of Operations Research 1(3), 1976. https://doi.org/10.1287/moor.1.3.197
A. Muhič, B. Plestenjak, On the singular two-parameter eigenvalue problem, Electronic Journal of Linear Algebra 18, 2009, pp. 420–437.
F. V. Atkinson, Multiparameter Eigenvalue Problems, vol. 1, Academic Press, 1972.
J. W. Demmel, Applied Numerical Linear Algebra, SIAM, 1997 (cited for the degree of $\det(A+wB)$ ).

18 thms1 active userReviewed

Economics Operations Research·Captain: mikedeng1

Revenue Volatility Under Uncertain Network Effects: The Worst-Case Relative Revenue Change over ε-Perturbed Networks Equals αλmax·ε/(1 − αλmax(1 + ε))Research Paper

Motivation

A seller of a good with network externalities (a social app, a telecom plan, a game console) gains from knowing how strongly each consumer's demand depends on the consumption of others. Candogan, Bimpikis and Ozdaglar (Operations Research, 2012) showed that, on a known network, the optimal price vector of a monopolist and the resulting revenue have closed forms built from the matrix $(I-\alpha W)^{-1}$ . In practice the network $W$ is estimated from data and is never known exactly. A seller who commits to prices on the basis of a forecast $W$ then faces revenue that moves with the true network $\tilde W$ .

Baron, Hu and Malekian (SSRN 3561270, 2020; published as a Technical Note in Operations Research, 2022, doi:10.1287/opre.2022.2302) ask how large that movement can be in the worst case, when the forecast error is bounded in spectral norm. Their Theorem 1 gives an exact answer depending on the network only through its largest eigenvalue. This mission formalizes that theorem, read in the SSRN version of 2020-03-25.

Setting

There are $n$ agents on a network $W\in\mathbb R^{n\times n}$ with $W_{ij}\ge0$ , $W^\top=W$ and, as for any network without self-loops, $W_{ii}=0$ . A parameter $\alpha\ge0$ scales the peer effect, $b\in\mathbb R^n$ collects the agents' primary values, and $c$ is the seller's marginal cost.

The game has two stages. In the first, the seller chooses a price vector $p\in\mathbb R^n$ . In the second, each agent $i$ chooses a quantity $x_i\ge0$ , with utility

u_i(x;W,b,p)=-\tfrac12x_i^2+b_ix_i+\alpha\sum_{j\neq i}W_{ij}x_ix_j-p_ix_i .

A consumption equilibrium is a profile $x\ge0$ in which each $x_i$ maximizes $u_i(\cdot,x_{-i})$ over $\mathbb R_+$ . The seller's revenue is $\sum_i(p_i-c)x_i$ , and the optimal revenue $R(W,\alpha,b)$ is its supremum over all prices and their equilibria. Assumption 1 asks $\alpha\sum_jW_{ij}<1$ for every $i$ ; Assumption 2 asks $b>c\mathbf 1$ .

The forecast error is measured by the uncertainty set

\mathcal W(W,\epsilon)=\{\tilde W:\ \|W-\tilde W\|_2\le\epsilon\|W\|_2,\ \tilde W\ge0,\ \tilde W^\top=\tilde W\},

with $\|\cdot\|_2$ the spectral norm. The seller fixes the price that is optimal for the forecast $W$ ; consumers then play the equilibrium on the realized $\tilde W$ , producing revenue $R(\tilde W,\alpha,b)$ . The revenue volatility $\mathrm{RV}(W,\epsilon)$ is the supremum of the relative change $|R(W,\alpha,b)-R(\tilde W,\alpha,b)|/R(W,\alpha,b)$ over $\tilde W\in\mathcal W(W,\epsilon)$ and $b>c\mathbf 1$ . Finally, $\lambda_{\max}=\lambda_{\max}(W)$ is the largest absolute value of an eigenvalue of $W$ .

Formalization targets

Goal: Theorem 1 (p. 11)

Under Assumptions 1 and 2, for every $\epsilon\ge0$ with $\epsilon<1/(\alpha\lambda_{\max})-1$ , every $\tilde W\in\mathcal W(W,\epsilon)$ admits an interior consumption equilibrium at the seller's ex-ante price, and

\mathrm{RV}(W,\epsilon)=\frac{\alpha\lambda_{\max}\epsilon}{1-\alpha\lambda_{\max}(1+\epsilon)} .

Milestones

Theorem 4 (p. 34): $\rho(A)<1$ iff $A^k\to0$ , and then $(I-A)^{-1}=\sum_kA^k$ ; for $\rho(A)>1$ the powers are unbounded.
Proposition 1 (p. 8): the consumption game is an exact potential game with a unique equilibrium, equal to $(I-\alpha W)^{-1}(b-p)>0$ when $b>p$ .
Proposition 2 (p. 9): the optimal price is $(b+c\mathbf 1)/2$ and $R(W,\alpha,b)=\big(\tfrac{b-c\mathbf 1}{2}\big)^{\top}(I-\alpha W)^{-1}\big(\tfrac{b-c\mathbf 1}{2}\big)$ .
The equality of spectral norm and spectral radius for symmetric matrices (p. 12).
Part 1 of the proof (pp. 11–12): $\rho(\alpha\tilde W)<1$ and $(I-\alpha\tilde W)^{-1}\ge0$ on $\mathcal W(W,\epsilon)$ .
Part 2 (p. 12): the witness $\tilde W=(1+\epsilon)W$ with the top eigenvector attains the bound.
Steps 1–2 of Part 3 (p. 13), Lemma 1 (p. 14), and eq. (6) (p. 14): the reduction to $f^\top L^{-1}Mf$ , its stationarity at eigenvectors of $M$ , and $\|M\|_2\le\alpha\lambda_{\max}\epsilon/(1-\alpha\lambda_{\max}(1+\epsilon))$ .

Significance

The theorem turns a robustness question about an equilibrium of a game into a single spectral quantity. A seller can read off the worst-case relative revenue change from $\lambda_{\max}(W)$ , $\alpha$ and $\epsilon$ , and compare networks by their largest eigenvalue: denser, more central networks are more exposed to estimation error. The paper uses it to compare chains and complete networks (Proposition 3) and as the deterministic benchmark for its stochastic analysis (Theorem 2).

The result is proved on paper; no machine-checked proof exists. A formalization adds three pieces that are absent from the platform: the network pricing game stated as an equilibrium (not as a closed-form demand), the optimality of the price $(b+c\mathbf 1)/2$ over all of $\mathbb R^n$ , and the Neumann series for real matrices under $\rho(A)<1$ .

Difficulty

The obvious argument substitutes Proposition 2's closed form and bounds a difference of resolvents. Two steps resist this. First, the realized network $\tilde W$ need not satisfy Assumption 1, so the existence, uniqueness and positivity of the equilibrium on $\tilde W$ must come from the spectral bound $\alpha\|\tilde W\|_2<1$ alone. Second, the bound is a supremum of a generalized Rayleigh quotient $f^\top(L^{-1}-\tilde L^{-1})f/f^\top L^{-1}f$ over $f>0$ , which must be related to the spectral norm of $I-L\tilde L^{-1}$ through a constrained-optimization argument. Tightness needs the top eigenvector, which is only non-negative in general, so the supremum is generally not attained in the open set $b>c\mathbf 1$ .

The game-theoretic layer is not a formality: Proposition 2 asserts optimality over every price vector, including those at which some agents consume nothing.

Formalization scope

Agents are Fin n; vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ. The norm is Mathlib's scoped spectral norm (Matrix.Norms.L2Operator). $\lambda_{\max}$ is the supremum of $|\mu|$ over the real spectrum (used only for symmetric matrices), and $\rho$ is computed from the complex spectrum. Condition (1) is written $\alpha\lambda_{\max}(1+\epsilon)<1$ , equivalent to the printed form when $\alpha\lambda_{\max}>0$ , and avoiding Lean's convention $1/0=0$ .

Conventions added to the page, each disclosed in the items:

$W$ and every $\tilde W$ have a zero diagonal (the utility sums over $j\neq i$ , while the paper's formulas use the full matrix);
$\epsilon\ge0$ ;
$\mathrm{RV}(W,\epsilon)$ is stated as a least upper bound, not an attained maximum;
$R(\tilde W,\alpha,b)$ is the revenue at the seller's optimal price for $W$ with the consumers' equilibrium on $\tilde W$ (p. 11);
the myopic-best-response clause of Proposition 1 is not stated.

The optimal revenue and the revenue on $\tilde W$ are defined from the game (suprema over prices and equilibria), never by Proposition 2's closed form; a formalization that substitutes the closed form would make Propositions 1–2 vacuous and reduce the goal to a matrix inequality, and is ruled out.

A complete development needs: potential games with concave potentials on $\mathbb R_+^n$ , linear complementarity for diagonally dominant matrices, the Neumann series and Perron–Frobenius for non-negative matrices, the spectral theorem for real symmetric matrices, and a Lagrange multiplier rule for a quadratic constraint. The Neumann series criterion and the norm–radius equality for symmetric matrices are reusable well beyond this mission. Proofs of any milestone are welcome, as are alternative decompositions of Part 3.

Selected references

O. Baron, M. Hu, A. Malekian, Revenue volatility under uncertain network effects, SSRN preprint 3561270 (version of 2020-03-25). https://ssrn.com/abstract=3561270 ; published as a Technical Note in Operations Research, 2022. https://doi.org/10.1287/opre.2022.2302
O. Candogan, K. Bimpikis, A. Ozdaglar, Optimal pricing in networks with externalities, Operations Research 60(4), 2012. https://doi.org/10.1287/opre.1120.1066
R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press, 1990. https://doi.org/10.1017/CBO9780511810817
D. Monderer, L. S. Shapley, Potential games, Games and Economic Behavior 14(1), 1996. https://doi.org/10.1006/game.1996.0044

11 thms1 active userReviewed

Optimization Statistics Theoretical Computer Science·Captain: mikedeng1

Proportional Volume Sampling and Approximation Algorithms for A-Optimal Design: Sampling with an α-Approximate (d−1, d)-Wise Independent Measure Gives an α-ApproximationResearch Paper

Motivation

In linear regression with a budget, an experimenter holds $n$ candidate experiments, each described by a vector $v_i\in\mathbb R^d$ , and may run only $k$ of them. If the experiments in $S\subseteq[n]$ are run and the unknown parameter is estimated by least squares, the covariance of the estimate is proportional to $\big(\sum_{i\in S}v_iv_i^\top\big)^{-1}$ . A-optimal design chooses $S$ to minimise the trace of that matrix, which is the mean squared error of the estimator. The criterion is one of the classical optimality criteria of experimental design (Pukelsheim, Optimal Design of Experiments, SIAM 2006) and appears in feature selection, sensor placement and matrix sparsification.

Selecting the best $k$ -set exactly is NP-hard (the paper proves this in its Theorem 1.7), so the question is approximation. Avron and Boutsidis (SIAM J. Matrix Anal. Appl. 2013) connected A-optimal design to volume sampling (Deshpande–Rademacher, FOCS 2010), which samples a set with probability proportional to $\det(V_SV_S^\top)$ , and obtained the approximation ratio $\frac{n-d+1}{k-d+1}$ . Nikolov, Singh and Tantipongpipat (arXiv:1802.08318; Mathematics of Operations Research, 2022) reweight volume sampling by a second measure $\mu$ that can depend on a solution of the natural convex relaxation. Their first result, Theorem 1.3, shows that the approximation ratio of this scheme is controlled by a single combinatorial property of $\mu$ , approximate $(d-1,d)$ -wise independence. Their later theorems obtain ratios $d$ (when $k=d$ ) and $1+\epsilon$ (when $k$ is large) by exhibiting such measures.

Setting

Let $V=[v_1,\dots,v_n]$ be a real $d\times n$ matrix and $d\le k\le n$ . For $S\subseteq[n]$ , $V_S$ is the $d\times|S|$ submatrix of the columns indexed by $S$ , so $V_SV_S^\top=\sum_{i\in S}v_iv_i^\top$ . The A-optimal design problem is

\mathrm{OPT}=\min_{S\subseteq[n],\,|S|=k}\operatorname{tr}\big(V_SV_S^\top\big)^{-1},

with the value $+\infty$ for sets whose Gram matrix is singular.

The convex relaxation (1)–(3) replaces the indicator of $S$ by $x\in\mathbb R^n$ :

\mathrm{CP}=\min\ \operatorname{tr}\Big(\sum_{i=1}^n x_iv_iv_i^\top\Big)^{-1}\quad\text{s.t.}\quad\sum_{i=1}^n x_i=k,\quad 0\le x_i\le 1.

Write $V_S(x)$ for the matrix with columns $\sqrt{x_i}\,v_i$ , $i\in S$ , so that $V(x)V(x)^\top=\sum_ix_iv_iv_i^\top$ , and $x^L=\prod_{i\in L}x_i$ .

Let $\mathcal U_k$ ( $\mathcal U_{\le k}$ ) be the subsets of $[n]$ of size exactly (at most) $k$ , and $\mu$ a probability measure on them. Proportional volume sampling with measure $\mu$ (Definition 1.1) is the distribution $\mu'$ with

\Pr_{\mu'}[\mathcal S=S]=\frac{\mu(S)\det(V_SV_S^\top)}{\sum_{S'}\mu(S')\det(V_{S'}V_{S'}^\top)}.

The measure $\mu$ is $\alpha$ -approximate $(d-1,d)$ -wise independent with respect to a feasible $x$ (Definition 1.2) if for all $T,R\subseteq[n]$ with $|T|=d-1$ and $|R|=d$ ,

\frac{\Pr_{\mathcal S\sim\mu}[T\subseteq\mathcal S]}{\Pr_{\mathcal S\sim\mu}[R\subseteq\mathcal S]}\le\alpha\,\frac{x^T}{x^R}.

For a square matrix $M$ with eigenvalues $\lambda_1,\dots,\lambda_m$ , $E_k(M)$ is the $k$ -th elementary symmetric polynomial $e_k(\lambda_1,\dots,\lambda_m)$ ; $E_m(M)=\det M$ .

Algorithm 1 (p. 8) solves the relaxation for $x$ , samples $\mathcal S\sim\mu'$ , and pads $\mathcal S$ with arbitrary indices to size $k$ if it is smaller.

Formalization targets

Goal: Theorem 1.3

If $x$ is an optimal solution of (1)–(3) and $\mu$ is $\alpha$ -approximate $(d-1,d)$ -wise independent with respect to $x$ , then the output $\operatorname{pad}(\mathcal S)$ of Algorithm 1 satisfies, for every $k$ -set $S^{\mathrm{opt}}$ ,

\mathbb E_{\mathcal S\sim\mu'}\Big[\operatorname{tr}\big(V_{\operatorname{pad}(\mathcal S)}V_{\operatorname{pad}(\mathcal S)}^\top\big)^{-1}\Big]\le\alpha\operatorname{tr}\big(V_{S^{\mathrm{opt}}}V_{S^{\mathrm{opt}}}^\top\big)^{-1},

so the algorithm is an $\alpha$ -approximation in expectation, and some $k$ -set has objective at most $\alpha\,\mathrm{CP}$ (the integrality gap is at most $\alpha$ ). The constant $\alpha$ is a parameter: the goal fixes no value of it, so later constructions of better measures plug into it unchanged.

Milestones

Lemma 2.1: $\det(V_T(x)^\top V_T(x))=x^T\det(V_T^\top V_T)$ for $|T|\le d$ .
Identity (4): $E_k(VV^\top)=E_k(V^\top V)=\sum_{S\in\mathcal U_k}\det(V_S^\top V_S)$ .
Identity (6): $\operatorname{tr}M^{-1}=E_{d-1}(M)/\det M$ for a $d\times d$ matrix of rank $d$ .
The expected objective under $\mu'$ is at most $\sum_{|T|=d-1}\det(V_T^\top V_T)\Pr_\mu[\mathcal S\supseteq T]\big/\sum_{|R|=d}\det(V_R^\top V_R)\Pr_\mu[\mathcal S\supseteq R]$ (p. 9).
$\operatorname{tr}(V(x)V(x)^\top)^{-1}=\sum_{|T|=d-1}\det(V_T^\top V_T)x^T\big/\sum_{|R|=d}\det(V_R^\top V_R)x^R$ (p. 9).
Inequality (5): $\mathbb E_{\mathcal S\sim\mu'}[\operatorname{tr}(\sum_{i\in\mathcal S}v_iv_i^\top)^{-1}]\le\alpha\operatorname{tr}(\sum_ix_iv_iv_i^\top)^{-1}$ .
$\mathrm{CP}\le\mathrm{OPT}$ (p. 7).
Padding a set with further vectors does not increase $\operatorname{tr}(V_SV_S^\top)^{-1}$ (p. 8).

Significance

Theorem 1.3 turns an approximation question about a continuous, spectral objective into a question about the marginals of a distribution on sets: any measure with approximately independent $(d-1)$ - and $d$ -marginals relative to the relaxation's solution yields an approximation algorithm with the same ratio, and simultaneously bounds the integrality gap of the relaxation. The paper's Theorems 1.4 and 1.5 are proved by applying it to hard-core distributions, giving a $d$ -approximation for $k=d$ and a $(1+\epsilon)$ -approximation for $k=\Omega\big(\frac d\epsilon+\frac{\log(1/\epsilon)}{\epsilon^2}\big)$ .

The result is proved in the paper; nothing here is open. To our knowledge none of it has a machine-checked proof. The formalization produces, beyond the theorem itself, a reusable linear-algebra layer that the pinned Mathlib lacks: the Cauchy–Binet formula for Gram matrices, its extension (4) to all elementary symmetric functions of the spectrum, and the identity $\operatorname{tr}M^{-1}=E_{d-1}(M)/\det M$ . These are standard tools for determinantal point processes and volume sampling, and a later formalization of the hard-core constructions (Theorems 1.4, 1.5) would build directly on this mission's goal.

Difficulty

The reduction itself is a short calculation once both sides of (5) are written as ratios of sums over $(d-1)$ - and $d$ -subsets; the difficulty is in the linear algebra that produces those ratios. Identity (4) needs Cauchy–Binet for non-square matrices together with the relation between the coefficients of the characteristic polynomial, its roots and sums of principal minors; none of this is in Mathlib in the required form, and the eigenvalue side requires that the characteristic polynomial of a real symmetric matrix splits over $\mathbb R$ . Applying (4) to every $V_S$ separately and exchanging the order of summation is bookkeeping between index sets of different sizes, which is where informal proofs are quietest. The expectation also has to be handled honestly at sets $S$ with singular $V_SV_S^\top$ : they are never sampled, but the paper's displayed equality on p. 9 counts them, so the first display holds only as an inequality.

Formalization scope

Everything is over $\mathbb R$ , with index sets Finset (Fin n) and $V$ a Matrix (Fin d) (Fin n) ℝ. A probability measure on $\mathcal U_{\le k}$ is a nonnegative function on subsets of $[n]$ with total mass $1$ vanishing on sets larger than $k$ ; this covers $\mathcal U_k$ as a special case. $E_k$ is the elementary symmetric function of the real roots of the characteristic polynomial, applied only to symmetric matrices. Lean's matrix inverse is $0$ on singular matrices, so every comparison of objectives assumes positive definiteness of the inverted matrix, and OPT is expressed by quantifying over $k$ -sets with positive definite Gram matrix rather than by an infimum.

The statements add the following, each disclosed in the item's Formalization Note: $1\le d$ (for the natural-number subtraction $d-1$ ); a positive normaliser $\sum_S\mu(S)\det(V_SV_S^\top)>0$ , which Definition 1.1 presupposes; positive definiteness of $\sum_ix_iv_iv_i^\top$ , which is what a finite CP means; Definition 1.2 in cross-multiplied form; and " $\le$ " in place of the printed " $=$ " in the first display of p. 9. Theorem 1.3 assumes a suitable $\mu$ only for the optimal $x$ , as the remark after the theorem says; this implies the printed form. The padding of Algorithm 1 is an arbitrary map $\operatorname{pad}$ with $S\subseteq\operatorname{pad}(S)$ and $|\operatorname{pad}(S)|=k$ on the support of $\mu$ .

The goal is not inequality (5) alone and $E_k$ is not defined as a sum of minors, and the expectation is not defined as the ratio of p. 9; any of those would make milestones true by definition. A sorry-free sanity file shows that all hypotheses of the goal are simultaneously satisfiable ( $d=k=n=2$ , $V=I$ , $x=(1,1)$ , $\mu$ the point mass at $[2]$ , $\alpha=1$ ).

Contributions are welcome at every milestone; the Cauchy–Binet layer (milestones 2 and 3) is reusable well beyond this mission and is the natural place to start.

Selected references

A. Nikolov, M. Singh, U. Tantipongpipat, Proportional Volume Sampling and Approximation Algorithms for A-Optimal Design, arXiv:1802.08318v5, 2018; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1802.08318
H. Avron, C. Boutsidis, Faster Subset Selection for Matrices and Applications, SIAM Journal on Matrix Analysis and Applications 34(4):1464–1499, 2013. https://arxiv.org/abs/1201.0127
A. Deshpande, L. Rademacher, Efficient Volume Sampling for Row/Column Subset Selection, FOCS 2010, 329–338. https://doi.org/10.1109/FOCS.2010.38
Z. Mariet, S. Sra, Elementary Symmetric Polynomials for Optimal Experimental Design, NeurIPS 2017. https://arxiv.org/abs/1705.09677
F. Pukelsheim, Optimal Design of Experiments, SIAM Classics in Applied Mathematics, 2006. https://doi.org/10.1137/1.9780898719109

10 thms1 active userReviewed

Harmonic Analysis Quantum Information·Captain: mikedeng1

Product Decomposition of Periodic Functions in Quantum Signal Processing: Every SU(2)-Valued Laurent Polynomial of Degree n in E_n Is Uniquely a Product of n Primitive Matrices and a UnitaryResearch Paper

Motivation

Quantum signal processing transforms the eigenphases of a unitary operator by a sequence of controlled operations and single qubit rotations. To know which transformations such a sequence can realize, one must characterize the matrix functions produced by the sequence. Haah's product decomposition theorem gives such a characterization without the restriction on the projectors used in some earlier quantum signal processing constructions. The result concerns exact functions; the numerical synthesis algorithm and its precision analysis are separate parts of the paper.

Setting

Let $t$ be a nonzero complex number. A rank one orthogonal projector $P$ on $\mathbb C^2$ is a Hermitian matrix with $P^2=P$ and trace one. Its complementary projector is $I-P$ . The associated primitive matrix is

E_P(t)=tP+t^{-1}(I-P).

For $|t|=1$ , this matrix is unitary with determinant one. Given $n$ such projectors, indexed in their multiplication order, and a constant matrix $E_0\in SU(2)$ , the product of interest is

F(t)=E_0E_{P_1}(t)E_{P_2}(t)\cdots E_{P_n}(t).

The leftmost primitive factor is $E_{P_1}$ , and the product has exactly $n$ primitive factors. At $n=0$ the product of primitive factors is the identity and $F$ is the constant matrix $E_0$ . Although the physical interpretation uses points on the unit circle, the formula defines $F$ at every nonzero complex $t$ . These conventions follow §2, equations (2) and (3).

A matrix Laurent polynomial of width $n$ is written

F(t)=\sum_{j=-n}^{n} C_jt^j,

where each $C_j$ is a complex $2\times2$ matrix and all coefficients outside $[-n,n]$ vanish. The set $\mathcal P_n$ consists of these polynomials for which $F(\eta)\in SU(2)$ whenever $|\eta|=1$ . A member has degree $n$ when $C_n\ne0$ or $C_{-n}\ne0$ . The subset $\mathcal E_n$ consists of members whose nonzero exponents have the parity of $n$ , so $C_{-n+k}=0$ for every odd integer $k$ . The notation $F^\dagger(t)$ conjugate transposes each coefficient while leaving its exponent unchanged: $F^\dagger(t)=\sum_j C_j^\dagger t^j$ . These are the conventions of Definition 1 and equations (4) and (5).

Formalization targets

The goal is all of Theorem 2. First, every product of $n$ primitive matrices belongs to $\mathcal E_n$ . Conversely, every $F\in\mathcal E_n$ of degree $n$ has a unique ordered tuple $(E_0,P_1,\ldots,P_n)$ satisfying the product formula, with $E_0\in SU(2)$ and each $P_j$ a rank one orthogonal projector. For $n>0$ , the final projector is determined by the leading coefficient:

P_n=\frac{C_n^\dagger C_n}{\operatorname{Tr}(C_n^\dagger C_n)}.

The formula includes the assertion that its denominator is nonzero under the theorem's hypotheses; that is a consequence to establish, rather than an extra assumption. The $n=0$ case retains the product characterization and uniqueness, while having no final projector. The milestones state the source's primitive matrix observation, polynomial identities, leading coefficient conditions, degree reduction, and the relation between the two extreme coefficients.

Significance

The theorem identifies the Laurent polynomials that admit the specified quantum signal processing product and says that the factors are uniquely recoverable from the matrix function when the number of factors is fixed. This supports the exact synthesis question motivating the paper: whether a desired $SU(2)$ valued function on the unit circle is achievable by the primitive operations. The formula for $P_n$ also identifies the last factor directly from a coefficient of the target function. Haah's §4 algorithm uses the decomposition, but its numerical guarantees are outside this mission.

The paper proves Theorem 2. The formalization target is a machine checked version of that known theorem and its source stated intermediate claims. The definitions of matrix Laurent polynomial evaluation, parity restricted coefficient families, and primitive projector factors can also support later work on polynomial matrix functions. The mission does not claim that these statements have already been proved in Lean.

Difficulty

Membership in $SU(2)$ is given only on the unit circle, while coefficient identities needed for the decomposition concern Laurent polynomials throughout $\mathbb C\setminus\{0\}$ . A pointwise unitary identity on the circle must therefore be promoted to an identity of Laurent polynomials before its extreme coefficients can be compared. The main structural difficulty is that a matrix product may lose its highest and lowest powers even when its factors are nonzero. Identifying a projector that lowers the degree must control both extremes at once and preserve the parity and $SU(2)$ conditions. Uniqueness also depends on fixing exactly $n$ factors: extra complementary factors can cancel.

Formalization scope

Lean represents a Laurent polynomial by a coefficient family $C:\mathbb Z\to\operatorname{Mat}_{2}(\mathbb C)$ with explicit width support, and evaluates it by a finite sum of integer powers. Equalities of Laurent polynomials are stated for every nonzero complex $t$ . The positive integer $n$ is represented as a natural number, with integer casts for exponents. The special unitary group is Mathlib's $SU(2)$ ; the paper's rank one orthogonal projectors are represented by Hermitian idempotence together with trace one. This trace condition is equivalent to rank one for these $2\times2$ projectors. An ordered function on $\operatorname{Fin}(n)$ supplies precisely $n$ factors. The last factor has index $n-1$ in Lean.

The set $\mathcal E_n$ retains both the width and $SU(2)$ conditions of $\mathcal P_n$ and adds the parity condition. It is defined from coefficients, not from the existence of a product decomposition. Allowing rank zero or rank two projectors, dropping unitarity, or allowing a variable factor count would change the theorem. The source's remark that any orthogonal projector yields a member of $\mathcal E_1$ is read with the rank one condition of equation (2): the literal unrestricted remark fails for $0$ and $I$ . The singular leading coefficient milestones require $n>0$ , and the last projector formula has the same domain.

The development needs facts about $2\times2$ determinants, conjugate transpose, projectors, finite matrix products, and uniqueness of finite Laurent expansions. The Laurent polynomial infrastructure and rank one matrix facts are reusable beyond this theorem. Contributions proving the source stated milestones, their faithful supporting algebraic lemmas, and the main product characterization are in scope. The parity refinement of §3.1, Lemma 4, and the §4 synthesis algorithm with its running time claim are outside this mission.

Selected references

J. Haah, Product Decomposition of Periodic Functions in Quantum Signal Processing, Quantum 3, 190 (2019); formalization source: arXiv:1806.10236v4, 2020, pp. 3–5.

10 thms1 active userReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

A Hierarchical Approach to Robust Stability of Multiclass Queueing Networks: Chen-S at Every Static-Priority Corner Implies Chen-S for Every Queue-Ratio PolicyResearch Paper

Motivation

A multiclass queueing network routes jobs of several classes through shared stations. Whether such a network is stable depends on the scheduling policy and not only on the load: the Lu–Kumar and Rybko–Stolyar examples are unstable under a static-priority policy with every station loaded below capacity (Bramson, Stability of Queueing Networks, 2008). A network operator who does not control, or does not know, the policy in use therefore wants robust stability: stability under every policy of a given family.

Zhao, Gurvich and Hasenbein (arXiv:2303.17746v3) study robust stability over the family of queue-ratio policies, which steer each station's workload towards fixed proportions across its classes and contain the static-priority and quadratic max-weight policies as special cases. Their analysis is hierarchical. Under a queue-ratio policy the fluid model first reaches state-space collapse and then follows a linear Skorohod problem. This mission formalizes the second layer: a purely algebraic sufficient condition for stability of that Skorohod problem holds for every queue-ratio policy as soon as it holds at the finitely many static-priority "corners".

Timeline. Dai (1995) reduced stability of the queueing network to stability of its fluid model. Delgado (2010) related fluid stability under state-space collapse to stability of a Skorohod problem. Chen (1996) gave the Chen- $\mathcal S$ sufficient condition for stability of a linear Skorohod problem. Zhao, Gurvich and Hasenbein (preprint 2023, Operations Research 2025) proved that Chen- $\mathcal S$ is inherited from the static-priority corners (their Theorem 4).

Setting

Fix an open network with $J$ stations and $K$ classes. Class $k$ is served at station $s(k)$ , and the $J\times K$ constituency matrix $C$ has $C_{jk}=1$ if $s(k)=j$ and $0$ otherwise. $M=\operatorname{diag}(m_1,\dots,m_K)$ holds the mean service times $m_k>0$ . $P$ is the substochastic routing matrix, and $\alpha\ge 0$ the vector of exogenous arrival rates. The network is open: $I+P+P^2+\cdots$ converges and $I-P^\top$ is invertible. Then $Q=(I-P^\top)^{-1}$ , $\lambda=Q\alpha$ and the traffic intensities are $\rho=CM\lambda$ .

A ratio matrix is a $K\times J$ matrix $\Delta$ with $\Delta_{kj}=\delta_k\ge 0$ if $s(k)=j$ and $\Delta_{kj}=0$ otherwise, normalized by

CM\Delta=I.

It is static-priority if at each station $j$ exactly one class $k$ with $s(k)=j$ has $\Delta_{kj}=1/m_k$ and all others have $\Delta_{lj}=0$ . For a ratio matrix with $CMQ\Delta$ invertible, the reflection matrix and drift are

R_\Delta=(CMQ\Delta)^{-1},\qquad \theta_\Delta=R_\Delta(\rho-e).

A square matrix $R$ is an S-matrix if $Ru>0$ for some $u>0$ , and completely- $\mathcal S$ if every principal sub-matrix is an S-matrix. The pair $(R,\theta)$ is Chen- $\mathcal S$ if $R$ is completely- $\mathcal S$ and some $h>0$ satisfies $h_a^\top[\theta_a+R_{ab}u]<0$ for every partition $(a,b)$ of the stations with $a\neq\emptyset$ and every $u\ge 0$ with $\theta_b+R_bu=0$ . Ratio matrices are neighbors if they differ in at most one column.

Formalization targets

Goal: Theorem 4

If for every static-priority $\Delta$ the matrix $CMQ\Delta$ is invertible and $(R_\Delta,\theta_\Delta)$ is Chen- $\mathcal S$ , and all $\det(CMQ\Delta)$ over static-priority $\Delta$ have one sign, then

\forall\,\Delta\ \text{ratio matrix}:\quad CMQ\Delta\ \text{invertible and}\ (R_\Delta,\theta_\Delta)\ \text{Chen-}\mathcal S.

The network is arbitrary: any $J$ , $K$ , routing and service times.

Milestones

For neighbors $\Delta_1,\Delta_2$ and $\Delta_3=\lambda\Delta_1+(1-\lambda)\Delta_2$ with $\lambda\in(0,1)$ :

Lemma 4. The $k$ th rows of $R_{\Delta_1}$ and $R_{\Delta_2}$ are proportional with ratio $\det(CMQ\Delta_2)/\det(CMQ\Delta_1)$ , and $R_{\Delta_3}$ is a rank-one update of either.
Theorem 6. $R_{\Delta_3}=\beta R_{\Delta_1}+(1-\beta)R_{\Delta_2}$ , with $\beta=\lambda\det R_{\Delta_2}/(\lambda\det R_{\Delta_2}+(1-\lambda)\det R_{\Delta_1})$ .
Lemma 3. Invertibility of $CMQ\Delta_3$ when the determinants of $CMQ\Delta_1$ and $CMQ\Delta_2$ share a sign.
Theorem 5(i), (ii). Completely- $\mathcal S$ , and Chen- $\mathcal S$ of $(R_\Delta,\theta_\Delta)$ , pass from $\Delta_1,\Delta_2$ to $\Delta_3$ .
Theorem 3. The completely- $\mathcal S$ analogue of the goal.

Significance

By Chen's theorem, Chen- $\mathcal S$ of $(R_\Delta,\theta_\Delta)$ makes the Skorohod problem of the policy $\Delta$ stable. Theorem 4 reduces this requirement over a continuum of policies to a finite check, one per static-priority policy, and the paper combines it with a state-space-collapse result to certify robust queue-ratio stability of the DHV, push-started Lu–Kumar and Lu–Kumar networks. The orthogonal convexity of Theorem 5 is of independent interest: the Chen- $\mathcal S$ region of ratio matrices is in general not convex, yet it is convex along every axis-parallel segment.

The results are proved on paper and nothing in this mission has been machine-checked. A formal development checks the matrix algebra (adjugate and Sherman–Morrison identities, determinant-sign arguments) and settles the details the paper leaves out. The proof of Theorem 5(ii) is given there only as "an identical argument" to that of part (i). Theorem 6's claim $\beta\in(0,1)$ needs a same-sign hypothesis that the page omits (see below).

Difficulty

The obvious argument fails because the convexity is only orthogonal. The set of ratio matrices is a product of simplices. A convex combination of two arbitrary Chen- $\mathcal S$ ratio matrices need not be Chen- $\mathcal S$ , and the inverse $R_\Delta=(CMQ\Delta)^{-1}$ is not affine in $\Delta$ . Two pieces of structure must be found and exploited instead. Moving one column of $\Delta$ changes $CMQ\Delta$ in one column, which makes $R_\Delta$ move along a line in a reparametrized coordinate $\beta$ . Then completely- $\mathcal S$ and Chen- $\mathcal S$ , whose definitions quantify over all partitions and over the solution sets $\{u\ge 0:\theta_b+R_bu=0\}$ , must be shown to survive that line. The latter sets move with $\beta$ in a way that does not follow from convexity of either endpoint's set. Passing from neighbors to all ratio matrices needs a column-by-column descent through faces of the product of simplices. Invertibility must be maintained along the way, which is where the common determinant sign at the corners enters.

Formalization scope

Stations are Fin J, classes Fin K; the paper's index $i$ is Lean's $i-1$ . The network is a structure Network J K with fields $s$ , $m$ , $P$ , $\alpha$ and the hypotheses $m>0$ , $P\ge 0$ , row sums of $P$ at most one, $\alpha\ge 0$ , summability of $P^n$ , and invertibility of $I-P^\top$ . The remark $K>J$ and the renewal arrivals are not used.
$C$ , $M=\operatorname{diag}(m)$ , $Q=(I-P^\top)^{-1}$ , $\lambda=Q\alpha$ , $\rho=CM\lambda$ are definitions computed from the network. $R_\Delta$ and $\theta_\Delta$ are definitions computed from $\Delta$ ; $\theta_\Delta$ is never a free vector.
Ratio matrices include $\delta\ge 0$ . Without it the goal would assert extrapolation outside the polytope of ratio matrices.
Lean's matrix inverse is $0$ on singular matrices. Every hypothesis on a corner and the goal's conclusion state invertibility of $CMQ\Delta$ explicitly.
Partitions are a : Finset (Fin J) with $b=a^{\mathrm c}$ ; sub-matrices are indexed by the subtypes. Chen- $\mathcal S$ quantifies over $a\neq\emptyset$ (for $a=\emptyset$ the condition reads $0<0$ and would make Chen- $\mathcal S$ unsatisfiable and the goal vacuous); $b=\emptyset$ is allowed. Principal sub-matrices in completely- $\mathcal S$ are those of nonempty index sets.
"All determinants have the same sign" is a single sign for all corners: either all are positive or all are negative.
The "Then, $\Delta_1,\Delta_2,\Delta_3$ are ratio-matrix neighbors" sentence of Lemmas 3, 4 and Theorems 5, 6 is kept as a first conjunct.
Deviation. Theorem 6 asserts $\beta\in(0,1)$ under invertibility alone, which fails when $\det R_{\Delta_1}$ and $\det R_{\Delta_2}$ have opposite signs. That clause is stated under $\det R_{\Delta_1}\det R_{\Delta_2}>0$ ; the two identities are stated unconditionally.

A complete development needs the adjugate and determinant identities for matrices differing in one column, a Sherman–Morrison formula for rank-one updates, and a decomposition of ratio matrices along faces of a product of simplices. The definitions of S-matrices, completely- $\mathcal S$ and Chen- $\mathcal S$ are reusable for other work on reflected processes. Proofs of the milestones, alternative proofs of Theorem 5 that avoid linear-programming duality, and counterexamples showing a hypothesis cannot be dropped are all welcome.

Selected references

Y. Zhao, I. Gurvich, J. Hasenbein, A Hierarchical Approach to Robust Stability of Multiclass Queueing Networks, arXiv:2303.17746v3, 2024. https://arxiv.org/abs/2303.17746
H. Chen, A sufficient condition for the positive recurrence of a semimartingale reflecting Brownian motion in an orthant, Annals of Applied Probability 6(3):758–765, 1996 (reference [5] of the source).
J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1):49–77, 1995 (reference [10] of the source).
R. Delgado, State space collapse and stability of queueing networks, Mathematical Methods of Operations Research 72(3):477–499, 2010 (reference [16] of the source).
M. Bramson, Stability of Queueing Networks, Lecture Notes in Mathematics 1950, Springer, 2008. https://doi.org/10.1007/978-3-540-68896-9

10 thms1 active userReviewed

Control Theory Dynamical Systems Graph Theory·Captain: mikedeng1

Sub/Super-Stochastic Matrix with Applications to Bipartite Tracking Control over Signed Networks 3: ψ < 1/(τd_M), Structural Balance and Leader Reachability Give Asynchronous Bipartite TrackingResearch Paper

Motivation

Networks of agents that interact both cooperatively and competitively are modelled by signed graphs: a positive edge weight means that one agent moves towards another, a negative weight means that it moves towards the other's opposite. Since Altafini's work on consensus over antagonistic networks (IEEE TAC 2013), the standard target on such networks has been bipartite consensus or bipartite tracking: the agents split into two camps that converge to values of equal size and opposite sign. With a leader, the camp containing the leader tracks the leader's state and the other camp tracks its negative.

Most analyses assume that all agents update at the same instants. In practice agents sample and communicate on their own clocks. Shi, Zheng, Shao and Cheng (arXiv:2004.01867v2, SIAM J. Control Optim. 2021) handle this asynchronous setting with a matrix tool: products of sub-stochastic matrices (nonnegative, row sums at most one) whose row-sum deficits propagate along the communication graph. This mission formalizes their first application, bipartite tracking of first-order agents with a static leader (§3).

Setting

There is one leader $v_0$ and $n$ followers $v_1,\dots,v_n$ . Follower weights form a matrix $\mathcal A=[a_{ij}]\in\mathbb R^{n\times n}$ : the edge $(v_j,v_i)$ exists iff $a_{ij}\neq 0$ , cooperative if $a_{ij}>0$ , competitive if $a_{ij}<0$ . The number $a_{i0}$ is the weight of the leader edge $(v_0,v_i)$ , which exists iff $a_{i0}\ne 0$ . The digraph $\tilde{\mathcal G}$ consists of the followers' digraph, the leader and the leader edges.

C1 (structural balance). The agents split as $\mathcal V_1\cup\mathcal V_2$ with $v_0\in\mathcal V_1$ , every weight inside a set is $\ge 0$ and every weight between the sets is $\le 0$ .
C2 (leader reachability). Every follower is reached from $v_0$ by a directed path in $\tilde{\mathcal G}$ .

Time is discrete with step size $\tau>0$ . Follower $v_i$ communicates only at its own instants $s^i_0\tau<s^i_1\tau<\cdots$ with $s^i_0=0$ and

s^i_{k+1}-s^i_k\le h\qquad(2.10)

for a constant $h\in\mathbb Z_+$ . Positions $x_i(k)\in\mathbb R^p$ evolve by $x_0(k+1)=x_0(k)$ and $x_i(k+1)=x_i(k)+\tau u_i(k)$ , with the asynchronous protocol

u_i(k)=\psi\sum_{v_j\in\mathcal N_i}|a_{ij}|\big[\operatorname{sgn}(a_{ij})x_j(k)-x_i(k)\big]+\psi|a_{i0}|\big[\operatorname{sgn}(a_{i0})x_0(k)-x_i(k)\big]

at the instants of $v_i$ , and $u_i(k)=0$ otherwise. Here $\psi>0$ is a gain. Bipartite tracking (Definition 3.1) means $\|x_i(k)-x_0(k)\|\to 0$ for $v_i\in\mathcal V_1$ and $\|x_i(k)+x_0(k)\|\to 0$ for $v_i\in\mathcal V_2$ . With $d_M=\max_i\big(\sum_{v_j\in\mathcal N_i}|a_{ij}|+|a_{i0}|\big)$ , the gain condition is

\psi<\frac{1}{\tau d_M}.\qquad(3.7)

In the error coordinates $e_i=x_i-x_0$ on $\mathcal V_1$ and $e_i=-x_i-x_0$ on $\mathcal V_2$ , the closed loop is $e(k+1)=(M(k)\otimes I_p)e(k)$ with $M(k)=I_n-\tau\psi\mathcal D(k)-\tau\psi\mathcal B(k)+\tau\psi|\mathcal A(k)|$ , where only the rows of followers active at time $k\tau$ differ from the identity.

Formalization targets

Goal: Theorem 3.3, sufficiency

\psi<\frac1{\tau d_M},\ \ \mathrm{C1},\ \ \mathrm{C2}\ \Longrightarrow\ \lim_{k\to\infty}\|x_i(k)-x_0(k)\|=0\ (v_i\in\mathcal V_1),\quad \lim_{k\to\infty}\|x_i(k)+x_0(k)\|=0\ (v_i\in\mathcal V_2),

for every choice of instants satisfying (2.10) and every initial state.

Milestones

Theorem 2.4 1): a product $F_q\cdots F_1$ of sub-stochastic matrices is sub-stochastic.
Theorem 2.4 2): with positive diagonals, if every row $i_2$ is fed through $[F_{s_2}]_{i_2i_1}>0$ by a row $i_1$ with $\Lambda_{i_1}[F_{s_1}]<1$ , $s_1<s_2$ , then $\|\prod_{s=1}^qF_s\|_\infty<1$ and $\rho(\prod_{s=1}^qF_s)<1$ .
The matrices $M(k)$ (p. 15): under (3.7) they are sub-stochastic with positive diagonals, and $\Lambda_i[M(k)]<1$ exactly when $v_i$ hears the leader at $k\tau$ .
Error system (3.6): under C1, $e_i(k+1)=\sum_j[M(k)]_{ij}e_j(k)$ .
Lemma 3.2: under (3.7), C1 and C2, $\big\|\prod_{s=k}^{k+Ph-1}M(s)\big\|_\infty<1$ for every $k$ , where $P=\max_i d(v_0,v_i)$ is the largest directed distance from the leader.

Significance

The theorem says that asynchrony costs nothing qualitatively: as long as every follower communicates at least once every $h$ steps and the gain respects (3.7), the network reaches bipartite tracking under the same topological conditions C1 and C2 as in the synchronous case. No common clock, dwell-time condition or joint connectivity of the switching graphs is required. The same product argument is reused in the rest of the paper for second-order and general linear agents, delays and switching topologies, so the milestones here are the base case of that series.

The result is proved in the paper; it has not been formalized. Formalizing it produces a checked theory of products of sub-stochastic matrices with row-sum deficits (Theorem 2.4), which applies to positive switched systems in general, and a reusable encoding of signed digraphs with a leader, structural balance and asynchronous protocols.

Difficulty

Each single matrix $M(k)$ is only marginally stable: its rows of followers that do not hear the leader at time $k\tau$ sum to exactly one, so no single step contracts, and the spectral radius of an individual $M(k)$ may equal one. Contraction appears only in products, and only once a deficit created at a leader edge has had time to travel along the paths of C2, one edge per window of $h$ steps; this requires that deficits never disappear again, which is where positive diagonals (from (3.7)) enter. The passage from "every window product has $\|\cdot\|_\infty<1$ " to convergence also needs a uniform bound below one over all windows; the paper's (3.14) uses it without comment. The bound holds because $M(k)$ depends on $k$ only through the set of active followers, so the window products range over a finite set.

Formalization scope

Followers are Fin n (0-based) and the leader is not an index; $a_{ij}$ is a i j and $a_{i0}$ is b i. Positions lie in EuclideanSpace ℝ (Fin p); the paper's norm is unspecified and all norms on $\mathbb R^p$ give the same limits. Eigenvalues are complex: $\rho(F)<1$ means every element of spectrum ℂ of the complexified matrix has modulus $<1$ . $\|F\|_\infty$ is the largest absolute row sum. Products multiply later factors on the left. $\operatorname{sgn}$ is Real.sign. The maxima $d_M$ and $P$ are given as values with IsGreatest hypotheses over exactly the printed sets, and (3.7) is kept as printed. C1 is stated for the partition $\mathcal V_1=\{v_0\}\cup V_1$ , $\mathcal V_2=$ the remaining followers; fixing the leader in $\mathcal V_1$ is the paper's "with no loss of generality" convention. Definition 3.1 is stated for that same partition.

Only the "if" half of Theorem 3.3 is a target. Definition 3.1 presupposes the partition of C1, so necessity of C1 has no formal meaning, and the printed necessity argument is an informal case discussion. Theorem 2.4 2) is stated with one $(i_1,s_1,s_2)$ per row $i_2$ , as its proof and the example on p. 8 use it; this is implied by the literal reading.

Three formalizations would trivialize the goal and are ruled out: a protocol in which every follower updates at every step (the synchronous special case, which drops the asynchronous instants); dropping the sign conditions of C1, or leaving the leader's side free, under which the followers of $\mathcal V_2$ need not approach $-x_0$ ; and a goal stated about the error system (3.6) instead of the agents' positions $x_i$ .

The development needs finite matrix products, the ∞-norm bound on eigenvalues (Gershgorin), and elementary walk reachability in digraphs. All of these exist in Mathlib in some form. Contributions are welcome on every milestone. The product theorem 2.4 does not depend on the network model and is reusable for positive switched systems.

Selected references

L. Shi, W. X. Zheng, J. Shao, Y. Cheng, Sub/super-stochastic matrix with applications to bipartite tracking control over signed networks, arXiv:2004.01867v2, 2020; SIAM J. Control Optim. 59 (2021). https://arxiv.org/abs/2004.01867, https://doi.org/10.1137/19M1239982
C. Altafini, Consensus problems on networks with antagonistic interactions, IEEE Trans. Automat. Control 58(4), 2013. https://doi.org/10.1109/TAC.2012.2224251

9 thms1 active userReviewed

Combinatorics Graph Theory·Captain: mikedeng1

Three Conjectures in Extremal Spectral Graph Theory 3: For Large n, a Connected n-Vertex Graph Maximizing Spectral Radius Minus Average Degree Is a Pineapple GraphResearch Paper

Motivation

How far is a graph from being regular? Several numerical irregularity measures answer this question, and spectral graph theory supplies a natural one. For a graph $G$ with $n$ vertices and $e(G)$ edges, the largest eigenvalue $\lambda_1(G)$ of the adjacency matrix is always at least the average degree $d(G) = 2e(G)/n$ , with equality exactly when $G$ is regular. The difference $\lambda_1 - d$ is therefore a measure of irregularity; it was studied by Bell (1992) alongside the variance of the degrees, and it is one of several such measures, with Albertson's $\sum_{uv \in E} |d_u - d_v|$ and Nikiforov's degree deviation among the others. The measures are incomparable in general, and one way to understand what each gauges is to determine its extremal graphs.

A basic extremal question asks which graphs are the most irregular. Among all graphs the question is uninteresting, because isolated vertices lower $d$ without lowering $\lambda_1$ . Among connected graphs it is a genuine optimization problem. Using the variable neighbourhood search system AutoGraphiX, Aouchiche, Bell, Cvetković, Hansen, Rowlinson, Simić and Stevanović (2008) found that the maximizers of $\lambda_1 - d$ over connected graphs on $n$ vertices are always pineapple graphs, a clique with pendant vertices hanging from one clique vertex, and they conjectured that this holds for every $n$ (Aouchiche et al., European J. Oper. Res. 2008).

Timeline:

1992: Bell compares $\lambda_1 - d$ with the degree variance as irregularity measures.
1988: Hong proves $\lambda_1^2 \le 2e(G) - (n-1)$ for graphs without isolated vertices.
2008: Aouchiche et al. state the pineapple conjecture from computer experiments, and determine which pineapple is best (clique size $\lceil n/2\rceil + 1$ ).
2017: Tait and Tobin prove the conjecture for all sufficiently large $n$ (arXiv:1606.01916, J. Combin. Theory Ser. B), in the same paper that settles the spectral extremal problems for outerplanar and planar graphs.

This mission formalizes Section 4 of Tait and Tobin.

Setting

All graphs are finite and simple; an $n$ -vertex graph has vertex set $\{0, \dots, n-1\}$ . The spectral radius $\lambda_1(G)$ is the largest eigenvalue of the adjacency matrix $A$ of $G$ , the published platform definition specRad. The average degree is $d(G) = 2e(G)/n$ , a real number.

A connected graph $G$ on $n$ vertices is a maximizer of $\lambda_1 - d$ (Lean: IsIrregMax G) if

\lambda_1(G') - d(G') \le \lambda_1(G) - d(G) \quad \text{for every connected graph } G' \text{ on the same } n \text{ vertices.}

The pineapple $PA(p,q)$ (Lean: pineapple p q) has $p+q$ vertices: the first $p$ form a complete graph $K_p$ , and each of the other $q$ vertices is a pendant vertex, adjacent only to the clique vertex $0$ . Stars ( $p \le 2$ ) and complete graphs ( $q = 0$ ) are degenerate pineapples.

The lemmas of the mission speak about the leading eigenvector $\mathbf v$ of a maximizer $G$ : a vector with $A\mathbf v = \lambda_1 \mathbf v$ , all entries positive, normalized so that its largest entry is $1$ . Such a vector exists by the Perron–Frobenius theorem because $G$ is connected. $x$ denotes a vertex with $\mathbf v_x = 1$ , $d_u$ the degree of $u$ , and $N(x)$ the neighbourhood of $x$ . Some statements carry a small parameter $\varepsilon > 0$ , fixed before $n$ .

Formalization targets

Goal: Theorem 21

\exists N\ \forall n \ge N\ \forall G \text{ on } n \text{ vertices}:\quad G \text{ maximizes } \lambda_1 - d \;\Longrightarrow\; \exists\, p, q,\ p + q = n,\ G \cong PA(p,q).

The clique size $p$ is left free. The optimal value $p = \lceil n/2\rceil + 1$ is determined by Aouchiche et al. by optimizing a cubic polynomial over pineapples; Tait and Tobin cite it and do not prove it, so it is not part of the goal.

Milestones, in the order of the proof

Hong's inequality $\lambda_1^2 \le 2e(G) - (n-1)$ for connected $G$ (cited, p. 14).
The pineapple $H = PA(\lceil n/2\rceil+1, \lfloor n/2\rfloor-1)$ has $\lambda_1(H) - 2e(H)/n \ge n/4 - 3/2$ (p. 14).
Lemma 16: $\lambda_1 = n/2 + c_1\sqrt n$ and $d = n/4 + c_2\sqrt n$ with $|c_1|, |c_2| < 1$ .
Lemma 17: $0 \le \frac{1}{|N(x)|}\sum_{y\sim x}(d_y - \lambda_1\mathbf v_y) \le c_3\sqrt n$ .
Lemma 18: a vertex $u \ne x$ with $\mathbf v_u > 1 - 2\varepsilon$ , $d_u - \lambda_1\mathbf v_u = O(\sqrt n)$ and $d_u \ge (1/2 - 2\varepsilon)n$ .
Inequality (11): $n/2 + \sqrt n + 5 \ge \mathbf v^t\mathbf v > n/2 - 2\varepsilon n - O(\sqrt n)$ .
Lemma 19 (corrected): $\mathbf v_a\mathbf v_b > 1/2 + n^{-1/2} + 5n^{-1}$ forces $a \sim b$ ; $\mathbf v_a\mathbf v_b < 1/2 - 3\varepsilon$ forbids $a \sim b$ when $G - ab$ is connected.
Every vertex other than a lone vertex of entry $1$ is adjacent to a vertex of entry $1$ (p. 18, corrected).
Proposition 20: a partition $U, V, W$ with $U$ a clique of size about $n/2$ and entries near $1$ , $V$ pendant vertices of entry below $(2+\varepsilon)/n$ , and $W$ vertices of entry near $1/2$ adjacent only to $U$ .
$W = \emptyset$ : $G$ is a clique together with pendant vertices (pp. 20–21).

Significance

The result. Theorem 21 identifies the most spectrally irregular connected graphs for large $n$ , confirming a conjecture that came from computer search and that had resisted the usual graph-transformation arguments. Combined with the cited optimization over pineapples, it gives the exact maximum of $\lambda_1 - d$ over connected $n$ -vertex graphs for large $n$ , which in turn bounds $\lambda_1$ by $d$ plus an explicit term for every connected graph. The intermediate statements, notably Lemma 19 which converts products of Perron entries into adjacency, are reusable in other spectral extremal problems over connected graphs.

Formalizing it. The theorem is proved on paper for large $n$ ; no machine-checked proof of it, or of Hong's inequality, is known. The formalization must make every "for $n$ sufficiently large" and every $O(\sqrt n)$ explicit, and it repairs two statements that are false as printed (see Formalization scope). A small- $n$ verification, or a proof for all $n$ , would be further contributions.

Difficulty

The obvious approach is local improvement: given a non-pineapple, move an edge and show that $\lambda_1 - d$ increases. Each move changes both terms, by amounts of order $\mathbf v_a\mathbf v_b/\mathbf v^t\mathbf v$ and $2/n$ respectively, and these are comparable; neither the sign of the change nor connectivity of the modified graph is under control without first knowing the global structure. The proof therefore needs the whole chain of asymptotic estimates: the size of $\lambda_1$ and $d$ , a second vertex of nearly maximal entry, the norm of the Perron vector, and only then the adjacency rules of Lemma 19. Every edge deletion must also keep the graph connected, since the maximum ranges over connected graphs.

Formalization scope

Vertices are Fin n; graphs are SimpleGraph (Fin n) with classical decidability. $\lambda_1$ is the published WangKangXue.SpectralTuran.specRad, the largest eigenvalue of G.adjMatrix ℝ. $d$ is avgDeg G = 2 · #edges / n in $\mathbb R$ .
The maximum is over connected graphs on the same vertex set (IsIrregMax); dropping connectivity changes the problem.
The Perron vector enters as universally quantified hypotheses: any v with (G.adjMatrix ℝ).mulVec v = specRad G • v, all entries positive, all entries at most $1$ , and a vertex x with v x = 1. It is never quantified existentially.
"For $n$ sufficiently large" is ∃ N, ∀ n ≥ N. Constants from $O(\sqrt n)$ and "a constant $c_3$ not depending on $n$ " are existentially quantified before $N$ , $n$ and $G$ . In Lemma 18, inequality (11) and Lemma 19 the proof works for every $\varepsilon > 0$ , which is universally quantified; Proposition 20 needs $\varepsilon$ small and is stated for $0 < \varepsilon < \varepsilon_0$ .
$\lceil n/2\rceil$ and $\lfloor n/2\rfloor$ are the natural-number quotients $(n+1)/2$ and $n/2$ ; the pineapple lower bound assumes $n \ge 2$ .
" $G$ is a pineapple" is a graph isomorphism G ≃g pineapple p q with $p + q = n$ . The pineapple is defined by its edges, clique plus pendants at one vertex; it is not defined by any property that the proof establishes, and the clique size is not pinned.
Two printed statements are corrected and the corrections are disclosed. Lemma 19's second half requires $G - ab$ to be connected (without it, a pendant edge of the extremal pineapple is a counterexample), and both halves are for distinct vertices. The claim on p. 18 that every vertex has a neighbour of entry $1$ excludes only a vertex that is the unique vertex of entry $1$ (the hub of a pineapple is the exception). Lemma 17's summand is $(d_y - \lambda_1\mathbf v_y)$ , as in its proof.
A trivializing formalization is ruled out: the class is connected graphs, extremality is the hypothesis rather than a consequence, the eigenvector is universally quantified, constants do not depend on $n$ , and the clique size is free. A maximizer exists for every $n \ge 1$ , so the goal is not vacuous.
Needed infrastructure: Perron–Frobenius for connected graphs, the Rayleigh-quotient characterization of $\lambda_1$ , Cauchy interlacing (or monotonicity of $\lambda_1$ under subgraphs), and Hong's inequality. These are reusable well beyond this mission, and contributions of any of them are welcome.

Selected references

M. Tait and J. Tobin, Three conjectures in extremal spectral graph theory, J. Combin. Theory Ser. B (2017); arXiv:1606.01916v2. https://arxiv.org/abs/1606.01916
M. Aouchiche, F. K. Bell, D. Cvetković, P. Hansen, P. Rowlinson, S. K. Simić and D. Stevanović, Variable neighborhood search for extremal graphs. 16. Some conjectures related to the largest eigenvalue of a graph, European J. Oper. Res. 191(3) (2008) 661–676. (Reference [3] of Tait–Tobin.)
Y. Hong, A bound on the spectral radius of graphs, Linear Algebra Appl. 108 (1988) 135–139. (Reference [37].)
F. K. Bell, A note on the irregularity of graphs, Linear Algebra Appl. 161 (1992) 45–54. (Reference [5].)
M. O. Albertson, The irregularity of a graph, Ars Combin. 46 (1997) 219–225. (Reference [1].)
V. Nikiforov, Eigenvalues and degree deviation in graphs, Linear Algebra Appl. 414(1) (2006) 347–360. (Reference [26].)

13 thms1 active userReviewed

Mathematical Physics Quantum Information·Captain: mikedeng1

Quantum Algorithm for Simulating Real Time Evolution of Lattice Hamiltonians 1: Lieb–Robinson Bound ‖[A(t),B]‖ ≤ (2/√η)‖A‖‖B‖(e^{ζ|t|√(8η)}−1)Σ_{x∈X}e^{−μ dist(x,Y)} Under Small CommutatorsResearch Paper

Motivation

A local quantum system is built from degrees of freedom placed at sites of a lattice. Its Hamiltonian may contain many terms, each acting on a small group of sites. Even though a term is local, time evolution can spread an observable beyond its original support. A Lieb–Robinson bound limits the size of a commutator between the evolved observable and one supported elsewhere. It gives a quantitative way to say that information propagates with an effective finite velocity. The Appendix C bound of Haah, Hastings, Kothari and Low treats interactions with exponential spatial decay and makes the effect of almost commuting Hamiltonian terms explicit.

The paper studies quantum simulation, where a system's real time evolution is approximated by a circuit. Lemma 12 is an analytic ingredient: it controls how far a local observable can spread during the simulated evolution. The mission targets that lemma and the displayed estimates in its proof, with the constants printed in the pinned arXiv version. The paper proves the results; the remaining task here is to give the stated finite system version machine checked proofs.

Setting

Let $\Lambda$ be a finite set of sites equipped with a metric $\operatorname{dist}(x,y)$ . Each site has the same local Hilbert space $\mathbb C^q$ , and the whole system has product basis indexed by configurations $\sigma:\Lambda\to\{0,\ldots,q-1\}$ . An operator supported on $X\subseteq\Lambda$ is a matrix of the form $m_X\otimes I_{\Lambda\setminus X}$ : it may change the configuration on $X$ , but acts as the identity on every site outside $X$ . The matrix norm throughout is the spectral operator norm.

For every $X\subseteq\Lambda$ , let $h_X$ be a Hermitian operator supported on $X$ , and define the time independent Hamiltonian $H=\sum_{X\subseteq\Lambda}h_X$ . The sum includes all subsets, including the empty set. Let

O(t;J)=e^{iJt}Oe^{-iJt},\qquad O(t)=O(t;H).

For site sets, write $X\sim Y$ when $X\cap Y\ne\varnothing$ , and $\operatorname{dist}(x,Y)=\min_{y\in Y}\operatorname{dist}(x,y)$ when $Y$ is nonempty. The diameter is $\operatorname{diam}(X)=\max_{x,y\in X}\operatorname{dist}(x,y)$ for nonempty $X$ . The paper imposes two quantitative conditions. First, for some $0\le\eta\le1$ , every pair of terms has a small commutator:

\|[h_X,h_Y]\|\le 2\eta\|h_X\|\|h_Y\|.\tag{14}

Second, for some $\zeta,\mu>0$ , the interactions decay in the weighted sense

\sum_{X\ni x}\|h_X\|\,|X|^2e^{\mu\operatorname{diam}(X)}\le\zeta \qquad(x\in\Lambda).\tag{15}

Neither condition bounds each $\|h_X\|$ by one. This matters because the result is meant to include large but nearly commuting terms. These conventions are from Appendix C.1 of the source.

Formalization targets

The goal is Lemma 12. For an operator $A$ supported on $X$ and an operator $B$ supported on a disjoint set $Y$ , and every real $t$ , the proposed formal statement is

\|[A(t),B]\|\le \frac{2}{\sqrt\eta}\|A\|\|B\| \bigl(e^{\zeta|t|\sqrt{8\eta}}-1\bigr) \sum_{x\in X}e^{-\mu\operatorname{dist}(x,Y)}. \tag{16}

The coefficient of $|t|$ in the exponential is proportional to $\sqrt\eta$ . The goal keeps the paper's explicit factor $2/\sqrt\eta$ , its $\sqrt{8\eta}$ inside the exponential, and the full sum over sites in $X$ . The statement is for $\eta>0$ , as the displayed formula is undefined at $\eta=0$ ; a family satisfying (14) with $\eta=0$ also satisfies it for any positive $\eta\le1$ .

The milestones follow the source's numbered displays: the initial estimates for $C_B$ and $D_B$ in (28), their integral inequalities (24) and (27), the linked set series (32), the four estimates of Proposition 13, and the bound on its $k$ th line in (37). Here $C_B(X,t)$ takes a supremum over supported operators of norm at most one, and $D_B(X,t)=\|[h_X(t),B]\|$ . The milestone list is a map of the quantities that the proof controls, while the goal itself mentions only the physical operators and the two hypotheses.

Significance

The bound shows that a commutator is small when the support of $B$ is far from $X$ , with a rate determined by the decay parameter $\mu$ and the small commutator parameter $\eta$ . It applies to finite systems of any size with the same constants in (14) and (15). This makes it useful for reasoning about local approximations of time evolution in the quantum simulation setting of the paper. The authors also explain why a velocity proportional to $\sqrt\eta$ can occur under their hypotheses, so a linear dependence on $\eta$ is not generally available. See the discussion immediately after Lemma 12 in Appendix C.1.

Formalizing the result would supply a reusable finite matrix model of local observables and a checked version of the analytic estimates for near commuting interactions. The source paper provides a proof, but this proposed statement and its milestones currently have no machine checked proof in the mission. The definitions of support, Heisenberg evolution and linked interactions may also be reused in later formalizations of quantum lattice dynamics.

Difficulty

The obvious global norm bound $\|[A(t),B]\|\le2\|A\|\|B\|$ ignores the distance between supports. Merely bounding $\|H\|$ also loses spatial information and can grow with the whole system. The sharper statement simultaneously tracks where an interaction overlaps the current support and how the small commutator factor enters repeated interactions. A rigorous treatment must control a supremum over local operators, time dependent matrix exponentials, and an infinite series of finite linked set sums without changing any of the paper's constants.

Formalization scope

Sites form an arbitrary finite metric space, a disclosed generalization of the lattice setting used for the main algorithm. A common local dimension $q$ is used at every site; qubits occur at $q=2$ . Operators are complex matrices on the configuration space $\Lambda\to\operatorname{Fin}(q)$ , with Mathlib's scoped L2 operator norm. Every term is Hermitian and explicitly supported on its stated set, and $H$ is the sum over all subsets. Time is real and $H$ is constant in time. The paper mentions a piecewise continuous time dependent extension, which this mission does not state.

The goal explicitly requires $X\cap Y=\varnothing$ . The printed sentence of Lemma 12 omits this, but its derivation on page 24 assumes it; without disjointness the right side is zero at $t=0$ while the left side need not be. The positive $\eta$ condition is likewise explicit. These are the two repairs to the printed lemma, and they are recorded on each relevant item. The milestones (24) and (27) are restricted to $t\ge0$ , the direction for which the displayed forward integral uses $D_B(Z,s)$ and $C_B(Z\cup X,s)$ .

For an empty set, the Lean point to set distance and the local set distance are taken to be zero; a supported operator on the empty set is a scalar, so its commutators vanish. $C_B$ uses a real supremum of a nonempty, bounded set, and (32) states an actual sum with HasSum. The integral milestones involve continuous finite dimensional evolution. The support definition includes nonconstant single site operators, and the $q=2$ case is part of the goal. These choices prevent the result from being obtained through a vacuous support predicate, an entrywise norm, division by zero at $\eta=0$ , a default value of an unbounded supremum or divergent sum, or omitted disjointness. Contributions that establish the support calculus, matrix evolution estimates, integral inequalities, or linked set bounds are all within scope.

Selected references

Jeongwan Haah, Matthew B. Hastings, Robin Kothari and Guang Hao Low, Quantum algorithm for simulating real time evolution of lattice Hamiltonians, SIAM Journal on Computing, 2021. arXiv:1801.03922v4, Appendix C.1–C.3, pp. 21–25.

9 thms1 active userReviewed

Computational Geometry Machine Learning·Captain: mikedeng1

Turning Big Data into Tiny Data: Constant-Size Coresets for k-Means, PCA, and Projective Clustering II: An SVD Coreset of at Most 2(j + ⌈j/ε⌉ − 1) Weighted Points for Affine j-SubspacesResearch Paper

Motivation

Principal component analysis (PCA) asks for the $j$ -dimensional affine subspace that best fits a cloud of $n$ points in $\mathbb R^d$ in the least-squares sense. When $n$ is very large, or the points arrive as a stream or are spread over many machines, one wants to replace the data by a small summary on which the cost of every candidate subspace can still be evaluated, up to a factor $1+\varepsilon$ . Such a summary is a coreset. Coresets for the $j$ -subspace problem are the building block of the streaming and distributed PCA and projective clustering algorithms of Feldman, Schmidt and Sohler (SIAM J. Comput. 49(3), 2020), whose sizes depend on $j$ and $\varepsilon$ only, not on $n$ or $d$ .

For linear subspaces (through the origin) the paper's Theorem 17 gives a deterministic coreset of $m=O(j/\varepsilon)$ points read off the singular value decomposition. Data are rarely centred, though, and subtracting the mean before the computation does not survive the union of coresets with different means (p. 616). Section 4 of the paper repairs this: Theorem 19 gives a coreset for affine $j$ -subspaces whose points already carry the mean, at the price of doubling the size and weighting the points. This mission formalizes Theorem 19.

Setting

A data set of $n$ points in $\mathbb R^d$ is a matrix $A\in\mathbb R^{n\times d}$ whose rows $A_{i*}$ are the points. For a nonempty set $C\subseteq\mathbb R^d$ and a point $p$ , $\operatorname{dist}(p,C)=\inf_{c\in C}\|p-c\|_2$ . The cost of $C$ is

\operatorname{dist}^2(A,C)=\sum_{i=1}^n\operatorname{dist}^2(A_{i*},C),

and for weights $w_1,\ldots,w_r\ge0$ on the rows of $S\in\mathbb R^{r\times d}$ the weighted cost is $\sum_i w_i\operatorname{dist}^2(S_{i*},C)$ . The squared Frobenius norm is $\|M\|_F^2=\sum_{i,k}M_{ik}^2$ .

A singular value decomposition (SVD) of $A$ is a factorization $A=U\Sigma V^T$ with $U\in\mathbb R^{n\times n}$ and $V\in\mathbb R^{d\times d}$ orthogonal and $\Sigma\in\mathbb R^{n\times d}$ rectangular diagonal with nonnegative, nonincreasing diagonal entries $\sigma_1\ge\sigma_2\ge\cdots$ . $\Sigma^{(m)}$ keeps the first $m$ diagonal entries and sets the rest to $0$ ; the $m$ -rank approximation is $A^{(m)}=U\Sigma^{(m)}V^T$ (Definition 1).

The mean row is $\mu(A)=\frac1n\sum_iA_{i*}$ and the centred matrix is $A'=A-\mathbb 1\cdot\mu(A)$ , whose rows are $A_{i*}-\mu(A)$ .

Algorithm 1, subspace-Coreset $(A,j,\varepsilon)$ , sets $m=\min\{n,d,j+\lceil j/\varepsilon\rceil-1\}$ , returns the matrix $S$ of the first $m$ rows of $\Sigma^{(m)}V^T$ (all other rows are zero), the weights $w_i=1$ , and $\Delta=\|A-A^{(m)}\|_F^2$ .

Algorithm 2, affine- $j$ -subspace-Coreset $(A,j,\varepsilon)$ , runs Algorithm 1 on $A'$ , obtaining $(S',\Delta)$ with $m=|S'|$ , and returns

S=\mathbb 1\cdot\mu(A)+\sqrt{\frac mn}\cdot\begin{bmatrix}S'\\-S'\end{bmatrix}\in\mathbb R^{2m\times d},\qquad w=\Bigl(\frac n{2m},\ldots,\frac n{2m}\Bigr),

together with $\Delta$ .

Formalization targets

Goal: Theorem 19 (p. 617)

Let $n\ge1$ , $j\in[1,d-1]$ and $\varepsilon>0$ , and let $(S,\Delta,w)$ be the output of Algorithm 2 for any SVD of $A'$ . Then $S\in\mathbb R^{(2m)\times d}$ , $m\le j+\lceil j/\varepsilon\rceil-1$ , $\Delta\ge0$ , and for every affine $j$ -dimensional subspace $C$ of $\mathbb R^d$ ,

\operatorname{dist}^2(A,C)\le\sum_{i=1}^{2m}w_i\operatorname{dist}^2(S_{i*},C)+\Delta\le(1+\varepsilon)\operatorname{dist}^2(A,C).

Milestones

Theorem 17 (p. 615): for any SVD of $A$ , the output of Algorithm 1 satisfies $\operatorname{dist}^2(A,L)\le\sum_{i=1}^m\operatorname{dist}^2(S_{i*},L)+\Delta\le(1+\varepsilon)\operatorname{dist}^2(A,L)$ for every $j$ -dimensional linear subspace $L$ .
Lemma 18 (p. 616): if $\mu(M)=\vec0$ , $L$ is a linear $j$ -subspace and $t\in L^\perp$ , then $\operatorname{dist}^2(M,t+L)=\operatorname{dist}^2(M,L)+n\|t\|^2$ .
Display (7) (p. 618): with $S''=\sqrt{m/n}\,[S';-S']$ , $\operatorname{dist}^2(A',L)\le\frac n{2m}\operatorname{dist}^2(S'',L)+\Delta\le(1+\varepsilon)\operatorname{dist}^2(A',L)$ for every linear $j$ -subspace $L$ .

Theorem 17 rests on Corollary 16 and Claim 3 of the paper; those are milestones of the companion mission Turning Big Data into Tiny Data … I and are not posed again here.

Significance

The result. Theorem 19 gives a deterministic summary of $2m\le2(j+\lceil j/\varepsilon\rceil-1)$ weighted points and one scalar that preserves the cost of every affine $j$ -subspace within $1+\varepsilon$ , for arbitrary data, with no assumption on the mean. Because its points carry the mean, coresets of different data sets can be merged, which the merge-and-reduce streaming constructions of the paper's later sections need. Any $(1+\varepsilon')$ -approximate PCA solution computed on the coreset is then a $(1+\varepsilon)(1+\varepsilon')$ -approximate solution for the full data.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any coreset theorem, exists on the platform. A complete development would produce the cost identities for sums of squared distances to linear and affine subspaces in Lean, the effect of centring and orthogonal translation on these costs, and the use of the SVD truncation as a summary, all of which are reusable for other PCA, low-rank approximation and projective clustering results.

Difficulty

The obvious construction, centring the data, computing the linear coreset of the centred data and adding the mean back, fails: the linear coreset $S'$ need not have mean $\vec0$ , and translating a subspace by $t\perp L$ changes the cost of a point set by a multiple of $\|t\|^2$ that depends on the number of points (p. 617). The paper's construction has to match both the mean and the total weight of the original data while keeping the linear-subspace guarantee, and the formal proof has to carry this through the reduction of an arbitrary affine subspace to a linear one plus an orthogonal translation. Beneath it lies Theorem 17, which needs the SVD-based estimate of the companion mission (Corollary 16) and the passage from the $n$ -row matrix $A^{(m)}=U\Sigma^{(m)}V^T$ to the $m$ nonzero rows of $\Sigma^{(m)}V^T$ . Distances to subspaces in Lean are infima over sets, so the identities $\operatorname{dist}^2(A,L)=\|AY\|_F^2$ for an orthonormal basis $Y$ of $L^\perp$ must themselves be established.

Formalization scope

Representation. Points are rows of Matrix (Fin n) (Fin d) ℝ, read as points of EuclideanSpace ℝ (Fin d). $\operatorname{dist}$ is Metric.infDist. Linear $j$ -subspaces are Submodules of finrank $j$ ; affine ones are AffineSubspaces whose direction has finrank $j$ , and $t+L$ is AffineSubspace.mk' t L. The SVD and $A^{(m)}$ are the published ProjLikeRetr.FixedRank.IsSVD and truncSVD. Every statement holds for an arbitrary SVD; none is chosen.
Pinned hypotheses and readings.
1. The page's " $\Delta>0$ " (Theorems 17 and 19) is false when $\operatorname{rank}A'\le m$ , for instance when all points coincide; the statements claim $\Delta\ge0$ .
2. $n\ge1$ is added to Theorem 19 and (7), since Algorithm 2 divides by $n$ .
3. "subspace-Coreset $(P,j,\varepsilon)$ " is read with $P=A$ .
4. Theorem 17's $S\in\mathbb R^{m\times d}$ is the first $m$ rows of $\Sigma^{(m)}V^T$ , as the text before it says, although Algorithm 1, line 3 writes the whole matrix.
5. Lemma 18's "affine $j$ -dimensional subspace $L$ " is a linear subspace: the lemma uses $L^\perp$ , and the proof of Theorem 19 applies it to linear $L$ .
6. Theorem 19's affine subspace $C$ is also required to be nonempty; this follows from $j\ge1$ and guards against Mathlib's convention that the distance to $\emptyset$ is $0$ .
Conventions. $m\le j+\lceil j/\varepsilon\rceil-1$ is written $m+1\le j+\lceil j/\varepsilon\rceil$ . Diagonal positions of $\Sigma$ are 0-based in Lean. The $2m$ output rows are $\mu+\sqrt{m/n}\,S'_{i*}$ followed by $\mu-\sqrt{m/n}\,S'_{i*}$ . Weights are the real number $n/(2m)$ with $m=|S'|$ , not the cap $j+\lceil j/\varepsilon\rceil-1$ .
Not trivializable. The goal quantifies over affine, not linear, subspaces; the coreset is built from an SVD of the centred matrix $A'$ and $\Delta$ is the residual of $A'$ , so neither the mean nor the centring can be dropped; and no hypothesis is vacuous (any data matrix with any of its SVDs satisfies them).
Not formalized. The running-time clauses (" $O(\min\{nd^2,dn^2\})$ time") and §4.1 (weighted inputs).
Welcome contributions. Lemmas computing $\operatorname{dist}^2$ to subspaces via orthogonal projections, invariance of these costs under orthogonal maps, and the cost identity for symmetric point sets.

Selected references

D. Feldman, M. Schmidt, C. Sohler, Turning Big Data into Tiny Data: Constant-Size Coresets for k-Means, PCA, and Projective Clustering, SIAM J. Comput. 49(3):601–657, 2020. https://doi.org/10.1137/18M1209854
P.-A. Absil, J. Malick, Projection-like Retractions on Matrix Manifolds, SIAM J. Optim. 22(1):135–158, 2012 (source of the published SVD definition used here). https://doi.org/10.1137/100802529

7 thms1 active userReviewed

Optimization Quantum Information·Captain: mikedeng1

The Sum-of-Squares Hierarchy on the Sphere, and Applications in Quantum Information Theory II: The Dual of the ℓ-th DPS Cone Is the Set of M for Which ‖y‖^{2(ℓ−1)}·p_M Is a Real Sum of SquaresResearch Paper

Motivation

Deciding whether a bipartite quantum state is entangled is a basic computational problem of quantum information theory, and it is NP-hard in general (Gurvits 2003). The most widely used family of tests is the DPS hierarchy of Doherty, Parrilo and Spedalieri (DPS 2002, DPS 2004): a sequence of semidefinite programs, indexed by an integer level $\ell\ge1$ , whose feasible sets shrink to the set of separable states. On the dual side, a matrix $M$ that is nonnegative on separable states is an entanglement witness, and certifying such witnesses is the problem of certifying nonnegativity of a biquadratic Hermitian form, a classical question in real algebraic geometry.

That the DPS hierarchy is, dually, a sum-of-squares hierarchy for these forms has been used repeatedly in the literature, but, as Fang and Fawzi note (arXiv:1908.05155v1, p. 4), without a formal and complete proof. Their Theorem 12 gives one. They then combine it with their sum-of-squares convergence rate on the sphere (Theorem 2 of the same paper) to recover the $O(d_B^2/\ell^2)$ convergence rate of Navascués, Owari and Plenio 2009 for the DPS hierarchy.

Timeline:

2002–2004: Doherty, Parrilo, Spedalieri introduce the hierarchy and prove completeness.
2009: Navascués, Owari, Plenio prove $h_{\mathrm{DPS}_\ell}\le(1+O(d_B^2/\ell^2))h_{\mathrm{Sep}}$ by a quantum argument.
2019: Fang and Fawzi prove the duality (Theorem 12) and recover the 2009 rate from sums of squares (Theorem 15).

Setting

Let $\mathcal H_A=\mathbb C^{d_A}$ and $\mathcal H_B=\mathbb C^{d_B}$ . A matrix $M$ on $\mathcal H_A\otimes\mathcal H_B$ has entries $M_{ij,kl}$ (row $(i,j)$ , column $(k,l)$ ); $\mathrm{Herm}(d_Ad_B)$ is the space of Hermitian ones.

The separable cone $\mathcal{SEP}$ is the set of finite conic combinations $\sum_ip_i(x_ix_i^\dagger)\otimes(y_iy_i^\dagger)$ , $p_i\ge0$ .
Fix $\ell\ge1$ and $\ell$ copies $B_1,\dots,B_\ell$ of $\mathcal H_B$ . The DPS cone $\mathcal{DPS}_\ell$ is the set of positive semidefinite $\rho$ on $\mathcal H_A\otimes\mathcal H_B$ that have a positive semidefinite extension $\rho_{AB[\ell]}$ on $\mathcal H_A\otimes\mathcal H_B^{\otimes\ell}$ with three properties: tracing out $B_2,\dots,B_\ell$ returns $\rho$ ; $(I\otimes\Pi_\ell)\rho_{AB[\ell]}(I\otimes\Pi_\ell)=\rho_{AB[\ell]}$ , where $\Pi_\ell=\frac1{\ell!}\sum_{\sigma\in\mathfrak S_\ell}P_\sigma$ projects onto the symmetric subspace of $\mathcal H_B^{\otimes\ell}$ ; and every partial transpose $\rho_{AB[\ell]}^{\mathsf T_{B[s]}}$ on $B_1,\dots,B_s$ , $s=1,\dots,\ell$ , is positive semidefinite.
The EXT cone $\mathcal{EXT}_\ell$ is the same without the partial-transpose conditions.
For a set $K$ , the dual cone is $K^*=\{M\in\mathrm{Herm}(d_Ad_B):\mathrm{Tr}[M\rho]\ge0\ \forall\rho\in K\}$ .
To $M$ is attached the Hermitian polynomial $p_M(x,\bar x,y,\bar y)=\sum_{ijkl}M_{ij,kl}x_i\bar x_ky_j\bar y_l$ .
A real-valued polynomial in $(x,\bar x,y,\bar y)$ is rsos if it is a finite sum of squares of Hermitian polynomials, equivalently of real polynomials in the real and imaginary parts of $x,y$ ; it is csos if it is a finite sum $\sum_i|q_i(x,y)|^2$ with $q_i$ holomorphic polynomials.

Formalization targets

Goal: Theorem 12

\mathcal{SEP}^*=\{M: p_M\ge0\},\qquad \mathcal{DPS}_\ell^*=\{M:\|y\|^{2(\ell-1)}p_M\ \text{is rsos}\},\qquad \mathcal{EXT}_\ell^*=\{M:\|y\|^{2(\ell-1)}p_M\ \text{is csos}\},

for all $d_A,d_B$ and all $\ell\ge1$ , with $M$ ranging over $\mathrm{Herm}(d_Ad_B)$ .

Milestones

Theorem 12 (i), the first equality.
The identity (37): $(x\otimes\bar y^{\otimes s}\otimes y^{\otimes\ell-s})^\dagger W(\cdot)=(x\otimes y^{\otimes\ell})^\dagger W^{\mathsf T_{B[s]}}(x\otimes y^{\otimes\ell})$ .
Lemma 19: $\|y\|^{2(\ell-1)}p_M$ is rsos iff it is $\sum_{s=0}^\ell(x\otimes\bar y^{\otimes s}\otimes y^{\otimes\ell-s})^\dagger W_s(x\otimes\bar y^{\otimes s}\otimes y^{\otimes\ell-s})$ with $W_s\succeq0$ .
(39): $(x\otimes y^{\otimes\ell})^\dagger(Y-\Pi_\ell Y\Pi_\ell)(x\otimes y^{\otimes\ell})=0$ .
The dual SDP description: $\mathcal{DPS}_\ell^*=\{M: M\otimes I_{B[2:\ell]}=(Y-\Pi_\ell Y\Pi_\ell)+\sum_{s=0}^\ell W_s^{\mathsf T_{B[s]}},\ Y\in\mathrm{Herm},\ W_s\succeq0\}$ .
Lemma 20: $\|y\|^{2(\ell-1)}p_M$ is csos iff it is $(x\otimes y^{\otimes\ell})^\dagger W(x\otimes y^{\otimes\ell})$ with $W\succeq0$ .
Theorem 15: there are absolute $C,C'>0$ with $h_{\mathrm{Sep}}(M)\le h_{\mathrm{DPS}_\ell}(M)\le(1+Cd_B^2/\ell^2)h_{\mathrm{Sep}}(M)$ for $\ell\ge C'd_B$ , whenever $(x\otimes y)^\dagger M(x\otimes y)\ge0$ .

Significance

Theorem 12 makes the DPS hierarchy and the sum-of-squares hierarchy for biquadratic forms interchangeable. A convergence bound for one is a convergence bound for the other: the paper uses this to derive the DPS rate (Theorem 15) from a rate for sums of squares on the sphere, and conversely quantum de Finetti arguments give sum-of-squares bounds. Part (iii) separates the two notions of Hermitian sum of squares: dropping the partial transposes corresponds exactly to passing from real to complex sums of squares. This explains, for example, why $(z+\bar z)^2$ (rsos but not csos) behaves differently in the two hierarchies.

The results are proved on paper; none is formalized. The mission produces a machine-checked statement and proof of the duality, together with the matrix-analytic infrastructure behind it: partial traces and partial transposes on $\mathcal H_A\otimes\mathcal H_B^{\otimes\ell}$ , the symmetric projector, conic duality for semidefinite cones, and the passage between Gram matrices and sums of squares. Theorem 15 additionally depends on the sphere rate of the companion mission (Theorem 6 there) and on the unproved Lemma 13 and display (26) of the paper.

Difficulty

The inclusion of each sum-of-squares cone in the corresponding dual cone is a direct computation. The reverse inclusions are harder: a certificate involving arbitrary Hermitian polynomials must yield positive semidefinite matrices indexed by the prescribed tensor products, even though its square terms can mix different patterns of complex conjugation. Likewise, weak semidefinite duality alone does not show that every element of $\mathcal{DPS}_\ell^*$ has the displayed finite certificate; limits of certificates may require a separate closedness argument. The symmetric-subspace condition adds another constraint because an extension must be supported on that subspace, not merely invariant under permutations.

Formalization scope

Indices: $\mathcal H_A\otimes\mathcal H_B$ is Fin dA × Fin dB (Mathlib's Kronecker convention); $\mathcal H_A\otimes\mathcal H_B^{\otimes\ell}$ is Fin dA × (Fin ℓ → Fin dB).
The level is written $\ell=m+1$ with $m\in\mathbb N$ , so $\ell\ge1$ is built in and $\|y\|^{2(\ell-1)}=\|y\|^{2m}$ ; $B_1,\dots,B_\ell$ are coordinates $0,\dots,m$ .
Matrices are complex; positive semidefiniteness is Mathlib's Matrix.PosSemidef (which includes Hermitian). Dual cones are subsets of $\mathrm{Herm}(d_Ad_B)$ with the pairing $\operatorname{Re}\mathrm{Tr}[M\rho]$ .
$p_M$ is (25) literally; " $p_M\ge0$ " is $\operatorname{Re}p_M\ge0$ .
rsos is a finite sum of squares of real polynomials (MvPolynomial over $\mathbb R$ ) in the real and imaginary parts of $(x,y)$ ; csos is a finite sum of $|q_i|^2$ with $q_i$ complex polynomials in $(x,y)$ only. Swapping the two, or allowing complex $g_i$ in rsos, would change parts (ii) and (iii).
Condition (21) is stated literally with the explicit projector; "commutes with all permutations" would be weaker and is not used.
In Theorem 15, $h_{\mathrm{Sep}}$ and $h_{\mathrm{DPS}_\ell}$ are real suprema over trace-one elements, $d_A,d_B\ge1$ is assumed so the sets are nonempty, and $C,C'$ are quantified before all dimensions.

No trivializing reading is available: the cones are defined by their page conditions, the dual cones keep the Hermitian constraint, and no degree bound or extra hypothesis is placed on the sums of squares. Welcome contributions include a general library for partial traces and transposes of multipartite matrices, the spanning property of $\{y^{\otimes\ell}\}$ in the symmetric subspace, and Gram-matrix characterizations of sums of squares of polynomials; all are reusable well beyond this mission.

Selected references

K. Fang, H. Fawzi, The sum-of-squares hierarchy on the sphere, and applications in quantum information theory, arXiv preprint, 2019. https://arxiv.org/abs/1908.05155v1
A. C. Doherty, P. A. Parrilo, F. M. Spedalieri, Distinguishing separable and entangled states, Physical Review Letters 88, 187904, 2002. https://arxiv.org/abs/quant-ph/0112007
A. C. Doherty, P. A. Parrilo, F. M. Spedalieri, Complete family of separability criteria, Physical Review A 69, 022308, 2004. https://arxiv.org/abs/quant-ph/0308032
M. Navascués, M. Owari, M. B. Plenio, Power of symmetric extensions for entanglement detection, Physical Review A 80, 052306, 2009. https://arxiv.org/abs/0906.2731
L. Gurvits, Classical deterministic complexity of Edmonds' problem and quantum entanglement, STOC 2003. https://doi.org/10.1145/780542.780545

9 thms1 active userReviewed

Combinatorics Graph Theory·Captain: mikedeng1

A Harary-Sachs Theorem for Hypergraphs: The Codegree-d Coefficient of the Characteristic Polynomial of a k-Graph as a Weighted Sum over Its Veblen InfragraphsResearch Paper

Motivation

The characteristic polynomial of an ordinary graph records spectral information in coefficients that can also be described by finite graph configurations. The classical Harary–Sachs theorem is an instance of this connection. For a uniform hypergraph, the adjacency object is a tensor rather than a matrix, and its characteristic polynomial is defined through a multivariate resultant. Clark and Cooper's hypergraph theorem gives a corresponding coefficient formula. It identifies the configurations that replace the elementary subgraphs of the graph case and assigns them weights determined by directed Eulerian structures. The result makes a tensor spectral invariant accessible through finite combinatorial objects.

The article appeared as Gregory J. Clark and Joshua N. Cooper, A Harary-Sachs theorem for hypergraphs, Journal of Combinatorial Theory, Series B (2021), DOI 10.1016/j.jctb.2021.01.002. This mission follows the pinned arXiv version 2, whose page and theorem numbers are used below.

Setting

A simple $k$ -graph $\mathcal H=([n],E)$ has a fixed vertex set of $n$ labeled vertices and a set $E$ of distinct edges, each containing exactly $k$ vertices. Isolated vertices remain part of $[n]$ . The normalized adjacency hypermatrix $\mathcal A_{\mathcal H}$ gives an ordered $k$ -tuple the value $1/(k-1)!$ when its underlying set is an edge, and zero otherwise. This normalization makes every ordering of the other $k-1$ vertices contribute the intended total weight.

The characteristic polynomial $\phi(\mathcal H)$ is the multivariate resultant of the coordinates of $(\lambda\mathcal I-\mathcal A_{\mathcal H})x^{k-1}$ . The resultant is characterized by three conditions: it vanishes exactly when homogeneous coordinate polynomials have a nonzero common complex root, it evaluates to one on the coordinate monomials, and it is irreducible over the complex coefficient field. Its degree in $\lambda$ is $t=n(k-1)^{n-1}$ . The codegree- $d$ coefficient $\phi_d(\mathcal H)$ is the coefficient of $\lambda^{t-d}$ ; this degree is fixed from the source theorem and is not read from an implementation of $\phi$ .

A multi-hypergraph $S$ is a multiset of $k$ -element edges. It is Veblen when the degree of every vertex is divisible by $k$ . Its flattening discards repeated edges, so $S$ is an infragraph of $\mathcal H$ when every edge of its flattening belongs to $E$ . Components use only vertices covered by edges; a labeled object may still sit in a larger ambient vertex set with unused vertices.

A rooting of $S$ is a sequence of its edges, each assigned a root vertex in that edge, with roots in nondecreasing order. An edge rooted at $u$ contributes a directed arc $u\to v$ to every other vertex $v$ of the edge. Summing these arcs with multiplicity produces a directed multigraph $D_R$ . An Euler rooting has balanced in- and out-degrees and connected positive-degree vertices. Its arborescence number $\tau(D_R)$ counts spanning trees of these active vertices directed toward a specified root, with parallel arcs distinguished. For connected $S$ , its associated coefficient is

C_S=\sum_{R:\,D_R\text{ Eulerian}}\frac{\tau(D_R)}{\prod_{v\in V(D_R)}\deg^-(v)}.

For disconnected $S$ , $C_S$ is the product of the coefficients of its connected components. These conventions follow Definitions 6–10 in the source.

Formalization targets

Differential trace and Euler rootings

The supporting targets identify when a monomial differential operator contributes to a matrix trace, and show that an Euler rooting determines a connected Veblen multi-hypergraph. The operator identity is counted by Euler tours with distinguishable parallel arcs. The resultant-to-trace identity quoted in the paper is also a milestone:

\phi_d(\mathcal H)=P_d\left(-\operatorname{Tr}_1(\mathcal H)/1,\ldots,-\operatorname{Tr}_d(\mathcal H)/d\right).

Here $P_d$ is the paper's sum over positive compositions of $d$ , and $\operatorname{Tr}_j$ is its differential trace from Equation (1).

Harary–Sachs coefficient formula

The goal uses the labeled form of Theorem 14. Let $\mathscr T_m(d,\mathcal H)$ be the set of ordered $m$ -tuples $(S_1,\ldots,S_m)$ of connected labeled Veblen infragraphs whose edge counts sum to $d$ . Then

\phi_d(\mathcal H)=\sum_{m=1}^{d}\frac{\bigl(-(k-1)^n\bigr)^m}{m!}\sum_{(S_1,\ldots,S_m)\in\mathscr T_m(d,\mathcal H)}\prod_{i=1}^{m}C_{S_i}.

The paper prints the equivalent sum over isomorphism classes, using automorphism groups and the copy weight $(\#H\subseteq\mathcal H)$ . The labeled expression is the result before that grouping. The isomorphism-class statement is outside this mission's Lean target and remains a separate formalization task.

Significance

The theorem expresses a coefficient of a resultant, defined algebraically over complex common roots, as a finite rational weighted sum over hypergraph configurations. It extends the graph case while preserving the exact normalization, sign, component count, and coefficient index. The formula can be used to study low codegree coefficients by enumerating finite Veblen infragraphs and their Euler rootings. Clark and Cooper also use associated coefficients to compare different hypergraph structures in the paper.

The formal development separates the resultant, the differential trace, and the combinatorial counts into reusable definitions. It would provide machine-checked statements of the paper's main equality and several links between those definitions. The Lean theorems in this draft are open targets with sorry placeholders; compiling their statements does not constitute a machine-checked proof of the paper's claims.

Difficulty

The ordinary matrix determinant has a direct expansion by permutations. A tensor characteristic polynomial is a multivariate resultant, so that expansion does not directly reveal which hypergraphs contribute to a coefficient. The trace side uses repeated partial derivatives, and repeated hyperedges can create several distinct rootings with the same directed arc multiplicities. Counting only a multiset of root assignments loses those orderings and changes the coefficient. The Eulerian condition, arborescence multiplicities, and factorial factors must agree simultaneously for the algebraic and combinatorial expressions to match.

Formalization scope

The Lean representation uses Fin n vertices, finite sets of simple edges, multisets of repeated edges, rational adjacency weights, and complex polynomials only for the resultant criterion. It assumes $k\ge2$ , $n\ge1$ , and $1\le d\le n(k-1)^{n-1}$ . The source fixes $k\ge2$ , and the latter two bounds expose the domain in which the printed coefficient expansion and its proof use $d$ . An isolated vertex of $\mathcal H$ counts in $n$ and in $(k-1)^n$ , while isolated vertices do not pad a multi-hypergraph component.

The formalization takes a polynomial satisfying the resultant's common-root, normalization, and irreducibility properties as an input. Separate sanity proofs give witnesses in the one-variable degree-zero and degree-one cases; degree one covers the first goal-domain degree when $k=2$ . The characteristic polynomial is evaluated from this polynomial, never defined by the trace identity. Rootings are sequences, arborescences are directed toward the least positive-degree vertex, and the associated coefficient is calculated on covered vertices. The goal uses the labeled sum, so no automorphism is computed on an ambient padded vertex set. Contributions formalizing the omitted isomorphism-class equivalence, the BEST circuit count, and proofs of the stated targets are welcome.

Selected references

Gregory J. Clark and Joshua N. Cooper, A Harary-Sachs theorem for hypergraphs, Journal of Combinatorial Theory, Series B, 2021. arXiv:1812.00468v2; DOI 10.1016/j.jctb.2021.01.002.

8 thms1 active userReviewed

Algebra Combinatorics Discrete Geometry·Captain: mikedeng1

Maximum Scattered Linear Sets and Complete Caps in Galois Spaces 1: Scattered 𝔽_q-Linear Sets of Rank rt/2 Exist in PG(r − 1, q^t) for t Even, in Three Families of (q, t)Research Paper

Motivation

Linear sets are the main tool for building point sets with few intersection sizes in finite projective spaces: sets meeting every hyperplane, two-intersection sets, translation ovoids, and the geometric side of finite semifields and rank-metric codes (Polverino, 2010). Among them, scattered linear sets are those whose points all carry the smallest possible weight, and a scattered linear set of the largest possible rank is called maximum scattered. By Blokhuis and Lavrauw (2000), a maximum scattered linear set of $\mathrm{PG}(r-1,q^t)$ of rank $rt/2$ is a two-intersection set with respect to hyperplanes, so each one yields a two-weight code and a strongly regular graph.

Timeline.

2000, Blokhuis–Lavrauw: the rank of a scattered $\mathbb F_q$ -linear set of $\mathrm{PG}(r-1,q^t)$ is at most $rt/2$ , and for $r$ even this bound is attained.
2000, Ball–Blokhuis–Lavrauw: examples of rank $6$ in $\mathrm{PG}(2,q^4)$ .
Classical: for $r=3$ , $t=2$ the bound $3$ is attained by Baer subplanes.
2000, Blokhuis–Lavrauw, Thm 4.4: existence (without explicit examples) for $r>3$ , $t=2$ , $q=2$ and for $r\ge3$ , $(t-1)\mid r$ , $t$ even, $q>2$ .
2015, Bartoli, Giulietti, Marino and Polverino (arXiv:1512.07467v1, Combinatorica 37 (2017)): three explicit families in $\mathrm{PG}(2,q^{2n})$ and, by direct sums, maximum scattered linear sets in $\mathrm{PG}(r-1,q^t)$ for $t$ even in three families of $(q,t)$ . This mission formalizes that result; the companion mission formalizes the paper's application to complete caps.

Setting

Let $q$ be a prime power, $t\ge1$ , and let $V$ be an $r$ -dimensional vector space over $\mathbb F_{q^t}$ ; $\mathrm{PG}(V,\mathbb F_{q^t})=\mathrm{PG}(r-1,q^t)$ has as points the spans $\langle v\rangle_{\mathbb F_{q^t}}$ of nonzero $v\in V$ . An $\mathbb F_q$ -subspace $U\subseteq V$ is a subset closed under addition and under multiplication by $\mathbb F_q$ . It defines the $\mathbb F_q$ -linear set

L_U=\{\langle u\rangle_{\mathbb F_{q^t}} : u\in U\setminus\{0\}\},

whose rank is $\dim_{\mathbb F_q}U$ . A linear set comes paired with $U$ , so every statement here is about $U$ . The weight of a point $\langle v\rangle$ is $\dim_{\mathbb F_q}(\langle v\rangle_{\mathbb F_{q^t}}\cap U)$ , and $L_U$ is scattered when every point of $L_U$ has weight $1$ ; equivalently, for every nonzero $u\in U$ ,

\lambda\in\mathbb F_{q^t},\ \lambda u\in U\ \Longrightarrow\ \lambda\in\mathbb F_q .

The plane construction (§2). Fix $n\ge2$ and the field $E=\mathbb F_{q^{6n}}$ with its subfields $\mathbb F_q\subseteq\mathbb F_{q^n}\subseteq\mathbb F_{q^{2n}}$ and $\mathbb F_{q^{3n}}$ . As an $\mathbb F_{q^{2n}}$ -space $E$ has dimension $3$ , so $\mathrm{PG}(E,\mathbb F_{q^{2n}})=\mathrm{PG}(2,q^{2n})$ . For $\omega\in\mathbb F_{q^{2n}}\setminus\mathbb F_{q^n}$ and an $\mathbb F_q$ -linear $f:\mathbb F_{q^{3n}}\to\mathbb F_{q^{3n}}$ the paper studies

U_f=\{f(x)+x\omega : x\in\mathbb F_{q^{3n}}\},

with $f$ a monomial $ax^{q^i}$ or a binomial $f_{i,a,b}(x)=ax^{q^i}+bx^{q^{2n+i}}$ . The relative norms $N_{q^m/q^d}(x)=\prod_{j<m/d}x^{q^{dj}}$ enter the hypotheses.

Formalization targets

Goal: Theorem 1.2 (p. 3)

For $t$ even and $r\ge2$ , in each of the cases (a) $q=2$ , $t\ge4$ ; (b) $t\not\equiv0\pmod3$ ; (c) $q\equiv1\pmod3$ , $t\equiv0\pmod3$ ,

\exists\,U\subseteq\mathbb F_{q^t}^{\,r}\ \ \mathbb F_q\text{-subspace}:\qquad \dim_{\mathbb F_q}U=\frac{rt}{2},\quad L_U\ \text{scattered}.

Milestones, in proof order

Proposition 2.1 (p. 5): $U_f$ has rank $3n$ , and $L_{U_f}$ is scattered iff $Q_f\cap\mathbb F_{q^{2n}}=\mathbb F_q$ , where $Q_f$ is the set of quotients $\frac{f(x)+x\omega}{f(y)+y\omega}$ , $y\ne0$ .
Proposition 2.2 (p. 6): the same criterion through the polynomial system (5)–(6).
Theorems 2.3, 2.4 (pp. 7, 9): the monomial families, for $n\not\equiv0\pmod 3$ and for $q\equiv1\pmod3$ .
Theorem 2.5 (p. 10): existence in $\mathrm{PG}(2,q^{2n})$ in those two regimes.
Lemma 2.6 (p. 11): $\varphi(x)/x$ and $\bar\varphi(x)/x$ have the same image, where $\bar\varphi$ is the trace adjoint.
Proposition 2.7, Lemma 2.8, Proposition 2.9, Theorem 2.10 (pp. 12–16): the binomial family for $q=2$ .
Theorem 3.1 (p. 16): direct sums of scattered linear sets are scattered, of rank $rt/2$ iff each summand has rank $s_it/2$ .
The line example (p. 2, cited from Lavrauw's thesis) and the Baer-subplane case $r=3$ , $t=2$ (p. 3).

Significance

Theorem 1.2 gives maximum scattered linear sets, and hence two-intersection sets, two-weight codes and strongly regular graphs, for infinitely many $(q,t)$ with $r$ odd, a regime where earlier existence results covered only a few values of $t$ . The $q=2$ case feeds the paper's second main result: scattered $\mathbb F_2$ -linear sets of $\mathrm{PG}(2,2^t)$ of rank $3t/2$ are translation caps, from which complete caps of size $2\sqrt{q^{\,n-1}}$ in $\mathrm{AG}(n,q)$ are built.

All statements are proved in the preprint; none has a machine-checked proof. Formalizing them requires a usable theory of subfields of a finite field as Frobenius fixed fields, relative norms and their images, linearized polynomials and their trace adjoints, and the passage between $\mathbb F_q$ -dimension, cardinality and weight. Each of these is reusable for later work on linear sets, MRD codes and semifields.

Difficulty

The criterion of Proposition 2.2 reduces scatteredness to a polynomial system, but the system has to be solved for a specific $f$ . For the monomials this rests on the solvability of $z^{q^i-1}=c$ in $\mathbb F_{q^{3n}}$ , a norm condition interacting with the gcd hypotheses. For the binomial with $q=2$ , the existence of a suitable $b$ (Lemma 2.8) needs a value-set bound for non-permutation polynomials (Turnwald, 1995) and a point count on a plane curve. The higher-dimensional statement then needs the elementary bound $\dim U\le st/2$ for scattered $U$ to obtain the rank equivalence in Theorem 3.1. A tempting shortcut, taking $U=\mathbb F_q^{\,r}$ or any small subspace, is scattered but has the wrong rank; the content is in the rank $rt/2$ .

Formalization scope

Citation basis. arXiv:1512.07467v1; page numbers equal PDF pages.
Fields. $\mathbb F_{q^m}\subseteq E$ is the fixed field of $x\mapsto x^{q^m}$ in a finite field $E$ of characteristic $p$ with $|E|=q^{6n}$ , $q=p^h$ . Norms and traces are explicit Frobenius products and sums.
Subspaces and rank. An $\mathbb F_q$ -subspace is a carrier set with closure conditions. Rank $k$ is $|U|=q^k$ ; in Theorem 3.1 rank $rt/2$ is $|W|^2=q^{rt}$ .
Points. Scatteredness takes the spanning field as an argument: $\mathbb F_{q^{2n}}$ in §2, the whole $\mathbb F_{q^t}$ in Theorem 1.2 and §3. $\mathrm{PG}(r-1,q^t)$ is modelled on Fin r → K; the plane of §2 on $E$ itself.
Pinned readings.
- Theorem 1.2 prints no range for $r$ . The preceding sentence and the proof (p. 17) say $r\ge5$ , and $r=1$ is false. The goal assumes $r\ge2$ , covered by the line example ( $r=2$ ), §2 with the Baer case ( $r=3$ ) and Theorem 3.1 ( $r\ge4$ ).
- $\omega$ is quantified over all of $\mathbb F_{q^{2n}}\setminus\mathbb F_{q^n}$ .
- The index ranges $1\le i\le3n-1$ (monomial) and $2n+i\le3n-1$ (binomial) come from the case headings on pp. 7 and 10.
- Proposition 2.7's printed " $wx$ " is $\omega x$ .
- Theorem 2.10 keeps its printed hypothesis $N_{2^{3n}/2^n}(b)\ne1$ .
- Theorem 3.1's rank clause assumes $t\ge2$ ; for $t=1$ it is false.
Ruled out. Taking the span over $E$ or over $\mathbb F_q$ , or dropping the rank, would make the statements false or trivial; every existence statement fixes the rank, and the span field is explicit.
Contributions welcome. Frobenius-fixed-field cardinalities, norm surjectivity, the criteria of Propositions 2.1–2.2, the monomial and binomial families, and the direct-sum rank computation.

Selected references

D. Bartoli, M. Giulietti, G. Marino, O. Polverino, Maximum scattered linear sets and complete caps in Galois spaces, arXiv:1512.07467v1 (2015); Combinatorica 37 (2017). https://arxiv.org/abs/1512.07467, https://doi.org/10.1007/s00493-016-3531-6
A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geom. Dedicata 81 (2000), 231–243. https://doi.org/10.1023/A:1005283806897
O. Polverino, Linear sets in finite projective spaces, Discrete Math. 310 (2010), 3096–3107. https://doi.org/10.1016/j.disc.2010.04.007
S. Ball, A. Blokhuis, M. Lavrauw, Linear (q + 1)-fold blocking sets in PG(2, q⁴), Finite Fields Appl. 6 (2000), 294–301.
M. Lavrauw, Scattered Spaces with respect to Spreads and Eggs in Finite Projective Spaces, Ph.D. thesis, TU Eindhoven, 2001.
G. Turnwald, A new criterion for permutation polynomials, Finite Fields Appl. 1 (1995), 64–82.

15 thms1 active userReviewed

Complexity Theory Graph Theory Optimization+1·Captain: mikedeng1

Most Tensor Problems Are NP-Hard 5: The Stability Number Is Read Off the Largest Eigenvalue of an Explicit Symmetric 3-TensorResearch Paper

Motivation

For a real symmetric matrix, the largest eigenvalue is the maximum of the quadratic form $\mathbf x^\top A\mathbf x$ on the unit sphere, and it is computable to any accuracy in polynomial time. Tensor eigenvalues, introduced independently by Lim (2005) and Qi (2005), extend this picture to higher order: they are the stationary values of the cubic form $\mathcal A(\mathbf x,\mathbf x,\mathbf x)$ on the unit sphere. They appear in multilinear statistics, signal processing, hypergraph theory and polynomial optimization, and for these applications the symmetric case is the natural one.

Hillar and Lim, in Most Tensor Problems Are NP-Hard (J. ACM 2013), show that the eigenvalue problem stays NP-hard when the tensor is required to be symmetric (their Theorem 9.3). The proof is short once one ingredient is available: a theorem of Nesterov (2003), in a form corrected by Hillar and Lim, that expresses the stability number of a graph as the maximum of an explicit cubic polynomial over a sphere. This mission formalizes that chain.

Setting

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,v\}$ , $v\ge1$ . A set of vertices is stable if no two of its members are adjacent; the stability number $\alpha(G)$ is the size of a largest stable set, so $1\le\alpha(G)\le v$ .

Put $n=v+v(v-1)/2$ and write a vector of $\mathbb R^n$ as $\mathbf z=(\mathbf x,\mathbf y)$ , with $\mathbf x=(x_1,\dots,x_v)$ indexed by vertices and $\mathbf y=(y_{ij})_{i<j}$ indexed by pairs of vertices. The tensor $\mathcal S_G=[\![s_{abc}]\!]\in\mathbb R^{n\times n\times n}$ has entry $1$ at the six orderings of the triple of coordinates $(x_i,x_j,y_{ij})$ for every non-adjacent pair $i<j$ , and $0$ elsewhere. It is symmetric: its entries do not change under any permutation of the three indices.

For a real 3-tensor $\mathcal A=[\![a_{abc}]\!]$ the cubic form is $\mathcal A(\mathbf z,\mathbf z,\mathbf z)=\sum_{a,b,c}a_{abc}z_az_bz_c$ , and a real $\lambda$ is a unit $\ell^2$ -eigenvalue of $\mathcal A$ if

\sum_{a,b}a_{abc}z_az_b=\lambda z_c\quad\text{for all }c,\qquad\text{for some }\mathbf z\text{ with }\|\mathbf z\|_2=1 .

Finally, $\lambda_l=2\sqrt{\tfrac23\left(1-\tfrac1l\right)}$ for $l\ge1$ . In Lean these are TensorNP.SymEigen.stabTensor, cubicForm, IsUnitL2Eigenvalue and lambdaL, and $\alpha(G)$ is Mathlib's SimpleGraph.indepNum.

Formalization targets

Goal: Theorem 9.3, core

\alpha(G)=\max\{\,l\in\{1,\dots,v\}:\ \lambda_l\text{ is a unit }\ell^2\text{-eigenvalue of }\mathcal S_G\,\}.

That is, $\lambda_{\alpha(G)}$ is an eigenvalue of $\mathcal S_G$ , and no $\lambda_l$ with $\alpha(G)<l\le v$ is. This is the statement on which the paper's $v$ -query reduction rests; nothing is claimed about $l<\alpha(G)$ .

Milestones, in the paper's order

Theorem 9.2 (Nesterov). With $\mathbb S^{n-1}=\{(\mathbf x,\mathbf y):\|\mathbf x\|_2^2+\|\mathbf y\|_2^2=1\}$ ,

\sqrt{1-\frac1{\alpha(G)}}=3\sqrt{\frac32}\cdot\max_{(\mathbf x,\mathbf y)\in\mathbb S^{n-1}}\ \sum_{i<j,\ \{i,j\}\notin E}x_ix_jy_{ij}.

The tensor. $\mathcal S_G$ is symmetric and $\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)=6\sum_{i<j,\{i,j\}\notin E}x_ix_jy_{ij}$ .
The maximum is an eigenvalue. $\max_{\|\mathbf z\|_2=1}\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)$ is attained and is a unit $\ell^2$ -eigenvalue of $\mathcal S_G$ .
Its value. $\max_{\|\mathbf z\|_2=1}\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)=\lambda_{\alpha(G)}$ .
Further result: Theorem 6.9 (Banach), (23). For every symmetric $\mathcal S\in\mathbb R^{n\times n\times n}$ ,

\sup_{\mathbf x,\mathbf y,\mathbf z\ne\mathbf 0}\frac{|\mathcal S(\mathbf x,\mathbf y,\mathbf z)|}{\|\mathbf x\|_2\|\mathbf y\|_2\|\mathbf z\|_2}=\sup_{\mathbf x\ne\mathbf 0}\frac{|\mathcal S(\mathbf x,\mathbf x,\mathbf x)|}{\|\mathbf x\|_2^3},

both sides finite. The paper uses it in §10 to transfer Theorem 9.3 to the spectral norm and the best rank-one approximation of symmetric tensors.

Significance

The result. Theorem 9.3 places symmetric tensor eigenvalue among the NP-hard problems of Hillar and Lim's Table I, and through Banach's theorem (Theorem 10.2 of the paper) the same holds for the largest singular value, the spectral norm and the best rank-one approximation of a symmetric 3-tensor. These are the quantities computed by higher-order power methods and by moment-based estimators, so the result marks where the matrix theory stops transferring.

Formalizing it. All results here are proved in the literature; none is machine-checked. Nesterov's theorem, which rests on the Motzkin–Straus theorem for the complement graph, is not on the platform or in Mathlib, and its formal statement settles the constant that the original paper got wrong by a factor $1/\sqrt2$ (Hillar–Lim, footnote 12). Banach's theorem on symmetric multilinear forms is likewise absent from Mathlib and is useful well beyond this mission.

Difficulty

The tensor identity (milestone 2) is bookkeeping. The analytic content sits in two places. First, Nesterov's theorem: the obvious route, fixing $\mathbf x$ and maximizing over $\mathbf y$ by Cauchy–Schwarz, reduces the cubic problem to a quartic one in $\mathbf x$ , whose value still has to be identified with $\alpha(G)$ ; that identification is the Motzkin–Straus theorem, which is not available in Lean and is itself a nontrivial optimization over the simplex. Second, the passage from a maximum to an eigenvalue needs a Lagrange multiplier argument on the sphere, and the symmetry of $\mathcal S_G$ is what makes the gradient of the cubic form match the eigen-equation. Part (b) of the goal needs a further, unprinted observation relating every unit eigenpair to the cubic form. Banach's theorem has no short proof; the classical arguments go through polarization estimates or a variational argument specific to symmetric forms.

Formalization scope

Tensors and indices. A 3-tensor is a function ι → ι → ι → ℝ on a finite index type. For $\mathcal S_G$ the index type is the disjoint union of the vertices Fin v and the pairs $\{(i,j): i<j\}$ ; this is $\mathbb R^n$ with coordinates labelled by name instead of by the paper's enumeration $\varphi(i,j)=(i-1)v-i(i-1)/2+j-i$ . Vertices are $0,\dots,v-1$ .
Normalization. Eigenvalues are taken with a unit eigenvector. The paper's Problem 9.1 and Definition 5.1 say only $\mathbf x\ne\mathbf 0$ ; since $(\lambda,\mathbf x)\mapsto(t\lambda,t\mathbf x)$ preserves the eigen-equation, that reading would make every nonzero real an eigenvalue of $\mathcal S_G$ and the goal false. The unit sphere (13) is where the paper derives the notion.
Explicit readings. The paper's index range " $1\le i<j<k\le v$ " in the definition of $s_{ijk}$ is read as $k\le n$ (taken literally it gives $\mathcal S_G=0$ ). Every "max" is stated as a greatest element, so attainment is claimed. In (23) the suprema are real suprema over nonzero vectors with boundedness part of the conclusion. $v\ge1$ is assumed wherever the paper uses $\alpha(G)\in\{1,\dots,v\}$ .
Not formalized. The oracle procedure of the proof of Theorem 9.3, the polynomial size of $\mathcal S_G$ , the input model of Problem 9.1 with quadratic irrationalities (Remark 9.4), and the NP-completeness of the stability number (Karp 1972, via $\alpha(G)=\omega(\overline G)$ ). The goal is the mathematical core of the Turing reduction, not a complexity statement.
Trivializations ruled out. Without the unit normalization the eigenvalue statements are trivial or false; a goal stating only (a), or only an inequality between the maximum and $\lambda_{\alpha(G)}$ , would not determine $\alpha(G)$ ; both are excluded by the statements above.
Infrastructure. Everything rests on Mathlib (SimpleGraph.indepNum, real analysis on finite-dimensional spaces, Lagrange multipliers). A Motzkin–Straus theorem for SimpleGraph and Banach's theorem for symmetric trilinear forms are both reusable beyond this mission; contributions of either, or of a general "maximum of a symmetric cubic form on the sphere is an eigenvalue" lemma, are welcome.

Selected references

C. J. Hillar, L.-H. Lim, Most Tensor Problems Are NP-Hard, Journal of the ACM 60(6), Article 45, 2013. https://doi.org/10.1145/2512329 (arXiv:0911.1393v5: https://arxiv.org/abs/0911.1393)
Yu. Nesterov, Random walk in a simplex and quadratic optimization over convex polytopes, CORE Discussion Paper 2003/71, 2003. http://edoc.bib.ucl.ac.be:83/archive/00000238/01/dp2003-71.pdf
E. de Klerk, The complexity of optimizing over a simplex, hypercube or sphere: a short survey, Central European Journal of Operations Research 16, 111–125, 2008. https://doi.org/10.1007/s10100-007-0052-9
T. S. Motzkin, E. G. Straus, Maxima for graphs and a new proof of a theorem of Turán, Canadian Journal of Mathematics 17, 533–540, 1965. https://doi.org/10.4153/CJM-1965-053-6
S. Banach, Über homogene Polynome in ( $L^2$ ), Studia Mathematica 7(1), 36–44, 1938 (reference [Banach 1938] of Hillar–Lim).
L.-H. Lim, Singular values and eigenvalues of tensors: a variational approach, Proc. IEEE CAMSAP 1, 129–132, 2005. https://arxiv.org/abs/math/0607648
L. Qi, Eigenvalues of a real supersymmetric tensor, Journal of Symbolic Computation 40, 1302–1324, 2005. https://doi.org/10.1016/j.jsc.2005.05.007
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

8 thms1 active userReviewed

Complexity Theory Graph Theory Optimization+1·Captain: mikedeng1

Most Tensor Problems Are NP-Hard 3: The Clique Number Is the Unique l for Which an Explicit Graph Tensor Has Spectral Norm 1Research Paper

Motivation

The spectral norm of a matrix, its largest singular value, is computable in polynomial time to any accuracy. Its analogue for 3-tensors appears in the analysis of multilinear systems, in the best rank-1 approximation of a data array, in quantum information (the geometric measure of entanglement), and in the injective norm of tensor products. Hillar and Lim, Most Tensor Problems Are NP-Hard (J. ACM 60(6), 2013, Article 45; final version arXiv:0911.1393v5), show that, in contrast with matrices, deciding whether a fixed nonzero rational number is a singular value or the spectral norm of a rational 3-tensor is NP-hard (their Theorems 6.5 and 1.10).

The proof is a reduction from the clique number $\omega(G)$ of a graph. It combines three classical ingredients: the theorem of Motzkin and Straus (1965), which expresses $\omega(G)$ as the value of a quadratic program over the simplex; a theorem of Banach (1938) on the spectral norm of symmetric tensors; and an observation from He, Li and Zhang (2010) on maxima of sums of squared bilinear forms. Deciding $\omega(G)\ge l$ is one of Karp's (1972) NP-complete problems.

Setting

A real 3-tensor is an array $\mathcal A=[\![a_{ijk}]\!]\in\mathbb R^{l\times m\times n}$ with trilinear form $\mathcal A(\mathbf x,\mathbf y,\mathbf z)=\sum_{i,j,k}a_{ijk}x_iy_jz_k$ . With the Euclidean norm $\|\cdot\|_2$ , its spectral norm is

\|\mathcal A\|_{2,2,2}=\sup_{\mathbf x,\mathbf y,\mathbf z\ne\mathbf 0}\frac{|\mathcal A(\mathbf x,\mathbf y,\mathbf z)|}{\|\mathbf x\|_2\|\mathbf y\|_2\|\mathbf z\|_2}.

A real $\sigma$ is a unit $\ell^2$ -singular value of $\mathcal A$ if there are unit vectors $\mathbf u,\mathbf v,\mathbf w$ with

\textstyle\sum_{j,k}a_{ijk}v_jw_k=\sigma u_i,\quad \sum_{i,k}a_{ijk}u_iw_k=\sigma v_j,\quad \sum_{i,j}a_{ijk}u_iv_j=\sigma w_k

for all $i,j,k$ : the stationarity conditions of $\mathcal A(\mathbf u,\mathbf v,\mathbf w)$ on a product of unit spheres.

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,v\}$ , $v\ge1$ , with $e$ edges $\{i_k,j_k\}$ , $k=1,\dots,e$ , and clique number $\omega$ . Let $\Delta_v$ be the standard simplex, $A_G$ the adjacency matrix and $J$ the all-ones matrix. For a positive integer $l$ set $Q_l=A_G+\frac1lJ$ and $M_l=\max_{\mathbf x\in\Delta_v}\mathbf x^\top Q_l\mathbf x$ . Let $E_k=\frac12E_{i_kj_k}+\frac12E_{j_ki_k}$ , and let $T_l$ be the maximum over unit $\mathbf u,\mathbf v\in\mathbb R^v$ , $\mathbf w\in\mathbb R^{l+2e}$ of the multilinear form

\sum_{i=1}^l\Big(\mathbf u^\top\tfrac1lI\mathbf v\Big)w_i+\sum_{k=1}^e(\mathbf u^\top E_k\mathbf v)w_{l+k}+\sum_{k=1}^e(\mathbf u^\top E_k\mathbf v)w_{e+l+k}. \tag{26}

The graph tensor $\mathcal A_l\in\mathbb Q^{v\times v\times(l+2e)}$ has as entry $a_{ijk}$ the coefficient of $u_iv_jw_k$ in (26).

Formalization targets

Goal: Theorems 6.5 and 1.10, encoding-free core

For every graph $G$ on $v\ge1$ vertices and every enumeration of its edges:

\forall l\ge1:\ \|\mathcal A_l\|_{2,2,2}=1\iff l=\omega;\qquad 1\text{ is a unit singular value of }\mathcal A_\omega;\qquad \forall l>\omega:\ 1\text{ is not one of }\mathcal A_l,

so $\omega$ is the largest $l\in\{1,\dots,v\}$ for which $1$ is a unit singular value of $\mathcal A_l$ . The paper's $v$ -query Turing reductions rest on exactly this.

Milestones (in attack order)

Theorem 6.7 (Motzkin–Straus): $1-1/\omega=2\max_{\mathbf x\in\Delta_v}\sum_{\{i,j\}\in E}x_ix_j$ .
(22): $M_l=1+\frac{\omega-l}{l\omega}$ ; so $M_\omega=1$ , $M_l>1$ for $l<\omega$ , $M_l<1$ for $l>\omega$ .
Lemma 6.8: $M_l=N_l$ , where $N_l=\max_{\|\mathbf u\|_2=1}\{\sum_{i=1}^l(\mathbf u^\top\frac1lI\mathbf u)^2+2\sum_k(\mathbf u^\top E_k\mathbf u)^2\}$ .
Theorem 6.9 (Banach), (24): for a symmetric 4-tensor, $\|\mathcal S\|_{2,2,2,2}=\sup_{\mathbf x\neq\mathbf 0}|\mathcal S(\mathbf x,\mathbf x,\mathbf x,\mathbf x)|/\|\mathbf x\|_2^4$ .
Proposition 6.10 (He–Li–Zhang): for symmetric $A_k$ , $\max_{\|\mathbf u\|=\|\mathbf v\|=1}\sum_k(\mathbf u^\top A_k\mathbf v)^2=\max_{\|\mathbf v\|=1}\sum_k(\mathbf v^\top A_k\mathbf v)^2$ .
Lemma 6.11: $T_l=M_l^{1/2}$ , hence $T_l=1$ iff $l=\omega$ , $T_l>1$ iff $l<\omega$ , $T_l<1$ iff $l>\omega$ .
Proof of Theorem 6.5: $\|\mathcal A_l\|_{2,2,2}=T_l$ , $T_l$ is a unit singular value of $\mathcal A_l$ , and every unit singular value has absolute value at most $T_l$ .
§7 (content of Theorem 1.13): $\min_{\sigma\ge0,\ \text{unit }\mathbf u,\mathbf v,\mathbf w}\|\mathcal A-\sigma\,\mathbf u\otimes\mathbf v\otimes\mathbf w\|_F^2=\|\mathcal A\|_F^2-\|\mathcal A\|_{2,2,2}^2$ , attained only with $\sigma=\|\mathcal A\|_{2,2,2}$ .

Significance

The result. The goal shows that a single comparison with $1$ of the spectral norm, or of the singular-value spectrum, of an explicit rational tensor of size $v\times v\times(l+2e)$ encodes whether $l=\omega(G)$ . It is the step that makes the spectral norm, the largest singular value, and (through §7) the best rank-1 approximation of a 3-tensor NP-hard, whereas all three are polynomial-time for matrices. It explains why the higher-order power method and its relatives carry no global guarantees, and it is the starting point for inapproximability results such as the paper's Theorem 1.11.

Formalizing it. The results are proved on paper; none of them is formalized. Motzkin–Straus, Banach's polarization theorem for symmetric 4-tensors, and the He–Li–Zhang identity are classical results that are not in Mathlib and not on the platform; each is reusable well beyond this mission (Turán-type bounds, polynomial optimization over spheres, injective norms). The mission also checks the paper's construction at the level of indices and constants.

Difficulty

The construction of $\mathcal A_l$ is explicit, and the comparison with $1$ is arithmetic once $T_l=M_l^{1/2}$ is known. Everything rests on the three cited theorems. Motzkin–Straus is an optimization statement over the simplex whose maximizers may lie on the boundary and need not be unique, so a first-order computation at an interior critical point does not settle it. Banach's theorem asserts equality, not equality up to a constant: the standard polarization identity bounds the 4-linear form by its diagonal values only up to a factor. Proposition 6.10 is where the paper's own argument is loose: the 4-linear form it introduces is not symmetric, so (24) does not apply as printed. Finally, the singular-value clauses require that the maximum of a trilinear form on a product of spheres is a stationary value. This must be proved, not assumed.

Formalization scope

Tensors are arrays Fin l → Fin m → Fin n → ℝ with 0-based indices: the paper's $a_{ijk}$ is A (i-1) (j-1) (k-1). The Euclidean norm is Real.sqrt (∑ i, x i ^ 2). Suprema and maxima are sSup of sets that are nonempty and bounded under the stated hypotheses; where the paper's "max" carries content (Motzkin–Straus, (22), §7), attainment is stated with IsGreatest/IsLeast. The graph is a SimpleGraph (Fin v) with $v\ge1$ , clique number Mathlib's SimpleGraph.cliqueNum, and its edges are enumerated by an arbitrary Fin e ≃ G.edgeSet. Every statement holds for each enumeration, so the tensor depends on the choice and the conclusions do not. $\mathcal A_l$ is a rational tensor, read over $\mathbb R$ by casting.

Explicit readings of the paper:

Definition 6.1 has no norm constraint. Since $(\sigma,\mathbf u,\mathbf v,\mathbf w)\mapsto(t\sigma,t\mathbf u,t\mathbf v,t\mathbf w)$ preserves (20), unnormalized singular values make every nonzero real a singular value of $\mathcal A_l$ , so the clause "not for $l>\omega$ " would be false. Singular vectors are therefore unit vectors, as in the paper's derivation on p. 0:21.
The statement of Lemma 6.11 prints $w_{m+l+k}$ . There is no $m$ in §6, and the proof uses $w_{e+l+k}$ , which is formalized.
$E_k$ is written entrywise as $\frac12[\{i,j\}=\{i_k,j_k\}]$ , which equals $\frac12E_{i_kj_k}+\frac12E_{j_ki_k}$ for a loopless edge.
" $T_l$ is just the maximum $\ell^2$ -singular value of $\mathcal A_l$ " is made explicit as milestone 7.
The goal does not claim that $1$ fails to be a singular value of $\mathcal A_l$ for $l<\omega$ ; the paper neither claims nor uses this.

This is the mathematical core of a polynomial-time Turing reduction, not an NP-hardness theorem. The polynomial size of $\mathcal A_l$ , the $v$ -query procedure, the scaling to a general fixed $0\ne\sigma\in\mathbb Q$ , and the NP-completeness of CLIQUE (Karp 1972, cited) are not formalized. Theorem 1.11 and Corollary 1.12 are out of scope.

Two formalizations would make the goal trivial, and both are excluded. One is dropping the unit-norm constraint, which makes every nonzero number a singular value. The other is a spectral norm taken as a supremum over all vectors without normalization, which makes it unbounded and junk-valued; here the quotients are normalized.

Contributions are welcome on each milestone. Motzkin–Straus, Banach (24) and He–Li–Zhang are self-contained and reusable. Lemma 6.11 and milestone 7 need Cauchy–Schwarz and a Lagrange-type stationarity argument on spheres, which Mathlib supports through IsLocalExtrOn and the Lagrange multiplier files.

Selected references

C. J. Hillar, L.-H. Lim, Most Tensor Problems Are NP-Hard, J. ACM 60(6), Article 45, 2013. https://doi.org/10.1145/2512329 (final version arXiv:0911.1393v5, https://arxiv.org/abs/0911.1393v5)
T. S. Motzkin, E. G. Straus, Maxima for graphs and a new proof of a theorem of Turán, Canadian J. Math. 17, 533–540, 1965. https://doi.org/10.4153/CJM-1965-053-6
S. Banach, Über homogene Polynome in (L²), Studia Math. 7, 36–44, 1938. https://doi.org/10.4064/sm-7-1-36-44
S. He, Z. Li, S. Zhang, Approximation algorithms for homogeneous polynomial optimization with quadratic constraints, Math. Program. Ser. B 125(2), 353–383, 2010. https://doi.org/10.1007/s10107-010-0409-z
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

11 thms1 active userReviewed

Missions

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

Motivation

Setting

Formalization targets

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

Theorem 4.2, first sentence (p. 1968)

Supporting results (milestones, in attack order)

Significance

Difficulty

Formalization scope

Selected references

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

Motivation

Setting

Formalization targets

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

Milestones: the three bullets of Theorem 1

Significance

Difficulty

Formalization scope

Selected references

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

Motivation

Setting

Formalization targets

Goal: the admissible class has dimension n2n^2n2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Analytical Solution to a Discrete-Time Model for Dynamic Learning and Decision Making: the two-action frontier difference equations have a unique closed-form solution with explicit det YResearch Paper

Learning while doing, and the frontier of continuation values

Setting

Formalization targets

Goal: Theorem 6 (Complete), EC p. 11

Milestones

Significance

Difficulty

Formalization scope

Selected references

Equilibria and Systemic Risk in Saturated Networks: necessary and sufficient conditions for uniqueness of saturated network equilibria, class by class, when the spectral radius is at most oneResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 16)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On Geometric Connections of Embedded and Quotient Geometries in Riemannian Fixed-rank Matrix Optimization: Gradient and Hessian Connections for Fixed-rank PSD Matrices via YYᵀResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 21)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Technical Note—Global Robust Stability in a General Price and Assortment Competition Model: Robust Best-Response Price Dynamics Contract Geometrically to the Special Equilibrium from Any StartResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (global robust stability)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Quantum computation, quantum state engineering, and quantum phase transitions driven by dissipation: The DQC Liouvillian Has a Unique Steady State Encoding the Circuit and a Gap Above 1/T²Research Paper

Motivation

Setting

Formalization targets

Main goal

Supporting targets

Significance

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