Linear algebra

Motivation

Many classical search algorithms are random walks: a Markov chain $P$ on a finite state space $X$ is run until it hits a marked state. Szegedy (2004) attached to every such chain a unitary quantum walk $W(P)$, and Magniez, Nayak, Roland and Santha (SIAM J. Comput. 2011, arXiv:quant-ph/0608026) used it to search quadratically faster than the classical walk for every reversible ergodic chain. The search runs Grover-style rotations, and each rotation needs the reflection $\mathrm{ref}(\pi)$ about the stationary state $|\pi\rangle$. Preparing $|\pi\rangle$ exactly can cost far more than one step of the walk, so the paper builds an approximate reflection $R(P)$ from the walk alone, by phase estimation. Theorem 6 of the paper is the guarantee for that circuit, and this mission formalizes it.

Timeline:

• Jordan, 1875. Two subspaces of a Euclidean space decompose it into one- and two-dimensional invariant pieces ("principal angles").
• Cleve, Ekert, Macchiavello and Mosca, 1998 (Proc. R. Soc. A). The phase-estimation circuit $C(U)$ and its output distribution (Theorem 5 of the paper).
• Szegedy, 2004. The walk $W(P)$, and its spectrum in terms of the singular values of the discriminant matrix (Theorem 4 of the paper).
• Magniez, Nayak, Roland and Santha, 2007/2011. The circuit $R(P)$ and Theorem 6, the search algorithm (Theorem 7), and the bound $\Delta(P)\ge2\sqrt{\delta(P)}$ relating the phase gap to the eigenvalue gap.

Setting

$X$ is a finite set of size $n$. A Markov chain is a row-stochastic matrix $P=(p_{xy})_{x,y\in X}$. It is ergodic if some power of $P$ has all entries positive. A stationary distribution $\pi$ satisfies $\pi_x>0$, $\sum_x\pi_x=1$ and $\sum_x\pi_xp_{xy}=\pi_y$. The time-reversed chain $P^*$ is defined by $\pi_xp_{xy}=\pi_yp^*_{yx}$, and $P$ is reversible if $P^*=P$.

The space is $\mathcal H=\mathbb C^{X\times X}$ with basis $|x\rangle|y\rangle$. Put $|p_x\rangle=\sum_y\sqrt{p_{xy}}\,|y\rangle$ and $|p^*_y\rangle=\sum_x\sqrt{p^*_{yx}}\,|x\rangle$, and

$$\mathcal A=\mathrm{Span}(|x\rangle|p_x\rangle:x\in X),\qquad \mathcal B=\mathrm{Span}(|p^*_y\rangle|y\rangle:y\in X).$$

For a subspace $\mathcal K$, $\mathrm{ref}(\mathcal K)=2\Pi_{\mathcal K}-\mathrm{Id}$, where $\Pi_{\mathcal K}$ is the orthogonal projector onto $\mathcal K$. The quantum walk is $W(P)=\mathrm{ref}(\mathcal B)\cdot\mathrm{ref}(\mathcal A)$, and the stationary state is $|\pi\rangle=\sum_x\sqrt{\pi_x}\,|x\rangle|p_x\rangle$.

The discriminant matrix is $D(P)=(\sqrt{p_{xy}p^*_{yx}})_{x,y}$. Its singular values lie in $[0,1]$. The phase gap $\Delta(P)$ is $2\theta$, where $\theta$ is the smallest angle in $(0,\pi/2)$ such that $\cos\theta$ is a singular value of $D(P)$.

The phase-estimation circuit $C(U)$ acts on $\mathbb C^\iota\otimes\mathbb C^{2^s}$. It is

$$C(U)=(\mathrm{Id}\otimes F^\dagger)\Big(\sum_{j<2^s}U^j\otimes|j\rangle\langle j|\Big)(\mathrm{Id}\otimes H^{\otimes s}),$$

where $H^{\otimes s}$ is the Walsh–Hadamard matrix and $F$ is the $2^s$-point Fourier transform.

The circuit $R(P)$ uses $s=\lceil\log_2(2\pi/\Delta(P))\rceil$ and acts on $\mathcal H\otimes(\mathbb C^{2^s})^{\otimes k}$. It is built in three steps:

1. $V$ applies $C(W(P))$ $k$ times, each time to the system register and a fresh ancilla register.
2. $F_{\neq0}$ multiplies by $-1$ every basis state with a non-zero estimate in some register.
3. Then $R(P)=V^\dagger F_{\neq0}V$.

Formalization targets

Goal: Theorem 6, properties 2 and 3

For $P$ ergodic and reversible on $n\ge2$ states, and every integer $k\ge0$:

$$R(P)\,|\pi\rangle|0^{ks}\rangle=|\pi\rangle|0^{ks}\rangle,\qquad \big\|(R(P)+\mathrm{Id})\,|\psi\rangle|0^{ks}\rangle\big\|\le2^{1-k}\|\psi\|\quad(\psi\in\mathcal A+\mathcal B,\ \psi\perp|\pi\rangle).$$

Milestones

The milestones follow the order in which the paper's proof uses them:

1. Theorem 4 (Szegedy). The spectrum of $W(P)$ on $\mathcal A+\mathcal B$. On that space $W(P)$ has the eigenvalues $1$ (on $\mathcal A\cap\mathcal B$), $-1$, and $e^{\pm2i\theta}$ for $\cos\theta$ a singular value of $D(P)$ in $(0,1)$, with matching multiplicities. The mission has two items for it: the full statement, and the direction the proof uses.
2. §3.2. For ergodic reversible $P$, $|\pi\rangle$ is the only $1$-eigenvector of $W(P)$ in $\mathcal A+\mathcal B$, up to scalars, and every other eigenvalue $\mu$ there satisfies $|1-\mu|\ge|1-e^{i\Delta(P)}|$.
3. Theorem 5, properties 2 and 3. $C(U)$ fixes $|\psi\rangle|0^s\rangle$ when $U\psi=\psi$. If $U\psi=e^{2i\theta}\psi$ with $\theta\in(0,\pi)$, it outputs $|\psi\rangle|\omega\rangle$ with $|\langle0^s|\omega\rangle|=|\sin(2^s\theta)|/(2^s\sin\theta)$.
4. Single-copy bound. For $\Delta/2\le\theta\le\pi-\Delta/2$ and the $s$ above, $|\sin(2^s\theta)|/(2^s\sin\theta)\le1/2$.
5. $k$-copy bound. For $\psi\in\mathcal A+\mathcal B$ with $\psi\perp|\pi\rangle$, the all-zero-estimate component $\psi_0$ of $V|\psi\rangle|0^{ks}\rangle$ has $\|\psi_0\|\le2^{-k}\|\psi\|$. For every $\psi$, $\|(R(P)+\mathrm{Id})|\psi\rangle|0^{ks}\rangle\|=2\|\psi_0\|$.

Significance

Theorem 6 replaces the reflection about $|\pi\rangle$ with a circuit that only calls the walk. Its cost scales as $1/\Delta(P)$ rather than as the cost of preparing $|\pi\rangle$. Combined with $\Delta(P)\ge2\sqrt{\delta(P)}$, where $\delta(P)$ is the eigenvalue gap, this gives the search cost $S+\frac1{\sqrt\varepsilon}\big(\frac1{\sqrt\delta}U+C\big)$ of Theorem 7, up to logarithmic factors. The same approximate-reflection device recurs in later quantum-walk and amplitude-amplification algorithms.

The results are proved in the paper, which takes Theorem 4 from Szegedy and Theorem 5 from Cleve et al. As far as the platform index shows, none of Theorems 4, 5 or 6 has a machine-checked proof. The mission produces three reusable components: a Lean definition of the Szegedy walk and of the phase-estimation circuit, a formal Jordan-type spectral theorem for products of two reflections, and the analysis of phase estimation on an eigenvector.

Difficulty

Most of the work is linear algebra. The proof of Theorem 6 has a short outline: expand $\psi$ in eigenvectors of $W(P)$, apply Theorem 5 to each, and bound each amplitude by $1/2$. Three steps carry the weight:

• Theorem 4. The eigen-decomposition of $W(P)$ on $\mathcal A+\mathcal B$ is Jordan's two-subspace decomposition, with the multiplicities read off the singular value decomposition of $D(P)$. The decomposition has to be built, and the cases at singular values $0$ and $1$ have to be handled separately.
• Uniqueness of $|\pi\rangle$. This step needs ergodicity, through Perron–Frobenius, and reversibility, because $D(P)$ is then symmetric and its singular values are the moduli of the eigenvalues of $P$. Without reversibility $D(P)$ can have the singular value $1$ twice, and property 3 then fails.
• Repetition. The $k$ phase estimations share one system register. Their product acts on an eigenvector as a tensor power on the ancillas. This needs the eigenvectors of the unitary $W(P)$ restricted to the invariant subspace $\mathcal A+\mathcal B$ to be orthogonal.

Formalization scope

• $\mathcal H$ is EuclideanSpace ℂ (X × X), with the first coordinate the first register.
• The ancilla register is indexed by Fin (2^s), and $k$ registers by Fin k → Fin (2^s); the all-zeros state is the zero index.
• $\mathrm{ref}(\mathcal K)$ is Mathlib's Submodule.reflection.
• The stationary distribution $\pi$ is passed as data with its defining hypotheses. "Ergodic" is Matrix.IsPrimitive.
• Singular values of the real matrix $D(P)$ are LinearMap.singularValues.
• When $D(P)$ has no singular value in $(0,1)$, the paper leaves $\Delta(P)$ undefined, and the formalization sets $\Delta(P)=\pi$.
• $\log_2$ is Real.logb 2 and the ceiling is Nat.ceil.

Deviations from the page.

• Reversibility, the standing assumption of §3.2, is a hypothesis of the goal.
• Property 3 is stated for vectors and is homogeneous in $\|\psi\|$.
• Theorem 5 is stated for any finite-dimensional unitary, not only $2^m\times2^m$, and with $|\sin(2^s\theta)|$, because the printed right-hand side can be negative.
• The single-copy bound also covers the eigenvalue $-1$.

Only exact statements are formalized. The cost halves (gate counts, calls to $c$-$W(P)$, "$s\in\log_2(1/\Delta)+O(1)$", the qubit count, uniformity) are out of scope.

The circuit $R(P)$ is the explicit composition above, built from $C(W(P))$. It is neither "some circuit with properties 2–3" nor anything defined through the projector onto $|\pi\rangle$, either of which would make the goal a tautology.

Contributions welcome: proofs of the milestones, Jordan's lemma for two subspaces as a standalone result, and the bound $\Delta(P)\ge2\sqrt{\delta(P)}$ of §3.3.

Selected references

• F. Magniez, A. Nayak, J. Roland, M. Santha, Search via Quantum Walk, SIAM J. Comput. 40(1), 2011. https://arxiv.org/abs/quant-ph/0608026 (v4), https://doi.org/10.1137/090745854
• M. Szegedy, Quantum speed-up of Markov chain based algorithms, FOCS 2004. https://doi.org/10.1109/FOCS.2004.53
• R. Cleve, A. Ekert, C. Macchiavello, M. Mosca, Quantum algorithms revisited, Proc. R. Soc. Lond. A 454, 1998. https://doi.org/10.1098/rspa.1998.0164
• C. Jordan, Essai sur la géométrie à n dimensions, Bull. Soc. Math. France 3, 1875. https://doi.org/10.24033/bsmf.90

Motivation

For a square matrix $A$, the spectrum alone does not control the size of $p(A)$: a nonzero nilpotent matrix has spectrum $\{0\}$ yet $\|A\|>0$. The numerical range $W(A)=\{u^*Au:\ \|u\|=1\}$ is a compact convex set containing the spectrum (Toeplitz–Hausdorff), and it does retain enough information. Crouzeix's conjecture (2004) asserts that for every polynomial $p$,

$$\|p(A)\|\le 2\max_{z\in W(A)}|p(z)|,$$

i.e. that $W(A)$ is a $2$-spectral set; the constant $2$ would be optimal. Such bounds are used to estimate matrix functions in numerical linear algebra (for example GMRES convergence through Faber polynomials) and in operator theory. The complete version asks for the same constant when the polynomial has $m\times m$ matrix coefficients, uniformly in $m$; by Paulsen's theorem this is equivalent to similarity of the conformal disk image of $A$ to a contraction with condition number at most $2$.

Background

• 1918–1919 — Toeplitz and Hausdorff prove convexity of the numerical range (Math. Z. 1918, Math. Z. 1919).
• 1972, 1984 — Arveson's dilation theory (Acta Math. 128, 1972) and Paulsen's similarity theorem (Proc. AMS 92, 1984) relate complete contractivity, dilations and similarity.
• 1999 — Delyon and Delyon's positive integral representations (Bull. SMF 1999).
• 2004 — Crouzeix formulates the constant-two question (IEOT 2004); 2007 — he proves a universal complete bound $11.08$ (JFA 2007).
• 2006 — Badea, Crouzeix and Delyon obtain the complete constant $2$ for $2\times2$ matrices (Math. Z. 2006).
• 2017–2018 — Crouzeix and Palencia prove the complete bound $1+\sqrt2$ (SIMAX 2017); Ransford and Schwenninger simplify the argument (SIMAX 2018).
• 2026 — Scalar ($m=1$) constant-two proofs appear in preprints of Jin, Lorist–Schwenninger (arXiv:2608.03841) and Luo; Åhag, Czyż and Virtanen prove the complete inequality for base matrices of order at most three (arXiv:2608.27346).
• September 2026 — Two OpenAI preprints claim the complete inequality in all dimensions: a structural proof via an optimal similarity and a common positive boundary density, extended to all bounded Hilbert-space operators (source), and a direct coefficient proof for matrices (source).

This mission asks for a formal proof of the complete Crouzeix inequality for all bounded operators on complex Hilbert spaces, with its sharpness, as stated in Corollary 6.3 of an OpenAI preprint dated September 23, 2026 (source), together with the preprint's structural theorems as milestones. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Setting

For $A\in M_n(\mathbb C)$ ($n\ge1$) let $W(A)=\{u^*Au: u\in\mathbb C^n,\ u^*u=1\}$. A matrix polynomial of degree $d$ with coefficient size $m\ge1$ is $P(z)=\sum_{k=0}^dB_kz^k$ with $B_k\in M_m(\mathbb C)$. Its evaluation at $A$ is

$$P[A]=\sum_{k=0}^d A^k\otimes B_k\ \in M_n(\mathbb C)\otimes M_m(\mathbb C),$$

with the base space first. All norms are Euclidean operator norms. For $m=1$ this is the usual $p(A)$.

For a bounded operator $A$ on a complex Hilbert space $\mathcal H\neq\{0\}$, $W(A)=\{\langle x,Ax\rangle:\|x\|=1\}$ and $K=\overline{W(A)}$; $P[A]=\sum_kA^k\otimes B_k$ acts on $\mathcal H\otimes\mathbb C^m$. A bounded open convex $\Omega\subset\mathbb C$ is admissible if its boundary is a regular real-analytic Jordan curve. For such $\Omega\supset W(A)$ ($A$ a matrix) with interior conformal map $f:\Omega\to\mathbb D$, put $T=f(A)$ and

$$\kappa^2=\min\{\tau:\ I\preceq H\preceq\tau I,\ T^*HT\preceq H\ \text{for some } H=H^*\}.$$

Formalization targets

Milestone: geometry of the numerical range (Corollary 6.3, p. 16, first assertion)

For $\mathcal H\neq\{0\}$, $K=\overline{W(A)}$ is compact and convex and contains $\operatorname{spec}(A)$.

Milestone: the zero space (Corollary 6.3, p. 16, case $\mathcal H=\{0\}$)

If $\mathcal H=\{0\}$, the numerical range is empty, every polynomial, holomorphic and rational evaluation is $0$, and the corresponding inequalities read $0\le0$ (with the supremum over the empty set taken to be $0$).

Milestone: optimal metric and common positive representation (Lemma 1.1, Theorems 1.2–1.3, p. 2)

For admissible $\Omega$ conformal coordinates exist; for every $n\ge1$ and $A\in M_n(\mathbb C)$ with $W(A)\subset\Omega$, the problem defining $\kappa^2$ is strictly feasible with attained minimum $1\le\kappa^2\le4$; for a minimizer $H$, $S=H^{1/2}$ satisfies $\|S\|\|S^{-1}\|=\kappa\le2$ and $D=Sf(A)S^{-1}$ is a contraction with $\rho(D)<1$; and one continuous $\Lambda:\mathbb T\to M_n(\mathbb C)$ with $\Lambda\succeq0$, $\int\Lambda\,d\sigma=I$ represents $v[SAS^{-1}]=\int\Lambda(t)\otimes v(G(t))\,d\sigma(t)$ for every $m$ and every $M_m$-valued $v$ holomorphic near $\overline\Omega$, giving $\|v[A]\|\le\kappa\max_{\overline\Omega}\|v\|$.

Milestone: the matrix inequality (Corollary 6.1, p. 15)

For all $n,m\ge1$, $d\ge0$, $A\in M_n(\mathbb C)$, $B_k\in M_m(\mathbb C)$: $\|P[A]\|\le2\max_{W(A)}\|P\|$, and no smaller universal constant works.

Goal: Corollary 6.3 (p. 16)

For every complex Hilbert space $\mathcal H$ (no separability assumption) and $A\in B(\mathcal H)$: if $\mathcal H\neq\{0\}$ then $K$ is compact, convex, contains the spectrum, and for every $m\ge1$

$$\|P[A]\|\le 2\sup_{W(A)}\|P\|=2\max_K\|P\|,\qquad \|F[A]\|\le2\max_K\|F\|,\qquad \|R[A]\|\le 2\max_K\|R\|$$

for matrix polynomials $P$, matrix functions $F$ holomorphic on an open $U\supseteq K$ (holomorphic functional calculus), and matrix rational functions $R$ with poles off $K$; if $\mathcal H=\{0\}$ the degenerate statements above hold; and the constant $2$ is optimal.

Significance

The result itself. It resolves the complete Crouzeix conjecture in its operator formulation, independent of the Hilbert space, the coefficient size and the degree: $\overline{W(A)}$ is a complete $2$-spectral set for every bounded operator. The structural theorems give more than the inequality: an optimal similarity, attained, with condition number at most $2$, and one positive boundary density that represents every matrix-valued analytic evaluation simultaneously. These are the objects predicted abstractly by Paulsen's and Arveson's theorems, constructed here explicitly. A companion OpenAI preprint gives an independent direct proof of the matrix inequality.

Formalizing it. Mathlib has bounded operators, the holomorphic functional calculus is only partially available, and conformal mapping of analytic Jordan domains is absent. A complete development needs the Riemann mapping theorem with boundary extension, semidefinite optimization over Hermitian matrices, Haar integration on the circle, and a finite-compression argument for nonseparable spaces.

Difficulty

Two obstacles stand out. First, the passage from the scalar to the complete inequality: scalar proofs exploit commutativity that fails for matrix coefficients, so a structure valid for every coefficient size at once is needed; here it is the optimal metric chosen before any test function. Proving $\kappa\le2$ for that metric requires an endpoint extremal pair (Proposition 2.2, p. 6) and an ordered density comparison (Lemma 5.1, p. 14). Second, the passage from matrices to arbitrary operators: the numerical range of a compression lies in $W(A)$, but one must show every vector of $\mathcal H\otimes\mathbb C^m$ and its image under $P[A]$ live in a finite-dimensional compression, and treat holomorphic and rational calculi through contour integrals around the closed numerical range.

Formalization scope

• H is any type with InnerProductSpace ℂ H and CompleteSpace H; operators are H →L[ℂ] H. The amplification $\mathcal H\otimes\mathbb C^m$ is the completion of the algebraic tensor product, and $A^k\otimes B_k$ is the completed TensorProduct.mapL.
• supNorm S F = sSup (insert 0 (‖F ·‖ '' S)), so the supremum over an empty set is $0$, matching the convention of Corollary 6.3.
• Holomorphic evaluation is defined by a contour integral over a CalculusContour around $K$ inside $U$; the goal asserts such contours exist and that the evaluation is contour-independent. Rational evaluation inverts aeval A denom; the goal asserts these denominators are units and that the rational evaluation agrees with the holomorphic one.
• SharpConstant is witnessed by a $2\times2$ matrix with $\sup_{W}|P|=1$ and $\|P[A]\|=2$.
• The structural milestone also includes, as an extra conjunct, that the open unit disk is admissible.

Two further published supporting statements are included as items but not milestones: existence of a finite-dimensional compression representing a given vector (a step in the proof of Corollary 6.3) and invertibility of rational denominators (the well-definedness part of the rational calculus).

Selected references

• OpenAI, The complete Crouzeix theorem: optimal similarity and a common positive boundary representation, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-complete-Crouzeix-theorem-September-23-2026/paper.pdf
• OpenAI, A direct proof of the complete Crouzeix inequality, OpenAI Math Release preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-direct-proof-of-the-complete-Crouzeix-inequality-September-26-2026/paper.pdf
• V. I. Paulsen, Completely bounded homomorphisms of operator algebras, Proc. Amer. Math. Soc. 92 (1984), 225–228.
• W. Arveson, Subalgebras of C-algebras II*, Acta Math. 128 (1972), 271–308.
• M. Crouzeix, Bounds for analytical functions of matrices, Integral Equations Operator Theory 48 (2004), 461–477. https://doi.org/10.1007/s00020-002-1188-6
• M. Crouzeix, Numerical range and functional calculus in Hilbert space, J. Funct. Anal. 244 (2007), 668–690. https://doi.org/10.1016/j.jfa.2006.10.013
• M. Crouzeix, C. Palencia, The numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 38 (2017), 649–655. https://doi.org/10.1137/17M1116672
• T. Ransford, F. L. Schwenninger, Remarks on the Crouzeix–Palencia proof that the numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 39 (2018), 342–345. https://doi.org/10.1137/17M1143757
• C. Badea, M. Crouzeix, B. Delyon, Convex domains and K-spectral sets, Math. Z. 252 (2006), 345–365. https://doi.org/10.1007/s00209-005-0857-y
• B. Delyon, F. Delyon, Generalization of von Neumann's spectral sets and integral representation of operators, Bull. Soc. Math. France 127 (1999), 25–41. https://doi.org/10.24033/bsmf.2340
• E. Lorist, F. L. Schwenninger, A solution to Crouzeix's conjecture, arXiv:2608.03841 (2026). https://arxiv.org/abs/2608.03841v2
• P. Åhag, R. Czyż, J. Virtanen, The complete Crouzeix conjecture in dimension three and the Clouâtre–Ostermann–Ransford conjecture, arXiv:2608.27346 (2026). https://arxiv.org/abs/2608.27346v4
• O. Toeplitz, Das algebraische Analogon zu einem Satze von Fejér, Math. Z. 2 (1918), 187–197. https://doi.org/10.1007/BF01212904
• F. Hausdorff, Der Wertvorrat einer Bilinearform, Math. Z. 3 (1919), 314–316. https://doi.org/10.1007/BF01292610

Motivation

For a square matrix $A$, the spectrum alone does not control the size of $p(A)$: a nonzero nilpotent matrix has spectrum $\{0\}$ yet $\|A\|>0$. The numerical range $W(A)=\{u^*Au:\ \|u\|=1\}$ is a compact convex set containing the spectrum (Toeplitz–Hausdorff), and it does retain enough information. Crouzeix's conjecture (2004) asserts that for every polynomial $p$,

$$\|p(A)\|\le 2\max_{z\in W(A)}|p(z)|,$$

i.e. that $W(A)$ is a $2$-spectral set; the constant $2$ would be optimal. Such bounds are used to estimate matrix functions in numerical linear algebra (for example GMRES convergence through Faber polynomials) and in operator theory. The complete version asks for the same constant when the polynomial has $m\times m$ matrix coefficients, uniformly in $m$; by Paulsen's theorem this is equivalent to similarity of the conformal disk image of $A$ to a contraction with condition number at most $2$.

Background

• 1918–1919 — Toeplitz and Hausdorff prove convexity of the numerical range (Math. Z. 1918, Math. Z. 1919).
• 1972, 1984 — Arveson's dilation theory (Acta Math. 128, 1972) and Paulsen's similarity theorem (Proc. AMS 92, 1984) relate complete contractivity, dilations and similarity.
• 1999 — Delyon and Delyon's positive integral representations (Bull. SMF 1999).
• 2004 — Crouzeix formulates the constant-two question (IEOT 2004); 2007 — he proves a universal complete bound $11.08$ (JFA 2007).
• 2006 — Badea, Crouzeix and Delyon obtain the complete constant $2$ for $2\times2$ matrices (Math. Z. 2006).
• 2017–2018 — Crouzeix and Palencia prove the complete bound $1+\sqrt2$ (SIMAX 2017); Ransford and Schwenninger simplify the argument (SIMAX 2018).
• 2026 — Scalar ($m=1$) constant-two proofs appear in preprints of Jin, Lorist–Schwenninger (arXiv:2608.03841) and Luo; Åhag, Czyż and Virtanen prove the complete inequality for base matrices of order at most three (arXiv:2608.27346).
• September 2026 — Two OpenAI preprints claim the complete inequality in all dimensions: a structural proof via an optimal similarity and a common positive boundary density, extended to all bounded Hilbert-space operators (source), and a direct coefficient proof for matrices (source).

This mission asks for a formal proof of the complete Crouzeix inequality for matrices, with its sharpness, as stated in Theorem 1.1 of an OpenAI preprint dated September 26, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Setting

For $A\in M_n(\mathbb C)$ ($n\ge1$) let $W(A)=\{u^*Au: u\in\mathbb C^n,\ u^*u=1\}$. A matrix polynomial of degree $d$ with coefficient size $m\ge1$ is $P(z)=\sum_{k=0}^dB_kz^k$ with $B_k\in M_m(\mathbb C)$. Its evaluation at $A$ is

$$P[A]=\sum_{k=0}^d A^k\otimes B_k\ \in M_n(\mathbb C)\otimes M_m(\mathbb C),$$

with the base space first. All norms are Euclidean operator norms. For $m=1$ this is the usual $p(A)$.

Formalization targets

Milestone: the inequality (Theorem 1.1, p. 1, first assertion)

For all $n,m\ge1$, $d\ge0$, $A\in M_n(\mathbb C)$ and $B_0,\dots,B_d\in M_m(\mathbb C)$,

$$\Bigl\|\sum_{k=0}^dA^k\otimes B_k\Bigr\|\ \le\ 2\max_{z\in W(A)}\Bigl\|\sum_{k=0}^dB_kz^k\Bigr\| .$$

Milestone: sharpness (Theorem 1.1, p. 1, second assertion)

If the inequality holds with a constant $c$ in place of $2$ for all $n,m,d,A,B$, then $c\ge2$.

Goal: Theorem 1.1 (p. 1)

Both assertions together: the constant $2$ is valid and no smaller universal constant is.

Significance

The result itself. It settles the complete Crouzeix conjecture in its matrix formulation, uniformly in the base dimension $n$, the coefficient size $m$ and the degree, including matrices whose numerical range is a point or a segment. The scalar case $m=1$ had recently been proved by other authors and the complete case was known only for $n\le3$; a scalar argument need not survive matrix amplification because coefficient matrices do not commute. Equivalently, the numerical range is a complete $2$-spectral set for every matrix, which via Paulsen's theorem gives a similarity of condition number at most $2$ making the conformal disk image of $A$ a contraction. A companion OpenAI preprint gives a separate structural proof and extends the bound to all bounded operators on Hilbert spaces.

Formalizing it. The proof uses exterior conformal maps of analytic convex domains, Faber-type coefficients, a positive double-layer kernel, and a $2\times2$ block positivity argument; Section 4 then approximates an arbitrary numerical range by analytic convex domains. A formal proof would provide numerical ranges, Faber polynomials and conformal collars in Lean, all reusable in matrix analysis. No machine-checked proof of any constant-$2$ Crouzeix bound is known.

Difficulty

The naive approach through the spectrum fails for non-normal matrices, and the classical Crouzeix–Palencia method (a positive double-layer potential plus a Cauchy transform of conjugate data) loses a factor and yields $1+\sqrt2$. To reach $2$ in the complete setting, the argument must keep both multiplication orders $FG$ and $GF$ of matrix-valued test functions, since the coefficients do not commute. The preprint chooses a top singular pair $(x,y)$ of $F[A]$, represents three functionals through the resolvent, and must show that the resulting coefficient weights (one on the constant term, one half on the others) match exactly the Fourier weights of the diagonal compressions (Section 2, Proposition 2.2, p. 5; Theorem 3.2, p. 6). Degenerate numerical ranges with empty interior require a separate approximation step (Lemma 4.1, p. 9).

Formalization scope

• Matrices are Matrix (Fin n) (Fin n) ℂ with the L2 operator norm (Matrix.Norms.L2Operator). The numerical range is the set of $\langle x, Ax\rangle$ over unit vectors of EuclideanSpace ℂ (Fin n).
• Coefficients are B : Fin (d+1) → Matrix (Fin m) (Fin m) ℂ; the evaluation is $\sum_k A^k\otimes_{\mathrm{Kron}}B_k$ indexed by Fin n × Fin m, base factor first.
• rangeMaximum A B is the sSup of $\|P(z)\|$ over $W(A)$. Since $n\ge1$, $W(A)$ is nonempty and compact, so this is the true maximum; UniversalBound C quantifies over all $n,m\ge1$, all $d$, all $A$ and $B$.
• The goal OAI.CompleteCrouzeix.main is UniversalBound 2 ∧ ∀ C, UniversalBound C → 2 ≤ C. The two milestones state the same two clauses in the DirectCrouzeix namespace, whose definitions are identical in content.
• No normality, invertibility or nonempty-interior hypothesis is imposed on $A$.

Selected references

• OpenAI, A direct proof of the complete Crouzeix inequality, OpenAI Math Release preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-direct-proof-of-the-complete-Crouzeix-inequality-September-26-2026/paper.pdf
• OpenAI, The complete Crouzeix theorem: optimal similarity and a common positive boundary representation, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-complete-Crouzeix-theorem-September-23-2026/paper.pdf
• M. Crouzeix, Bounds for analytical functions of matrices, Integral Equations Operator Theory 48 (2004), 461–477. https://doi.org/10.1007/s00020-002-1188-6
• M. Crouzeix, Numerical range and functional calculus in Hilbert space, J. Funct. Anal. 244 (2007), 668–690. https://doi.org/10.1016/j.jfa.2006.10.013
• M. Crouzeix, C. Palencia, The numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 38 (2017), 649–655. https://doi.org/10.1137/17M1116672
• T. Ransford, F. L. Schwenninger, Remarks on the Crouzeix–Palencia proof that the numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 39 (2018), 342–345. https://doi.org/10.1137/17M1143757
• C. Badea, M. Crouzeix, B. Delyon, Convex domains and K-spectral sets, Math. Z. 252 (2006), 345–365. https://doi.org/10.1007/s00209-005-0857-y
• B. Delyon, F. Delyon, Generalization of von Neumann's spectral sets and integral representation of operators, Bull. Soc. Math. France 127 (1999), 25–41. https://doi.org/10.24033/bsmf.2340
• E. Lorist, F. L. Schwenninger, A solution to Crouzeix's conjecture, arXiv:2608.03841 (2026). https://arxiv.org/abs/2608.03841v2
• P. Åhag, R. Czyż, J. Virtanen, The complete Crouzeix conjecture in dimension three and the Clouâtre–Ostermann–Ransford conjecture, arXiv:2608.27346 (2026). https://arxiv.org/abs/2608.27346v4
• O. Toeplitz, Das algebraische Analogon zu einem Satze von Fejér, Math. Z. 2 (1918), 187–197. https://doi.org/10.1007/BF01212904
• F. Hausdorff, Der Wertvorrat einer Bilinearform, Math. Z. 3 (1919), 314–316. https://doi.org/10.1007/BF01292610

Motivation

A finite strategic game can be changed in ways that no player can detect strategically. Adding to player $m$'s utility any function that does not depend on player $m$'s own strategy leaves every unilateral comparison "is strategy $a$ better for me than strategy $b$, given what the others do?" unchanged, so it leaves every best response and every pure Nash equilibrium unchanged. Such changes are not irrelevant, however: they move the payoff levels, and therefore change which outcomes are efficient.

Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405; Math. Oper. Res. 36(3), 2011, DOI 10.1287/moor.1110.0500) make this precise. They decompose every finite game uniquely into a potential component, a harmonic component and a nonstrategic component (their Theorem 4.1). The first two determine all pairwise comparisons; the third determines nothing about equilibria. Section 5.3 of the paper asks what the third component can do to efficiency, and answers with Theorem 5.9: by changing only the nonstrategic component, the pure Nash equilibria of a game can be made to coincide exactly with its Pareto optimal profiles. This mission formalizes that result.

The question matters wherever a designer can transfer payoffs without altering incentives (for instance side payments to a player that depend only on the other players' actions): the theorem says such transfers can always align equilibrium with efficiency, provided an equilibrium exists.

Setting

There is a finite set $\mathcal M$ of players. Player $m$ has a finite nonempty set $E^m$ of strategies; a strategy profile is $p = (p^m)_{m\in\mathcal M} \in E = \prod_m E^m$, and $(q^m, p^{-m})$ denotes $p$ with player $m$'s strategy replaced by $q^m$. A game is a family of utilities $u = (u^m)_m$, $u^m : E \to \mathbb R$.

Two profiles are $m$-comparable if they differ, and differ only in player $m$'s strategy. The game graph has node set $E$ and an edge between every pair of profiles that are $m$-comparable for some $m$. On this graph:

• $C_0$ is the space of functions $E \to \mathbb R$ with $\langle \varphi, \psi\rangle_0 = \sum_p \varphi(p)\psi(p)$;
• $C_1$ is the space of edge flows $X$ ($X(p,q) = -X(q,p)$ on edges, $0$ off edges) with $\langle X, Y\rangle_1 = \tfrac12\sum_{(p,q)} X(p,q)Y(p,q)$, summed over ordered adjacent pairs;
• $\delta_0 : C_0 \to C_1$, $(\delta_0\varphi)(p,q) = \varphi(q) - \varphi(p)$ on edges, is the combinatorial gradient;
• $D_m : C_0 \to C_1$ is the same difference restricted to $m$-comparable pairs, and $D u = \sum_m D_m u^m$. For $m$-comparable $p,q$, $(Du)(p,q) = u^m(q) - u^m(p)$: $D$ records the game's pairwise comparisons.

Games form the space $C_0^M$ with the inner product $\sum_m\langle u^m, v^m\rangle_0$. With $\dagger$ the Moore–Penrose pseudoinverse for these inner products, the potential and harmonic components of a game are

$$u_{\mathcal P} = D^\dagger\delta_0\delta_0^\dagger D u, \qquad u_{\mathcal H} = D^\dagger(I - \delta_0\delta_0^\dagger) D u ,$$

and the nonstrategic component is what remains. A profile $p$ is a pure Nash equilibrium of $u$ if $u^m(q^m, p^{-m}) \le u^m(p)$ for all $m$ and $q^m$, and it is Pareto optimal (Definition 5.3) if no profile $q$ has $u^m(q) \ge u^m(p)$ for all $m$ and $u^k(q) > u^k(p)$ for some $k$.

Formalization targets

Goal: Theorem 5.9

For every game $u$ that has a pure Nash equilibrium there is a game $\bar u$ with

$$\bar u_{\mathcal P} = u_{\mathcal P},\qquad \bar u_{\mathcal H} = u_{\mathcal H},\qquad \{p : p \text{ pure NE of } \bar u\} = \{p : p \text{ Pareto optimal in } \bar u\}.$$

The statement is existential and fixes nothing about $\bar u$ beyond its potential and harmonic components; it asserts the full equality of the two sets, not one inclusion.

Milestones

1. §5.3, p. 32. Games with the same potential and harmonic components have the same pure Nash equilibria.
2. Lemma 5.4. For every game $u$ there is a game $\hat u$ with $\hat u_{\mathcal P} = u_{\mathcal P}$, $\hat u_{\mathcal H} = u_{\mathcal H}$, and $\hat u^m(p) = 0$ for every player $m$ at every pure Nash equilibrium $p$ of $u$.

Significance

The result. The nonstrategic component has no influence on the pairwise comparisons, and hence on equilibria, yet Theorem 5.9 shows that it controls efficiency completely: whenever a pure equilibrium exists, some choice of it makes every equilibrium Pareto optimal and every Pareto optimal profile an equilibrium. Read the other way, two games that are strategically indistinguishable can have opposite efficiency properties, so any efficiency statement about a class of games (a price-of-anarchy bound, for instance) must depend on more than the strategic structure. The paper also uses Lemma 5.4 as a normalisation: the payoff levels at equilibria are a free parameter of the nonstrategic component.

Formalizing it. The theorem has a short proof on paper, but the proof works with the pairwise comparisons, whereas the statement is about the components $u_{\mathcal P}$, $u_{\mathcal H}$ defined through pseudoinverses. Connecting the two requires the identities of the decomposition: that $u_{\mathcal P} + u_{\mathcal H} = D^\dagger D u$ and that $D D^\dagger D = D$. The mission therefore produces a machine-checked link between the linear-algebraic decomposition of games and their equilibrium sets, which other results of the paper (and of the literature on near-potential games) also need. To the best of our knowledge, none of these statements has been formalized before; the result itself is proved in the paper.

Difficulty

The construction on pp. 31–33 is explicit, so the difficulty is not finding $\bar u$ but keeping two descriptions of "differ only in the nonstrategic component" consistent. The statement uses the component maps; the proof checks pointwise that $u^m(p) - u^m(q) = \bar u^m(p) - \bar u^m(q)$ for $m$-comparable $p, q$. Passing from the second to the first needs the pseudoinverse identities for $D$ and $\delta_0$ with respect to the specific inner products of $C_0^M$ and $C_1$; a naive argument that treats $D^\dagger$ as an inverse fails because $D$ has a large kernel. A second point is the case analysis in the definition of $\bar u$: whether a profile is $m$-comparable to an equilibrium must be shown independent of which of two $m$-comparable profiles is examined, and the case where a non-equilibrium profile is $m$-comparable to an equilibrium for every player $m$ needs the separate argument of p. 33.

Formalization scope

Players form a finite type ι with decidable equality; strategy sets E m are finite, nonempty and have decidable equality. A game is an element of PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)), i.e. $C_0^M$ with the unweighted sum inner product of Section 4; the weighted inner product of Section 6 is not used. $C_1$ carries the inner product with the factor $\tfrac12$. The pseudoinverse is defined directly (Mathlib has none) as the inverse of $L$ on $(\ker L)^\perp$ composed with the orthogonal projection onto the range. Pure Nash equilibrium is AGT.IsPureNash from the published agt_games bundle; Pareto optimality is Definition 5.3, stated for a plain utility function.

Added hypothesis. The paper leaves implicit that $G$ has a pure Nash equilibrium, and the goal carries it as a hypothesis. It is necessary: every finite game has a Pareto optimal profile (a maximizer of $\sum_m u^m$), while a game without pure equilibria, such as matching pennies, has none in any game with the same potential and harmonic components, so the set equality would fail. The paper's proof uses an equilibrium in the step "deviation to a NE increases the payoff of at least one player". Lemma 5.4 needs no such hypothesis.

"Same potential and harmonic components" is stated as equality of the two component maps of Theorem 4.1, never as membership of $u - \bar u$ in $\ker D$; the two are equivalent only through the decomposition theorem. Without condition (i) the goal would be trivial (take $\bar u$ constant, so that every profile is both an equilibrium and Pareto optimal), so condition (i) is what makes the statement nontrivial.

Needed infrastructure: the Penrose identities for the pseudoinverse; $D D^\dagger D = D$; the fact that $Du$ determines each $D_m u^m$ (the $m$-comparable edge sets for different $m$ are disjoint); and the explicit constructions of $\hat u$ and $\bar u$. The pseudoinverse lemmas and the "same comparisons, same equilibria" bridge are reusable throughout the series. Proofs of the milestones, of the bridge in either direction, and of the Penrose identities are welcome as separate contributions.

Selected references

• O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, arXiv:1005.2405v2, 2010. https://arxiv.org/abs/1005.2405 — journal version: Mathematics of Operations Research 36(3):474–503, 2011. https://doi.org/10.1287/moor.1110.0500
• D. Monderer, L. S. Shapley, Potential Games, Games and Economic Behavior 14(1):124–143, 1996. https://doi.org/10.1006/game.1996.0044
• R. Penrose, A generalized inverse for matrices, Mathematical Proceedings of the Cambridge Philosophical Society 51(3):406–413, 1955. https://doi.org/10.1017/S0305004100030401

Motivation

Finite games in strategic form are the basic model of interaction between self-interested agents in economics, engineering and computer science. Among them, potential games (Monderer and Shapley, 1996) are the class with the most tractable equilibrium behaviour: every finite potential game has a pure Nash equilibrium, and simple learning dynamics such as best response and fictitious play converge to one. A natural question is what lies at the opposite end of the space of games, and how far a general game is from that tractable class.

Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405; Mathematics of Operations Research 36(3), 2011, DOI 10.1287/moor.1110.0500) answer this with a canonical decomposition of every finite game into a potential, a harmonic and a nonstrategic component, obtained by viewing the payoff differences of a game as a flow on a graph and applying the combinatorial Helmholtz decomposition. Harmonic games, those whose potential component vanishes, are the complement of potential games, and the paper shows that their equilibrium behaviour is opposite as well. This mission formalizes the first such result: harmonic games generically have no pure Nash equilibrium, so the guaranteed existence of pure equilibria in potential games has no counterpart on the harmonic side. The decomposition has since been used to study near-potential games and the convergence of learning dynamics in them.

Setting

A finite game has a finite set of players $\mathcal M$ with $M = |\mathcal M|$ and, for each player $m$, a nonempty finite strategy set $E^m$ with $h_m = |E^m|$ elements. A strategy profile is $p = (p^m)_m \in E = \prod_m E^m$, and $(q^m, p^{-m})$ denotes $p$ with player $m$'s strategy replaced by $q^m$. The utilities $u = (u^m)_m$ assign to each player a function $u^m : E \to \mathbb R$; for fixed $\mathcal M$ and $E$ a game is identified with its utilities, an element of $C_0^M$, where $C_0 = \{f : E \to \mathbb R\}$ carries the inner product $\langle \varphi_1,\varphi_2\rangle_0 = \sum_p \varphi_1(p)\varphi_2(p)$.

A profile $p$ is a pure Nash equilibrium if $u^m(p^m, p^{-m}) \ge u^m(q^m, p^{-m})$ for every player $m$ and every $q^m \in E^m$.

Two profiles are $m$-comparable if they are distinct and differ only in player $m$'s strategy. The game graph has the profiles as nodes and joins every comparable pair. An edge flow is a function $X$ on ordered pairs of profiles with $X(p,q) = -X(q,p)$ on edges and $X = 0$ off edges; the space $C_1$ of edge flows carries $\langle X,Y\rangle_1 = \tfrac12\sum_{(p,q)\in A} X(p,q)Y(p,q)$. The combinatorial gradient is $(\delta_0\varphi)(p,q) = W(p,q)(\varphi(q)-\varphi(p))$, with $W$ the edge indicator, and $\delta_0^*$ is its adjoint. Restricting to $m$-comparable pairs gives $D_m : C_0 \to C_1$, and $D u = \sum_m D_m u^m$ is the flow of payoff differences of the game $u$. With $\Pi_m = D_m^\dagger D_m$ (Moore–Penrose pseudoinverse) and $\Pi = \operatorname{diag}(\Pi_1,\dots,\Pi_M)$, the paper's Definition 4.2 sets

$$\mathcal P = \{u \mid u = \Pi u,\ Du \in \operatorname{im}\delta_0\},\quad \mathcal H = \{u \mid u = \Pi u,\ Du \in \ker\delta_0^*\},\quad \mathcal N = \ker D .$$

A game is a harmonic game if $u \in \mathcal H \oplus \mathcal N$: its payoff differences form a flow with no source or sink at any profile.

Formalization targets

Goal: Proposition 5.1

For finite games in which at least two players have at least two strategies each, and for any additive Haar measure $\mu$ on the finite-dimensional space $\mathcal H \oplus \mathcal N$,

$$\mu\big(\{u \in \mathcal H\oplus\mathcal N : u \text{ has a pure Nash equilibrium}\}\big) = 0 .$$

This is the paper's "harmonic games generically do not have pure Nash equilibria", with "generically" read as the paper defines it: true except on a set of measure zero within the harmonic games.

Stronger structural form

For each profile $p$, the harmonic games having $p$ as a pure Nash equilibrium form a proper linear subspace of $\mathcal H \oplus \mathcal N$. The exceptional set of the goal is then a finite union of lower-dimensional subspaces.

Milestones

1. Lemma 5.1: at a pure Nash equilibrium of a harmonic game, every player is indifferent among all of their strategies.
2. Proposition 4.1: $\dim\mathcal P = \prod_m h_m - 1$, $\dim\mathcal H = (M-1)\prod_m h_m - \sum_m\prod_{k\ne m}h_k + 1$, $\dim\mathcal N = \sum_m\prod_{k\ne m}h_k$.

Significance

The result separates harmonic games sharply from potential games. A finite potential game always has a pure equilibrium; a harmonic game almost never has one. Together with the decomposition theorem, it says that the obstruction to pure equilibria in a general game is carried by its harmonic component, and it motivates the paper's later results on mixed equilibria of harmonic games (the uniformly mixed profile is always a mixed equilibrium). Proposition 4.1, a milestone here, also gives the dimension of the harmonic games, $(M-1)\prod_m h_m + 1$, and so measures how large that class is.

The results are proved in the paper; none of them is machine-checked. Formalizing them requires the paper's operator layer (flows on the game graph, the gradient with its adjoint, pseudoinverses) in Lean for the first time, and pins down two points the paper leaves informal: the measure with respect to which "generically" is meant, and the shape condition on the game under which the statement holds.

Difficulty

Lemma 5.1 is a short counting argument once the divergence-free condition $\delta_0^* D u = 0$ is unpacked, but unpacking it requires knowing that $D$ kills $\mathcal N$ and computing $\delta_0^*$ from the $\tfrac12$-weighted inner product. The main obstacle of the goal is showing that the exceptional subspaces are proper. The proof needs a harmonic game with nonzero payoff differences, that is $\dim\mathcal H > 0$, and the only route the paper offers is the dimension count of Proposition 4.1. That count rests on the full decomposition $C_0^M = \mathcal P\oplus\mathcal H\oplus\mathcal N$, on the kernel of each $D_m$ and on the connectivity of the game graph, all of which must be built in Lean. The measure-theoretic last step, that a finite union of proper subspaces is Haar-null, is in Mathlib.

A tempting shortcut fails: placing Lebesgue measure on all of $C_0^M$ and observing that $\mathcal H \oplus \mathcal N$ is a proper subspace would prove the goal without saying anything about equilibria.

Formalization scope

Players form a finite type ι with decidable equality, and the strategy sets E m are nonempty finite types, as in the paper ($E^m = \{1,\dots,h_m\}$). A game is an element of PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)), with the unweighted sum inner product of p. 14. $C_1$ is the subspace of edge flows with the inner product $\tfrac12\sum$ of (7). $\delta_0^*$ is Mathlib's adjoint, and the pseudoinverse is defined directly as the inverse of $L$ on $(\ker L)^\perp$ composed with the orthogonal projection onto $\operatorname{im} L$. $\mathcal P,\mathcal H,\mathcal N$ are defined by (28), not by the alternative description (29). Harmonic games are the submodule H ⊔ N, and pure Nash equilibrium is AGT.IsPureNash from the published agt_games definitions.

Added hypothesis. The paper leaves implicit that at least two distinct players have at least two strategies each. Its proof uses this through "dimension of $\mathcal H$ is larger than zero". Without it Proposition 5.1 is false: with two players having $1$ and $h$ strategies, $\dim\mathcal H = (2-1)h - (h+1) + 1 = 0$, every harmonic game is nonstrategic, and every profile is a pure equilibrium of every harmonic game. The goal and the structural theorem therefore carry this hypothesis explicitly.

The measure. The measure is an arbitrary additive Haar measure on the subspace $\mathcal H\oplus\mathcal N$ itself, with the Borel σ-algebra of its subspace topology. A measure on the ambient $C_0^M$ would make the statement trivial, because the whole subspace is null there. Proposition 4.1 is stated as equalities in $\mathbb Z$, so that $M-1$ and the subtraction in part 2 are not truncated.

Needed infrastructure: kernels of the $D_m$ (the paper's Lemma 4.2), the projection property of $D^\dagger D$, the decomposition theorem, and the connectivity of the game graph. The operator layer is shared with the other missions of this series and is reusable for any work on flows on graphs. Proofs of the milestones, and of the structural form independently of the goal, are welcome.

Selected references

• O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, arXiv:1005.2405v2, 2010; Mathematics of Operations Research 36(3):474–503, 2011. https://arxiv.org/abs/1005.2405, https://doi.org/10.1287/moor.1110.0500
• D. Monderer, L. S. Shapley, Potential Games, Games and Economic Behavior 14(1):124–143, 1996. https://doi.org/10.1006/game.1996.0044
• X. Jiang, L.-H. Lim, Y. Yao, Y. Ye, Statistical ranking and combinatorial Hodge theory, Mathematical Programming 127(1):203–244, 2011. https://doi.org/10.1007/s10107-010-0419-x