Linear algebra

Motivation

Misinformation campaigns target specific people in a social network and rely on the network to spread what they plant. Whether such a campaign can succeed depends on how people combine what they see themselves with what their neighbours believe. Mostagir, Ozdaglar and Siderius (SSRN 3474643; Management Science, 2022, doi:10.1287/mnsc.2021.4265) model a network in which a strategic principal injects slanted news into chosen agents. Some agents are Bayesian and know the truth; the rest are DeGroot agents who average their own news-based opinion with their neighbours' beliefs.

The paper asks when society as a whole can be manipulated. Every later result in it — which agents the principal targets, which networks resist manipulation, how the answer depends on the network's density — is a statement about the agents' long-run beliefs. Its Theorem 2 supplies those beliefs in closed form, and that closed form is the subject of this mission.

DeGroot updating (DeGroot, 1974) and its combination with personal Bayesian updates (Jadbabaie, Molavi, Sandroni and Tahbaz-Salehi, 2012) are standard models of non-Bayesian social learning. Stubborn agents in averaging dynamics were studied by Acemoglu, Como, Fagnani and Ozdaglar (2013). The present model adds a principal who corrupts the signals of targeted agents.

Setting

There are $n$ agents and a binary state $y\in\{S,R\}$ with prior $q=\mathbb P(y=S)\in(0,1)$. Agent $i$ has a signal quality $p_i\in[1/2,1)$. At each time $\tau=1,2,\dots$ agent $i$ receives a signal $s_{i,\tau}\in\{S,R\}$:

• Organic news equals the state with probability $p_i$: $\mathbb P(s_{i,\tau}=S\mid y=S)=\mathbb P(s_{i,\tau}=R\mid y=R)=p_i$.
• The principal fixes an influence state $\hat y$ and an influence strategy $\mathbf x=(x_1,\dots,x_n)\in\{0,1\}^n$. A targeted agent ($x_i=1$) receives the principal's message $\hat y$ with probability $\lambda^*/(\lambda+\lambda^*)$ and organic news with probability $\lambda/(\lambda+\lambda^*)$. Here $\lambda>0$ and $\lambda^*>0$ are the intensities of the organic and the principal's news. An untargeted agent receives only organic news.

Agent $i$'s signals are independent over time. Its personal experience is the posterior it would compute taking every signal at face value. With $z^S_{i,t},z^R_{i,t}$ the numbers of $S$ and $R$ signals among $s_{i,1},\dots,s_{i,t}$,

$$\mathrm{BU}_i(S\mid h_{i,t})=\frac{p_i^{z^S_{i,t}}(1-p_i)^{z^R_{i,t}}q}{p_i^{z^S_{i,t}}(1-p_i)^{z^R_{i,t}}q+p_i^{z^R_{i,t}}(1-p_i)^{z^S_{i,t}}(1-q)},$$

and $\mathrm{BU}_i(R\mid h_{i,t})=1-\mathrm{BU}_i(S\mid h_{i,t})$.

A set $B$ of agents is Bayesian. A Bayesian agent knows $y$ and always believes it. Each DeGroot agent $i\notin B$ has weights $\theta_i\ge0$ and $\alpha_{ij}\ge0$ with $\theta_i+\sum_j\alpha_{ij}=1$. For a state $y'$, its belief $\pi_{i,t}(y'\mid y)$ follows the DeGroot update

$$\pi_{i,t+1}=\theta_i\,\mathrm{BU}_i(y'\mid h_{i,t+1})+\sum_{j=1}^n\alpha_{ij}\,\pi_{j,t}.$$

The influence matrix $\mathbf W$ has zero rows for Bayesian agents and row $(\alpha_{ij})_j$ for DeGroot agents. The vector $\boldsymbol\theta=(\mathbf 1_B,\theta_{m+1},\dots,\theta_n)$ has entry $1$ on Bayesians. The unweighted graph $G^*$ has a link $i\to j$ when $i$ listens to $j$; for a DeGroot agent this means $\alpha_{ij}>0$.

Assumption 1 (pp. 10–11):

• (i) $p_i<(\lambda^*+\lambda)/(2\lambda)$ for every agent;
• (ii) $G^*$ is strongly connected;
• (iii) a DeGroot agent has $\theta_i>0$ exactly when $p_i>1/2$;
• (iv) some agent has $p_i>1/2$.

Formalization targets

Goal: Theorem 2 (p. 11)

Under Assumption 1, for every principal action $\mathbf x^*$, each DeGroot agent's personal experience converges almost surely to a constant $\mathrm{BU}_i(h_{i,\infty}(\mathbf x^*))(y'\mid y)$, and

$$\boldsymbol\pi_t(y'\mid y)\xrightarrow{\text{a.s.}}(\mathbf I-\mathbf W)^{-1}\big(\mathrm{BU}(\mathbf h_\infty(\mathbf x^*))(y'\mid y)\odot\boldsymbol\theta\big),$$

where the Bayesian entries of the vector $\mathrm{BU}(\mathbf h_\infty(\mathbf x^*))$ are the correct belief. The goal does not fix the constants: the paper computes them only later (display (2), p. 12).

Milestones

1. Lemma 3 (p. 45): the spectral radius of $\mathbf W$ is strictly less than $1$.
2. Proof of Theorem 2 (p. 47): $\mathbf I-\mathbf W$ and its DeGroot block $\mathbf I-\mathbf A_{DD}$ are invertible.
3. §3.2 (p. 11): $\mathrm{BU}_i(h_{i,t})$ converges almost surely to a constant.
4. Proof of Theorem 2 (p. 47): if $\mathbf u_t\to\mathbf u_\infty$ and $\boldsymbol\pi_{t+1}=\mathbf u_{t+1}+\mathbf W\boldsymbol\pi_t$, then $\boldsymbol\pi_t\to\boldsymbol\pi_\infty=(\mathbf I-\mathbf W)^{-1}\mathbf u_\infty$, the solution of $\boldsymbol\pi_\infty=\mathbf u_\infty+\mathbf W\boldsymbol\pi_\infty$.

Significance

Theorem 2 reduces the paper's manipulation question to linear algebra. A DeGroot agent ends up believing the wrong state exactly when the corresponding entry of $(\mathbf I-\mathbf W)^{-1}(\mathrm{BU}_\infty\odot\boldsymbol\theta)$ crosses a threshold. The principal's targeting problem then becomes a combinatorial problem over $\mathbf x^*$ in which the network enters only through $(\mathbf I-\mathbf W)^{-1}$. The paper's DeGroot centrality (Proposition 2) and its results on dense and sparse networks all start from this formula.

On formalization: the paper proves Theorem 2, but no machine-checked version exists. The mission's statements also record two places where the written argument needs repair. The text attributes the almost-sure convergence of $\mathrm{BU}_i$ to the martingale convergence theorem, but $\mathrm{BU}_i$ is a face-value posterior and not a martingale under the corrupted signal law. The proof's step from small increments of $\boldsymbol\pi_t$ to convergence of $\boldsymbol\pi_t$ is also not valid as written. Both claims are true under Assumption 1, and a complete development supplies correct arguments. The supporting results — spectral radius below one for a substochastic matrix with leakage reachable from every row, and convergence of linear recursions with convergent input — are reusable beyond this paper.

Difficulty

Two steps resist the obvious arguments.

First, $\mathrm{BU}_i(S\mid h_{i,t})$ is a function of the drift $z^S_{i,t}-z^R_{i,t}$ of a random walk. Its limit exists only if the walk is transient or $p_i=1/2$. For a targeted agent the walk's step law mixes the principal's message with organic news. For one boundary value of $p_i$ the step has mean zero, the walk is recurrent and $\mathrm{BU}_i$ oscillates forever. Assumption 1(i) excludes exactly that value. A proof must use it; a martingale argument does not apply.

Second, $\mathbf W$ is substochastic but not strictly so: a DeGroot row sums to $1-\theta_i$, which equals $1$ whenever $p_i=1/2$. A row-sum bound alone gives $\rho(\mathbf W)\le1$, not $<1$. Strict inequality needs every DeGroot agent to reach, in the weighted graph, an agent that leaks weight — a Bayesian or a DeGroot agent with $\theta_i>0$. This uses the interaction of Assumption 1 (ii), (iii) and (iv), with Bayesian agents' outgoing links playing no role in $\mathbf W$.

Formalization scope

Agents are Fin n and the Bayesian set is a Finset. Time is discrete, and the history at time $t$ is the signals at times $1,\dots,t$. The state space is a two-element inductive type. The signals are random variables on a probability space $(\Omega,P)$. Each agent's sequence is independent over time with the law above; signals of different agents may be dependent. This is deliberate: in the paper all targeted agents receive the same principal stream, so cross-agent independence would exclude the paper's own model. The principal's action is pure ($\mathbf x^*\in\{0,1\}^n$), as §3.2 allows without loss of generality. The DeGroot initial belief can be any value in $[0,1]$, and the conclusion holds for every such initial belief on one almost-sure event. "Spectral radius" is Mathlib's spectralRadius ℂ of the complexified matrix. $(\mathbf I-\mathbf W)^{-1}$ is Mathlib's matrix inverse; no invertibility hypothesis is added, because Assumption 1 implies it. In the graph $G^*$, a DeGroot agent's links are exactly its positive weights; Bayesian agents' links are free.

The personal experience is the explicit face-value posterior of the given signal process, and the conclusion of the goal includes its almost-sure convergence to the constants used in the limit. The goal therefore cannot be met by an abstract learning rule or a free limit vector.

A complete development needs:

• the strong law of large numbers (available in Mathlib) applied to the signal counts;
• a Perron–Frobenius-type spectral bound for substochastic matrices on a strongly connected graph;
• convergence of $\boldsymbol\pi_{t+1}=\mathbf u_{t+1}+\mathbf W\boldsymbol\pi_t$ when $\rho(\mathbf W)<1$.

Contributions of any of these, as standalone lemmas, are welcome.

Selected references

• M. Mostagir, A. Ozdaglar, J. Siderius, When Is Society Susceptible to Manipulation?, SSRN preprint 3474643 (version of 2020-06-08); Management Science 68(10), 2022. https://ssrn.com/abstract=3474643, https://doi.org/10.1287/mnsc.2021.4265
• M. H. DeGroot, Reaching a Consensus, Journal of the American Statistical Association 69(345), 1974. https://doi.org/10.1080/01621459.1974.10480137
• A. Jadbabaie, P. Molavi, A. Sandroni, A. Tahbaz-Salehi, Non-Bayesian Social Learning, Games and Economic Behavior 76(1), 2012. https://doi.org/10.1016/j.geb.2012.06.001
• D. Acemoglu, G. Como, F. Fagnani, A. Ozdaglar, Opinion Fluctuations and Disagreement in Social Networks, Mathematics of Operations Research 38(1), 2013. https://doi.org/10.1287/moor.1120.0570

Motivation

Spectral clustering recovers group labels from a similarity matrix: compute its leading eigenvectors, embed each point as a row of the eigenvector matrix, and cluster the rows with k-means. It is a standard last step of convex-relaxation methods for clustering, which first estimate a clustering matrix $X$ (with $X_{ij} = 1$ when $i$ and $j$ belong to the same cluster) and then have to turn the estimate back into labels.

Srivastava, Sarkar and Hanasusanto (arXiv:1912.07546v3; Operations Research 71(1), 2023) estimate $X$ by a linear program on a thresholded Gaussian kernel and then round it this way (Algorithm 1, steps 3–4). Their Theorem 2 controls the error of the rounding step in terms of the $\ell_1$ error of the estimate. The argument follows Lei and Rinaldo (Ann. Statist. 43(1), 2015), who analysed spectral clustering for stochastic block models with a polynomial-time $(1+\epsilon)$-approximate k-means step, combined with the Davis–Kahan theorem in the form of Yu, Wang and Samworth (Biometrika 102(2), 2015). The same pattern, "matrix estimation error ⇒ eigenvector error ⇒ misclassification count", recurs throughout the analysis of SDP and spectral methods for community detection and mixture models.

Setting

There are $n$ points and $r$ clusters. A fixed labelling $\varphi : [n] \to [r]$ gives clusters $C_k = \{i : \varphi(i) = k\}$ of sizes $n_k \ge 1$, and $n_{\min} = \min_k n_k$. The true clustering matrix is $X^0_{ij} = 1$ if $\varphi(i) = \varphi(j)$ and $0$ otherwise. Its scaled membership matrix is

$$U^0 = Z^0\,\mathrm{Diag}(1/\sqrt{n_1},\dots,1/\sqrt{n_r}),\qquad U^0_{ik} = \begin{cases} 1/\sqrt{n_k} & \varphi(i) = k,\\ 0 & \text{otherwise.}\end{cases}$$

The estimate $\hat X \in \mathbb R^{n\times n}$ is any symmetric matrix with entries in $[0,1]$. Spectral rounding takes a matrix $\hat U \in \mathbb R^{n\times r}$ of orthonormal eigenvectors of $\hat X$ for its $r$ largest eigenvalues (ties broken arbitrarily), and runs k-means on the rows of $\hat U$. A membership matrix $\Theta \in \mathbb M_{n,r}$ is a $\{0,1\}$-matrix with exactly one $1$ per row; a pair $(\hat\Theta, \hat B)$ with $\hat B \in \mathbb R^{r\times r}$ is a $(1+\epsilon)$-approximate k-means solution on the rows of $\hat U$ if

$$\|\hat U - \hat\Theta\hat B\|_F^2 \le (1+\epsilon)\min_{\Theta\in\mathbb M_{n,r},\, B\in\mathbb R^{r\times r}}\|\hat U - \Theta B\|_F^2 .$$

Let $O$ be an optimal rotation, an orthogonal $r\times r$ matrix minimising $\|\hat U - U^0O\|_F$. With $v_i$ and $\bar v_i$ the rows of $U^0O$ and $\hat\Theta\hat B$, the misclassified set of cluster $k$ is

$$\mathcal S_k = \Big\{ i \in C_k : \|\bar v_i - v_i\| \ge \tfrac{1}{2\sqrt{n_k}} \Big\}.$$

Norms: $\|A\|_1 = \sum_{i,j}|A_{ij}|$ (entrywise), $\|A\|_F^2 = \sum_{i,j}A_{ij}^2$.

Formalization targets

Goal: Theorem 2, (15), without outliers

For every $\hat X$, $\hat U$, $(\hat\Theta,\hat B)$ and optimal $O$ as above and every $\epsilon > 0$,

$$\sum_{k\in[r]}\frac{|\mathcal S_k|}{n_k} \;\le\; 64(2+\epsilon)\,\frac{\|X^0 - \hat X\|_1}{n_{\min}^2}.$$

Milestones

1. Davis–Kahan (Theorem 3, case $s=1$): an eigengap $g$ of a symmetric $\Sigma$ below its top $r$ eigenvalues gives an orthogonal $\hat O$ with $\|U - \hat U\hat O\|_F \le 2^{3/2}\|\hat\Sigma - \Sigma\|_F/g$.
2. Eigenstructure of $X^0$: $U^0$ consists of top-$r$ eigenvectors of $X^0$ with eigenvalues $n_1,\dots,n_r$, and $X^0$ vanishes on the orthogonal complement, so the eigengap is $n_{\min}$.
3. (G.6)(iii): $\|A - B\|_F^2 \le \|A - B\|_1$ for matrices with entries in $[0,1]$.
4. (G.6): $\|\hat U - U^0 O\|_F^2 \le 8\|\hat X - X^0\|_1/n_{\min}^2$.
5. Lemma 5, (G.4) (Lei–Rinaldo): for $V = \Theta^*B^*$ and a $(1+\epsilon)$-approximate k-means solution on any $\hat V$, $\sum_k |\mathcal S_k|\delta_k^2 \le 4(4+2\epsilon)\|V - \hat V\|_F^2$.
6. Centre separation: the rows of $B^* = \mathrm{Diag}(1/\sqrt{n_k})O$ satisfy $\|b^*_l - b^*_k\| = \sqrt{1/n_k + 1/n_l}$.

Companion: permutation recovery

If $64(2+\epsilon)\|X^0 - \hat X\|_1/n_{\min}^2 \le 1$, the k-means labels agree with $\varphi$ up to one permutation of $[r]$ on every point outside $\bigcup_k\mathcal S_k$.

Significance

Inequality (15) separates the analysis of the algorithm into an estimation part (how close $\hat X$ is to $X^0$ in $\ell_1$, Theorem 1 of the paper) and a purely deterministic rounding part. Any estimator of the clustering matrix with entries in $[0,1]$ — the Robust-LP, the SDP relaxations of Peng–Wei or Amini–Levina, a thresholded kernel — inherits a misclassification bound from its $\ell_1$ error through this one statement, with an explicit constant. The companion statement shows that the sets $\mathcal S_k$ really are the misclassified points.

The result is proved on paper; none of it is formalized. Mathlib has the spectral theorem for Hermitian matrices but no eigenspace perturbation bound of Davis–Kahan type, and the platform has no k-means approximation lemma for membership matrices. A machine-checked Davis–Kahan theorem in Frobenius norm and a machine-checked Lei–Rinaldo lemma are reusable well beyond this paper: they are the two standard ingredients of every spectral clustering guarantee for block models and mixtures.

Difficulty

The k-means part is elementary but bookkeeping-heavy: the comparison point in the $(1+\epsilon)$ bound must be a feasible k-means solution, which is why the true embedding $U^0O$ has to factor as a membership matrix times a centre matrix. The main obstacle is the Davis–Kahan step. The naive route through individual eigenvectors fails when eigenvalues of $\hat X$ or of $X^0$ are repeated (here $X^0$ has eigenvalue $n_k$ with multiplicity whenever cluster sizes coincide), and only the subspace is stable; the bound must be stated up to an orthogonal matrix and proved for the whole eigenspace, with no ordering or separation assumption on the eigenvalues of $\hat X$.

Formalization scope

Points are Fin n, clusters Fin r, matrices Matrix ι κ ℝ; the norms are explicit sums, not Mathlib's matrix norm instances. The labelling $\varphi$ is fixed; membership matrices are encoded by assignments $a : [n]\to[r]$, and "$\le (1+\epsilon)\min$" by "$\le (1+\epsilon)\cdot$ the cost of every assignment and every centre matrix". "Top-$r$ eigenvectors" is variational: orthonormal columns, eigenvector equations, and every Rayleigh quotient on the orthogonal complement at most each selected eigenvalue. $n_{\min}$ is a finite minimum and requires $r \ge 1$.

Departures from the printed text, each disclosed in the item concerned:

• No outliers ($m = 0$). The printed Theorem 2 allows outliers; it is false for $m \ge 1$, because the outlier rows of $U^0$ are zero, so the true embedding is not k-means feasible and Lemma 5 does not apply. A counterexample with two clusters of size $M > 256$, one isolated outlier and $\epsilon = 2$ violates (15).
• No probability, no $\bar\epsilon$, no separation condition. (15) is deterministic in $\|X^0 - \hat X\|_1$; the printed probabilistic hypotheses only feed Theorem 1 into the permutation claim.
• The printed $n_{\min} > r$ is replaced by the weaker $n_k \ge 1$.
• Davis–Kahan is stated for the leading eigenspace ($s = 1$), the only case used.
• In Lemma 5 the thresholds are required to satisfy $\delta_k \ge 0$, which the page leaves implicit; for a negative $\delta_k$ the bound (G.4) fails at $\hat V = V$.

The goal quantifies over every optimal rotation $O$, not over some orthogonal matrix chosen afterwards (which could make $\mathcal S_k$ empty), and over every top-eigenvector matrix and every approximate k-means solution; a formalization that fixes $\hat U$ to good eigenvectors, compares only against the true labels, or drops the eigenvalue-dominance clause (allowing bottom eigenvectors) proves a different and partly false statement.

Contributions welcome: Davis–Kahan in Frobenius norm for symmetric real matrices (general $s$ included), the Lei–Rinaldo lemma in full, and the eigenstructure of block-constant matrices.

Selected references

• P. R. Srivastava, P. Sarkar, G. A. Hanasusanto, A Robust Spectral Clustering Algorithm for Sub-Gaussian Mixture Models with Outliers, arXiv:1912.07546v3, 2021; Operations Research 71(1), 2023. https://arxiv.org/abs/1912.07546
• J. Lei, A. Rinaldo, Consistency of spectral clustering in stochastic block models, Annals of Statistics 43(1), 215–237, 2015. https://doi.org/10.1214/14-AOS1274
• Y. Yu, T. Wang, R. J. Samworth, A useful variant of the Davis–Kahan theorem for statisticians, Biometrika 102(2), 315–323, 2015. https://doi.org/10.1093/biomet/asv008
• C. Davis, W. M. Kahan, The rotation of eigenvectors by a perturbation. III, SIAM Journal on Numerical Analysis 7(1), 1–46, 1970. https://doi.org/10.1137/0707001

Why this formulation matters

Clustering separates observations into groups whose members resemble one another. In kernel clustering, a matrix $K$ records a similarity score for each pair of observations, and an assignment seeks groups with high total within-group similarity. Real data can also contain outliers, observations that should not be assigned to any cluster. Srivastava, Sarkar, and Hanasusanto use a binary assignment program that permits those unassigned observations and then express the same exact problem through a matrix of pairwise co-memberships. The relationship is stated as Proposition 1 of their preprint. It is the algebraic starting point for the tractable relaxations introduced immediately after the proposition in §3.

The two exact programs have different variables. The assignment program describes each observation's cluster directly. The lifted program records whether each pair belongs to the same cluster. The latter representation makes positive semidefiniteness and rank explicit, and it is the one the paper relaxes to obtain its semidefinite program. A precise equivalence matters because a relaxation of the wrong feasible set would no longer be a relaxation of the stated assignment problem.

The two finite matrix programs

Let $N$ be the number of observations and $r$ the number of available clusters. A binary assignment matrix $Z\in\{0,1\}^{N\times r}$ has one row per observation and one column per cluster. In formulation (3), each row sums to at most one. A row with one nonzero entry assigns its observation to that cluster; a zero row leaves the observation unassigned. Thus the same matrix represents both inliers and outliers. Cluster sizes need not be equal, and unused cluster columns are allowed.

The clustering matrix $X=ZZ^\top$ has one row and column per observation. Its entry $X_{ij}$ is one when observations $i$ and $j$ share a cluster and zero otherwise, including when either observation has a zero assignment row. Formulation (4) asks instead for an $N\times N$ matrix $X$ whose entries lie in $\{0,1\}$, that is positive semidefinite, and whose rank is at most $r$. The rank bound limits the number of distinct nonzero cluster directions. Positive semidefiniteness is a property of the full real matrix, including its symmetry; it is not merely a condition on its diagonal.

Let $K\in\mathbb R^{N\times N}$ be the similarity matrix, $\gamma\in\mathbb R$ a penalty parameter, and $E_N$ the all-ones $N\times N$ matrix. The entrywise Frobenius inner product is $\langle A,B\rangle=\sum_{i,j}A_{ij}B_{ij}$. The programs maximize, respectively, $\langle K-\gamma E_N,ZZ^\top\rangle$ over feasible $Z$ and $\langle K-\gamma E_N,X\rangle$ over feasible $X$. Both have a feasible zero matrix, even at the boundary values $N=0$ and $r=0$.

Formalization targets

The goal is Proposition 1, stated with its factor and rotation. If $X^*$ is an optimal matrix for (4), there must exist $G\in\mathbb R^{N\times r}$ and an orthogonal $O\in\mathbb R^{r\times r}$ such that $Z^*=GO$ is feasible and optimal for (3), with

$$X^*=GG^\top,\qquad \langle K-\gamma E_N,Z^*Z^{*\top}\rangle =\langle K-\gamma E_N,X^*\rangle.$$

Here “feasible and optimal” includes the zero-one entry condition, the row-sum bound, and comparison with every feasible assignment matrix. The objective identity alone would say little: once the Gram factorization and orthogonality hold, it follows algebraically. The substantive result is the existence of an assignment-compatible rotation of a factor of every lifted optimum.

The milestone list follows the five claims in Appendix B of the preprint: lifting a feasible assignment to a feasible $X$ without changing its value; factoring a rank-bounded positive semidefinite $X$ through $r$ columns; classifying factor rows as zero or unit vectors; showing that distinct nonzero rows are orthogonal; and rotating those rows into assignment coordinates. These statements address both directions of the feasible-set correspondence used by Proposition 1.

What the result supplies

The proposition says that the matrix constraints in (4) describe the same exact clustering choices as the assignment constraints in (3), up to a choice of orthogonal coordinates for the factor. A lifted optimum therefore represents an assignment optimum rather than merely a matrix with the same numerical objective. Conversely, an assignment can always be lifted to a matrix accepted by (4). The paper can then drop the binary or rank constraints to obtain relaxations while keeping a clear exact program as their reference point; see §3 of the preprint.

The proposition is proved in the source paper. This mission seeks a machine-checked proof of that known claim and reusable finite-matrix results about binary positive semidefinite Gram matrices. In particular, the factorization and row-structure milestones can be used beyond spectral clustering whenever a zero-one Gram matrix appears with a rank bound. The Lean declarations here are proposed statements; their sorry proofs remain for solvers to complete.

Where the difficulty lies

The forward implication is immediate once a valid assignment matrix is given: its Gram matrix is positive semidefinite and has rank at most the number of cluster columns. The reverse implication carries the mathematical work. Positive semidefiniteness and low rank alone produce a real factor, but the factor need not have zero-one entries. A generic factor rotation also need not yield one-hot rows. The zero-one condition on every Gram entry is what constrains the relative positions of the nonzero rows strongly enough to recover assignment directions. The result must work when several observations share a direction, when some rows vanish, and when fewer than $r$ clusters are occupied.

Formalization scope

The formalization uses Mathlib matrices indexed by Fin N and Fin r over $\mathbb R$. Feasibility of (3) is entrywise membership in $\{0,1\}$ together with row sums at most one. Feasibility of (4) is entrywise membership in $\{0,1\}$, Matrix.PosSemidef, and Matrix.rank ≤ r. The objectives use the explicit sum of entrywise products, so no operator norm or alternate matrix inner product enters the statement. Global optimality is defined by comparison against the corresponding whole feasible set. The factor $G$ has exactly $r$ columns, and the rotation belongs to the real orthogonal group of dimension $r$.

The paper obtains $K$ from a Gaussian kernel and takes $\gamma\in(0,1)$ for the clustering application. Proposition 1 and Appendix B use only the displayed algebraic programs, so the formal statement permits arbitrary real $K$ and $\gamma$. No probability model, symmetry assumption on $K$, positive dimension assumption, or nonempty-cluster condition is needed. The boundary cases $N=0$ and $r=0$ retain their literal meanings. The formalization cannot assume that a feasible $X$ is already block diagonal or is already a Gram matrix of a binary assignment; that is the conclusion being established.

Useful contributions include proofs of the five Appendix B milestones, a finite-dimensional factorization theorem with the prescribed number of columns, and the rotation theorem that handles repeated or zero rows. These pieces should share the stated definitions so that the eventual proof of Proposition 1 uses precisely formulations (3) and (4).

Selected references

• P. R. Srivastava, P. Sarkar, and G. A. Hanasusanto, A Robust Spectral Clustering Algorithm for Sub-Gaussian Mixture Models with Outliers, Operations Research 71(1), 2023; arXiv:1912.07546v3, §3, Proposition 1 and Appendix B.

Motivation

The Hubble constant $H_0$ is the present expansion rate of the Universe. Its value measured locally with distance-ladder methods disagrees with the value inferred from the early Universe under the standard $\Lambda$CDM model (the Hubble tension). The H0DN Collaboration (A&A 708, A166, 2026) combined geometric distances, Cepheids, the tip of the red giant branch, Miras, carbon stars, Type Ia and Type II supernovae, surface brightness fluctuations, the fundamental plane, Tully–Fisher relations and megamasers into a single Local Distance Network, reporting the baseline value $H_0=73.50\pm0.81\ \mathrm{km\,s^{-1}\,Mpc^{-1}}$.

That number comes from one statistical step. All equations of the network are linear (or linearized) in the parameters, the measurement errors are correlated, and the parameters are obtained by generalized least squares with a non-diagonal covariance matrix (Appendix B of the paper). The paper relies on three mathematical facts: the covariance-weighted solution is the Best Linear Unbiased Estimator (Aitken 1935); weighting by the inverse covariance gives the lowest variance among weighted least-squares solutions; and replacing the inverse of a singular covariance matrix by its Moore–Penrose inverse (Penrose 1956) is "completely equivalent to analytically making sure that only linearly independent equations are used". This mission formalizes exactly those facts.

Timeline of the mathematics used:

• Gauss (1820s): least squares gives minimum-variance linear unbiased estimates for uncorrelated errors of equal variance.
• Aitken (1935): extension to correlated errors with a known covariance matrix, i.e. generalized least squares.
• Penrose (1955–1956): the generalized inverse characterized by the four Penrose equations, and its use for best approximate solutions of linear equations.

Setting

The data vector $Y\in\mathbb R^{m}$ has one entry per equation of the network (host-distance, host-group, calibrator and Hubble-flow equations; $m=255$ in the baseline). The parameter vector $X\in\mathbb R^{n}$ collects host distance moduli, group distance moduli, reference absolute magnitudes and $\log_{10}H_0$. The coefficient matrix $A\in\mathbb R^{m\times n}$ gives the theory prediction $AX$, and the data have covariance matrix $C\in\mathbb R^{m\times m}$.

For a symmetric positive-definite weight matrix $W$ the quadratic form of Eq. (B.2) is

$$Q(X)=(Y-AX)^{\mathsf T}W(Y-AX),$$

and $W=C^{-1}$ gives the $\chi^2$ of Eq. (B.1). When $A$ has full column rank, the GLS estimator matrix is $L_W=(A^{\mathsf T}WA)^{-1}A^{\mathsf T}W$ and the GLS estimate is $\hat X_W=L_WY$. A linear estimator $LY$ has covariance $LCL^{\mathsf T}$. A matrix $P$ is a Moore–Penrose inverse of $M$ if $MPM=M$, $PMP=P$, and $MP$ and $PM$ are symmetric.

In the network the $m$ equations are built from only $k$ distinct measurements ($k=183$ in the baseline): $Y=BZ$ with $Z\in\mathbb R^{k}$ the vector of distinct measurements, of positive-definite covariance $S$, and $B$ of full column rank. Then $C=BSB^{\mathsf T}$ is singular whenever $m>k$.

Formalization targets

Goal: the $\chi^2$ solution is BLUE

For $Y=AX_0+\varepsilon$ with $\mathbb E\varepsilon=0$, $\operatorname{Cov}(\varepsilon)=C\succ0$ and $A$ of full column rank, the estimate $\hat X=L_{C^{-1}}Y$ is unbiased, and for every $L$ such that $LY$ is unbiased for every true parameter, and every $v\in\mathbb R^n$,

$$\operatorname{Var}(v^{\mathsf T}\hat X)\le\operatorname{Var}(v^{\mathsf T}LY).$$

Milestones

1. Eq. (B.2): $\hat X_W$ minimizes $Q$.
2. Unbiasedness: $L_WA=I$.
3. Parameter covariance: $L_{C^{-1}}CL_{C^{-1}}^{\mathsf T}=(A^{\mathsf T}C^{-1}A)^{-1}$.
4. Variance propagation: $\operatorname{Var}(v^{\mathsf T}LY)=v^{\mathsf T}LCL^{\mathsf T}v$.
5. Aitken, matrix form: $LA=I\Rightarrow LCL^{\mathsf T}-(A^{\mathsf T}C^{-1}A)^{-1}\succeq0$.
6. Optimal weight: $L_WCL_W^{\mathsf T}-L_{C^{-1}}CL_{C^{-1}}^{\mathsf T}\succeq0$ for every $W\succ0$.
7. Penrose: the Moore–Penrose inverse exists and is unique.
8. Appendix B.2: if $Y=BZ$, $C=BSB^{\mathsf T}$, $A=BA_0$ and $P$ is a Moore–Penrose inverse of $C$, then $(Y-AX)^{\mathsf T}P(Y-AX)=(Z-A_0X)^{\mathsf T}S^{-1}(Z-A_0X)$ for all $X$, and the two GLS estimates coincide.

Numerical claims of the paper

With the tension $T(x,\sigma_x;y,\sigma_y)=|x-y|/\sqrt{\sigma_x^2+\sigma_y^2}$ between independent measurements:

9. Abstract (2): relative uncertainties $0.809/73.499$ and $0.697/73.994$ (Table 4, V00 and V99) round to $1.1\%$ and $0.9\%$.
10. Abstract (6): $T(73.50,0.81;\,67.24,0.35)$ rounds to $7.1$.
11. Abstract (6): $T(73.50,0.81;\,68.51,0.58)$ rounds to $5.0$.
12. Sect. 5.2.4: $T(73.994,0.697;\,67.24,0.35)$ and $T(73.656,0.713;\,67.24,0.35)$ (Table 4, V99 and V99A) round to $8.7$ and $8.1$.

Significance

The result itself. These statements are what makes the reported $H_0$ and its error bar meaningful as statistical quantities: the estimate is unbiased, its reported uncertainty is the covariance $(A^{\mathsf T}C^{-1}A)^{-1}$, no other linear unbiased combination of the same data is more precise, and the pseudoinverse shortcut used in the public code neither adds nor removes information compared with an explicit reduction to independent equations. The same facts underlie every covariance-weighted combination of correlated measurements.

Formalizing it. All of these results are classical and proved in the statistics literature. This mission adds machine-checked versions stated in the form used by the paper, including the pseudoinverse equivalence of Appendix B.2, which the paper states without proof. The astrophysical inputs (data selection, linearization, the numerical value of $H_0$) are outside the scope of formal proof.

Difficulty

Each statement is classical, but the formal versions are not one-liners. The goal connects measure-theoretic expectation, variance and covariance with matrix algebra: variances of linear combinations of square-integrable random variables must be expanded through bilinearity of covariance before a Loewner-order inequality applies. The pseudoinverse equivalence fails without the full-column-rank hypothesis on $B$, and has to handle a singular $C$ for which $C^{-1}$ does not exist. Existence of the Moore–Penrose inverse needs a spectral or rank-factorization argument; it is not available as a ready-made matrix operation.

Formalization scope

Everything is over $\mathbb R$ with arbitrary finite index types. "Full column rank" is stated as injectivity of $X\mapsto AX$. Positive (semi)definiteness uses Mathlib's Matrix.PosDef / Matrix.PosSemidef, which include symmetry. Mathlib's matrix inverse returns $0$ on singular matrices; every statement that uses $(A^{\mathsf T}WA)^{-1}$ carries hypotheses under which that matrix is invertible. The Moore–Penrose inverse is a predicate (the four Penrose equations), and the uniqueness milestone makes it a well-defined object. The probabilistic goal assumes only mean zero, finite second moments and a given covariance matrix (no Gaussianity). Unbiasedness of the competing estimator is required for every value of the true parameter, which rules out estimators that are unbiased only at one parameter value.

The numerical items check only the arithmetic from the published central values and uncertainties to the quoted significances and percentages; "rounds to $a$" is stated as $a-0.05\le\cdot<a+0.05$ (or the corresponding percentage interval). They say nothing about whether the inputs are correct.

The shared definitions (quadratic form, GLS estimator, estimator covariance, Moore–Penrose predicate) can be reused for any weighted least-squares development. Contributions are welcome on all milestones, as well as on a reusable construction of the matrix pseudoinverse.

Selected references

• H0DN Collaboration (S. Casertano et al.), The Local Distance Network: A community consensus report on the measurement of the Hubble constant at ∼1% precision, A&A 708, A166, 2026. https://doi.org/10.1051/0004-6361/202557993
• A. C. Aitken, On least squares and linear combination of observations, Proc. Royal Soc. Edinburgh 55, 42, 1935 (as cited in Appendix B of the paper above).
• R. Penrose, On best approximate solutions of linear matrix equations, Math. Proc. Camb. Philos. Soc. 52, 17, 1956 (as cited in Appendix B.2 of the paper above).

Motivation

Kramers–Wannier duality was found in 1941 as a map between the high- and low-temperature phases of the two-dimensional Ising model (Kramers–Wannier 1941). In its quantum form it exchanges the transverse field $X_j$ and the nearest-neighbour coupling $Z_{j-1}Z_j$ of the transverse-field Ising chain, and it fixes the critical point. In conformal field theory it is implemented by a topological defect line (Fröhlich–Fuchs–Runkel–Schweigert 2004), the prototypical non-invertible symmetry: its fusion with itself is a sum of operators, not a single invertible one (Shao, TASI lectures 2023).

On a finite periodic chain the duality cannot be a unitary operator, because it maps the $\mathbb Z_2$-even sector to itself and annihilates the odd sector. Seiberg–Shao 2023 and Seiberg–Seifnashri–Shao 2024 wrote the exact lattice operator $\mathsf D$ on the tensor-product Hilbert space $(\mathbb C^2)^{\otimes L}$. They showed that its algebra closes only after the lattice translation is included: $\mathsf D^2=(1+\eta)T^{-1}$. This is a lattice relation that a fusion category does not describe, since the continuum fusion rule $\mathcal N^2=1+\eta$ appears only at low energy. The same identity drives the LSM-type constraint proved in that paper.

Timeline. 1941: Kramers and Wannier find the duality of the 2D Ising model. 2004: Fröhlich, Fuchs, Runkel and Schweigert realise it as a conformal defect. 2016: Aasen–Mong–Fendley construct the lattice defects. 2023–2024: Seiberg, Seifnashri and Shao find the exact operator algebra on the tensor-product Hilbert space, including the translation factor.

Setting

Fix $L\ge1$ qubits on a ring, with site indices in $\mathbb Z/L$ (Fin L with modular arithmetic). A computational-basis state is labelled by a configuration $s=(s_0,\dots,s_{L-1})\in(\mathbb Z/2)^L$ (Config L). Operators are complex $2^L\times2^L$ matrices indexed by configurations (Op L). Write $\operatorname{sgn}(a)=(-1)^a$.

• Pauli operators. $X_j|s\rangle=|s+e_j\rangle$ flips spin $j$ (pauliX), and $Z_j|s\rangle=(-1)^{s_j}|s\rangle$ (pauliZ).
• $\mathbb Z_2$ symmetry. $\eta=\prod_j X_j$ flips every spin (eta).
• Translation. $T|s\rangle=|s'\rangle$ with $s'_k=s_{k-1}$ (transl), so that $TX_jT^{-1}=X_{j+1}$.
• Kramers–Wannier operator (kwD):

$$\langle t|\,\mathsf D\,|s\rangle \;=\; 2^{-L/2}\,(-1)^{\sum_{k} t_k\,(s_k+s_{k+1})}.$$

This explicit formula is the definition used throughout. Relations (1.5) together with $\mathsf D\eta=\mathsf D$ determine $\mathsf D$ up to a scalar, and (1.4) fixes the scalar up to a sign. Every statement below is invariant under $\mathsf D\mapsto-\mathsf D$, so this is the operator of Seiberg–Seifnashri–Shao in that paper's normalisation (footnote 1). Its equality with their matrix-product presentation (2.64) is not formalised here.

Formalization targets

Goal: the non-invertible fusion rule (eqs. (1.4), (2.65), (F.18))

$$\mathsf D^2=(1+\eta)\,T^{-1}\qquad\text{for every }L\ge1 .$$

Milestones

1. Invertible algebra (eqs. (1.1)–(1.3), (2.10), (2.65)): $\eta^2=1$, $T\eta=\eta T$, $T^L=1$, $TX_jT^{-1}=X_{j+1}$, $TZ_jT^{-1}=Z_{j+1}$, $\eta X_j=X_j\eta$, $\eta Z_j=-Z_j\eta$.
2. Duality on $X$ (eq. (1.5)): $\mathsf D X_j=Z_{j-1}Z_j\,\mathsf D$.
3. Duality on $ZZ$ (eq. (1.5)): $\mathsf D Z_{j-1}Z_j=X_{j-1}\,\mathsf D$.
4. Absorbing $\eta$ (eqs. (1.4), (2.65)): $\mathsf D\eta=\eta\mathsf D=\mathsf D$.
5. Translation and adjoint (eq. (2.65), Table 1): $T\mathsf D=\mathsf DT$ and $\mathsf D^\dagger=\mathsf DT$.
6. Non-invertibility (§1.1): $\mathsf D$ is not a unit, and $\ker\mathsf D\neq0$.

Significance

The result. The goal identity is the defining relation of the lattice Kramers–Wannier symmetry. Together with milestones 4–5 it shows that $\mathsf D/\sqrt2$ restricted to the $\eta$-even sector squares to a translation, so $\mathsf D$ is a square root of $T^{-1}$ there. The paper uses this to derive its LSM-type constraint, and also to show that the lattice symmetry is not a fusion category, because the continuum rule $\mathcal N^2=1+\eta$ only emerges at low energy. Milestones 2–3 are the lattice Kramers–Wannier map on $\mathbb Z_2$-invariant operators, so $\mathsf D$ commutes with the critical Ising Hamiltonian $H=-\sum_j(Z_{j-1}Z_j+X_j)$.

Formalizing it. The identities are proved in the physics literature by tensor-network manipulations ((F.14)–(F.18)) and checked numerically, but none of this is machine-checked. This mission produces a reusable Lean setup for qubit chains: Pauli strings on $(\mathbb Z/2)^L$, $\mathbb Z_2$ and translation symmetries, and an exact non-invertible operator with its full operator algebra for every chain length. No mission on the platform or file in Mathlib currently formalizes a non-invertible lattice symmetry.

Difficulty

Each identity is easy to check for a fixed small $L$ by brute force. The content is that it holds for all $L$ at once, on a $2^L$-dimensional space. The difficulty is bookkeeping with periodic indices: sums over $(\mathbb Z/2)^L$ of characters $(-1)^{\langle t,\,\cdot\rangle}$, reindexing $k\mapsto k\pm1$ in Fin L (including $L=1$, where $k+1=k$, and $L=2$, where $k+1=k-1$), and the exact normalisation $2^{-L/2}$, so that the right-hand side carries no stray factor $2^L$. The goal also involves the matrix inverse $T^{-1}$, so a proof must establish that $T$ is invertible rather than rely on Lean's junk value.

Formalization scope

• Representation. Operators are Matrix (Fin L → ZMod 2) (Fin L → ZMod 2) ℂ; products are matrix products; $T^{-1}$ is Mathlib's matrix inverse (transl L)⁻¹; $\dagger$ is conjTranspose. Every theorem assumes [NeZero L], i.e. $L\ge1$.
• Conventions committed to. $Z_j=(-1)^{s_j}$ on basis states, translation to the right ($s'_k=s_{k-1}$), and $\mathsf D$ normalised by $2^{-L/2}$ as in eqs. (1.4)/(2.65). Other conventions (left translation, unnormalised $\mathsf D$) change the statements to $T$ instead of $T^{-1}$ or add a factor $2^L$; the conventions here reproduce the paper's equations verbatim.
• No trivialisation. kwD is an explicit formula, not a hypothesis. The goal fixes both sides completely, and milestone 1 pins the translation convention against eq. (2.10).
• Out of scope. The defect Hamiltonians, the MPO presentation (2.64) itself, the $\mathbb Z_2$- and duality-twisted operators of §§2.3.3–2.3.4, and the LSM constraint of §4.
• Reusable. Pauli operators, translation and $\eta$ on qubit chains; character-sum lemmas over $(\mathbb Z/2)^L$. Contributions of general Mathlib lemmas on Walsh–Hadamard-type sums are welcome.

Selected references

• H. A. Kramers, G. H. Wannier, Statistics of the Two-Dimensional Ferromagnet. Part I, Phys. Rev. 60, 252–262 (1941). doi:10.1103/PhysRev.60.252
• J. Fröhlich, J. Fuchs, I. Runkel, C. Schweigert, Kramers–Wannier duality from conformal defects, Phys. Rev. Lett. 93, 070601 (2004). arXiv:cond-mat/0404051
• D. Aasen, R. S. K. Mong, P. Fendley, Topological Defects on the Lattice I: The Ising model, J. Phys. A 49, 354001 (2016). arXiv:1601.07185
• N. Seiberg, S.-H. Shao, Majorana chain and Ising model – (non-invertible) translations, anomalies, and emanant symmetries, SciPost Phys. 16, 064 (2024). arXiv:2307.02534
• S.-H. Shao, What's Done Cannot Be Undone: TASI Lectures on Non-Invertible Symmetries (2023). arXiv:2308.00747
• Source: N. Seiberg, S. Seifnashri, S.-H. Shao, Non-invertible symmetries and LSM-type constraints on a tensor product Hilbert space, SciPost Phys. 16, 154 (2024). arXiv:2401.12281

Motivation

Dynamic stochastic general equilibrium (DSGE) models are the standard framework used by central banks and fiscal authorities for policy analysis and forecasting (Wikipedia overview). The models used for monetary-policy analysis are built from three interrelated blocks — demand, supply and a monetary-policy rule — that jointly determine output, inflation and the nominal interest rate. The canonical small-scale instance is the three-equation New Keynesian model (Woodford 2003; Galí 2008; Clarida, Galí and Gertler 1999).

A basic question about such a model is whether it pins down a unique equilibrium path at all. If many bounded paths solve the model, the model makes no definite prediction and expectations can become self-fulfilling. The answer for the three-equation model is the Taylor principle: the interest-rate rule must respond to inflation strongly enough.

Timeline. Blanchard and Kahn (1980) gave the eigenvalue-counting criterion for existence and uniqueness of bounded solutions of linear rational-expectations models. Kydland and Prescott (1982) started the real-business-cycle/DSGE programme. Rotemberg and Woodford (1997) introduced the New Keynesian DSGE framework. Bullard and Mitra (2002) derived the explicit determinacy condition $\kappa(\phi_\pi - 1) + (1-\beta)\phi_y > 0$ for the model with a contemporaneous Taylor rule, presented in textbook form by Galí (2008, Ch. 3).

Setting

Time is discrete, $t = 0, 1, 2, \dots$. All variables are deviations from the zero-inflation steady state: $y_t$ is the output gap, $\pi_t$ inflation, and $i_t$ the nominal interest rate. The parameters are $\sigma > 0$ (inverse elasticity of intertemporal substitution), $\beta \in (0,1)$ (discount factor), $\kappa > 0$ (slope of the Phillips curve), and the policy coefficients $\phi_\pi, \phi_y \ge 0$.

A triple of real sequences $(y, \pi, i)$ is an equilibrium if for every $t$

$$\begin{aligned} y_t &= y_{t+1} - \tfrac{1}{\sigma}(i_t - \pi_{t+1}) && \text{(demand: dynamic IS curve)}\\ \pi_t &= \beta \pi_{t+1} + \kappa y_t && \text{(supply: New Keynesian Phillips curve)}\\ i_t &= \phi_\pi \pi_t + \phi_y y_t && \text{(monetary policy: Taylor rule).} \end{aligned}$$

The demand equation is the log-linearised consumption Euler equation, which equates marginal utility of consumption today with discounted marginal utility tomorrow. The model is determinate if the zero path is its only equilibrium in which $y$, $\pi$ and $i$ all stay bounded.

Formalization targets

Goal: the Taylor principle

For $\sigma > 0$, $0 < \beta < 1$, $\kappa > 0$, $\phi_\pi, \phi_y \ge 0$:

$$\text{the model is determinate} \iff \kappa(\phi_\pi - 1) + (1 - \beta)\phi_y > 0 .$$

Milestones

1. Consumption Euler equation. At an interior optimum of the two-period consumption–saving problem, $u'(c_0) = \beta(1+r)u'(c_1)$.
2. State-space form. For $\sigma, \beta \ne 0$, the model is equivalent to $(y_{t+1}, \pi_{t+1})^\top = M(y_t, \pi_t)^\top$ together with the Taylor rule, for an explicit $2\times2$ matrix $M$.
3. Equilibria are parametrised by initial conditions. Each $(y_0, \pi_0)$ determines exactly one equilibrium.
4. Schur–Cohn test. For real $T$ and $D > 0$, both roots of $z^2 - Tz + D$ have modulus $> 1$ iff $D > 1$ and $|T| < 1 + D$.
5. Blanchard–Kahn lemma. For a real square matrix $M$, the only bounded solution of $x_{t+1} = Mx_t$ is zero iff every complex eigenvalue of $M$ has modulus $> 1$.

Significance

The result itself. The Taylor principle is the standard criterion for whether an interest-rate rule yields a well-defined equilibrium in New Keynesian models, and it is the first property checked when a policy rule is proposed. The determinacy region it describes is the starting point for the analysis of optimal policy and of learnability (Bullard and Mitra 2002).

Formalizing it. The result is classical and proved on paper. This mission formalizes the known argument. The mission produces a reusable Lean definition of the basic New Keynesian model, a general lemma on bounded orbits of linear recursions (which applies to any linear rational-expectations model with only forward-looking variables), and a formal Schur–Cohn criterion for real quadratics.

Difficulty

The economic content is elementary, but the obvious argument skips the hardest step. Textbook treatments state "determinacy holds iff both eigenvalues lie outside the unit circle" without proof, and the equivalence between "no nonzero bounded solution" and an eigenvalue condition has to be established for real sequences while the eigenvalues may be complex. In particular the converse direction needs a real bounded solution built from a complex eigenvector, and the boundary case of eigenvalues on the unit circle must come out on the non-determinate side. The parameter translation also has to handle complex-conjugate eigenvalues, not only real ones.

Formalization scope

• Sequences are functions $\mathbb N \to \mathbb R$; the model is the deterministic (shock-free) version, so there are no expectation operators. Stochastic shocks do not change the determinacy condition, but that extension is outside the scope of this mission.
• "Bounded" means a single real bound for all $t$; determinacy requires $y$, $\pi$ and $i$ to be bounded. Boundedness of $i$ follows from that of $y$ and $\pi$, so this adds no restriction.
• Division is Lean's total division; every statement that divides by $\sigma$ or $\beta$ assumes they are nonzero (or positive).
• Eigenvalues are complex roots of the characteristic polynomial of the complexified matrix.
• The goal is not trivial: the zero path is always an equilibrium, determinacy is a genuine uniqueness claim, and the parameter hypotheses are satisfiable (e.g. $\sigma = 1$, $\beta = 0.99$, $\kappa = 0.1$, $\phi_\pi = 1.5$, $\phi_y = 0.5$).
• All declarations live in the namespace DSGE. Contributions of general linear-recursion and polynomial-root lemmas are welcome.

Selected references

• Wikipedia, Dynamic stochastic general equilibrium. https://en.wikipedia.org/wiki/Dynamic_stochastic_general_equilibrium
• O. J. Blanchard and C. M. Kahn, The Solution of Linear Difference Models under Rational Expectations, Econometrica 48(5), 1980. https://doi.org/10.2307/1912186
• F. E. Kydland and E. C. Prescott, Time to Build and Aggregate Fluctuations, Econometrica 50(6), 1982. https://doi.org/10.2307/1913386
• R. Clarida, J. Galí and M. Gertler, The Science of Monetary Policy: A New Keynesian Perspective, Journal of Economic Literature 37(4), 1999. https://doi.org/10.1257/jel.37.4.1661
• J. Bullard and K. Mitra, Learning about Monetary Policy Rules, Journal of Monetary Economics 49(6), 2002. https://doi.org/10.1016/S0304-3932(02)00144-7
• M. Woodford, Interest and Prices: Foundations of a Theory of Monetary Policy, Princeton University Press, 2003.
• J. Galí, Monetary Policy, Inflation, and the Business Cycle, Princeton University Press, 2008 (Chapter 3).

Motivation

The spectral radius of a graph, the largest eigenvalue of its adjacency matrix, measures how densely and how unevenly the edges of the graph are distributed. Asking which graph in a class maximizes it is a spectral analogue of the extremal question "which graph in the class has the most edges". For planar graphs the question has a long history in spectral graph theory, going back at least to Schwenk and Wilson. It also arose in geography, where the spectral radius serves as a measure of the connectivity of planar networks. To compare real networks with a theoretical upper bound, geographers wanted the planar graph of maximum spectral radius (arXiv:1606.01916v2, p. 3).

Timeline, as recorded by Tait and Tobin (pp. 1–3):

• 1978, Schwenk and Wilson: early study of the eigenvalues of planar graphs.
• 1991, Boots and Royle, and independently 1993, Cao and Vince: conjecture that the planar graph on $n \ge 9$ vertices of maximum spectral radius is $P_2 + P_{n-2}$ (Conjecture 1 of the paper). The conjecture is false for $n \in \{7, 8\}$, so some lower bound on $n$ is necessary (p. 2).
• 1988–2000: successive improvements of the upper bound on the spectral radius of planar graphs, by Hong (1988, 1995, 1998), Cao and Vince (1993), Guiduli (1996) and Ellingham and Zha (2000). These bounds do not identify the extremal graph.
• 2010, Dvořák and Mohar: an upper bound on the spectral radius of planar graphs of given maximum degree.
• Guiduli and Hayes were reported by Ellingham and Zha to have proved the conjecture for large $n$. The preprint never appeared (p. 3).
• 2017, Tait and Tobin: proof of the conjecture for all sufficiently large $n$ (Theorem 15).

Setting

All graphs are finite and simple. A graph on $n$ vertices has vertex set $\{0, 1, \dots, n-1\}$. Its adjacency matrix $A(G)$ is the $n \times n$ real matrix with entry $1$ in position $(u, w)$ when $u \sim w$ and $0$ otherwise. Its eigenvalues are real, and the largest is the spectral radius $\lambda_1(G)$.

A graph is planar if it can be drawn in the plane with vertices as distinct points and edges as simple arcs joining their ends, such that an arc meets no vertex other than its ends and two arcs meet only at common ends.

For graphs $G$ and $H$ on disjoint vertex sets, the join $G + H$ is the graph on the union of the two vertex sets that keeps every edge of $G$ and of $H$ and adds every edge between a vertex of $G$ and a vertex of $H$. Write $K_2$ for a single edge, $P_m$ for the path on $m$ vertices, and $K_2 + P_{n-2}$ for their join: two adjacent vertices, both joined to every vertex of a path on the remaining $n - 2$ vertices. The paper also writes it $P_2 + P_{n-2}$.

A planar graph $G$ on $n$ vertices is a planar spectral maximizer if $\lambda_1(G') \le \lambda_1(G)$ for every planar graph $G'$ on the same $n$ vertices.

The milestones refer to a leading eigenvector $\mathbf v$ of a maximizer, scaled so that every entry is positive and the largest entry is $1$, and to a vertex $x$ with $\mathbf v_x = 1$. For a parameter $\varepsilon > 0$ they use the sets $L = \{z : \mathbf v_z > \varepsilon\}$ and $S = V(G) \setminus L$, the edge counts $e(X)$ (edges inside $X$) and $e(X, Y)$ (edges between $X$ and $Y$), and a second vertex $w$ with $\mathbf v_w > 1 - 24\varepsilon$ that is adjacent to all but $94\varepsilon n$ vertices of $S$.

Formalization targets

Goal: Theorem 15

$$\exists N_0\ \forall n \ge N_0\ \forall G \text{ on } n \text{ vertices}: \quad G \text{ is a planar spectral maximizer} \iff G \cong K_2 + P_{n-2}.$$

The threshold $N_0$ is not fixed. The paper proves the statement only for $n$ beyond an unspecified bound, and the conjecture's bound $n \ge 9$ remains open. The equivalence encodes "the unique maximizer is $K_2 + P_{n-2}$": every maximizer is isomorphic to it, and it is itself a maximizer.

Milestones, in the order of the proof

1. If $H$ is a proper spanning subgraph of a connected graph $G$, then $\lambda_1(H) < \lambda_1(G)$ (§1.2, already proved on the platform).
2. A planar graph on $n \ge 3$ vertices has no $K_{3,3}$ subgraph and at most $3n - 6$ edges, and each of its bipartite subgraphs has at most $2n - 4$ edges (p. 8).
3. Lemma 8: $\sqrt{2n-4} < \lambda_1 < \sqrt{6n}$.
4. The counts $|L| \le 3\sqrt{2n-4}/\varepsilon$, $e(S, L) \le 2n - 4$, $e(S) \le 3n - 6$, $e(L) \le 9\sqrt{2n-4}/\varepsilon$ (p. 8).
5. Lemma 9: $\sum_{z \in L} \mathbf v_z \le \varepsilon\sqrt{2n-4} + 18/\varepsilon$ and $\sum_{z \in S} \mathbf v_z \le (1 + 3\varepsilon)\sqrt{2n-4}$.
6. Eq. (7): $\sum_{y \sim u,\, y \in S} \mathbf v_y \ge (\mathbf v_u - \varepsilon)\sqrt{2n-4} - 18/\varepsilon$ for $u \in L$.
7. Lemma 10: $\mathbf v_z > 1/\sqrt{6n}$ for every vertex $z$.
8. $|\{y \in S : y \not\sim x\}| \le 14\varepsilon n$ (p. 10).
9. Lemma 11: a vertex $w \in L$, $w \ne x$, with $\mathbf v_w > 1 - 24\varepsilon$ and $|\{y \in S : y \not\sim w\}| \le 94\varepsilon n$.
10. Lemma 12: $\mathbf v_u < 1/10$ for every $u \notin \{x, w\}$.
11. Lemma 13: $x \sim w$.
12. Lemma 14: every vertex other than $x$ and $w$ is adjacent to both.
13. A planar graph with two distinct vertices adjacent to all other vertices is a spanning subgraph of $K_2 + P_{n-2}$ (proof of Theorem 15, p. 13).

Significance

The result. Theorem 15 settles the Boots–Royle / Cao–Vince conjecture for all large $n$. It identifies the planar graph of maximum spectral radius exactly, so the theoretical upper bound that the geographic application asks for is $\lambda_1(K_2 + P_{n-2})$. Along the way, Lemmas 8–14 describe the eigenvector of the extremal graph: two vertices carry almost all of the eigenvector weight, and every other entry is below $1/10$. The same method proves the outerplanar analogue (Theorem 7, the companion mission of this series).

Formalizing it. The theorem is proved on paper and has no machine-checked proof. Formalizing it needs several pieces that are absent from Mathlib or the platform and are reusable: the edge bound $3n - 6$ and the bipartite bound $2n - 4$ for topologically planar graphs, the non-planarity of $K_{3,3}$ and $K_5$ and of their subdivisions, Rayleigh-quotient comparison of spectral radii, and the face structure of maximal planar graphs. Each milestone is a self-contained target.

Difficulty

Counting edges does not separate the candidates. A maximizer can be taken to be a maximal planar graph, so it has exactly $3n - 6$ edges. Every maximal planar graph on $n$ vertices has the same number of edges, and the standard lower bound $\lambda_1 \ge 2|E|/n$ is the same for all of them. The extremal graph is pinned down only through its eigenvector. One has to show that the weight concentrates on two vertices, which are then forced to be adjacent to each other (Lemma 13) and to every other vertex (Lemma 14). Lemma 13 is the step specific to planarity. It uses the triangular faces of a maximal planar graph to find an edge switch that keeps the graph planar. In the formal setting, planarity is topological, so every planarity fact of the argument (the edge counts, the $K_{3,3}$ and $K_5$ obstructions, the faces of a triangulation) has to be derived from the drawing.

Formalization scope

• Graphs are SimpleGraph (Fin n). "$G$ is $K_2 + P_{n-2}$" is a graph isomorphism G ≃g bookPath n, where bookPath n lives on Fin 2 ⊕ Fin (n - 2). It is not an equality on a fixed labelling.
• $\lambda_1$ is the published WangKangXue.SpectralTuran.specRad, the largest eigenvalue of the real adjacency matrix.
• Planarity is the published topological RobertsonSeymour1986.GM5.IsPlanar: a drawing by simple arcs. It is not replaced by $K_5$/$K_{3,3}$-minor-freeness or by an edge count, either of which would change the class the maximum ranges over.
• Extremality is IsSpecMax IsPlanar G: $G$ is planar and $\lambda_1(G') \le \lambda_1(G)$ for every planar $G'$ on Fin n. Every milestone from Lemma 8 to Lemma 14 assumes it. These lemmas are false for an arbitrary planar graph, so a statement that drops the hypothesis, or replaces it by a property implying the conclusion, is not acceptable.
• The eigenvector is universally quantified: every $\mathbf v$ with $A\mathbf v = \lambda_1 \mathbf v$, all entries positive, all entries at most $1$, and every $x$ with $\mathbf v_x = 1$. Such a vector exists because the maximizer is connected (Perron–Frobenius). A statement that only asserts the existence of some eigenvector is weaker and is ruled out.
• Quantifiers. "For $n$ sufficiently large" is $\exists N\ \forall n \ge N$, and $N$ may depend on $\varepsilon$. Milestones 4–8 hold for every $\varepsilon > 0$. Lemmas 11–14 hold for $0 < \varepsilon < \varepsilon_0$ with an unspecified $\varepsilon_0$, because the paper chooses $\varepsilon$ small. The quantifier on $\varepsilon$ is always outermost, so $\varepsilon$ never depends on $n$ or $G$. Lemmas 12–14 hold for every vertex $w$ satisfying the conclusion of Lemma 11 (the predicate IsSecondHub), with the constants $24$ and $94$.
• Added hypotheses. $n \ge 3$ in the planar facts and in Lemma 8, where the paper's standing "$n$ large enough" is needed only to that extent. The page names the vertex of Lemma 12 $v$, the same letter as the eigenvector; it is renamed $u$. Lemma 14's set $A$ is stated in unfolded form.
• Infrastructure that a complete development needs: Euler's formula for topologically planar graphs, the non-planarity of $K_{3,3}$ and $K_5$, Perron–Frobenius for connected graphs, and the Rayleigh quotient. Proofs of the planar facts (milestone 2) are reusable well beyond this mission. Contributions toward any of them are welcome.

Selected references

• M. Tait and J. Tobin, Three conjectures in extremal spectral graph theory, J. Combin. Theory Ser. B (2017). Preprint arXiv:1606.01916v2. https://arxiv.org/abs/1606.01916, DOI https://doi.org/10.1016/j.jctb.2017.04.006
• B. N. Boots and G. F. Royle, A conjecture on the maximum value of the principal eigenvalue of a planar graph, Geographical Analysis 23(3) (1991), 276–282.
• D. Cao and A. Vince, The spectral radius of a planar graph, Linear Algebra Appl. 187 (1993), 251–257.
• A. J. Schwenk and R. J. Wilson, On the eigenvalues of a graph, in: Selected Topics in Graph Theory, Academic Press, 1978, 307–336.
• Hong Yuan, A bound on the spectral radius of graphs, Linear Algebra Appl. 108 (1988), 135–139.
• M. N. Ellingham and X. Zha, The spectral radius of graphs on surfaces, J. Combin. Theory Ser. B 78(1) (2000), 45–56.
• Z. Dvořák and B. Mohar, Spectral radius of finite and infinite planar graphs and of graphs of bounded genus, J. Combin. Theory Ser. B 100(6) (2010), 729–739.

Bibliographic data as given in the bibliography of Tait and Tobin (pp. 21–23).