Graph Theory

Motivation

Betweenness centrality measures how much of the communication in a network passes through a node. Freeman's original measure (Freeman 1977) counts the fraction of shortest paths between each pair of nodes that pass through it, and Brandes' algorithm (Brandes 2001) made it computable on large graphs. Variants replace shortest paths by maximum flows (Freeman, Borgatti and White 1991), random walks (Newman 2005) or load-splitting rules (Goh, Kahng and Kim 2001), and group variants measure the traffic that passes through a set of nodes (Everett and Borgatti 1999).

Dolev, Elovici and Puzis (technical report 2009, J. ACM 2010) define routing betweenness centrality (RBC): given the actual routing scheme of a communication network and its traffic matrix, the RBC of a node is the expected number of packets that pass through it. Each of the measures above is a special choice of routing scheme. The application is the placement of traffic monitors: the RBC of an ordered sequence of monitors is the expected number of packets sampled by all of them in order, which measures, for example, redundant inspection along a path.

Setting

Let $V$ be a finite set of nodes. A routing scheme assigns to every source $s$, current node $u$, next node $v$ and target $t$ a number $R(s,u,v,t)$, the probability that $u$ forwards to $v$ a packet with source address $s$ and target address $t$. Routing decisions are independent. The scheme is assumed to be

• nonnegative;
• total: every node $u\ne t$ forwards a packet targeted at $t$ with total probability one, $\sum_v R(s,u,v,t)=1$, and the target forwards nothing;
• loop-free: for every pair $(s,t)$ the directed graph with an arc $a\to b$ whenever $R(s,a,b,t)>0$ is acyclic;
• source-oblivious where stated: $R(s,u,v,t)$ does not depend on $s$.

A route from $s$ to $t$ is a sequence of nodes from $s$ to $t$ whose every hop has positive forwarding probability; its probability is the product of the hop probabilities. For nodes $s,t,v$ and a sequence $S=(s_1,\dots,s_k)$:

• the pairwise dependency $\delta_{s,t}(v)$ is the total probability of the routes from $s$ to $t$ that visit $v$;
• the sequence dependency $\tilde\delta_{s,t}(S)$ is the total probability of the routes from $s$ to $t$ that visit $s_1$, then $s_2$, …, then $s_k$ (consecutive repetitions in $S$ collapsed).

A traffic matrix $T(s,t)$ gives the number of packets sent from $s$ to $t$, and sampling rates $\rho_v\in[0,1]$ give the fraction of passing packets a monitor at $v$ samples. The target dependency is $\delta_{\bullet,t}(v)=\sum_{s}\delta_{s,t}(v)T(s,t)$, and the RBC of the sequence $S_\rho$ of distinct nodes is

$$\tilde\delta_{\bullet,\bullet}(S_\rho)=\prod_{r\in S}\rho_r\cdot\sum_{s,t\in V}\tilde\delta_{s,t}(S)\,T(s,t).$$

Formalization targets

Goal: sequence RBC as a sum over targets of chained dependencies

For a source-oblivious scheme and a sequence $S=(s_1,\dots,s_k)$ of distinct nodes, $k\ge1$,

$$\prod_{r\in S}\rho_r\cdot\sum_{s,t\in V}\tilde\delta_{s,t}(S)\,T(s,t)=\sum_{t\in V}\delta_{\bullet,t}(s_1)\,\rho_{s_1}\prod_{i=1}^{k-1}\delta_{s_i,t}(s_{i+1})\,\rho_{s_{i+1}}.$$

The right side is the value returned by the paper's Algorithm 6. The identity contains no running time and no constant: it states the exact equality the algorithm relies on.

Milestones

1. Proposition 1: for a loop-free scheme (not necessarily source-oblivious), two different orderings of the same set of nodes cannot both have positive sequence dependency.
2. Lemma 1 (Dependency chaining): for $s\ne t$, $\tilde\delta_{s,t}((s_1,\dots,s_k))=\delta_{s,t}(s_1)\cdot\tilde\delta_{s_1,t}((s_2,\dots,s_k))$.
3. Eq. (16): for $s\ne t$, $\tilde\delta_{s,t}((s_1,\dots,s_k))=\delta_{s,t}(s_1)\prod_{i=2}^k\delta_{s_{i-1},t}(s_i)$.
4. Eq. (17): $\tilde\delta_{\bullet,t}((s_1,\dots,s_k))=\delta_{\bullet,t}(s_1)\prod_{i=2}^k\delta_{s_{i-1},t}(s_i)$.
5. Eq. (1) (off the goal's path): $\delta_{s,t}(s)=1$ and $\delta_{s,t}(v)=\sum_{u}\delta_{s,t}(u)R(s,u,v,t)$ for $v\ne s$, the sum over predecessors $u$ of $v$.
6. Eq. (9) (off the goal's path): $\delta_{\bullet,t}(v)=T(v,t)+\sum_u\delta_{\bullet,t}(u)R(\oslash,u,v,t)$ for source-oblivious schemes.

Significance

The goal reduces the RBC of a sequence of $k$ monitors to $O(nk)$ arithmetic on precomputed single-node quantities, instead of a pass over the routing graph of every source–target pair. This is what makes repeated evaluation of candidate monitor sequences, as in greedy or search-based placement, affordable on large networks. Eqs. (1) and (9) are the recursions behind the paper's algorithms for the RBC of single nodes; Eq. (9) replaces the loop over all source–target pairs by a loop over targets.

The paper's proof of Lemma 1 is an argument about conditional probabilities of informally described events. A formalization fixes what "the probability that a packet passes through $S$" means, as a sum over a finite set of routes, and checks the factorization against that definition, including the corner cases the prose passes over: sequences with repeated nodes, a first node equal to the source or to the target, and the source $s=t$ in the sum over all sources. No machine-checked version of these identities is known.

Difficulty

Dependency chaining is a Markov property: after the packet reaches $s_1$, its future does not depend on its past. The obvious argument splits every route through $s_1$ into a prefix ending at $s_1$ and a suffix starting there. Two points need care. First, the suffix must be a route of a packet with source $s_1$, which is where source-obliviousness enters; for source-dependent routing the lemma is false. Second, the prefix probabilities must sum to $\delta_{s,t}(s_1)$ while the suffix probabilities sum to one, which requires that no packet is lost: this is where totality of the forwarding probabilities and loop-freeness (every walk reaches the target in at most $|V|$ steps) are needed. The passage from Lemma 1 to the goal then requires the sum over all sources, including $s=t$, where Lemma 1 does not apply.

Formalization scope

Nodes form a type V with [Fintype V] [DecidableEq V]; probabilities, traffic and sampling rates are real numbers; sequences are Lean lists, indexed from $0$. Routes are repetition-free lists, and every dependency is a finite sum over them; no infinite sums, suprema or measure theory are used. The definitions file bundles the standing assumptions in IsRoutingScheme and source-obliviousness in IsSourceOblivious.

The paper's probabilities are informal. The following readings are explicit:

• every non-target node forwards with total probability one (implicit in the paper; without it Lemma 1 fails);
• the target forwards nothing;
• the paper's convention $R(\oslash,v,v,\oslash)=1$ is not adopted (it contradicts loop-freeness); collapsing consecutive repetitions in $S$ reproduces its only use;
• the "don't care" source $\oslash$ of Eq. (9) is an arbitrary fixed node, harmless under source-obliviousness;
• the printed index slips in Eqs. (16) and (17) are corrected;
• no sign condition is imposed on $T$; $0\le\rho_v\le1$ is kept in the goal as on the page.

Defining $\tilde\delta$ by the recursion (3) or the product (16), the target sequence dependency by (17), or the sequence RBC as the sum over targets of the chained product would make the goal true by definition; every dependency here is a sum of route probabilities, and the RBC of a sequence is the double sum of Eq. (4).

The running-time claims of the paper are out of scope. Lemma 2 of the paper (p. 17) is false as printed for a nonempty monitor set and is not posed. Contributions welcome: proofs of the milestones, a general lemma that the total route probability from any node is one under a total loop-free scheme (reusable for absorbing Markov chains on finite DAGs), and the prefix–suffix decomposition of routes.

Selected references

• S. Dolev, Y. Elovici, R. Puzis, Routing Betweenness Centrality, Technical Report #2009-09, Ben-Gurion University of the Negev, 2009; J. ACM 57(4), 2010. https://doi.org/10.1145/1734213.1734219
• L. C. Freeman, A set of measures of centrality based on betweenness, Sociometry 40(1), 1977. https://doi.org/10.2307/3033543
• U. Brandes, A faster algorithm for betweenness centrality, J. Math. Sociology 25(2), 2001. https://doi.org/10.1080/0022250X.2001.9990249
• L. C. Freeman, S. P. Borgatti, D. R. White, Centrality in valued graphs: a measure of betweenness based on network flow, Social Networks 13, 1991. https://doi.org/10.1016/0378-8733(91)90017-N
• M. E. J. Newman, A measure of betweenness centrality based on random walks, Social Networks 27, 2005. https://doi.org/10.1016/j.socnet.2004.11.009
• K.-I. Goh, B. Kahng, D. Kim, Universal behavior of load distribution in scale-free networks, Phys. Rev. Lett. 87, 2001. https://doi.org/10.1103/PhysRevLett.87.278701
• M. G. Everett, S. P. Borgatti, The centrality of groups and classes, J. Math. Sociology 23(3), 1999. https://doi.org/10.1080/0022250X.1999.9990219

Motivation

Treewidth measures how closely a graph resembles a tree. Many problems that are NP-hard on general graphs can be solved in time linear in the number of vertices once a tree decomposition of bounded width is available, so computing such decompositions quickly is a basic task in algorithmic graph theory. Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (SIAM J. Comput. 45(2), 2016) gave an algorithm that, for a graph $G$ on $n$ vertices and an integer $k$, either reports that the treewidth of $G$ exceeds $k$ or returns a tree decomposition of width at most $5k+4$, in time $2^{O(k)} n$.

The paper's headline is that algorithm, a statement about pseudo-code and running times. This mission does not formalize it. It formalizes one of the paper's combinatorial lemmas, Lemma 6.5 (p. 369), which the algorithm's data structure uses to answer its balanced-separator query: it turns the search for a small balanced separator into two maximization problems that a dynamic program can solve.

Timeline. Robertson and Seymour (Graph Minors II, J. Algorithms 7, 1986) proved that graphs of treewidth $k$ have balanced separators of size $k+1$ (Lemma 2.1 of the paper). Robertson and Seymour (Graph Minors XIII, 1995) used it in an $O(3^{3k} n^2)$ approximation algorithm, Reed (1992) improved the dependence on $n$ to $n \log n$, and Bodlaender et al. (2016) reached linear time with a single-exponential dependence on $k$.

Setting

All graphs are finite and simple. For $X \subseteq V(G)$, $G \setminus X$ is the graph obtained by deleting $X$; its components are the vertex sets of its connected components.

A separation of $G$ is a partition $(L, X, R)$ of $V(G)$ (parts may be empty) such that no edge of $G$ joins $L$ to $R$. Its order is $|X|$. It is $\alpha$-balanced if $|L|, |R| \le \alpha|V(G)|$.

For $W \subseteq V(G)$ and sets of terminals $T_L, T_R$, a terminal separation of the induced subgraph $G[W]$ of order $\ell$ (Definition 6.4) is a partition $(L, X, R)$ of $W$ with

$$T_L \subseteq L,\qquad T_R \subseteq R,\qquad \text{no edge between } L \text{ and } R,\qquad |X| \le \ell.$$

It is left-pushed if $|L|$ is maximum, and right-pushed if $|R|$ is maximum, among all terminal separations of $G[W]$ of order $\ell$ with the same terminals.

The treewidth $\mathrm{tw}(G)$ is the least width of a tree decomposition of $G$ (Definition 1.1), where the width is the largest bag size minus one.

Formalization targets

Goal: Lemma 6.5

Let $\mathrm{tw}(G) \le k$ and let $(A_1, B, A_2)$ be a separation of $G$ with $|A_1|, |A_2| \le \tfrac34|V(G)|$. Then there are a partition $(T_L, X_B, T_R)$ of $B$ and integers $k_1, k_2$ with $k_1 + k_2 + |X_B| \le k+1$ such that, for $G_i = G[A_i \cup (B \setminus X_B)]$ with terminals $T_L, T_R$,

1. $G_1$ and $G_2$ have terminal separations of orders $k_1$ and $k_2$;
2. for every left-pushed $(L_1, X_1, R_1)$ of order $k_1$ in $G_1$ and every right-pushed $(L_2, X_2, R_2)$ of order $k_2$ in $G_2$, the triple $(L_1 \cup T_L \cup L_2,\ X_1 \cup X_B \cup X_2,\ R_1 \cup T_R \cup R_2)$ is a terminal separation of $G$ of order at most $k+1$ with

$$|L_1 \cup T_L \cup L_2|,\ |R_1 \cup T_R \cup R_2| \le \tfrac78|V(G)| + \frac{|B| + (k+1)}{2}.$$

Milestones

In the order of the proof, the milestones are: Lemma 2.1 (balanced $S$-separators of size $k+1$, cited from Graph Minors II); the packing step of the proof sketch of Lemma 2.2 (components holding at most $\tfrac12|S|$ of $S$ each split into two sides holding at most $\tfrac23|S|$ each); the folklore $\tfrac23$-balanced separation of order $k+1$; the restriction of that separation to $G_1, G_2$, which gives part (i); four lower bounds on $|L \cap A_i|$, $|R \cap A_i|$; the dichotomy that two opposite "quadrants" have at least $\tfrac18|V(G)| - \tfrac{|B|+(k+1)}{2}$ vertices each; the comparison of pushed separations with the restricted one; and the gluing step of part (ii).

Significance

Lemma 6.5 is what makes the paper's balanced-separator query computable: given a bag $B$ that splits a component in a balanced way, a left-pushed and a right-pushed terminal separation are each the solution of a maximization problem, and the lemma guarantees that gluing them gives a separator of order $k+1$ whose sides are bounded away from $|V(G)|$. The $\tfrac78$ constant feeds into the approximation ratio of the whole algorithm.

The proof is complete in the paper and elementary given Lemma 2.1. No part of it is formalized in Lean's Mathlib or, as far as a search of the Prove2Me catalog shows, on the platform. Lemma 2.1 itself, Robertson and Seymour's balanced-separator theorem for bounded treewidth, is not in Mathlib; a machine-checked proof of it would be reusable wherever treewidth separators are used (divide-and-conquer on tree decompositions, Lipton–Tarjan style arguments, grid-minor theorems).

Difficulty

Everything after Lemma 2.1 is counting with partitions, but the bookkeeping is the obstacle: the two separations $(A_1, B, A_2)$ and $(L, X, R)$ cut $V(G)$ into nine pieces, the induced subgraphs $G_1, G_2$ overlap on $B \setminus X_B$, and pushedness is a maximum over a family of partitions of a subset, not of $V(G)$.

Lemma 2.1 is the hard milestone. It is a statement about tree decompositions, and any proof has to relate subtrees of the decomposition tree to components of $G \setminus X$ for a bag $X$, infrastructure that does not yet exist in Mathlib.

Formalization scope

• Vertices. A finite type V : Type with decidable equality; vertex sets are Finset V, $V(G)$ is Finset.univ, $|V(G)|$ is Fintype.card V. Universe 0 matches the published definition of treewidth.
• Treewidth. "$\mathrm{tw}(G) \le k$" is the published RobertsonSeymour1986.GM5.TreewidthLE G k: a decomposition tree on a finite type whose bags have at most $k+1$ vertices. Definition 1.1 roots the tree; rooting does not change the width.
• Components of $G \setminus X$. The component of $u \notin X$ is avoidComp G X u: the vertices reachable from $u$ by a walk of $G$ none of whose vertices, endpoints included, lies in $X$.
• Partitions are pairwise disjoint triples with the given union; empty parts are allowed.
• Induced subgraphs $G[W]$ are encoded by their vertex set $W$: a terminal separation of $G[W]$ is a partition of $W$, with $G$'s adjacency restricted to $W$. Pushedness maximizes over partitions of $W$ only.
• "Of order $\ell$" means $|X| \le \ell$, as in Definition 6.4 (iii).
• Arithmetic. Bounds with fractions or subtraction ($\tfrac34$, $\tfrac23$, $\tfrac78$, $\tfrac18|V(G)| - \tfrac{|B|+(k+1)}{2}$) are stated over $\mathbb R$; bounds without subtraction may be cleared of denominators in $\mathbb N$ ($2|C \cap S| \le |S|$, $3|L' \cap S| \le 2|S|$).
• Corrections of the page. The printed bound of Lemma 6.5 has $|X|$ where the proof derives $|B|$; the goal states $|B|$. The proof's "$\tfrac14$- and $\tfrac13$-balanced" means $\tfrac34$ and $\tfrac23$; the milestone uses the latter.

Part (i) is part of the goal: without it, left- and right-pushed separations of the chosen orders might not exist and part (ii) would hold vacuously. Choosing $X_B = B$ does not trivialize the goal, because the size bound and the budget $k_1 + k_2 + |X_B| \le k+1$ must hold simultaneously.

Welcome contributions: a proof of Lemma 2.1 from tree decompositions (reusable on its own), the packing lemma, and the counting milestones of the proof of Lemma 6.5.

Selected references

• H. L. Bodlaender, P. G. Drange, M. S. Dregi, F. V. Fomin, D. Lokshtanov, M. Pilipczuk, A $c^k n$ 5-approximation algorithm for treewidth, SIAM J. Comput. 45(2):317–378, 2016. https://doi.org/10.1137/130947374
• N. Robertson, P. D. Seymour, Graph minors. II. Algorithmic aspects of tree-width, J. Algorithms 7(3):309–322, 1986. https://doi.org/10.1016/0196-6774(86)90023-4
• N. Robertson, P. D. Seymour, Graph minors. XIII. The disjoint paths problem, J. Combin. Theory Ser. B 63(1):65–110, 1995. https://doi.org/10.1006/jctb.1995.1006
• B. A. Reed, Finding approximate separators and computing tree width quickly, STOC 1992, 221–228. https://doi.org/10.1145/129712.129734

Motivation

Graph coloring asks whether vertices can be assigned colors so that adjacent vertices receive different colors. Restricting the graphs by forbidden induced paths can expose structure that is absent from general graphs. Bonomo, Chudnovsky, Maceli, Schaudt, Stein and Zhong study list three-coloring when the graph has no induced path on seven vertices, building on earlier work on coloring graphs with shorter forbidden induced paths. Their paper proves an algorithmic result, but its treatment also uses a purely graph-theoretic statement: a connected $P_7$-free graph has a small connected set that reaches every vertex within two steps, unless the graph contains a four-vertex clique. This mission isolates that statement as Corollary 5 of the paper.

The structural input to the corollary is a theorem of Camby and Schaudt about connected dominating sets in $P_t$-free graphs, quoted as Theorem 4 in the coloring paper. That result applies to every allowed path length $t$, rather than only to the seven-vertex case. It is a milestone here in the precise form printed in the source article. The Camby–Schaudt paper develops connected domination as a characterization of graphs without long induced paths.

Setting

A simple graph $G$ has a vertex set $V(G)$ and an undirected edge relation with no loops. The graphs in this mission are finite. The path $P_t$ has $t$ vertices and consecutive vertices adjacent. A graph is $P_t$-free when it has no induced subgraph isomorphic to $P_t$: the graph may contain a path with $t$ vertices as a non-induced subgraph if extra edges join vertices of that path. This distinction matters throughout the source paper.

For a vertex set $S$, its open neighborhood $N(S)$ consists of vertices outside $S$ with a neighbor in $S$. Write $\bar S=S\cup N(S)$. The set $S$ is dominating when $\bar S=V(G)$, so each vertex lies in $S$ or has an edge to $S$. It is 2-dominating when $\overline{\bar S}=V(G)$, meaning each vertex is at graph distance at most two from some vertex of $S$. A dominating or 2-dominating set is connected when the subgraph $G[S]$ induced by $S$ is connected. In this mission, connectedness includes nonemptiness, as in the paper's use of such sets.

A clique of size four is a set of four pairwise adjacent vertices. The notation $K_4\subseteq G$ below asserts the existence of such a set. Since all edges between those four vertices are present, it is also an induced complete subgraph. The notation $G[S]\cong P_{t-2}$ means there is a graph isomorphism from the induced graph on $S$ to that path.

Formalization targets

Corollary 5: a small connected 2-dominating set or a clique

For a finite, connected, $P_7$-free graph $G$, the goal is

$$\left(\exists S\subseteq V(G): |S|\le 3,\;G[S]\text{ connected},\; \overline{\bar S}=V(G)\right)\quad\lor\quad K_4\subseteq G.$$

The four-vertex clique is a genuine alternative in the claim; the mission does not assume its absence. The result is the first, structural sentence of Corollary 5. Its following sentence gives a running time for finding the set or clique and is outside this mission.

Theorem 4: connected domination across forbidden path lengths

For every $t\ge 3$, the cited theorem asserts that each finite connected $P_t$-free graph has a connected dominating set $S$ for which

$$G[S]\text{ is }P_{t-2}\text{-free}\quad\lor\quad G[S]\cong P_{t-2}.$$

The other milestones are statements identified in the proof of Corollary 5: a connected $P_3$-free graph is complete, domination inside a dominating set yields 2-domination in the original graph, and the three non-leaf vertices work when the induced dominating graph is a $P_5$. These are listed in the paper's order of use, with the quoted theorem also available as a separate target.

Significance

Corollary 5 gives a bounded set of vertices from which the rest of a connected $P_7$-free graph can be reached in two steps, except when a $K_4$ is present. Its bound is the concrete number three, independent of graph size. In the coloring paper this supplies a small structural seed for later restrictions on vertex palettes. A formal statement of the corollary makes that finite structural claim available independently of any coloring algorithm.

Theorem 4 has broader reuse: it links forbidden induced paths to connected dominating sets for general $t$. The remaining milestones isolate the graph facts needed to connect this general result to the seven-vertex corollary. The article and the cited theorem provide mathematical proofs; these Lean declarations are open theorem statements, with machine-checked proofs still to be supplied. This mission therefore asks for formal proofs of known graph-theoretic results, not for a new resolution of an open mathematical problem.

Difficulty

The difficult step is finding a connected dominating set whose induced graph has the much stronger path restriction in Theorem 4. Ordinary domination by itself does not impose that restriction, and replacing induced-path exclusion with exclusion of all paths would change the class of graphs. The later cases require careful handling of connectedness and the passage from domination within $G[S]$ to distance-two domination in $G$. These issues are mathematical as well as formal: an empty set or a merely preconnected induced graph would erase the intended content.

Formalization scope

Lean represents $G$ as SimpleGraph V with a finite vertex type. Vertex sets are Finset V; $P_t$ is Mathlib's pathGraph t; $P_t$-freeness is the absence of an induced copy using IsIndContained. The definitions of $N(S)$, $\bar S$, domination and 2-domination are shared within P7ThreeColor.Seed. A connected induced graph uses Connected, which requires at least one vertex. Four-clique existence is ¬ G.CliqueFree 4. The only added standing convention is finiteness, implicit in the source's graph algorithm and finite cardinalities. No extra colorability or clique-free hypothesis is attached to the goal.

The running-time claim in the second sentence of Corollary 5 and the paper's headline Theorem 1 are not formalized because this mission has no machine model. A statement that merely postulates a small set as a hypothesis, or substitutes ordinary domination for 2-domination, would miss the result. Contributions are welcome for proofs of the goal and milestones, reusable facts about induced paths and connected domination, and auxiliary Mathlib lemmas needed to cross between graph isomorphisms, induced subgraphs and finite sets.

Selected references

• F. Bonomo, M. Chudnovsky, P. Maceli, O. Schaudt, M. Stein and M. Zhong, Three-coloring and list three-coloring of graphs without induced paths on seven vertices, Combinatorica, OnlineFirst 2017, DOI: 10.1007/s00493-017-3553-8.
• E. Camby and O. Schaudt, A new characterization of $P_k$-free graphs, Algorithmica 75 (2016), 205–217, DOI: 10.1007/s00453-015-9989-6; arXiv:1402.7213.

Interacting diffusions on large weighted graphs

Classical mean field theory describes $n$ exchangeable diffusions, each interacting with the empirical average of all the others. As $n\to\infty$ the particles become independent copies of a McKean–Vlasov process (propagation of chaos). Many systems of interest are not exchangeable. Particles sit at the vertices of a network and interact only with their neighbours, as in models of opinion dynamics, epidemics on contact networks, synchronisation of oscillators and systemic risk in financial networks. When the network is dense and its adjacency structure converges, the natural limit object is a graphon, a symmetric measurable function $G:[0,1]^2\to[0,1]$ that encodes the limiting edge density between "positions" $u,v\in[0,1]$ (Lovász, Large Networks and Graph Limits, 2012).

Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) develop a law of large numbers for such systems. This mission formalizes their second main result, Theorem 3.1. Under cut-metric convergence of the interaction kernels, the empirical measure of the $n$-particle system converges in probability to the averaged law of a continuum graphon particle system. Related work includes Bhamidi, Budhiraja and Wu (Stochastic Process. Appl., 2019) on weakly interacting particles on inhomogeneous random graphs, Coppini, Dietert and Giacomin (Stoch. Dyn., 2020) on Erdős–Rényi graphs, and Bet, Coppini and Nardi (arXiv:2006.07670) on oscillators on dense random graphs.

Setting

Write $I=[0,1]$ with Lebesgue measure and fix a horizon $T>0$. Let $\mathcal C_d=C([0,T]:\mathbb R^d)$ with the uniform norm $\|x\|_{*,T}=\sup_{s\le T}|x_s|$. On one probability space take independent initial states $X_u(0)$ with laws $\mu_u(0)$ and independent $d$-dimensional Brownian motions $B_u$, for all $u\in I$. The graphon particle system (2.1) for a graphon $G$ and Lipschitz coefficients $b,\sigma$ is the continuum of nonlinear diffusions

$$X_u(t)=X_u(0)+\int_0^t\!\!\int_I\!\int_{\mathbb R^d}b(X_u(s),x)G(u,v)\,\mu_{v,s}(dx)\,dv\,ds+\int_0^t\!\!\int_I\!\int_{\mathbb R^d}\sigma(X_u(s),x)G(u,v)\,\mu_{v,s}(dx)\,dv\,dB_u(s),$$

where $\mu_{v,s}$ is the law of $X_v(s)$. Write $\mu_u\in\mathcal P(\mathcal C_d)$ for the path law of $X_u$ and $\bar\mu=\int_I\mu_u\,du$ for the averaged law.

The $n$-particle system (3.1) places particle $i$ at label $i/n$, starts it at $X_{i/n}(0)$, drives it by $B_{i/n}$, and weights its interaction with particle $j$ by $\xi^n_{ij}$:

$$X^n_i(t)=X_{i/n}(0)+\int_0^t\frac1n\sum_{j=1}^n\xi^n_{ij}\,b(X^n_i(s),X^n_j(s))\,ds+\int_0^t\frac1n\sum_{j=1}^n\xi^n_{ij}\,\sigma(X^n_i(s),X^n_j(s))\,dB_{i/n}(s).$$

The weights come from a step graphon $G_n$, constant on the squares of the $n$-grid. Either $\xi^n_{ij}=G_n(i/n,j/n)$, or $\xi^n_{ij}=\xi^n_{ji}$ are independent Bernoulli$(G_n(i/n,j/n))$ variables for $i\le j$, independent of the noise (Condition 3.1). The kernels converge in the cut norm $\|W\|_\square=\sup_{S,T}\big|\int_{S\times T}W\big|$. Two further norms appear: the operator norm $\|W\|=\sup_{\|g\|_\infty\le1}\int_I|\int_I W(u,v)g(v)\,dv|\,du$, and the Wasserstein-2 distance $W_{2,T}$ on $\mathcal P(\mathcal C_d)$.

Formalization targets

Goal: Theorem 3.1

Assume the initial laws are measurable in $u$ with a uniform $(2+\varepsilon)$-moment and $b,\sigma$ are Lipschitz (Condition 2.1). Assume $u\mapsto\mu_u(0)$ is $W_2$-continuous on each interval of a finite cover of $I$ (Condition 2.2(a)), and that Condition 3.1 holds with $G_n\to G$ in the cut metric. Then

$$\mu^n:=\frac1n\sum_{i=1}^n\delta_{X^n_i}\longrightarrow\bar\mu\quad\text{in }\mathcal P(\mathcal C_d)\text{ in probability}.$$

If, in addition, $G$ is continuous at $(u,v)$ for a.e. $v$ at each interior point $u$ of the cover (Condition 2.2(b)), then

$$\frac1n\sum_{i=1}^n\mathbb E\|X^n_i-X_{i/n}\|^2_{*,T}\longrightarrow0 .$$

Milestones

In order: Remark 2.1, where cut-norm convergence implies operator-norm convergence; Theorem 2.1(a), continuity of $u\mapsto\mu_u$ in $W_{2,T}$; the weak-LLN bound (6.4); the discretization bound (6.11); Lemma 6.1,

$$\limsup_{n}\frac1n\sum_i\mathbb E\|X^n_i-X_{i/n}\|^2_{*,T}\le\kappa(M)\limsup_n\|G_n-G\|+\kappa M^{-\varepsilon};$$

Lemma 6.2, a law of large numbers for the continuum particles $X_{1/n},\dots,X_{n/n}$; the approximation of $G$ by continuous graphons; the continuity (6.12) of $\bar\mu$ in the graphon, in a corrected qualitative form; the empirical coupling bound for $W_{2,T}$; and (6.14).

Significance

Theorem 3.1 shows that the averaged graphon law $\bar\mu$ is the correct macroscopic description of a dense heterogeneous particle system. This holds for deterministic weights and for Erdős–Rényi-type random weights, and the graphon may be discontinuous. It is the foundation for graphon mean field games and for control of large networked systems, where $\bar\mu$ replaces the intractable $n$-particle law. Under the regularity Condition 2.2(b) the convergence holds in $L^2$, particle by particle, along the natural coupling.

The result is proved in the paper (§6.1–§6.2). Nothing in it is formalized. A formal proof would produce reusable infrastructure: graphons, the cut and operator norms, Lusin approximation of graphons, Wasserstein distances between empirical measures, and laws of large numbers for random probability measures on path space. It also needs pathwise stability estimates for SDE systems built on Itô integrals, which goes well beyond what Mathlib has today.

Difficulty

The particles are neither exchangeable nor identically distributed. The classical propagation-of-chaos argument compares each particle with an i.i.d. copy of one McKean–Vlasov process, and it does not apply here. Each $X^n_i$ must be compared with its own limit $X_{i/n}$, and the error has two sources: the random or discretized weights $\xi^n_{ij}$, and the replacement of $G$ by $G_n$. Cut-metric convergence controls $G_n-G$ only through integrals against bounded test functions. The interaction term, however, integrates the unbounded function $b(X_{i/n}(s),\cdot)$ against varying laws $\mu_{j/n,s}$. When $G$ is merely measurable, the map $u\mapsto\mu_u$ need not be continuous, and the error of replacing $\int_I\cdot\,dv$ by the average over the labels $j/n$ need not vanish. The direct estimate therefore fails for (3.3) without Condition 2.2(b), and this is the case the goal must cover.

Formalization scope

The setting file GraphonMF.DenseLLN.Setting fixes these conventions:

• $\mathbb R^d$ is Fin d → ℝ with the sup norm. All statements are invariant under this choice: constants are existential and the other conclusions are limits.
• Processes are path-valued maps $\Omega\to\mathcal C_d$, and $\mathcal C_d$ carries its Borel σ-algebra.
• Each SDE is encoded through the published Itô-process predicate Peng1990.SMP.IsItoProcess. The filtrations are the uncompleted natural filtrations $\sigma(X_u(0),B_u(r):r\le t)$ and $\sigma(\xi^n,X_{j/n}(0),B_{j/n}(r):j\le n,r\le t)$.
• A solution of (2.1) carries the membership of its law family in the class $\mathcal M$ (measurable in $u$, uniformly bounded second moments), which makes every Bochner integral of the drift meaningful.
• $W_2$ and $W_{2,T}$ are the published WassersteinDRO.Duality.wassersteinDistance with values in $[0,\infty]$.
• Expectations of nonnegative quantities are lower Lebesgue integrals.
• Convergence in probability is topological: $\mathbb P(\mu^n\notin U)\to0$ for every weak-topology neighbourhood $U$ of $\bar\mu$.
• The $n$-particle system shares the noise of the graphon system: particle $i$ (Lean index $i$, label $(i+1)/n$) uses $X_{(i+1)/n}(0)$ and $B_{(i+1)/n}$.
• Each $\xi^n$ is assumed measurable.

Two encodings would trivialize the targets, and both are ruled out. A pointwise or almost-sure reading of (3.3), or convergence of $\int f\,d\mu^n$ for a single test function, is not the claim. Choosing the constants of Lemma 6.1 and (6.11) after the sequence $(G_n)$ would make them nearly empty, so they are chosen before it. A sorry-free check confirms that the solution predicates are satisfiable: with $b=\sigma=0$ the constant paths solve both systems.

Solvers will need several pieces of library work: the inequality $\|W\|_{\infty\to1}\le4\|W\|_\square$, BDG-type moment bounds for the Itô integrals of Peng's library, Gronwall estimates, Lusin's theorem on $[0,1]^2$, and the metrization of weak convergence on $\mathcal P(\mathcal C_d)$ (Lévy–Prokhorov). Contributions to any of these are welcome independently of the goal. The paper's proofs are in its §5 (Theorem 2.1) and §6.1–§6.2 (Lemmas 6.1, 6.2 and Theorem 3.1).

Selected references

• E. Bayraktar, S. Chakraborty, R. Wu, Graphon mean field systems, Ann. Appl. Probab. 33(5):3587–3619, 2023. https://doi.org/10.1214/22-AAP1901
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60, 2012. https://doi.org/10.1090/coll/060
• S. Bhamidi, A. Budhiraja, R. Wu, Weakly interacting particle systems on inhomogeneous random graphs, Stochastic Process. Appl. 129:2174–2206, 2019. https://doi.org/10.1016/j.spa.2018.06.014
• F. Coppini, H. Dietert, G. Giacomin, A law of large numbers and large deviations for interacting diffusions on Erdős–Rényi graphs, Stoch. Dyn. 20:2050010, 2020. https://doi.org/10.1142/S0219493720500100
• G. Bet, F. Coppini, F. R. Nardi, Weakly interacting oscillators on dense random graphs, arXiv preprint, 2020. https://arxiv.org/abs/2006.07670
• A.-S. Sznitman, Topics in propagation of chaos, École d'Été de Probabilités de Saint-Flour XIX, LNM 1464, 1991. https://doi.org/10.1007/BFb0085169

Interacting diffusions on large heterogeneous networks

Classical mean-field theory describes $n$ diffusions that interact symmetrically, each feeling the empirical average of all the others, and shows that as $n\to\infty$ every particle behaves like an independent copy of a single McKean–Vlasov process. Many systems of interest are not symmetric: neurons, agents in a financial network, or oscillators interact through a graph, and particles in different parts of the graph feel different neighbourhoods. A graphon $G:[0,1]^2\to[0,1]$ is the limit object of dense graph sequences (Lovász, Large Networks and Graph Limits, AMS 2012), and it is the natural way to describe the interaction structure of such systems in the limit.

Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) study a continuum of diffusions indexed by labels $u\in[0,1]$ whose interaction is weighted by a graphon, and prove laws of large numbers and rates of convergence for $n$-particle systems on graphs sampled from the graphon. This mission targets their uniform rate of convergence for weights sampled from a Lipschitz graphon (Theorem 3.2).

Setting

Write $I=[0,1]$ with Lebesgue measure. Fix a horizon $T\in(0,\infty)$ and let $\mathcal C_d=C([0,T]:\mathbb R^d)$ with $\|x\|_{*,t}=\sup_{0\le s\le t}|x_s|$.

On one probability space, $\{B_u:u\in I\}$ are i.i.d. $d$-dimensional Brownian motions and $\{X_u(0):u\in I\}$ are independent initial states with laws $\mu_u(0)$, independent of the Brownian motions. Given a graphon $G$ and coefficients $b,\sigma$, the graphon particle system (2.1) is

$$X_u(t)=X_u(0)+\int_0^t\!\!\int_I\!\int_{\mathbb R^d}b(X_u(s),x)G(u,v)\,\mu_{v,s}(dx)\,dv\,ds+\int_0^t\!\!\int_I\!\int_{\mathbb R^d}\sigma(X_u(s),x)G(u,v)\,\mu_{v,s}(dx)\,dv\,dB_u(s),$$

with $\mu_{u,t}=\mathcal L(X_u(t))$. The particles are independent but not identically distributed, and their laws are coupled through the $dv$-integral.

The $n$-particle system (3.1) uses the same randomness at the labels $i/n$:

$$X^n_i(t)=X_{i/n}(0)+\int_0^t\frac1n\sum_{j=1}^n\xi^n_{ij}\,b(X^n_i(s),X^n_j(s))\,ds+\int_0^t\frac1n\sum_{j=1}^n\xi^n_{ij}\,\sigma(X^n_i(s),X^n_j(s))\,dB_{i/n}(s),$$

so particle $i$ and the continuum particle at $u=i/n$ share their initial state and Brownian motion.

The hypotheses are:

• Condition 2.1: $u\mapsto\mu_u(0)$ is measurable, $\sup_u\mathbb E|X_u(0)|^{2+\varepsilon}<\infty$ for some $\varepsilon>0$, and $b$, $\sigma$ are Lipschitz in both arguments.
• Condition 2.3: there are finitely many intervals $I_1,\dots,I_N$ covering $I$ and a $\kappa>0$ with $W_2(\mu_{u_1}(0),\mu_{u_2}(0))\le\kappa|u_1-u_2|$ on each $I_i$ and $|G(u_1,v_1)-G(u_2,v_2)|\le\kappa(|u_1-u_2|+|v_1-v_2|)$ on each block $I_i\times I_j$. The graphon may jump across block boundaries.
• Condition 3.2: the weights are sampled from $G$ itself, either deterministically, $\xi^n_{ij}=G(i/n,j/n)$, or as a random graph, $\xi^n_{ij}=\xi^n_{ji}\sim\mathrm{Bernoulli}(G(i/n,j/n))$ independently for $i\le j$ and independently of the noise.

Formalization targets

Goal: Theorem 3.2 (p. 3596)

Under Conditions 2.1, 2.3 and 3.2 there is $\kappa\in(0,\infty)$ such that

$$\max_{i=1,\dots,n}\mathbb E\|X^n_i-X_{i/n}\|^2_{*,T}\le\frac{\kappa}{n}\qquad\forall n\in\mathbb N.$$

Milestones (§6.3, in attack order)

• (6.15): $\mathbb E\|X^n_i-X_{i/n}\|^2_{*,t}$ is bounded by $\kappa$ times the time-integrated mean-square mismatch between the finite-$n$ drift and diffusion and their graphon counterparts.
• The drift mismatch is split by (6.16) into three terms $\tilde T^{n,1}_s,\tilde T^{n,2}_s,\tilde T^{n,3}_s$, bounded by

$$\tilde T^{n,1}_s\le2\kappa\max_i\mathbb E|X^n_i(s)-X_{i/n}(s)|^2\ \ (6.17),\qquad\tilde T^{n,2}_s\le\frac{\kappa}{n}\ \ (6.18),\qquad\tilde T^{n,3}_s\le\frac{\kappa}{n^2}\ \ (6.19).$$

• Theorem 2.1(b) (p. 3593): under Condition 2.3, $W_{2,T}(\mu_u,\mu_v)\le\kappa|u-v|$ whenever $u,v$ lie in the same interval $I_i$. It is used in (6.19).

Significance

The result. Theorem 3.2 gives a quantitative propagation of chaos for heterogeneous interactions: with weights sampled from a blockwise Lipschitz graphon, every particle of the finite system, not just an average particle, is within $O(n^{-1/2})$ in root-mean-square path distance of the continuum particle with the same label. The rate matches the classical mean-field rate (e.g. Sznitman 1991), so heterogeneity of the interaction costs nothing in the exponent. The same estimate covers the deterministic weighted graph and the random graph sampled from $G$ (in the annealed sense), and it is the dense counterpart of Theorem 4.2 for percolated graphs.

Formalizing it. The result is proved in the paper (§6.3); it has no machine-checked proof. A formal development would produce a reusable account of graphon particle systems and their finite-$n$ approximations: graphon-weighted McKean–Vlasov drifts, couplings through shared noise, and the decomposition of the interaction error into a Lipschitz feedback term, a law-of-large-numbers term and a Riemann-sum discretization term.

Difficulty

The obvious approach is to compare $X^n_i$ with $X_{i/n}$ directly and close a Gronwall inequality. The difficulty is that the comparison involves the empirical, graph-weighted average of the other particles, which is neither the graphon average nor an average of independent terms. Three different errors must be controlled simultaneously and uniformly in $i$: the feedback of all particles' errors into particle $i$, the fluctuation of a sum of independent but non-identically distributed terms whose weights may themselves be random, and the error of replacing an integral over labels by a sum over the grid $\{j/n\}$. The last needs regularity of the law $\mu_u$ in the label $u$, which is itself a theorem about the graphon system (Theorem 2.1(b)) and fails at block boundaries of $G$, where only the small number of boundary cells saves the $1/n^2$ rate. Averaging over $i$, as in the law of large numbers of Theorem 3.1, is not enough: the goal bounds the maximum.

Formalization scope

• $\mathbb R^d$ is Fin d → ℝ with the sup norm; matrices are measured entrywise. All statements are norm-invariant because every constant is existential. Particle $i\in\{1,\dots,n\}$ is Lean's i : Fin n with label $(i+1)/n$; time is ℝ≥0; $I$ is Mathlib's unitInterval.
• Brownian motions, Itô integrals and Itô processes are the published Peng1990.SMP.Stochastic definitions; an SDE with random initial value $X(0)$ is stated as an Itô process for $X-X(0)$. Each continuum particle uses the natural filtration of $(X_u(0),B_u)$; the $n$-particle system uses the natural filtration of the weights, initial states and Brownian motions at the labels.
• $W_2$ and $W_{2,T}$ are the published WassersteinDRO.Duality.wassersteinDistance 2, valued in $[0,\infty]$; expectations of nonnegative quantities are lower Lebesgue integrals.
• A solution of (2.1) is required to have continuous paths, measurable path maps, and a law family in the class $\mathcal M$ (measurable in $u$, uniformly bounded second moments), as Proposition 2.1 asserts; this makes every inner integral meaningful.
• The constant $\kappa$ is chosen after the data and before $n$ and $i$. A $\kappa$ chosen after $n$, a bound on the average over $i$, or a solution predicate that no process satisfies would trivialize the goal; the first two are excluded by the statement, and a sanity check exhibits the zero-coefficient system as a solution of both systems.
• Condition 2.2 is not assumed, and the weights come from $G$, not from a step graphon $G_n$; no cut-metric hypothesis appears.
• Needed infrastructure: Doob/Burkholder–Davis–Gundy for Itô integrals, Gronwall's inequality in integrated form, moment bounds for the graphon system, Kantorovich–Rubinstein-type duality for Lipschitz test functions, and independence of functionals of independent noises. Proofs of the milestones, of Theorem 2.1(b), and of the goal are all welcome; the paper's proofs are in its §5–§6.

Selected references

• E. Bayraktar, S. Chakraborty, R. Wu, Graphon mean field systems, Ann. Appl. Probab. 33(5):3587–3619, 2023. https://doi.org/10.1214/22-AAP1901
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60, 2012. https://doi.org/10.1090/coll/060
• A.-S. Sznitman, Topics in propagation of chaos, École d'Été de Probabilités de Saint-Flour XIX, LNM 1464, Springer, 1991. https://doi.org/10.1007/BFb0085169
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4):966–979, 1990. https://doi.org/10.1137/0328054

Motivation

Large interacting diffusion systems often have different interaction strengths between different pairs of agents. A graphon gives a continuum description of such weighted networks: each agent carries a label in $[0,1]$, and a kernel assigns the strength of interaction between two labels. The question in this mission is whether the law of the resulting continuum stochastic system changes continuously when its graphon changes. This matters when a large finite network is represented by an approximate graphon, since an approximation of the network should lead to an approximation of the dynamics. Bayraktar, Chakraborty and Wu establish this stability as Theorem 2.1(c) of Graphon mean field systems.

The paper also studies dense and less dense finite-particle systems. Their convergence results use a limiting graphon particle system even when the limiting kernel is only measurable, with no continuity in the labels. Theorem 2.1(c) is the continuity result that makes approximation by simpler graphons useful in those later sections Bayraktar–Chakraborty–Wu, §§3–4.

Setting

Let $I=[0,1]$, fix a time horizon $T>0$, and let $\mathcal C_d=C([0,T];\mathbb R^d)$ be the space of continuous paths with the uniform norm $\|x\|_{*,t}=\sup_{0\le s\le t}|x_s|$. A graphon $G:I^2\to[0,1]$ is measurable and symmetric. Its cut norm is the largest absolute integral of $G$ over a measurable rectangle $S\times U\subseteq I^2$. For two graphons, their cut distance is the cut norm of their difference.

For each label $u\in I$, an initial state $X_u(0)$ and a $d$-dimensional Brownian motion $B_u$ live on one probability space. Initial states are mutually independent, Brownian motions are mutually independent, and the two families are independent of each other. The initial state has law $\mu_u(0)$. The process $X_u$ evolves with a drift obtained by averaging $b(X_u(s),x)G(u,v)$ first against the time-$s$ law of $X_v$ and then over $v\in I$. Its diffusion coefficient averages the matrix-valued $\sigma(X_u(s),x)G(u,v)$ in the same way and drives $B_u$. This is the graphon particle system (2.1) Bayraktar–Chakraborty–Wu, p. 3591.

Condition 2.1 requires measurable initial laws, a uniform $(2+\varepsilon)$ moment for some $\varepsilon>0$, and a common global Lipschitz bound for $b$ and $\sigma$. The path-law family $\mu=(\mathcal L(X_u))_{u\in I}$ belongs to $\mathcal M$ when it is measurable as a family of probability measures on $\mathcal C_d$ and has uniformly bounded second moments. The distance $W_{2,t}$ between path laws uses the supremum norm through time $t$; $W^\mathcal M_{2,t}$ is the supremum of these distances over labels Bayraktar–Chakraborty–Wu, pp. 3591–3592.

Formalization targets

Stability of path laws

For graphons $G_n$ converging to $G$ in cut metric, let $\mu^{G_n}_u$ and $\mu^G_u$ be the laws of the associated solutions, with the same initial laws and coefficients. The target is

$$\|G_n-G\|_\square\longrightarrow0 \quad\Longrightarrow\quad \int_I[W_{2,T}(\mu^{G_n}_u,\mu^G_u)]^2\,du\longrightarrow0.$$

The conclusion is an integrated law convergence statement. It does not assert that the laws converge uniformly in $u$ or that paths converge almost surely. This is precisely Theorem 2.1(c) Bayraktar–Chakraborty–Wu, p. 3593.

Supporting results

The mission also states the paper's cut-to-operator convergence (Remark 2.1), existence of frozen-flow solutions (5.2), the squared estimate established in the proof of (5.3), well-posedness and moments for the nonlinear system (Proposition 2.1), and the quantitative stability display on p. 3604. These are the source's claims used to reach the target, with their provenance attached to each milestone Bayraktar–Chakraborty–Wu, §§2 and 5.

Significance

Stability shows that the continuum model is robust to graphon approximation in a metric natural for dense networks. Together with Proposition 2.1, it gives a well-defined solution-law family whose dependence on the network kernel can be controlled. The paper uses this framework in its later laws of large numbers for finite interacting systems Bayraktar–Chakraborty–Wu, §§3–4.

The theorem is proved in the paper; this mission asks for a machine-checked proof of the faithful statements. A complete development would also supply reusable Lean interfaces for graphons, cut and operator norms, measurable families of path laws, and stochastic systems whose coefficients depend on those families. The Itô-process and general Wasserstein definitions already available as published modules are reused. The remaining graphon-specific definitions and the estimates in §5 are open proof targets.

Difficulty

A direct stability argument for stochastic differential equations would compare the two coefficients point by point. Cut convergence does not provide pointwise convergence of $G_n(u,v)$ to $G(u,v)$, nor a uniform bound on their difference that tends to zero. The drift and diffusion also contain laws generated by the processes being compared, so a change in the graphon feeds back into the law family. The central challenge is to control these coupled differences using only a weak kernel metric while retaining the measurable structure needed to integrate over labels Bayraktar–Chakraborty–Wu, §5.2.

The result also depends on a well-posedness theory for a continuum of stochastic equations. The laws need to vary measurably with $u$ even though the paper does not assume the sample paths themselves vary measurably with $u$ Bayraktar–Chakraborty–Wu, Remark 2.3(b).

Formalization scope

Lean uses unitInterval for $I$, nonnegative real time, and continuous maps from $[0,T]$ to Fin d → ℝ for $\mathcal C_d$. The norm on $\mathbb R^d$ is the sup norm; the paper's Euclidean norm is equivalent in finite dimension, so existential Lipschitz and stability constants may change while the qualitative claim remains the same. The diffusion coefficient is a $d\times d$ matrix, measured through its entries. Wasserstein quantities and nonnegative expectations are valued in $[0,\infty]$, avoiding defaults for infinite moments. The path-law family uses the measurable space of measures, with the Borel space on paths. A zero-time or zero-dimensional state space is admitted where the formulas still have their stated meaning; $T>0$ and $\varepsilon>0$ are explicit.

For each graphon, a solution is a continuous-path process driven by the same given initial variables and Brownian motions, adapted to the natural filtration of those variables for each label. Its path map is almost everywhere measurable, its law family belongs to $\mathcal M$, and the nested interaction integrals are required to be integrable. These clauses prevent a zero measure from arising through a nonmeasurable pushforward and prevent a nonintegrable Bochner integral from silently evaluating to zero. The graphons are explicitly measurable, symmetric, and $[0,1]$-valued, so the real cut and operator norms are used only on bounded kernels. The theorem also asserts measurability of each Wasserstein integrand, reflecting the paper's treatment of the displayed integral.

The paper's proofs are in §§5–7; this mission concerns §5. Contributions to any stated milestone and to the reusable measure and Itô lemmas needed for them are welcome. A formalization that assumes the stability limit, that treats arbitrary unbounded kernels as graphons, or that uses an empty solution class would not establish this target.

Selected references

• E. Bayraktar, S. Chakraborty and R. Wu, Graphon mean field systems, Annals of Applied Probability 33(5), 3587–3619, 2023. DOI 10.1214/22-AAP1901.

Two classical extremal problems and their common generalization

Two of the oldest results in extremal graph theory bound the number of edges of a graph under a single structural restriction. Turán's theorem (Turán 1941) determines the maximum number of edges $t(n,k)$ of an $n$-vertex graph with no complete subgraph on $k+1$ vertices. The Erdős–Gallai theorem (Erdős and Gallai 1959) determines the maximum number of edges of an $n$-vertex graph with no $s+1$ pairwise disjoint edges; for $n\ge 2s+1$ it is $\max\{\binom{2s+1}{2},\binom{s}{2}+s(n-s)\}$, attained by a clique on $2s+1$ vertices plus isolated vertices, or by $s$ vertices joined to everything.

N. Alon and P. Frankl (arXiv:2210.15076, published in J. Combin. Theory Ser. B, 2024, DOI 10.1016/j.jctb.2023.12.002) impose both restrictions at once and determine the maximum for all values of the parameters. Their answer is again the larger of two explicit constructions, and each of the two classical theorems is recovered as a degenerate range of theirs. The question belongs to a line of work on generalized Turán problems with an additional bound on the matching number, which has continued since this paper with other forbidden subgraphs in place of the clique.

Setting

All graphs are finite and simple, on the vertex set $\{0,1,\dots,n-1\}$.

• The clique number of $G$ is the largest number of vertices of a complete subgraph. "Clique number at most $k$" means that $G$ contains no complete subgraph on $k+1$ vertices.
• A matching is a set of pairwise disjoint edges. The matching number $\nu(G)$ is the largest size of a matching of $G$.
• A graph is complete $k$-partite if its vertex set is split into $k$ classes (some possibly empty) and two vertices are adjacent exactly when they lie in different classes.
• $T(n,k)$ is the complete $k$-partite graph on $n$ vertices whose classes have sizes as equal as possible, and $t(n,k)$ is its number of edges, the Turán number.
• $G(n,k,s)$ is the complete $k$-partite graph on $n$ vertices with $k-1$ classes of sizes as equal as possible and total size $s$, and one further class of size $n-s$. Its number of edges is $g(n,k,s)$.

A graph on $n$ vertices is admissible for $(k,s)$ when its clique number is at most $k$ and its matching number is at most $s$. Both constructions are admissible when $n\ge 2s+1$: $G(n,k,s)$ is $k$-colourable, and every edge of it meets the $s$ vertices of the small classes; the Turán graph $T(2s+1,k)$ on $2s+1$ of the vertices, with the other $n-2s-1$ vertices isolated, has no $s+1$ disjoint edges.

Formalization targets

Goal: Theorem 1.1

For $k\ge2$ and $n\ge 2s+1$,

$$\max\bigl\{|E(G)| : G \text{ on } n \text{ vertices},\ \omega(G)\le k,\ \nu(G)\le s\bigr\} \;=\; \max\{\,t(2s+1,k),\ g(n,k,s)\,\},$$

stated as an upper bound for every admissible graph together with an admissible graph attaining it.

Milestones

The milestones follow the proof of §2 of the paper, in attack order:

1. the two constructions are admissible (the lower bound);
2. the barrier: every graph has a vertex set $B$ such that every component of $G-B$ is odd and $|B|+\sum_i(|A_i|-1)/2=\nu(G)$;
3. Lemma 2.1: in the §2 choice of an extremal graph and barrier maximizing $\sum_i|A_i|^2$, non-adjacent vertices of $B$ have the same neighbourhood;
4. the graph induced on $B$ is then complete $k$-partite;
5. Claim 2.3: for that choice of graph and barrier, without loss of generality every component of $G-B$ has a vertex with no neighbour in the smallest class of $B$;
6. Lemma 2.2: for an extremal graph maximizing $\sum_i |A_i|^2$, at most one component of $G-B$ has more than one vertex;
7. the case analysis on $b=|B|$ that bounds the remaining structure by $\max\{t(2s+1,k),g(n,k,s)\}$;
8. the identity $t(s+\lfloor s/(k-1)\rfloor,k)+(n-s-\lfloor s/(k-1)\rfloor)\,s=g(n,k,s)$;
9. the Turán increment $t(N+1,k)-t(N,k)=N-\lfloor N/k\rfloor$ is non-decreasing in $N$, with steps at most $1$;
10. the function $f(b)=t(2s-b+1,k)+b(n-2s+b-1)$ has strictly increasing differences on the range of Case 4.

A companion item records the paper's parenthetical remark: for $n\le 2s+1$ the maximum is $t(n,k)$.

Significance

The theorem settles the edge-extremal problem for the two most basic graph parameters, clique number and matching number, jointly and for every admissible parameter value. It contains both classical theorems: when $n\le 2s+1$ the matching condition is void and the answer is Turán's $t(n,k)$; when $k\ge 2s+1$ the clique condition is void and the answer is the Erdős–Gallai bound. The two extremal constructions show that both regimes genuinely occur, and the threshold between them depends on $n$, $k$ and $s$ together. The same paper's Proposition 3.1 extends the answer $g(n,k,s)$ to every colour-critical forbidden graph for large $s$ and $n$, and the present theorem is the base case of that programme.

The theorem is proved in the paper; it has not been formalized. Mathlib has Turán's theorem (SimpleGraph.CliqueFree.card_edgeFinset_le), Tutte's theorem on perfect matchings, and extremal-graph infrastructure (SimpleGraph.IsExtremal), but no Tutte–Berge formula, no Gallai–Edmonds decomposition, and no Erdős–Gallai theorem for matchings. A formal proof would add the Tutte–Berge formula in the barrier form used here, a reusable Zykov symmetrization argument, and the first machine-checked proof of the Erdős–Gallai matching bound as a special case.

Difficulty

The arithmetic of the proof (milestones 8–10) is short. The difficulty is concentrated elsewhere.

First, the proof starts from a barrier $B$ whose removal leaves only odd components with $|B|+\sum_i(|A_i|-1)/2$ equal to the matching number. This is the Tutte–Berge formula sharpened to a maximal barrier, all of whose components are factor-critical. Mathlib's Tutte theorem covers perfect matchings only, so the deficiency version and the structure of maximal barriers have to be built.

Second, Lemma 2.1, Claim 2.3 and Lemma 2.2 are surgery on an extremal graph. Each modifies the graph (copying a neighbourhood, swapping two classes of $B$ in the neighbourhood of a component, merging two components) and must re-verify three things: the number of edges does not decrease, no clique on $k+1$ vertices appears, and the matching number stays at most $s$. The matching bound is re-verified through the barrier, so the components of the modified graph have to be tracked, and the extremality hypothesis has to be used in the right form. In particular, the paper's printed proof of Lemma 2.1 shows only that non-adjacency is transitive on $B$ and that non-adjacent vertices of $B$ have equal degree; the full "same neighbourhood" conclusion needs a further argument from extremality.

Third, the barrier equation of p. 2 is written with $s$, which presumes that an extremal graph has matching number exactly $s$; the paper does not prove this, and a solver who wants to chain the milestones needs it.

Formalization scope

Graphs are SimpleGraph (Fin n); edge counts are #G.edgeFinset. Clique number at most $k$ is G.CliqueFree (k + 1). The matching number is the supremum, in ℕ, of the edge counts of matching subgraphs (Subgraph.IsMatching); the set is nonempty and bounded, so the supremum is a maximum, and the companion sanity file proves $\nu(G)\le s$ iff every matching has at most $s$ edges. $T(n,k)$ is Mathlib's turanGraph n k. $G(n,k,s)$ is an explicit graph on Fin n (vertex $v<s$ in class $v \bmod (k-1)$, all others in class $k-1$), and $g(n,k,s)$ is defined as its edge count, not by a closed formula, so the identity of milestone 8 is a statement about the graph. Extremality is Mathlib's IsExtremal for the admissibility property. The maximality of $\sum_i a_i^2$ in Lemmas 2.1 and 2.2 and Claim 2.3 ranges over all extremal graphs together with all their odd barriers of value $s$, because the paper chooses $B$ together with $G$.

One hypothesis is added to the paper's statement: $k\ge2$. The paper says "every $k$", but $G(n,k,s)$ has $k-1$ classes of total size $s$, which is impossible for $k=1$ and $s>0$, and no nonempty graph has clique number at most $0$. Lemmas 2.1, 2.2 and Claim 2.3 keep the paper's barrier value $s$ as a hypothesis, while the barrier milestone itself is stated with $\nu(G)$.

The goal is an upper bound together with an attaining graph; an upper bound alone would be a weaker theorem. The surgery lemmas carry extremality as a hypothesis, never a hypothesis on the edge count that would presuppose the answer.

Contributions welcome beyond this mission: the Tutte–Berge formula and Gallai–Edmonds decomposition for SimpleGraph, the matching number as a reusable definition, and the Erdős–Gallai matching theorem.

Selected references

• N. Alon and P. Frankl, Turán graphs with bounded matching number, arXiv:2210.15076v1, 2022; J. Combin. Theory Ser. B, 2024. https://arxiv.org/abs/2210.15076, https://doi.org/10.1016/j.jctb.2023.12.002
• P. Turán, On an extremal problem in graph theory (in Hungarian), Mat. Fiz. Lapok 48 (1941), 436–452.
• P. Erdős and T. Gallai, On maximal paths and circuits of graphs, Acta Math. Acad. Sci. Hungar. 10 (1959), 337–356. https://doi.org/10.1007/BF02024498
• L. Lovász and M. D. Plummer, Matching Theory, North-Holland Mathematics Studies 121, 1986. https://doi.org/10.1090/chel/367
• A. A. Zykov, On some properties of linear complexes, Mat. Sbornik N.S. 24(66) (1949), 163–188.