Linear algebra

Motivation

Character sums express phase constraints on complex Hadamard matrices. In dimension six these constraints also bear on how many mutually unbiased bases can coexist. The pinned manuscript supplies the research context.

Setting

A complex Hadamard matrix has unit-modulus entries and conjugate-transpose product 6I. Equivalence permits row and column permutations and unit phases. Tao's cubic matrix supplies the exceptional class.

Formalization target

The selected goal is OAI.MUB6.fourier_and_family_bound. Its central assertion is

$$g_H(\pi(1,1,1,-1,-1,-1))=0,\qquad n_{\rm MUB}\leq5.$$

The theorem states a conjunction of two claims about 6x6 complex matrices and mutually unbiased bases in C^6. First, for every complex Hadamard matrix H of order 6 (all entries of modulus 1 and HH = 6I, where H is the conjugate transpose) that is not equivalent to the specific matrix tao, every permutation π of the six coordinates gives g(H, alpha∘π) = 0. Here the character of a column x at an integer exponent vector a is the product over i of x_i^{a_i}, g(H,a) is (1/6) times the sum over the six columns k of H of the character of column k at a, and alpha is the exponent vector (1,1,1,-1,-1,-1), so alpha∘π is alpha with its entries permuted. Equivalence of H and K means K_{ij} = u_i H_{r(i),c(j)} v_j for some row and column permutations r, c and unit-modulus complex phase vectors u and v. The matrix tao has entries ω^{e_{ij}}, where ω = exp(2πi/3) and e is a fixed 6x6 exponent matrix with zero first row and column and a five-cycle pattern of exponents 0, 1, 2 in the remaining 5x5 block. Second, for every natural number n, if there exist n orthonormal bases of C^6 that are pairwise mutually unbiased, meaning |<b_i, b'_j>|^2 = 1/6 for all vectors of two distinct bases, then n ≤ 5. This is stated as an admitted theorem, not a verified proof.

Significance and status

The goal is the conjunction of Fourier vanishing outside the specified equivalence class and the bound on attainable families. The cube-fiber statement is an additional published supporting target with its own hypotheses. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

Orthogonality immediately kills certain degree-two characters, but the target concerns a balanced degree-six character and a separate global bound on families of bases.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

• OAI.HadamardSix.rowRatio_cubeFiber_sum_zero (Open).

Selected references

• OpenAI, Exact Fourier certificates for complex Hadamard matrices of order six, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Noisy low-rank matrix completion asks to reconstruct an $m_1\times m_2$ matrix $A_0$ from $n$ noisy observations of randomly chosen entries. It is the statistical model behind collaborative filtering (recommender systems), sensor localization and system identification, and the nuclear-norm penalized least-squares estimator is its standard convex method. Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4, Ann. Statist. 2011) proved sharp oracle inequalities for this estimator and showed that its Frobenius error is of order $\operatorname{rank}(A_0)(m_1\vee m_2)\log(m_1+m_2)/n$ up to normalization, which matches the minimax lower bound up to a logarithmic factor.

An upper bound alone does not say whether the estimator really attains this rate on a given matrix, nor whether it reports the correct rank. Section 5.1 of the paper answers both questions with a single deterministic theorem, Theorem 8: with a slightly inflated regularization parameter the estimator never overestimates the rank of $A_0$; if the nonzero singular values of $A_0$ are separated from zero it recovers the rank exactly, and its error is then bounded below by a quantity of the same order as the upper bounds. Rank recovery is the property practitioners rely on when they use the estimator for model selection (choosing the number of latent factors). This mission formalizes Theorem 8 and the steps of its proof.

Setting

Fix integers $m_1,m_2,n\ge1$. The matrix completion basis is $\mathcal X=\{e_j(m_1)e_k(m_2)^\top\}$, the $m_1m_2$ matrices with a single entry equal to $1$. A sample consists of $n$ pairs $(X_i,Y_i)$ with $X_i\in\mathcal X$ (an observed position $(j_i,k_i)$) and $Y_i\in\mathbb R$ (a noisy observation of the corresponding entry of the unknown matrix $A_0$). Write $\langle A,B\rangle=\operatorname{tr}(A^\top B)$, $\|A\|_2$ for the Frobenius norm, $\|A\|_1$ for the nuclear norm (the sum of the singular values) and $\|A\|_\infty$ for the operator norm (the largest singular value). The singular values of $B$ are $\sigma_1(B)\ge\sigma_2(B)\ge\dots\ge\sigma_{m_1\wedge m_2}(B)\ge0$.

From the sample form

$$\mathbf X=\frac{m_1m_2}{n}\sum_{i=1}^nY_iX_i,\qquad \mathbf M=\frac1n\sum_{i=1}^n\big(Y_iX_i-\mathbb E(Y_iX_i)\big).$$

In the paper's model $\mathbb E(Y_i\mid X_i)=\langle A_0,X_i\rangle$ with $X_i$ uniform on $\mathcal X$, so $\mathbb E(Y_iX_i)=A_0/(m_1m_2)$ and $\mathbf X-A_0=m_1m_2\mathbf M$: the matrix $\mathbf M$ is the stochastic error. For $\lambda>0$ the estimator (3.1) is

$$\hat A^\lambda=\operatorname{argmin}_{A\in\mathbb R^{m_1\times m_2}}\Big(\|A-\mathbf X\|_2^2+\lambda m_1m_2\|A\|_1\Big).$$

The objective is strictly convex, so the minimizer is unique; by (3.2) it is obtained from a singular value decomposition of $\mathbf X$ by soft thresholding every singular value at level $\lambda m_1m_2/2$.

Formalization targets

Goal: Theorem 8 (p. 20)

Let $\lambda\ge2\|\mathbf M\|_\infty$, $0<\delta<1$ and $\lambda'=\lambda/(1-\delta)$, and put $\hat r=\operatorname{rank}(\hat A^{\lambda'})$. Then

$$\hat r\le\operatorname{rank}(A_0).\tag{5.1}$$

If in addition $\min_{j:\sigma_j(A_0)\ne0}\sigma_j(A_0)\ge\lambda'm_1m_2$, then

$$\hat r\ge\operatorname{rank}(A_0)\tag{5.2}$$

and

$$\|\hat A^{\lambda'}-A_0\|_2^2\ge\frac{\delta^2}{4(1-\delta)^2}\operatorname{rank}(A_0)\,(\lambda m_1m_2)^2.\tag{5.3}$$

Milestones

The milestones follow the proof on p. 20 in order:

1. the singular value perturbation display $|\sigma_j(\mathbf X)-\sigma_j(A_0)|\le\sigma_1(\mathbf X-A_0)=m_1m_2\|\mathbf M\|_\infty\le\lambda m_1m_2/2$;
2. the rank of $\hat A^\lambda$ equals the number of singular values of $\mathbf X$ above $\lambda m_1m_2/2$ (the consequence of (3.2) the proof uses);
3. (5.1);
4. (5.2);
5. $\|\mathcal P(\hat A^{\lambda'}-\mathbf X)\|_2=\sqrt r\,\lambda'm_1m_2/2$ when $\hat r=r$, for the projector $\mathcal P$ onto the span of the top $r$ singular pairs $u_j(\mathbf X)v_j(\mathbf X)^\top$;
6. $\|\mathcal P(\mathbf X-A_0)\|_2\le\sqrt r\|\mathbf M\|_\infty m_1m_2\le\sqrt r\lambda m_1m_2/2$.

Significance

The result. Theorem 8 turns the paper's upper bounds into two-sided statements. Combined with a probability bound for $\|\mathbf M\|_\infty$ (Corollary 3 of the paper), it shows that with high probability the estimator selects the true rank and that its error on well-conditioned low-rank matrices is not smaller than the rate of the upper bounds, so those bounds cannot be improved for this estimator. Because the theorem is deterministic given the event $\lambda\ge2\|\mathbf M\|_\infty$, it applies unchanged to any noise model for which such a bound on the stochastic error is available.

Formalizing it. The theorem is proved in the paper; nothing in it is open. The mission produces a machine-checked version and, along the way, reusable linear algebra that is not on the platform in this form: Weyl's perturbation inequality for singular values in operator norm, the rank of a nuclear-norm proximal point, and the Frobenius norm of a projection onto a span of orthonormal rank-one matrices. The soft-thresholding representation (3.2) itself is the open platform item CaiCandesShen.Convergence.shrink_eq_prox (Cai–Candès–Shen, Theorem 2.1, after halving the objective); this mission references it rather than posing it again, and a proof of it would serve both missions.

Difficulty

The arithmetic of the proof is three lines; the content is in two facts about singular values that the paper takes from the literature. The first is Weyl's inequality $|\sigma_j(B)-\sigma_j(C)|\le\|B-C\|_\infty$, which needs the min–max (Courant–Fischer) characterization of singular values; Mathlib defines singular values through the eigenvalues of $T^*T$ but has neither the min–max principle for them nor this inequality. The second is the description of the minimizer of $\|A-\mathbf X\|_2^2+\lambda m_1m_2\|A\|_1$: one needs the subdifferential of the nuclear norm (2.1), or an equivalent von Neumann trace inequality, to show that soft thresholding is optimal, and then that its rank and its projection onto the top singular pairs are what the formula suggests. A naive approach that compares the estimator with $\mathbf X$ entrywise gives nothing about the rank; the proof needs the spectral structure.

Formalization scope

Matrices are MatrixCompletion.RealMatrix m₁ m₂ (Matrix (Fin m₁) (Fin m₂) ℝ) with the published norms frobeniusNormSq, frobeniusNorm, nuclearNorm, spectralNorm and SVD data SVD. Singular values are Mathlib's LinearMap.singularValues of Matrix.toEuclideanLin, 0-based: the Lean singularValue B j is the paper's $\sigma_{j+1}(B)$. The conventions committed to:

• The statements are realization-wise: positions idx : Fin n → Fin m₁ × Fin m₂ and responses y : Fin n → ℝ are fixed, and every theorem holds for every data set satisfying $\lambda\ge2\|\mathbf M\|_\infty$. The matrix $\mathbf M$ is written as $\frac1n\sum_iY_iX_i-A_0/(m_1m_2)$, which is (2.2) under the model (1.1) and the uniform design; this is the paper's "Note that $\mathbf X-A_0=m_1m_2\mathbf M$". The probabilistic hypotheses are used for nothing else.
• $n,m_1,m_2\ge1$ and $\lambda>0$ are assumed, as in the paper.
• The estimator is any minimizer of (3.1) over all matrices, never the soft-thresholding formula; replacing the minimizer by formula (3.2) would assume the open Cai–Candès–Shen item.
• $\min_{j:\sigma_j(A_0)\ne0}\sigma_j(A_0)\ge\lambda'm_1m_2$ is written "for every $j$ with $\sigma_j(A_0)\ne0$"; for $A_0=0$ it is vacuous, as on the page. No real infimum over a possibly empty set is used.
• The projector $\mathcal P$ is built from a singular value decomposition of $\mathbf X$ carried as data, with decreasing singular values, from its first $r$ pairs.

No printed slip was found in Theorem 8 or its proof; no hypothesis beyond the above is added.

Contributions welcome: Weyl's inequality for singular values (generally useful), the rank and top-$r$ projection of the nuclear-norm proximal point, and a proof of CaiCandesShen.Convergence.shrink_eq_prox.

The source is the arXiv preprint arXiv:1011.6256v4; all page and display numbers refer to it.

Selected references

• V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, Ann. Statist. 39(5), 2011; preprint arXiv:1011.6256v4. https://arxiv.org/abs/1011.6256
• J.-F. Cai, E. J. Candès, Z. Shen, A singular value thresholding algorithm for matrix completion, SIAM J. Optim. 20(4), 2010. https://doi.org/10.1137/080738970
• G. W. Stewart, J.-G. Sun, Matrix Perturbation Theory, Academic Press, 1990 (reference [25] of the paper, p. 203).
• E. J. Candès, Y. Plan, Matrix completion with noise, Proc. IEEE 98(6), 2010. https://doi.org/10.1109/JPROC.2009.2035722

Motivation

Many estimation problems ask for a low-rank matrix from far fewer linear measurements than it has entries: matrix completion, quantum state tomography, recovery of positions from partial distances. The rank minimization problem $\min \operatorname{rank}(X)$ subject to $\mathcal S(X) = \mathcal M$ is NP-hard, so one solves a tractable surrogate instead, either the nuclear-norm minimization $\min \|X\|_*$ subject to $\mathcal S(X) = \mathcal M$ or an iterative scheme such as the iteratively reweighted least squares algorithm IRLS-M of Fornasier, Rauhut and Ward (arXiv:1010.2471).

Guarantees for these surrogates rest on conditions on the measurement map. Two are standard. The restricted isometry property (RIP) asks that $\mathcal S$ nearly preserve the Frobenius norm of every low-rank matrix; it holds with high probability for many random maps, and it is what one can verify in practice. The null space property asks that no nonzero matrix in the kernel of $\mathcal S$ be concentrated on few singular directions; it is what the recovery proofs actually use. This mission formalizes the bridge between them in the paper's form: a small restricted isometry constant implies the strong rank null space property (SRNSP) that drives the convergence analysis of IRLS-M.

Timeline.

• 2005: Candès and Tao introduce restricted isometry constants for sparse vectors and prove exact recovery by $\ell_1$ minimization under a condition on them (IEEE Trans. Inf. Theory).
• 2008: Candès shows that $\delta_{2s} < \sqrt 2 - 1$ suffices in the vector case (C. R. Math.).
• 2010: Recht, Fazel and Parrilo define the rank restricted isometry property and prove that nuclear-norm minimization recovers every rank-$r$ matrix when $\delta_{5r}$ is small enough (SIAM Review).
• 2011: Candès and Plan prove the matrix analogue of the $\sqrt 2 - 1$ threshold and the orthogonality estimate quoted here as Lemma 6.9 (IEEE Trans. Inf. Theory).
• 2011: Fornasier, Rauhut and Ward prove Proposition 6.8, the target of this mission: $\delta_{4k} < \sqrt 2 - 1$ implies the SRNSP of order $k$.

Setting

Fix integers $n, p, m$. A measurement map is a linear map $\mathcal S : \mathbb R^{n\times p} \to \mathbb R^m$; it is given by $m$ matrices $A_1,\dots,A_m$ through $\mathcal S(X)_\ell = \langle A_\ell, X\rangle$, where $\langle X, Y\rangle = \operatorname{Tr}(XY^{\top}) = \sum_{i,j} X_{ij}Y_{ij}$. The Frobenius norm is $\|X\|_F = \langle X, X\rangle^{1/2}$, the nuclear norm $\|X\|_*$ is the sum of the singular values of $X$, and $\|\mathcal S(X)\|_{\ell_2^m}$ is the Euclidean norm of the vector $\mathcal S(X)$. A matrix is $k$-rank if its rank is at most $k$.

The restricted isometry constant $\delta_k = \delta_k(\mathcal S)$ (Definition 1.1) is the smallest $\delta \ge 0$ such that

$$(1 - \delta)\|X\|_F^2 \le \|\mathcal S(X)\|_{\ell_2^m}^2 \le (1+\delta)\|X\|_F^2 \qquad \text{for all $k$-rank } X .$$

The map $\mathcal S$ has the strong rank null space property of order $k$ with constant $\eta \in (0,1)$ (Definition 6.4) if for every $X \in \ker \mathcal S \setminus\{0\}$ and every decomposition $X = X_1 + X_2$ with $X_1$ $k$-rank, there is another decomposition $X = H_1 + H_2$ with $\operatorname{rank} H_1 \le 2k$, $\langle H_1, H_2\rangle = 0$, $X_1H_2^{\top} = 0$, $X_1^{\top}H_2 = 0$, and

$$\|H_1\|_* \le \eta\,\|H_2\|_* .$$

In Lean these are IRLSM.RIP.ripConst A k, IRLSM.RIP.SRNSP A k η and IRLSM.RIP.measSq A X $= \|\mathcal S(X)\|^2_{\ell_2^m}$, built on the published module HighDimStat_MatrixRank_Core (traceInner, frobeniusNorm, nuclearNorm, observationOp).

Formalization targets

Goal: Proposition 6.8

If $\delta_{4k} > 0$ and

$$\delta_{4k} < \sqrt 2 - 1,$$

then $\mathcal S$ satisfies the SRNSP of order $k$ with constant

$$\eta = \sqrt 2\,\frac{\delta_{4k}}{1 - \delta_{3k}} \in (0,1).$$

The constant $\eta$ is the paper's explicit one; the goal asserts the full property for every kernel element and every decomposition, including $\eta \in (0,1)$.

Milestones

1. Lemma 6.9 (Candès–Plan): for $\langle X, Y\rangle = 0$ and $\operatorname{rank}X + \operatorname{rank}Y \le k$, $|\langle \mathcal S(X), \mathcal S(Y)\rangle| \le \delta_k \|X\|_F\|Y\|_F$.
2. Lemma 6.10 (Recht–Fazel–Parrilo): $XZ^{\top} = 0$ and $X^{\top}Z = 0$ imply $\|X + Z\|_* = \|X\|_* + \|Z\|_*$.
3. The block decomposition of the proof: relative to an SVD $X_1 = U(\begin{smallmatrix}\Sigma & 0\\ 0 & 0\end{smallmatrix})V^{\top}$, the matrices $H_0$ and $H_c$ obtained by zeroing blocks of $U^{\top}XV$ satisfy $X = H_0 + H_c$, $\operatorname{rank}H_0 \le 2k$, $X_1H_c^{\top} = 0$, $X_1^{\top}H_c = 0$, $\langle H_0, H_c\rangle = 0$.
4. $\|H\|_* \le \sqrt r\,\|H\|_F$ for $\operatorname{rank}H \le r$, and $\|H\|_F \le \|H + K\|_F$ for $\langle H, K\rangle = 0$.
5. The shelling bound: for a nonincreasing nonnegative sequence cut into blocks of length $\ell$, each block's $\ell_2$ norm is at most $\ell^{-1/2}$ times the $\ell_1$ norm of the previous block.
6. Monotonicity $\delta_k \le \delta_{k'}$ for $k \le k'$, and $\eta \in (0,1)$ under $0 < \delta_{4k} < \sqrt2 - 1$.

Significance

The result. Proposition 6.8 is the step that turns a verifiable, probabilistically typical hypothesis (a small rank restricted isometry constant, which Gaussian and many other random maps satisfy once $m$ is of order $k\max(n,p)$) into the deterministic null-space hypothesis under which the paper proves that IRLS-M converges to the nuclear-norm minimizer and recovers every $k$-rank matrix exactly (Theorem 6.11, Proposition 2.1). Through Lemma 6.6 and Corollary 6.7 of the same paper, the SRNSP also gives stable recovery by nuclear-norm minimization, with error controlled by the best $k$-rank approximation error in the nuclear norm.

Formalizing it. The result is proved on paper; it has no machine-checked proof that we know of. A complete development supplies the rank restricted isometry constant as a usable object (its monotonicity, its polarization estimate Lemma 6.9), the nuclear norm's additivity on orthogonal pieces, its comparison with the Frobenius norm, and the block-splitting of the singular value decomposition. These tools are reusable across low-rank recovery. The sibling mission of this series, IRLS-M Converges to the Nuclear-Norm Minimizer Under the Strong Rank Null Space Property, takes the SRNSP as its hypothesis; together the two give Proposition 2.1 of the paper.

Difficulty

The obvious argument would bound $\|H_1\|_*$ directly by the restricted isometry inequality, but that inequality controls only Frobenius norms of low-rank matrices, while the kernel element $X$ has full rank in general and the property is stated in nuclear norms. The restricted isometry hypothesis therefore cannot be applied to $X$, or to $H_2$, as a whole, and the constant $\eta$ depends on how the high-rank part is handled. In Lean, the singular value decomposition of a rectangular matrix and the behaviour of singular values under block operations are the main missing infrastructure: Mathlib has the spectral theorem for Hermitian matrices but little on singular values of rectangular matrices.

Formalization scope

• Real matrices Matrix (Fin n) (Fin p) ℝ; the paper treats real and complex matrices indifferently. $X^*$ is $X^{\top}$ and $\langle\cdot,\cdot\rangle$ is traceInner.
• Measurement map by matrices: $\mathcal S(X)_\ell = \langle A_\ell, X\rangle$ (observationOp); $\|\mathcal S(X)\|^2_{\ell_2^m}$ is a sum of squares, not Mathlib's sup norm on Fin m → ℝ.
• The squared RIP constant of Definition 1.1, defined as the infimum of the admissible $\delta \ge 0$ (attained, never a junk value), for every $k \in \mathbb N$; the page's range $1 \le k \le n$ is dropped because the goal uses $\delta_{4k}$ with $4k$ possibly larger than $n$. The unsquared constant $(1-\delta)\|X\|_F \le \|\mathcal S(X)\| \le (1+\delta)\|X\|_F$ used by other formalizations is a different quantity and is not used.
• Positivity $\delta_{4k} > 0$ is a hypothesis of the goal: it is Definition 1.1's own "$\delta_k > 0$", and without it $\eta = 0 \notin (0,1)$.
• No n ≤ p assumption: the proof does not use it.
• The block decomposition milestone states the page's explicit construction, with a general (not necessarily diagonal) top-left block, and without the unused hypothesis $X \in \ker\mathcal S$.
• The shelling bound is stated in its vector form for every block; the page writes "for $j \ge 2$" but display (6.7) uses it for every $j \ge 1$.

A formalization that proved only $\eta < 1$, or only the existence of some decomposition without the bound $\|H_1\|_* \le \eta\|H_2\|_*$, or that defined $\delta_k$ as any admissible constant rather than the smallest one, would not be this mission's goal.

Welcome contributions: singular value decomposition for rectangular real matrices in the Core encoding, singular values of block-diagonal and orthogonally-equivalent matrices, and proofs of the milestones in any order.

Selected references

• M. Fornasier, H. Rauhut, R. Ward, Low-rank matrix recovery via iteratively reweighted least squares minimization, SIAM J. Optim. 21(4), 2011; read as arXiv:1010.2471v4. https://arxiv.org/abs/1010.2471
• E. J. Candès, Y. Plan, Tight oracle inequalities for low-rank matrix recovery from a minimal number of noisy random measurements, IEEE Trans. Inf. Theory 57(4), 2011. https://doi.org/10.1109/TIT.2011.2111771
• B. Recht, M. Fazel, P. A. Parrilo, Guaranteed minimum-rank solutions of linear matrix equations via nuclear norm minimization, SIAM Review 52(3), 2010. https://doi.org/10.1137/070697835
• E. J. Candès, T. Tao, Decoding by linear programming, IEEE Trans. Inf. Theory 51(12), 2005. https://doi.org/10.1109/TIT.2005.858979
• E. J. Candès, The restricted isometry property and its implications for compressed sensing, C. R. Math. Acad. Sci. Paris 346, 2008. https://doi.org/10.1016/j.crma.2008.03.014

Motivation

Obstacle problems, contact problems and box-constrained quadratic programs share one finite-dimensional core: the linear complementarity problem "find $y \le \psi$ and $\lambda \ge 0$ with $Ay + \lambda = f$ and $\lambda_i(y_i - \psi_i) = 0$". After discretization by finite differences or piecewise linear finite elements, the matrix $A$ is typically an M-matrix, which is why this class sits at the centre of the numerical analysis of variational inequalities.

The primal-dual active set strategy solves such problems by guessing which constraints are active, solving one linear system on that guess, and updating the guess from the new primal and dual values. Hintermüller, Ito and Kunisch (SIAM J. Optim. 13 (2002) 865–888; authors' version hal-01660511) showed that this strategy is a semismooth Newton method for a nonsmooth reformulation of the problem. Local superlinear convergence then follows from Newton theory. This mission concerns the paper's global result: for M-matrices the method converges from every starting point, and its primal iterates decrease monotonically. A related global result for a purely primal active set method appears in Hoppe's 1987 analysis of multigrid methods for obstacle problems, which the paper cites as [H].

Setting

Fix $n \ge 0$, a matrix $A \in \mathbb{R}^{n\times n}$, vectors $f, \psi \in \mathbb{R}^n$ and a constant $c > 0$. Vectors are compared componentwise. The paper writes $A$ for the matrix and calligraphic $\mathcal{A}$, $\mathcal{I}$ for index sets; Lean uses A for the matrix and activeSet for $\mathcal{A}$.

Problem (3.1). Find $(y, \lambda) \in \mathbb{R}^n \times \mathbb{R}^n$ with

$$Ay + \lambda = f, \qquad \lambda - \max(0, \lambda + c(y - \psi)) = 0,$$

the maximum taken componentwise. For $c > 0$ the second equation says exactly $y \le \psi$, $\lambda \ge 0$ and $\lambda_i (y_i - \psi_i) = 0$ for every $i$.

M-matrix. $A$ is an M-matrix if it is nonsingular, its off-diagonal entries satisfy $a_{ij} \le 0$ for $i \ne j$, and its inverse is entrywise nonnegative, $A^{-1} \ge 0$.

Blocks. For an index set $\mathcal{I}$ with complement $\mathcal{A}$, $A_{\mathcal{I}}$ is the principal submatrix with rows and columns in $\mathcal{I}$, and $A_{\mathcal{I}\mathcal{A}}$ the submatrix with rows in $\mathcal{I}$ and columns in $\mathcal{A}$.

The algorithm. Start from arbitrary $(y^0, \lambda^0)$. Given $(y^k, \lambda^k)$, let

$$\mathcal{A}_k = \{ i : \lambda^k_i + c(y^k - \psi)_i > 0\}, \qquad \mathcal{I}_k = \{ i : \lambda^k_i + c(y^k - \psi)_i \le 0\},$$

and let $(y^{k+1}, \lambda^{k+1})$ solve

$$Ay^{k+1} + \lambda^{k+1} = f, \qquad y^{k+1} = \psi \text{ on } \mathcal{A}_k, \qquad \lambda^{k+1} = 0 \text{ on } \mathcal{I}_k.$$

A sequence obeying this rule for every $k$ is a run. The solution of (3.1) is written $x^* = (y^*, \lambda^*)$ and the iterates $x^k = (y^k, \lambda^k)$.

Formalization targets

Goal: Theorem 3.2 (p. 7)

If $A$ is an M-matrix, then for arbitrary initial data

$$x^k \to x^*, \qquad y^* \le y^{k+1} \le y^k \ \text{ for all } k \ge 1, \qquad y^k \le \psi \ \text{ for all } k \ge 2.$$

Milestones (Appendix A, p. 20)

1. For every partition $\mathcal{I}, \mathcal{A}$: $A_{\mathcal{I}}$ is regular, $A_{\mathcal{I}}^{-1} \ge 0$ and $A_{\mathcal{I}}^{-1} A_{\mathcal{I}\mathcal{A}} \le 0$.
2. Complementarity (A.1): $\lambda^k_i = 0$ or $y^k_i = \psi_i$, for all $i$ and $k \ge 1$, for every run and every matrix.
3. Monotonicity: $y^{k+1} \le y^k$ for $k \ge 1$.
4. Primal feasibility: $y^k \le \psi$ for $k \ge 2$.
5. Lower bound: $y^* \le y^k$ for $k \ge 1$.
6. Remark A.1 and dual feasibility: if $\lambda^{\bar k}_i < 0$ with $\bar k \ge 1$, then $\lambda^k_i = 0$ and $y^k_i \le \psi_i$ for all $k \ge \bar k + 1$; and $\lambda^k \ge 0$ for all $k$ beyond some $k_o$.

A companion item states that a run exists from every initial pair when $A$ is an M-matrix.

Significance

The result. Theorem 3.2 makes the active set strategy a globally convergent method for the discretized obstacle problem, with no line search, no merit function and no damping. The monotonicity statement says more: from the second iterate on, every primal iterate is feasible and lies above the solution, and the iterates descend to it. Combined with the paper's observation (p. 7) that convergent iterates of the method converge in finitely many steps, it gives finite termination from every starting point. The theorem is the model for later global results on the method under weaker hypotheses, two of which (a norm condition and small perturbations of M-matrices) appear in the same paper as Theorems 3.3 and 3.4.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known. A formal proof requires the classical sign facts on principal blocks of M-matrices, which Mathlib does not contain, and a careful treatment of the iteration as a relation on pairs of vectors. The M-matrix block lemma is reusable well beyond this mission, for instance in comparison principles for discretized elliptic problems.

Difficulty

The obvious argument would bound a merit function or a contraction factor; neither is available, because the iteration map is discontinuous and the active sets change from step to step. The paper's argument is instead an order argument. Its central step is the monotonicity $y^{k+1} \le y^k$: it requires the complementarity (A.1) of the previous iterate, which holds only from $k = 1$ on, and the sign structure of the blocks $A_{\mathcal{I}_k}^{-1}$ and $A_{\mathcal{I}_k}^{-1} A_{\mathcal{I}_k \mathcal{A}_k}$ for every possible active set. The index bounds are sharp in the sense that the statements fail at $k = 0$ (respectively $k = 1$ for feasibility), because the initial data are arbitrary. Convergence of the multipliers is a separate step: negative multiplier coordinates must be shown to vanish permanently after one more iteration.

Formalization scope

• Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, the product is A *ᵥ y, and $\le$ on vectors is componentwise. Convergence of $x^k$ is in the product topology on $\mathbb{R}^n \times \mathbb{R}^n$.
• Nonsingularity of an M-matrix is IsUnit A.det. Lean's inverse of a singular matrix is the zero matrix, so without this clause every singular matrix with nonpositive off-diagonal entries would count as an M-matrix; the M-matrix definition is the page's, not an equivalent characterization.
• The solution is a hypothesis IsSolution A f ψ c ystar lamstar. The paper speaks of "the unique solution"; for an M-matrix it exists and is unique by Berman–Plemmons, so the hypothesis assumes nothing the paper does not have. The uniqueness fact is not restated.
• The algorithm is a relation. One step is IsStep, a run is IsRun with free initial data y 0, lam 0. The stopping option of step (iv) is not modelled. Because a universally quantified statement over runs would be empty if no run existed, the companion item run_exists states existence of a run from every initial pair.
• The constant $c > 0$ is a binder of every statement that needs it; (A.1) needs neither $c > 0$ nor any hypothesis on $A$, and has none.
• Remark A.1 is printed without "$\bar k \ge 1$"; its proof assumes it and the statement is false at $\bar k = 0$, so the bound is kept.
• A trivializing formalization is ruled out: no statement assumes monotonicity, feasibility or convergence of the iterates, and the M-matrix hypothesis cannot be met by a singular matrix.
• Needed infrastructure: principal submatrices of M-matrices (Berman–Plemmons, Ch. 6), and inverse-nonnegativity arguments for block systems. Proofs of the block lemma, of (A.1) and of the order lemmas are welcome independently of the goal.

The printed closing step of the proof writes $\lambda^k = Ay^k + f$; step (iii) gives $\lambda^k = f - Ay^k$. No item quotes or depends on that line.

Selected references

• M. Hintermüller, K. Ito, K. Kunisch, The primal-dual active set strategy as a semismooth Newton method, SIAM J. Optim. 13(3):865–888, 2002. https://doi.org/10.1137/S1052623401383558 (authors' version: https://hal.science/hal-01660511)
• A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, Academic Press, 1979; reprinted as SIAM Classics in Applied Mathematics 9, 1994. https://doi.org/10.1137/1.9781611971262
• R. H. W. Hoppe, Multigrid algorithms for variational inequalities, SIAM J. Numer. Anal. 24(5):1046–1065, 1987. https://doi.org/10.1137/0724069
• L. Qi, J. Sun, A nonsmooth version of Newton's method, Math. Program. 58:353–367, 1993. https://doi.org/10.1007/BF01581275

Motivation

Learning in games asks whether players who adjust their strategies over time, by simple rules, end up at a Nash equilibrium. Many adaptive dynamics share one informational feature: each player's adjustment depends on the current play and on that player's own payoff function, but not on the payoffs of the others. Hart and Mas-Colell (AER 2003) call such dynamics uncoupled, and show that this feature alone rules out guaranteed convergence to Nash equilibrium, even for families of games in which every game has exactly one equilibrium. Earlier non-convergence results, such as Shapley's example for fictitious play and the cycling examples of Jordan (1993) and Foster and Young (1998), concern particular dynamics; this one applies to the whole class of uncoupled dynamics. It is one reason the learning literature turned to weaker targets such as correlated equilibrium, which regret-based uncoupled procedures do reach (Hart and Mas-Colell, Econometrica 2000).

The paper proves its theorem in two settings: a two-player game with a continuum of strategies (§II and the Appendix) and a three-player game with two strategies each (§III). This mission formalizes the first setting.

Setting

There are two players, $i=1,2$, and $j=3-i$ denotes the other player. Each player's strategy set is the closed unit disk $D=\{z\in\mathbb R^2:\|z\|\le1\}$, and a profile is $x=(x^1,x^2)\in X:=D\times D$. A game $\Gamma=(u^1,u^2)$ is a pair of payoff functions on $X$. A profile $\bar x$ is a (pure) Nash equilibrium if no player gains by changing only their own strategy. A dynamic for a family $\mathcal U$ of games is a vector field $F(x;\Gamma)$ on $X$ for each $\Gamma\in\mathcal U$, read $\dot x=F(x;\Gamma)$. It is uncoupled if $F^i$ depends on the game only through $u^i$: two games of $\mathcal U$ in which player $i$ has the same payoff function give the same $F^i(x;\cdot)$ at every $x\in X$.

A dynamic is Nash-convergent for $\mathcal U$ if, for every $\Gamma\in\mathcal U$ with its Nash equilibrium $\bar x(\Gamma)$:

1. $F(\cdot\,;\Gamma)$ is $C^1$ on $X$;
2. $F(\bar x(\Gamma);\Gamma)=0$;
3. all eigenvalues of the $4\times4$ Jacobian matrix of $F(\cdot\,;\Gamma)$ at $\bar x(\Gamma)$ have negative real parts;
4. every solution $x(t)$ converges to $\bar x(\Gamma)$ as $t\to\infty$, from any initial condition.

The game $\Gamma_0$ has payoffs $u_0^i(x^i,x^j)=-\|x^i-\varphi(x^j)\|^2$. Here $\varphi:D\to D$ is continuous, $\varphi(z)=2z$ for $\|z\|\le\frac13$, $\varphi$ rotates the unit circle by $\pi/4$, and $\varphi$ is affine on rays in between. The family $\mathcal U_0$ consists of the games $u^i(x^i,x^j)=-\|x^i-\xi^i(x^j)\|^2$ with continuous $\xi^i:D\to D$ such that $\xi^i(\xi^j(x^i))=x^i$ has a unique solution. Every such game has a unique Nash equilibrium, and $\Gamma_0\in\mathcal U_0$ has the equilibrium $(0,0)$.

Formalization targets

Goal: THEOREM 1 for the game $\Gamma_0$ of §II

Let $\mathcal U$ be a family in which each game has a single Nash equilibrium and which contains every game of $\mathcal U_0$ within some $\eta>0$ of $\Gamma_0$. Then

$$F\ \text{uncoupled for}\ \mathcal U\ \Longrightarrow\ F\ \text{is not Nash-convergent for}\ \mathcal U.$$

Milestones

• the explicit $\varphi$ has the two required properties, and rotates by an angle in $[0,\pi/4]$ (fn. 21);
• every game of $\mathcal U_0$ has a unique Nash equilibrium, and that of $\Gamma_0$ is $(0,0)$;
• Lemma 2: for an uncoupled Nash-convergent dynamic on $\mathcal U_0$, at a unique best reply $F^i=0$ and the own-strategy Jacobian block $J^i$ has eigenvalues with negative real parts;
• the derivative identity, giving the Jacobian at $\Gamma_0$ the block form

$$J=\begin{bmatrix}J^1&-2J^1\\-2J^2&J^2\end{bmatrix};$$

• the coefficient $a_3=3\det(J^1)\operatorname{tr}(J^2)+3\det(J^2)\operatorname{tr}(J^1)$ of $\lambda$ in $\det(J-\lambda I)$, and Lemma 3: if $J^1,J^2$ are stable, then $J$ has an eigenvalue with positive real part;
• the main-text result: no uncoupled dynamic is Nash-convergent for $\mathcal U_0$;
• the Appendix: the functions $\psi_a$ satisfy conditions (1)–(4), and the conclusions of Lemma 2 at $\Gamma_0$ already follow from the games of $\mathcal U_0$ near $\Gamma_0$.

A companion statement, that the coupled dynamic $\dot x=\bar x(\Gamma)-x$ is Nash-convergent, shows that the notion of Nash-convergence can be met.

Significance

The theorem identifies an informational obstruction rather than a computational one. Convergence to Nash equilibrium is easy if the dynamic may use the whole game, as the coupled dynamic $\dot x=\bar x(\Gamma)-x$ shows. It fails once each player may react only to their own payoff function, and the failure persists on an arbitrarily small neighborhood of a single game. It explains why no natural adaptive procedure has been found that converges to Nash equilibrium in general, and it motivates the stochastic, finite-memory and correlated-equilibrium variants studied afterwards (for example Hart and Mas-Colell, GEB 2006).

The result is proved in the paper. As far as the curators know, it has no machine-checked proof. A formalization fixes the model precisely. That matters here, because the conclusion depends on details the prose treats lightly: which perturbations the family must contain, what the Jacobian is at boundary points, and which solutions count.

Difficulty

The obvious argument fails because an uncoupled dynamic is a different vector field for each game, and nothing forces the fields to fit together except the uncoupledness constraint. The proof extracts information about $F(\cdot\,;\Gamma_0)$ from auxiliary games that share one player's payoff with $\Gamma_0$, and in which that player's best reply is constant. Making those auxiliary games lie in the family is the delicate part: in $\mathcal U_0$ they are immediate, but near $\Gamma_0$ they require the functions $\psi_a$ of the Appendix, whose fixed-point conditions (3) and (4) rest on an angle argument. The linear-algebra step is exact: the stability of $J^1$ and $J^2$ must be shown to force instability of the coupled $4\times4$ matrix through the sign of one coefficient of its characteristic polynomial.

Formalization scope

$\mathbb R^2$ is modelled as $\mathbb C$, and rotation by $\theta$ is multiplication by $e^{i\theta}$. Players are Fin 2, 0-based, and the other player is i + 1. A game is a pair of real functions on $\mathbb C^2$, but every definition looks only at its values on $X=D\times D$. Nash equilibria are pure equilibria in $X$ (fn. 9 notes there are no mixed ones). Derivatives are Fréchet derivatives within $X$. Eigenvalue conditions use the published predicate FatkhullinPolyak.Discrete.IsHurwitz, with the $4\times4$ Jacobian indexed in player-major order. The $C^1$ and Jacobian conditions, which the paper imposes on every dynamic it considers, are part of NashConvergent. The single-Nash-equilibrium property is a hypothesis of the goal.

Two encodings are deliberate:

• The neighborhood. "$\mathcal U$ contains a neighborhood of $\Gamma_0$" is read as the Appendix reads it: $\mathcal U$ contains every game of $\mathcal U_0$ close to $\Gamma_0$ in the sense of fn. 7. This is implied by the literal hypothesis, so the formal theorem is at least as strong. A full neighborhood contains games with several equilibria, so together with the single-equilibrium hypothesis it would make the theorem vacuous.
• Solutions. Solutions are curves that stay in $X$. If curves were allowed to leave $X$, they would follow values of $F$ that no game constrains, and Nash-convergence would fail for every $F$, which makes the goal trivial. The goal must also not be met through an empty family: the hypotheses are jointly satisfiable, for instance by $\{\Gamma\in\mathcal U_0:\Gamma\text{ within }1\text{ of }\Gamma_0\}$.

The development needs:

• calculus of $C^1$ maps on a product of disks;
• spectra of real matrices viewed over $\mathbb C$ and the characteristic polynomial of a $4\times4$ block matrix;
• elementary planar geometry of rotations and radial interpolation.

The linear-algebra milestones (block Jacobian, $a_3$, Lemma 3) are independent of game theory and reusable. Contributions are welcome on any milestone, in any order.

Selected references

• S. Hart and A. Mas-Colell, Uncoupled Dynamics Do Not Lead to Nash Equilibrium, American Economic Review 93(5), 1830–1836, 2003. https://doi.org/10.1257/000282803322655581
• S. Hart and A. Mas-Colell, A Simple Adaptive Procedure Leading to Correlated Equilibrium, Econometrica 68(5), 1127–1150, 2000. https://doi.org/10.1111/1468-0262.00153
• J. S. Jordan, Three Problems in Learning Mixed-Strategy Nash Equilibria, Games and Economic Behavior 5(3), 368–386, 1993. https://doi.org/10.1006/game.1993.1022
• D. P. Foster and H. P. Young, On the Nonconvergence of Fictitious Play in Coordination Games, Games and Economic Behavior 25(1), 79–96, 1998. https://doi.org/10.1006/game.1997.0615
• S. Hart and A. Mas-Colell, Stochastic Uncoupled Dynamics and Nash Equilibrium, Games and Economic Behavior 57(2), 286–303, 2006. https://doi.org/10.1016/j.geb.2005.09.007

Motivation

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

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

Timeline:

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal: Corollary 14 (corrected)

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Corrected statements, with milestone texts kept verbatim:

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

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

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

Selected references

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

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:

1. $\sum_{z\in Z^A_{unit}} m^A_z = \bar n^A$ and $\sum_{z\in Z^B_{unit}} m^B_z = n^B$.
2. 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}.$$

3. $\det Y \ne 0$.
4. 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