Graph Theory

Motivation

Mean field games describe Nash equilibria of large populations in which every player interacts with every other player symmetrically, through the empirical distribution of all states. Many systems of interest are not of this kind: agents in a network interact only with their neighbours, and the interaction structure is a graph rather than a complete graph. Understanding when equilibria on large graphs behave like mean field equilibria, and when they do not, requires models in which the equilibrium on a finite graph can be computed exactly.

Lacker and Soret (arXiv:2005.14102v2, Math. Oper. Res. 2022) introduced such a model: a linear–quadratic flocking game on an arbitrary finite graph, in which each player steers a Brownian particle and pays a terminal penalty for being far from the average of her neighbours. For vertex-transitive graphs they solved the game in closed form, up to a scalar ODE, with an equilibrium that depends on the graph only through the spectrum of its Laplacian. This mission formalizes that finite-graph result, Theorem 2.5 of the paper. Its large-graph consequences are the subject of missions II and III of this series.

Setting

Let $G$ be a finite simple graph on vertices $V=\{1,\dots,n\}$, with adjacency matrix $A_G$ and degree matrix $D_G$. When $G$ has no isolated vertices its random-walk Laplacian is

$$L_G := D_G^{-1}A_G - I .$$

$G$ is transitive if for every two vertices $u,v$ there is a graph automorphism mapping $u$ to $v$. A transitive graph is regular, so its Laplacian $L_G = A_G/\delta(G) - I$ is symmetric, with eigenvalues in $[-2,0]$.

Fix a horizon $T>0$, a noise level $\sigma>0$ and a cost constant $c>0$. Each vertex $v$ is a player with state

$$dX_v(t) = \alpha_v(t,X(t))\,dt + \sigma\,dW_v(t),\qquad t\in[0,T],$$

driven by independent Brownian motions $W_v$, from a non-random initial state $X(0)=x_0\in\mathbb R^V$. A Markovian control $\alpha_v$ is a Borel function of time and the full state vector with at most linear growth. Player $v$ minimises

$$J_v = \tfrac12\,\mathbb E\Big[\int_0^T|\alpha_v(t,X(t))|^2\,dt + c\,\Big|X_v(T)-\frac{1}{\deg(v)}\sum_{u\sim v}X_u(T)\Big|^2\Big].$$

A profile $(\alpha_v)_v$ is a Markovian Nash equilibrium if no player can lower her cost by switching unilaterally to another Markovian control.

The equilibrium is built from

$$Q_G(x) := \det(I-xL_G)^{1/n},\qquad f_G'(t) = c\,Q_G'(f_G(t)),\ f_G(0)=0,$$ $$P_G(t) := -f_G'(T-t)\,L_G\big(I-f_G(T-t)L_G\big)^{-1},\qquad \alpha^G_i(t,x) := -e_i^\top P_G(t)x .$$

Formalization targets

Goal: Theorem 2.5

For a finite transitive graph $G$ without isolated vertices:

1. $Q_G$ is well defined and continuously differentiable on $\mathbb R_+$, and the ODE has a unique solution $f_G:[0,T]\to\mathbb R_+$.
2. $(\alpha^G_i)_i$ is a Markovian Nash equilibrium for every initial state.
3. For every $t\in(0,T]$, the equilibrium state $X(t)$ is Gaussian with

$$\mathbb E X(t) = (I-f_G(T-t)L_G)(I-f_G(T)L_G)^{-1}x_0,\qquad \mathrm{Cov}\,X(t) = \sigma^2(I-f_G(T-t)L_G)^2\int_0^t(I-f_G(T-s)L_G)^{-2}\,ds .$$

4. The average equilibrium cost satisfies

$$\frac1n\sum_{v}J_v = \frac{|P_G(0)x_0|^2}{2\,\mathrm{Tr}\,P_G(0)} - \frac{\sigma^2}{2}\log\frac{\mathrm{Tr}\,P_G(0)}{n\,f_G'(T)} .$$

All four parts are in the goal statement.

Milestones

The milestones follow the paper's proof in §2.2, §3 and §4.

• Graph-spectral facts. Transitive graphs are regular with symmetric $L_G$ (§2.2). The spectrum of $L_G$ lies in $[-2,0]$ (Remark 2.4). The eigenvalue distribution $\mu_G$ has mean $-1$ ((3.2)), and $Q_G = Q_{\mu_G}$ (§2.3).
• The ODE. Bounds on $Q_\mu$ and its first two derivatives (Proposition 3.1), and well-posedness of $f_\mu' = cQ_\mu'(f_\mu)$ with explicit bounds (Proposition 3.2).
• Symmetry. Commutation of $L_G$ with automorphism matrices, and constancy of the diagonal of equivariant matrices (Lemma 4.1).
• The Riccati system. The properties of $P_G(t)$ (§4.4 (i)–(iii)), the reduction of the Nash PDE system to matrix Riccati equations (Lemma 4.2), and the verification that the explicit $F^i = (\mathrm{Tr}\,P/n)^{-1}Pe_ie_i^\top P$ solve them (§4.4).
• Law and value. The fundamental matrix $\exp(-\int_s^tP) = (I-f(T-t)L)(I-f(T-s)L)^{-1}$ (§4.5) and the averaged value identity (§4.6).

Significance

The result. Theorem 2.5 is one of the few explicit Nash equilibria of a stochastic differential game on a non-complete graph. Two features of it are not visible in mean field theory. The equilibrium controls are nonlocal: each player reacts to the whole state vector, not only to her neighbours. The whole equilibrium (law, value, controls) depends on the graph only through the spectrum of $L_G$. The second feature drives the paper's later results. Weak convergence of the eigenvalue distributions $\mu_{G_n}$ yields limits of the equilibrium, and these separate the dense regime, where the mean field approximation is valid, from the sparse regime, where it is not.

Formalizing it. The result is proved in the paper; nothing here is open. No machine-checked version of it or of its ingredients exists: the random-walk Laplacian of a graph, linear–quadratic stochastic differential games, verification theorems for Nash systems, and Gaussian laws of linear SDEs with time-dependent coefficients. The mission produces a checked statement of the equilibrium together with reusable layers: spectral facts about $D^{-1}A - I$, an ODE analysis for $Q_\mu$, and a Riccati reduction for quadratic Nash systems.

Difficulty

Three steps resist a direct approach.

• The verification theorem. The paper passes from a classical solution of the Nash system (4.1) to a Nash equilibrium by appeal to a standard verification argument. Over the full class of Borel controls with linear growth, this requires Itô's formula for the quadratic value functions, together with integrability of the deviated state processes.
• The Riccati system. The $n$ coupled matrix equations (4.6) have no general closed-form solution. The explicit solution exists only because transitivity forces $e_i^\top P(t)e_i = \mathrm{Tr}(P(t))/n$ for every $i$. That identity has to be derived from the action of the automorphism group (Lemma 4.1), not from regularity alone.
• The law of the state. It requires solving a linear SDE with a time-dependent matrix and identifying its Gaussian law, a step for which the library has little support.

Formalization scope

Lean conventions:

• Vertices. The vertex set is Fin n, so the paper's $1,\dots,n$ become $0,\dots,n-1$. The state space is the platform's EthierKurtz.SDEState n (Euclidean $\mathbb R^n$).
• The Laplacian. $L_G$ is the random-walk Laplacian $D^{-1}A-I$, not Mathlib's $D-A$.
• Time and controls. Time is real. Controls are Borel on $\mathbb R\times\mathbb R^n$ with linear growth on $[0,T]$; their values off $[0,T]$ are never used.
• Solutions of (2.1). A solution is a pathwise strong solution on a probability space that the solution itself carries, adapted to the completed Brownian filtration. Costs are compared across solutions; this is faithful because (2.1) has a unique strong solution.
• Costs are $[0,\infty]$-valued lower Lebesgue integrals. They are converted to reals only after their finiteness is asserted.
• Existence of the equilibrium state. The goal also asserts that the equilibrium state equation has a solution, so that the Nash property cannot hold vacuously.
• Derivatives. $f_G'(T-t)$ is written as its ODE value $cQ_G'(f_G(T-t))$. The ODE is solved on $[0,T]$ with one-sided derivatives at the endpoints, and uniqueness is agreement on $[0,T]$.
• Matrix conventions. Covariance integrals are entrywise. Gaussian laws are Mathlib's multivariateGaussian.
• Added hypotheses. $0<n$ is added to three milestones that are false on the empty graph.

A formalization that fixes $x_0=0$, restricts deviations to linear controls, drops the existence of the equilibrium state process, or replaces $L_G$ by $D-A$ is not this theorem.

Infrastructure that a complete development needs:

• symmetric-matrix spectral calculus for $L_G$ and for the matrix functions $(I-xL)^{-1}$ and $\log(I-xL)$;
• differentiation under the integral for $Q_\mu$;
• Picard–Lindelöf and Grönwall on $\mathbb R_+$;
• Itô's formula for quadratic functions of a diffusion with additive noise;
• the Gaussian law of $\int_0^t M(t,s)\,dW_s$ for deterministic $M$.

The spectral, ODE and Riccati layers are reusable beyond this mission. Proofs of individual milestones are welcome; so are general verification theorems for linear–quadratic games.

Selected references

• D. Lacker, A. Soret, A case study on stochastic games on large graphs in mean field and sparse regimes, arXiv:2005.14102v2, 2021; Math. Oper. Res. 47(2), 2022. https://arxiv.org/abs/2005.14102
• F. Chung, Spectral Graph Theory, CBMS Regional Conference Series in Mathematics 92, AMS, 1997. https://doi.org/10.1090/cbms/092
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I, Springer, 2018. https://doi.org/10.1007/978-3-319-58920-6
• A. Veretennikov, On strong solutions and explicit formulas for solutions of stochastic integral equations, Math. USSR-Sb. 39(3), 1981. https://doi.org/10.1070/SM1981v039n03ABEH001522

Motivation

Networks of identical dynamical systems coupled along a directed graph model power grids, sensor and robot swarms, neural populations and coupled oscillators. A basic control question is how to steer every node of such a network onto a prescribed reference trajectory by acting directly on only a few nodes. This is pinning control: feedback is injected at a small set of pinned vertices, and the coupling has to carry the reference signal to the rest of the network.

For undirected or strongly connected networks, criteria for pinning synchronization go back to Wang and Chen (2002) and Chen, Liu and Lu (2007), and the first mission of this series treats the strongly connected case of Yu, Chen, Lü and Kurths (2013). Many networks of interest are not strongly connected: information flows down a hierarchy of groups, and the minimal requirement for the reference to reach every node is that the network, with the reference added as a virtual leader, contains a directed spanning tree rooted at the leader. Section 4 of that paper gives a criterion for this general case that splits into one condition per strongly connected component. This mission formalizes that criterion, Theorem 4.5, with the lemmas its proof uses and three corollaries.

Setting

There are $N$ vertices with states $x_i(t)\in\mathbb R^n$. The coupling configuration matrix $G\in\mathbb R^{N\times N}$ has $G_{ij}\ge0$ for $i\ne j$, where $G_{ij}>0$ records a connection from vertex $j$ to vertex $i$, and zero row sums, $G_{ii}=-\sum_{j\ne i}G_{ij}$. Given a function $f:\mathbb R^n\times\mathbb R_+\to\mathbb R^n$, a coupling strength $c$, an inner coupling matrix $\Gamma\in\mathbb R^{n\times n}$ and pinning gains $d_i\ge0$ (vertex $i$ is pinned when $d_i>0$), the controlled network is

$$\dot x_i=f(x_i,t)+c\sum_{j=1}^N G_{ij}\Gamma x_j-c\,d_i\,\Gamma(x_i-s),\qquad i=1,\dots,N,$$

where the reference $s$ solves $\dot s=f(s,t)$. The network is globally synchronized when $x_i(t)-s(t)\to0$ for every vertex and every pair of solutions.

The nonlinearity is controlled by Assumption 1: there is a matrix $K$ with $(x-y)^{\mathsf T}(f(x,t)-f(y,t))\le(x-y)^{\mathsf T}K\Gamma(x-y)$ for all $x,y$ and $t\ge0$. Throughout §4 the paper also assumes that $K$ and $\Gamma$ commute, that $\Gamma$ is positive definite, and puts $\theta=\lambda_{\max}((K+K^{\mathsf T})/2)\ge0$.

The vertices split into strongly connected components $V_1,\dots,V_M$. In the Frobenius normal form the components are ordered so that no edge goes from a later component to an earlier one, which makes $G$ block lower triangular. For each component $j$ the mission uses three matrices:

• $\widetilde G_j$, the diagonal block of $G-\mathrm{diag}(d)$ on $V_j$;
• $A_j$, the within-component part of $G$ with zero row sums;
• $\widetilde\Pi_j=\mathrm{diag}(\Pi_j)$, where $\Pi_j$ is a positive vector with $\Pi_j^{\mathsf T}A_j=0$.

In Lean, component membership is a map blk : Fin N → Fin M, and Fin M carries the Frobenius order.

Formalization targets

Goal: Theorem 4.5

If, for every component $j$,

$$2\theta\widetilde\Pi_j+c\bigl(\widetilde\Pi_j\widetilde G_j+\widetilde G_j^{\mathsf T}\widetilde\Pi_j\bigr)<0, \tag{4.8}$$

then the controlled network with a directed spanning tree is globally synchronized.

Milestones

1. The θ bound (p. 1402). Commutation and $\Gamma>0$ turn Assumption 1 into $(x-y)^{\mathsf T}(f(x,t)-f(y,t))\le\theta(x-y)^{\mathsf T}\Gamma(x-y)$.
2. Lemma 2.13. The strict Schur complement test for a symmetric block matrix.
3. Lemma 4.4. If $\widetilde\Pi_j\widetilde G_j+\widetilde G_j^{\mathsf T}\widetilde\Pi_j<0$ on every diagonal block of a block lower-triangular $\overline G$, then positive block weights $\Delta_j$ exist with $\Delta\widetilde\Pi\overline G+\overline G^{\mathsf T}\widetilde\Pi\Delta<0$.
4. (4.10). Along solutions, $V=\sum_j\Delta_j\widetilde e_j^{\mathsf T}\widetilde\Pi_j\widetilde e_j$ satisfies $\dot V\le e^{\mathsf T}\{[\Delta\widetilde\Pi(c\overline G+\theta I_N)+(c\overline G+\theta I_N)^{\mathsf T}\widetilde\Pi\Delta]\otimes\Gamma\}e$.

Companions

• Corollary 4.7: the same conclusion under $\theta\widetilde\Pi_j+c(\overline A_j-\widetilde\Pi_jC_j-\widetilde\Pi_j\overline D_j)<0$, which separates the outer in-degrees $C_j$ from the pinning gains $\overline D_j$.
• Corollary 4.8 (i): an explicit coupling-strength threshold under Assumption 2.
• Corollary 4.9: partial synchronization of the first components.

Significance

Theorem 4.5 replaces a single $Nn\times Nn$ matrix inequality for the whole network with $M$ inequalities, one of the size of each component. In practice the test runs component by component down the Frobenius order: decide which components need pinning, choose gains for each one separately, and get synchronization of the whole network. Corollary 4.7 makes this explicit in terms of the outer in-degrees: a component with no incoming edges from earlier components has to be pinned (Remark 4), while a component that receives enough weight from upstream needs no control. These conditions underlie the pinning scheme algorithm of §5 of the paper.

On the formal side, as far as a search of the platform and of Mathlib shows, none of these results is machine-checked. Mathlib has the positive semidefinite Schur complement and irreducible nonnegative matrices, but not the strict Schur complement, block-diagonal Lyapunov scaling, or Lyapunov arguments for networked ODEs with Kronecker-structured couplings. The mission produces, beyond the paper's theorem:

• a reusable strict Schur complement lemma;
• a block-triangular diagonal-stability lemma;
• a template for Lyapunov estimates on coupled networks in Lean.

Difficulty

The obvious argument is to take one Lyapunov function weighted by a positive left null vector of the whole coupling matrix, as in the strongly connected case. Here it fails: the coupling matrix of a network that is not strongly connected has no positive left null vector, and condition (4.8) is local to each component. The central step is the passage from blockwise to global negative definiteness (Lemma 4.4). Condition (4.8) says nothing about the off-diagonal blocks that couple a component to earlier ones, and a block lower-triangular matrix whose symmetrized diagonal blocks are negative definite need not have a negative definite symmetric part; the component weights $\Delta_j$ have to be found so that those couplings are dominated, which is a quantitative statement about Schur complements. Turning the resulting matrix inequality into convergence of the trajectories then needs a differential inequality on $[0,\infty)$, a Kronecker-product definiteness argument with $\Gamma$, and the commutation of $K$ and $\Gamma$ to reach the θ bound.

Formalization scope

States are Fin n → ℝ and matrices are indexed by Fin N, Fin n, or the subtype of one component's vertices. Solutions are functions on ℝ that satisfy their ODE on $[0,\infty)$ through HasDerivWithinAt … (Set.Ici 0). "For any initial conditions" means for every pair of solutions $(s,x)$; existence of solutions is not claimed. Convergence is componentwise, which agrees with every norm on $\mathbb R^n$. "Positive definite" is Mathlib's Matrix.PosDef, which includes symmetry, and $X<0$ is (-X).PosDef. $\lambda_{\max}$ is the least Rayleigh bound, IsLamMax, never a supremum of a possibly empty set.

The vertices are not permuted into Frobenius form. The hypotheses say instead that:

• every component is nonempty;
• every component is strongly connected inside itself;
• every edge between components points forward in the order;
• every vertex is reachable from a pinned vertex.

The weights $\Pi_j$ are tied to the paper's object by $\Pi_j^{\mathsf T}A_j=0$. The standing assumptions of p. 1402 (Assumption 1, $K\Gamma=\Gamma K$, $\theta=\lambda_{\max}((K+K^{\mathsf T})/2)\ge0$, $\Gamma>0$) are hypotheses of every goal-level statement. The goal does not assume the weights $\Delta_j$, the bound (4.10), or definiteness of a whole-network matrix; it assumes only (4.8) on each component, so it cannot be trivialized by assuming its own conclusion. For $n=0$ the $\lambda_{\max}$ hypothesis cannot be met, so that degenerate dimension is excluded.

The pages contain three misprints. (4.10) has "$-c$" in its third line and "$++$" in its last; the last line, with a single $+$, is formalized. Corollary 4.9 ranges "$i=1,\dots,N$" where the component range is meant.

A complete development needs a Gronwall-type decay lemma on $[0,\infty)$, the strict Schur complement, definiteness of Kronecker products, and the square root of a positive definite matrix commuting with matrices that commute with it. Each of these is reusable well beyond this mission, and contributions to any of them are welcome, as are proofs of the milestones in any order.

Selected references

• W. Yu, G. Chen, J. Lü, J. Kurths, Synchronization via pinning control on general complex networks, SIAM J. Control Optim. 51(2) (2013), 1395–1416. https://doi.org/10.1137/100781699
• X. F. Wang, G. Chen, Pinning control of scale-free dynamical networks, Physica A 310 (2002), 521–531. https://doi.org/10.1016/S0378-4371(02)00772-0
• T. Chen, X. Liu, W. Lu, Pinning complex networks by a single controller, IEEE Trans. Circuits Syst. I 54(6) (2007), 1317–1326. https://doi.org/10.1109/TCSI.2007.895383
• S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777
• R. A. Brualdi, H. J. Ryser, Combinatorial Matrix Theory, Cambridge University Press, 1991. https://doi.org/10.1017/CBO9781107325708

Motivation

Counting the proper $q$-colorings of a graph, and sampling one uniformly at random, are basic problems of approximate counting with a long history in statistical physics, where proper colorings are the zero-temperature antiferromagnetic Potts model. On bipartite graphs these problems are tied to #BIS, the problem of approximately counting independent sets in a bipartite graph, whose complexity is unresolved. Galanis, Štefankovič, Vigoda and Yang showed that approximately counting proper $q$-colorings is #BIS-hard on bipartite graphs of maximum degree $\Delta$ whenever $q \le \Delta/(2\log\Delta)$ (SIAM J. Comput. 45(6), 2016). A positive result in that regime therefore has to use structure beyond bipartiteness and bounded degree.

Jenssen, Keevash and Perkins (SIAM J. Comput. 49(4) 2020) use expansion. Their Theorem 5 says that for $\Delta \ge Cq^2\log^2 q$ there is an FPTAS and a polynomial-time sampler for proper $q$-colorings on almost every $\Delta$-regular bipartite graph. This answered Conjecture 1 of the authors' SODA 2019 extended abstract. Liao, Lin, Lu and Mao (APPROX/RANDOM 2019) independently proved a similar result under a slightly stronger condition on $\Delta$. The organizing idea, that most colorings of a strongly expanding bipartite graph follow one of a few patterns, comes from the work of Peled and Spinka on rigidity of colorings of $\mathbb Z^d$ (arXiv:1808.03597).

This mission is the fourth of a series formalizing the four main results of that paper; it covers Theorem 5.

Setting

Fix integers $q \ge 3$, $\Delta \ge 3$ and $m \ge 1$. The vertex set is $V = \mathcal O \sqcup \mathcal E$, two sides of $m$ vertices each (so $n = 2m$). $\mathcal G^{\mathrm{bip}}(2m,\Delta)$ is the finite set of labelled simple graphs on $V$ whose edges all join $\mathcal O$ to $\mathcal E$ and in which every vertex has degree $\Delta$. A property holds for almost every $\Delta$-regular bipartite graph if the fraction of graphs in $\mathcal G^{\mathrm{bip}}(2m,\Delta)$ having it tends to $1$ as $m \to \infty$.

For $S \subseteq V$ the vertex boundary $\partial S$ is the set of vertices outside $S$ with a neighbour in $S$, and $S^+ = S \cup \partial S$. The graph is a bipartite $(\sigma,\rho)$-expander if $|\partial S| \ge \rho|S|$ for every $S$ inside one side with $|S| \le \sigma m$.

A proper $q$-coloring is a map $f : V \to [q]$ with $f(u) \ne f(v)$ on every edge; $\mathcal X_q(G)$ is their set and $Z_G(q) = |\mathcal X_q(G)|$. A pattern is a pair $(A,B)$ of disjoint sets with $A \cup B = [q]$; there are $2^q$ of them. A coloring agrees with $(A,B)$ at $v$ if $v \in \mathcal O$ and $f(v) \in A$, or $v \in \mathcal E$ and $f(v) \in B$. For $S \subseteq V$, $\chi_{A,B}(S)$ is the set of proper colorings that disagree with $(A,B)$ at every vertex of $S$ and agree everywhere else.

$G^3$ joins two vertices at $G$-distance at most $3$. A set is little if $|S| \le 4q\frac{\log\Delta}{\Delta}m$. A polymer is a little set that is connected in $G^3$; $\mathcal C(G)$ is the set of polymers, and two polymers are compatible if their $G$-distance exceeds $3$. For a pattern $(A,B)$, the weight and the polymer partition function are

$$w_{A,B}(\gamma) = \frac{|\chi_{A,B}(\gamma)|}{|A|^m|B|^m}, \qquad \Xi_{A,B}(G) = \sum_{\Gamma} \prod_{\gamma\in\Gamma} w_{A,B}(\gamma),$$

the sum over all families $\Gamma \subseteq \mathcal C(G)$ of pairwise compatible polymers, the empty family included. Finally $\hat Z$ is an $\varepsilon$-relative approximation to $Z$ if $e^{-\varepsilon}\hat Z \le Z \le e^{\varepsilon}\hat Z$.

Formalization targets

Goal: the deterministic core of Theorem 5

There is an absolute constant $C > 0$ such that for all $q \ge 3$ and $\Delta \ge Cq^2\log^2 q$, almost every $\Delta$-regular bipartite graph $G$ satisfies

$$e^{-\varepsilon}\tilde Z_G(q) \le Z_G(q) \le e^{\varepsilon}\tilde Z_G(q), \qquad \tilde Z_G(q) = \sum_{(A,B)} |A|^m|B|^m\,\Xi_{A,B}(G), \quad \varepsilon = e^{-m/(4q)},$$

and, for every pattern $(A,B)$ and every polymer $\gamma \in \mathcal C(G)$, the Kotecký–Preiss condition

$$\sum_{\gamma' \in \mathcal C(G):\ d(\gamma',\gamma)\le 3} w_{A,B}(\gamma')\,e^{|\gamma'| + g(\gamma')} \le |\gamma|, \qquad g(\gamma) = \frac{\Delta}{10q^2\log\Delta}|\gamma|.$$

The constant $C$ is left existential, as in the paper.

Milestones

In the order of the proof:

1. Lemma 23, the expansion of almost every regular bipartite graph;
2. Lemma 27, the bound on $|\chi_{A,B}(S)|$;
3. Lemma 28, the covering of $\mathcal X_q(G)$ by $\chi_{A,B}(S)$ with $S$ little;
4. the product formula after (13);
5. Claim 30, the size bound for sparse sets;
6. the binomial estimate, an existing platform theorem;
7. Lemma 29, the reduction;
8. the weight bound of §5.1;
9. the per-vertex estimate (15).

Significance

The goal is the whole mathematical content of Theorem 5. The paper's algorithm (its Theorem 8, adapted from Helmuth, Perkins and Regts, Algorithmic Pirogov–Sinai theory) takes exactly these two facts as input. Given the Kotecký–Preiss condition, the cluster expansion of each $\log\Xi_{A,B}(G)$ converges and truncating it gives the estimator; the reduction transfers the estimate to $Z_G(q)$. With the goal proved, the remaining distance to the FPTAS is algorithmic bookkeeping, not combinatorics.

The result has been proved since 2019 and is not formalized anywhere. A formal proof would add a machine-checked polymer-model reduction for a spin system with exponentially many ground states, a reusable model of uniformly random regular bipartite graphs, and a checked instance of the "expansion implies few ground states" argument used throughout this literature.

Difficulty

The obvious first idea is a one-ground-state expansion, as for the hard-core model, where configurations are close to "all even" or "all odd". For colorings there are $2^q$ patterns. A coloring can lie close to several of them, so the reduction must show that the sets $\chi_{A,B}(S)$ with $S$ little overlap only negligibly. That needs an inclusion–exclusion step whose error is exponentially small in $m/q$. A second difficulty is the size of polymers: little sets are $q$ times larger than the sets of the hard-core analysis. Claim 30 is what keeps the union of compatible polymers from becoming a large set that the expansion no longer controls. Finally, the constants must be uniform in $q$. The single condition $\Delta \ge Cq^2\log^2 q$ has to cover the expansion lemma, the reduction and the Kotecký–Preiss estimate at once.

Formalization scope

The FPTAS and the sampling algorithm are not formalized. Mathlib has no machine model in which "polynomial time" could be stated, and the running times carry unquantified constants. The goal is the mathematics the algorithm rests on: the reduction and the Kotecký–Preiss condition, with the paper's constants $e^{-m/(4q)}$, $4q\log\Delta/\Delta$ and $\Delta/(10q^2\log\Delta)$. Neither half may be dropped. Replacing $e^{-m/(4q)}$ by an existential error, or summing the Kotecký–Preiss condition over compatible rather than incompatible polymers, would make the goal trivial or wrong.

Conventions committed to in Lean:

• Vertices are Fin m ⊕ Fin m, and $\mathcal G^{\mathrm{bip}}(2m,\Delta)$ is the set of labelled $\Delta$-regular graphs with edges only between the two fixed sides. The paper does not fix a bipartition; this fixed-sides model is a disclosed choice, matching §5's $|\mathcal O| = |\mathcal E| = m$.
• Distances are Mathlib's extended distance edist, so vertices in different components are at distance $\infty$ and never incompatible.
• A pattern is encoded by $A \subseteq [q]$ with $B = [q]\setminus A$. Patterns with an empty side are kept: their weights are $0$ under Lean's $x/0 = 0$, so they contribute $0$ to $\tilde Z_G(q)$, as on the page for large $m$.
• log is the natural logarithm; the binomial estimate is used in nats.

Added hypotheses:

• $A, B \ne \emptyset$ in Lemma 27 and in the product formula, which divide by $|A|$ and $|B|$;
• $\Delta \ge 3$ in Lemma 28 and Claim 30, the paper's standing convention (§1.3);
• $m \ge 1$ in Lemma 29, which fails on the empty vertex set.

The goal needs none of these, since its limit is in $m$ and its constant absorbs $\Delta$.

A complete development needs a counting theory of random regular bipartite graphs (for Lemma 23, through Bassalygo's expansion theorem), counts of connected sets in bounded-degree graphs, and inclusion–exclusion over patterns. The random-graph model and the polymer-model definitions are reusable across this series and beyond. Proofs of any milestone, and alternative routes to Lemma 23, are welcome.

Selected references

• M. Jenssen, P. Keevash and W. Perkins, Algorithms for #BIS-hard problems on expander graphs, SIAM J. Comput. 49(4) (2020) 681–710. https://doi.org/10.1137/19M1286669
• A. Galanis, D. Štefankovič, E. Vigoda and L. Yang, Ferromagnetic Potts model: refined #BIS-hardness and related results, SIAM J. Comput. 45(6) (2016) 2004–2065.
• R. Peled and Y. Spinka, Rigidity of proper colorings of $\mathbb Z^d$, arXiv:1808.03597 (2018). https://arxiv.org/abs/1808.03597
• C. Liao, J. Lin, P. Lu and Z. Mao, Counting independent sets and colorings on random regular bipartite graphs, APPROX/RANDOM 2019, Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2019).
• T. Helmuth, W. Perkins and G. Regts, Algorithmic Pirogov–Sinai theory, Probab. Theory Related Fields (2020); extended abstract at STOC 2019.
• R. Kotecký and D. Preiss, Cluster expansion for abstract polymer models, Comm. Math. Phys. 103(3) (1986) 491–498.
• L. A. Bassalygo, Asymptotically optimal switching circuits, Problems Inform. Transmission 17(3) (1981) 206–211.

Motivation

The hard-core model assigns weight to independent vertex sets of a graph. Its partition function counts those sets when the activity is one and weights larger sets more heavily when the activity increases. Counting independent sets on bipartite graphs is a standard benchmark for approximate counting: the general problem is difficult, while random regular graphs have additional expansion that can make approximation possible. Jenssen, Keevash and Perkins prove an approximation and sampling theorem for almost every sufficiently high degree regular bipartite graph when the activity is above an explicit threshold Jenssen–Keevash–Perkins, Theorem 2.

The question is specific to a random graph model. It does not assert the same conclusion for every regular bipartite graph. The authors use a criterion attributed to Bassalygo to show that almost every graph in the model has the expansion needed by their argument Jenssen–Keevash–Perkins, Theorem 22 and Lemma 23. Liao, Lin, Lu and Mao independently obtained related counting results under somewhat stronger parameter conditions Liao–Lin–Lu–Mao, 2019.

Setting

Let $G$ be a simple graph with two labelled sides $\mathcal O$ and $\mathcal E$, each containing $m$ vertices, and let every vertex have degree $\Delta$. An independent set $I$ contains no adjacent pair. For activity $\lambda>0$, the hard-core partition function is

$$Z_G(\lambda)=\sum_{I\text{ independent}}\lambda^{|I|}.$$

For a vertex set $S$, its vertex boundary $\partial S$ consists of vertices outside $S$ with a neighbor in $S$. The graph is a bipartite $(\sigma,\rho)$-expander when every subset of either side with size at most $\sigma m$ has boundary of size at least $\rho$ times its size. The expansion parameters used here are $\sigma=4\log\Delta/\Delta$ and $\rho=\Delta/(4\log\Delta)-1/2$. A set is tiny when its size is at most $\sigma m$ Jenssen–Keevash–Perkins, Definition 21 and §4.4.

The graph $G^2$ joins distinct vertices whose distance in $G$ is at most two. On either side, a polymer is a nonempty, tiny, $G^2$-connected vertex set. Two polymers on the same side are compatible if every pair of their vertices is more than distance two apart in $G$. A polymer $\gamma$ has weight $w_\gamma=\lambda^{|\gamma|}/(1+\lambda)^{|\partial\gamma|}$. Summing products of weights over mutually compatible polymer families gives the partition functions $\Xi^{\mathcal E}(G)$ and $\Xi^{\mathcal O}(G)$ Jenssen–Keevash–Perkins, §§4.1, 4.4.

“Almost every” means that, for fixed $\Delta$, the fraction of labelled $\Delta$-regular bipartite graphs satisfying a property tends to one as $m$ tends to infinity. The random graph is chosen uniformly from graphs on the two fixed sides Jenssen–Keevash–Perkins, p. 3.

Formalization targets

The first target is the authors' expansion premise: for all sufficiently large $\Delta$, almost every graph is a bipartite $(4\log\Delta/\Delta,\Delta/(4\log\Delta)-1/2)$-expander. The main target combines two deterministic claims on almost every such graph. For every $\lambda>50\log^2\Delta/\Delta$, write $n=2m$ and

$$\widehat Z_G(\lambda)=(1+\lambda)^m\bigl(\Xi^{\mathcal E}(G)+\Xi^{\mathcal O}(G)\bigr),\qquad \varepsilon_0=(1+\lambda)^{-n/4}.$$

First, $\widehat Z_G$ is an $\varepsilon_0$-relative approximation in the paper's exponential convention:

$$e^{-\varepsilon_0}\widehat Z_G(\lambda)\le Z_G(\lambda)\le e^{\varepsilon_0}\widehat Z_G(\lambda).$$

Second, each of the two polymer models obeys the Kotecký–Preiss condition with decay $g(\gamma)=|\gamma|\Delta\log(1+\lambda)/(10\log\Delta)$:

$$\sum_{\gamma'\text{ incompatible with }\gamma}w_{\gamma'}e^{|\gamma'|+g(\gamma')}\le |\gamma|.$$

The same graph event must support every activity above the threshold; the activity quantifier is inside the limiting probability. The intermediate targets are Bassalygo's entropy criterion, the high probability expansion lemma, the tiny-side lemma for independent sets, the approximation lemma at its weaker activity threshold, a published binomial-entropy estimate, and the per-vertex polymer sum bound Jenssen–Keevash–Perkins, Theorem 22, Lemmas 23–25 and §4.5.

Significance

The reduction expresses a weighted independent-set count through two finite polymer partition functions whose weights decay under the same expansion condition. The KP bound supplies the convergence condition used by the paper's general polymer approximation theorem. Together these are the mathematical inputs to its algorithmic Theorem 2 Jenssen–Keevash–Perkins, Theorems 2, 8.

A formal proof would make the expansion assumptions, distance convention, graph probability limit, and error normalization explicit. The target is a formalization of a published result, not an open conjecture. The proposal contains statements and definitions; their proofs remain to be supplied. The binomial estimate is already machine checked on Prove2Me and is included by reference.

Difficulty

An independent set can occupy vertices on both sides of a bipartite graph. Merely taking one side as the dominant phase double counts sets that are sparse on both sides. The tiny-side lemma and the polymer decomposition identify and control that overlap. The random graph step also requires an expansion estimate strong enough to apply to every small subset of either side, rather than only to a typical subset Jenssen–Keevash–Perkins, §§4.4–4.5.

Formalization scope

Lean uses finite simple graphs on $\mathrm{Fin}(m)\oplus\mathrm{Fin}(m)$, with the left and right summands serving as the odd and even sides. This fixes a labelled bipartition for the uniform random graph model. Distances use extended natural graph distance, so vertices in different components have infinite distance. Polymer families include the empty family, and graph connectivity excludes the empty polymer. Sizes are natural numbers; thresholds involving logarithms are real inequalities. Binary entropy in the cited expansion theorem is measured in bits, while Mathlib's binary entropy is converted from natural units. The approximation uses exponential relative error exactly as in Definition 10 of the paper.

The FPTAS, sampling algorithm, and running-time assertion are outside this mission because Mathlib has no matching machine and cost model. The goal formalizes both the partition-function reduction and its KP condition, the mathematical inputs consumed by the paper's algorithm theorem. It quantifies over all activities above the threshold within the almost-every event, preventing a separate favorable graph set for each activity. The fixed-sides model and the explicit domain of Bassalygo's entropy formula are disclosed representation choices. The tiny-side milestone (Lemma 24) carries a graph-size threshold depending on the degree: as printed, for every graph size, it fails on small dense graphs (the complete bipartite graph minus disjoint complete blocks), and the main result uses it only as the graph size grows. Reusable contributions include finite graph expansion lemmas, polymer partition-function identities, and bounds on connected vertex sets.

Selected references

• M. Jenssen, P. Keevash and W. Perkins, Algorithms for #BIS-hard problems on expander graphs, SIAM Journal on Computing 49(4), 2020, 681–710. DOI.
• L. Bassalygo, Asymptotically optimal switching circuits, Problems of Information Transmission 17(3), 1981, 206–211. Publisher record.
• C. Liao, J. Lin, P. Lu and Z. Mao, Counting independent sets and colorings on random regular bipartite graphs, APPROX/RANDOM, 2019. DOI.