All missions

Motivation

A large language model (LLM) answers a request in two phases. In the prefill phase it reads the whole prompt; in the decode phase it generates the answer one token at a time, because each new token depends on all previous ones. Serving engines such as vLLM, SGLang and Sarathi-Serve run the GPU in iterations: each iteration processes one batch that may mix prefill tokens of some requests with single decode tokens of others, up to a token budget $b_{\max}$. Which tokens enter each batch is decided by a batch scheduling algorithm, and providers want to know how much traffic a given server can sustain and which scheduling rules achieve that.

Dai, Deng, Li and Peng (arXiv:2504.07347v3, 2026) cast this as a queueing problem: a two-class batch-service queue in which one batch couples the two classes through a shared budget, and a request contributes many tokens per batch in prefill but at most one in decode. Their Theorem 2 identifies the maximal throughput of a single server and shows that a broad class of practical schedulers attains it. The proof method is the fluid-limit approach to stability of stochastic processing networks (Dai 1995; Dai and Harrison, Processing Networks, 2020).

Setting

Time is divided into integer slots. A batch with token load $b$ (its number of tokens) takes

$$t_b = c + a\left\lceil \frac{b}{b_0}\right\rceil$$

slots (eq. (4)). Here $c,a\ge 0$ are integers and $b_0\ge 1$ is a block size dividing $b_{\max}$ (Assumption 1).

Requests are labelled $0,1,2,\dots$ in order of arrival. Request $i$ brings $v_p(i)\in\{1,\dots,v_p^{\max}\}$ prefill tokens and $v_d(i)\in\{1,\dots,v_d^{\max}\}$ decode tokens. The arrival counts $a_n$ of the slots are i.i.d. with mean $\lambda$, the sizes are i.i.d. with means $m_p, m_d$, and the two sequences are independent.

The state at the start of a slot is

$$X(n)=\big(R(n),\{(P_i(n),D_i(n)) : i\in Q_n\}\big),$$

where $R(n)$ is the remaining time of the current batch, $Q_n$ the set of requests in the system, and $P_i, D_i$ the unprocessed prefill and decode tokens of request $i$. When $R(n)=0$ the algorithm picks $(\delta^p_i,\delta^d_i)_{i\in Q_n}$ subject to the following feasibility rules (eq. (6)):

• prefill before decode;
• $\delta^p_i\le P_i$;
• $\delta^d_i\le 1$;
• total load $b=\sum_i(\delta^p_i+\delta^d_i)\le b_{\max}$.

The batch then runs for $t_b$ slots. When it finishes, requests with no tokens left depart, and new arrivals join at the end of every slot. The total number of unprocessed tokens is $|X(n)|=\sum_{i\in Q_n}(P_i(n)+D_i(n))$.

An algorithm is work-conserving if it forms a full batch ($b=b_{\max}$) whenever the supply $\sum_i\big(P_i+\mathbf 1(P_i=0)\big)$ is at least $b_{\max}$. It is K-FCFS if, whenever a request $j$ receives a decode token, every request $i\le j-K$ still in the system receives at least one token.

Formalization targets

Goal: Theorem 2

1. If $\lambda(m_p+m_d)>b_{\max}/t_{b_{\max}}$, then under every scheduling algorithm and from every initial state

$$\mathbb P\Big\{\lim_{n\to\infty}|X(n)|=\infty\Big\}=1 .$$

2. If $\lambda(m_p+m_d)<b_{\max}/t_{b_{\max}}$, then for every work-conserving K-FCFS algorithm there is a finite set $F$ of label-free configurations whose hitting time has finite expectation from every initial state whose requests respect the size bounds $v_p^{\max}, v_d^{\max}$:

$$\exists F \text{ finite},\ \forall x:\quad \mathbb E_x\big[\tau_F\big]<\infty,\qquad \tau_F=\min\{n\ge 1: (R(n),(P_i(n),D_i(n))_{i})\in F\}.$$

Part 2 is the corrected form of the paper's "the DTMC $\{X(n)\}$ is positive recurrent". The labelled state cannot recur, because each new request carries a new label.

Milestones

These follow the order of the paper's argument:

1. The rate bound: $b/t_b\le b_{\max}/t_{b_{\max}}$ for $1\le b\le b_{\max}$ (proof sketch, p. 16).
2. The cumulative processing bound $B_f(n_2t_{b_{\max}})-B_f(n_1t_{b_{\max}})\le (n_2-n_1+1)b_{\max}$ (eq. (43), corrected).
3. The strong law $E(n)/n\to\lambda$, $V_f(N)/N\to m_f$ almost surely (eq. (56)).
4. Bounded overtaking in departure order under K-FCFS (Lemma 11, corrected to departures).
5. Stability of the work-conserving fluid model (Proposition 15, with nonnegative fluid levels).

Significance

Theorem 2 gives a sharp stability threshold for a single LLM server: the arriving token workload per slot, $\lambda(m_p+m_d)$, against the maximal processing rate $b_{\max}/t_{b_{\max}}$ of full batches. It shows that every work-conserving K-FCFS scheduler, a class containing Sarathi-Serve-style chunked-prefill schedulers, is throughput-optimal. Schedulers that do not mix prefill and decode tokens in one batch can lose throughput. The result is the base case for the paper's multi-server, multi-class and agent-network extensions.

The paper proves part (a) in a sketch and part (b) by the fluid-limit method, with a separate Lyapunov argument in Appendix C. No part of the result has a machine-checked proof. Several printed steps are false as stated:

• the strict monotonicity of the step-endpoint rates;
• the constant in eq. (43);
• the prefill clause of Lemma 11;
• Proposition 15 without nonnegativity;
• the recurrence of the labelled chain.

A formalization fixes the exact statements that hold and supplies a complete argument.

Difficulty

Part (a) reduces to the rate bound, a pathwise count of completed batches, and the strong law. Part (b) is where the difficulty lies. A Lyapunov drift on the total token count fails directly: while a batch is in progress no tokens are completed, so the one-slot drift is positive whenever $R(n)>0$. A drift argument must account for the batch in progress. The naive bound "every slot completes $b_{\max}/t_{b_{\max}}$ tokens on average when the system is large" also needs the supply condition (9) to hold. Requests in decode contribute at most one token per batch, so many tokens can sit in few decode-phase requests. The fluid-limit route needs bounded overtaking, and the paper's prefill version of that is false.

Formalization scope

The Lean development (namespace LLMThroughput.TokenBudget) commits to the following:

• Slots and labels are 0-based, and $c, a, b_0, b_{\max}$ are natural numbers with $b_0\ge 1$, $b_0\mid b_{\max}$, $b_{\max}\ge 1$ and $t_{b_{\max}}\ge 1$.
• The state is a list of requests (label, $P_i$, $D_i$) in label order, together with $R$ and the next label.
• A policy is any function from states to batch configurations. It must be feasible (and, where assumed, work-conserving and K-FCFS) at every admissible state.
• Feasibility adds $\delta^d_i\le D_i$.
• The dynamics is a pathwise recursion driven by sequences $a_n$ and $(v_p(i),v_d(i))$.
• The randomness is a probability space with measurable, i.i.d., mutually independent sequences and integrable $a_1$.
• The expectation of a hitting time is the Lebesgue integral of an $\mathbb N\cup\{\infty\}$-valued time, so a time that is infinite with positive probability has infinite expectation.
• Positive recurrence is stated for the label-free configuration, with the finite set $F$ chosen before the initial state. In part 2 the initial requests obey the source's size bounds $P_i\le v_p^{\max}$, $D_i\le v_d^{\max}$; part 1 allows any admissible initial state.

A finite set $F$ is essential. The set of all states with small token count is infinite once labels are included, and hitting it would be a much weaker claim. Quantifying over a single named policy instead of all work-conserving K-FCFS policies would also change the theorem.

A complete development needs:

• sample-path lemmas for the recursion (admissibility is preserved, tokens are conserved);
• the strong law from Mathlib (ProbabilityTheory.strong_law_ae);
• a Foster–Lyapunov criterion for a process that is not a Markov kernel on the policy's input type;
• for the fluid route, Lipschitz calculus for the fluid model.

The pathwise model and the bounded-overtaking lemma can be reused for other batch-service systems. Proofs of any milestone, and alternative proofs of part (b) (a direct drift argument on an augmented workload), are welcome.

Selected references

• J. G. Dai, Y. Deng, Z. Li, Z. Peng, Throughput-Optimal Scheduling Algorithms for LLM Inference and AI Agents, arXiv:2504.07347v3, 2026. https://arxiv.org/abs/2504.07347
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1), 1995. https://doi.org/10.1214/aoap/1177004828
• J. G. Dai, J. M. Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press, 2020. https://doi.org/10.1017/9781108772662
• A. Agrawal et al., Taming Throughput-Latency Tradeoff in LLM Inference with Sarathi-Serve, OSDI 2024. https://arxiv.org/abs/2403.02310

Motivation

An apportionment method distributes the $H$ seats of a house among $n$ states in proportion to their populations. Exact proportionality is impossible with integer seats, so methods are judged by axioms. Two axioms date back to the debates over the seats of the US House of Representatives. Quota compliance asks that each state receive its exact proportional share rounded down or up. House monotonicity asks that no state lose a seat when the house grows; the Alabama paradox of 1880, in which Hamilton's method took a seat from Alabama when the house was enlarged, is the classic failure. The two axioms can hold together. Balinski and Young (Mathematics of Operations Research, 1979) and Still (SIAM Journal on Applied Mathematics, 1979) characterized the methods satisfying both through a recursive, seat-by-seat construction. Gölz, Peters and Procaccia (EC 2022) later gave a description by a fractional matching polytope.

Cembrano, Correa, Schmidt-Kraepelin, Tsigonias-Dimitriadis and Verdugo (arXiv:2410.23869, Mathematics of Operations Research, 2025) give a third characterization, by a network-flow linear program. It replaces the recursive construction with the vertex set of a polytope that can be written down and optimized over. This mission formalizes that characterization, Theorem 3 of the paper.

Setting

An instance is a pair $(p,H)$. Here $p=(p_1,\dots,p_n)$ is a vector of $n\ge1$ strictly positive integers (the populations of the states) and $H\ge1$ is an integer, the house size. Write $P=\sum_i p_i$; the quota of state $i$ is $q_i=\frac{p_i}{P}H$.

A solution $f$ assigns to every instance one vector $f(p,H)\in\mathbb N_0^n$ with $\sum_i f_i(p,H)=H$. It is defined for every number of states $n$ and every population vector. It is quota-compliant if $f_i(p,H)\in\{\lfloor q_i\rfloor,\lceil q_i\rceil\}$ always. It is house-monotone if $f(p,H_1)\le f(p,H_2)\le f(p,H_3)$ componentwise whenever $H_1<H_2<H_3$. The set of apportionments such solutions produce is

$$\mathcal A(p,H)=\{f(p,H): f\text{ a house-monotone and quota-compliant solution}\}.$$

For $L$ seats, the network-flow linear program (1)–(4) has a variable $x(i,t)\ge0$ for each state $i$ and seat $t\in[L]$, subject to

$$\sum_{i=1}^n x(i,t)=1,\qquad \Big\lfloor\frac{tp_i}{P}\Big\rfloor\le\sum_{\ell=1}^t x(i,\ell)\le\Big\lceil\frac{tp_i}{P}\Big\rceil .$$

Its feasible region is $K(p,L)$ and its set of extreme points is $\mathcal E(p,L)$. The count $A_i(x,T)=\sum_{\ell=1}^T x(i,\ell)$ is the number of seats state $i$ holds after $T$ seats.

The lookahead $\Phi(p,H)$ is the number of seats the LP must model so that its first $H$ seats are exactly the house-monotone, quota-compliant ones. For a vector $y$ and $k\ge1$, let $S_k(p,H,y)=\{i:\lfloor p_i(H+k)/P\rfloor>y_i\}$. Let $k^\star(p,H,y)$ be the least $k\ge1$ with $\sum_{i\in S_k}(\lfloor p_i(H+k)/P\rfloor-y_i)\ge k$. Set $\tau=k^\star$ unless $S_{k^\star}=[n]$, in which case $\tau=1$. Then $\Phi(p,0)=0$, $\Phi(p,1)=\min\{k\ge1:\sum_i\lfloor p_ik/P\rfloor\ge k\}$, and

$$\Phi(p,H+1)=\max_{T\in[H]}\Big\{T+\max\{\tau(p,T,A(x,T)):x\in\mathcal E(p,\Phi(p,H))\}\Big\}.$$

The Lean names are IsPop, Solution, QuotaCompliant, HouseMonotone, calA, K, calE, A, S, kStar, tau, Phi, all in the namespace MonoApport.Flow.

Formalization targets

Goal: Theorem 3

$$\mathcal A(p,H)=\big\{A(x,H): x\in\mathcal E(p,\Phi(p,H))\big\}\qquad\text{for every instance }(p,H).$$

Milestones

1. Proposition 8. A solution is house-monotone if and only if $f(p,H)\le f(p,H+1)$ for every $p$ and $H$.
2. Total unimodularity (proof of Lemma 3). The matrix with rows $e_{i,t}$, $-e_{i,t}$, $e'_t$, $-e'_t$ is totally unimodular. Here $e_{i,t}$ is the prefix-sum row of state $i$ up to seat $t$, and $e'_t$ is the column-sum row of seat $t$.
3. Lemma 3. The linear program (1)–(4) is integral: every extreme point has integer coordinates.
4. Remark after Lemma 3. $\mathcal E(p,L)$ is exactly the set of integer points of $K(p,L)$.
5. Balinski–Young characterization (§C.4). $f$ is a house-monotone and quota-compliant solution if and only if, with $f(p,0)=0$, each seat $H+1$ goes to one state of $\mathcal L(p,H,f(p,H))\cap\mathcal U(p,H,f(p,H))$. Here $\mathcal L(p,H,y)=\{i:\lfloor\frac{p_i}{P}(H+k^\star(p,H,y))\rfloor>y_i\}$ and $\mathcal U(p,H,y)=\{i:\frac{p_i}{P}(H+1)>y_i\}$.
6. Lemma 5. If $x\in\mathcal E(p,\Phi(p,H))$ and $T\le H-1$, then $x(i,T+1)=0$ for every $i\notin\mathcal L(p,T,A(x,T))\cap\mathcal U(p,T,A(x,T))$.

Significance

The result. Theorem 3 turns a recursive definition into a polyhedral one. The apportionments at house size $H$ that some house-monotone, quota-compliant solution can produce are the projections of the vertices of a network-flow polytope with $\Phi(p,H)$ seats. Optimizing a linear objective over all such apportionments is then a linear program of size $O(n\,\Phi(p,H))$. The paper also bounds the lookahead: $\Phi(p,H)-H\le\max_i\lceil P/p_i\rceil$ for $H\ge2$, and the bound is tight up to constants. Through the correspondence between methods and solutions (Lemma 2 of the paper), the theorem also characterizes house-monotone, quota-compliant methods. It underlies the paper's construction of randomized methods that are house-monotone, quota-compliant and ex-ante proportional (Theorem 4).

The formalization. The paper proves Theorem 3. None of the statements here has a machine-checked proof, and the Balinski–Young characterization is cited by the paper rather than proved in it. A formal development would check the full chain: total unimodularity of an interval-type constraint matrix, integrality of the polytope, the lookahead bound of Lemma 5, and the combination with the Balinski–Young construction. It would also make the network-flow polytope and the lookahead $\Phi$ available to later work on apportionment.

Difficulty

The inclusion $\mathcal A(p,H)\subseteq\{A(x,H)\}$ looks routine: the seat increments of a house-monotone, quota-compliant solution give a 0/1 feasible point. But that point must have $\Phi(p,H)$ seats, and it must be an extreme point, which requires the integrality of (1)–(4).

The reverse inclusion is the hard part. A vertex of the LP with $H$ seats need not extend to a quota-compliant sequence: a seat assignment can respect every quota bound up to $H$ and still force a violation a few seats later. The lookahead $\Phi$ is designed so that this cannot happen. However, $\Phi$ is defined by a recursion over extreme points of LPs of other sizes, and it is not monotone in $H$: for $p=(1,2)$ the values are $\Phi=0,3,2,3,4,\dots$. An argument that truncates a vertex for $\Phi(p,H)$ seats to one for $\Phi(p,H-1)$ seats, or assumes $\Phi(p,H)\ge\Phi(p,H-1)$, is therefore unavailable.

Closing the inclusion also needs the Balinski–Young construction never to get stuck: $\mathcal L\cap\mathcal U$ must be nonempty along every sequence it builds. The paper takes this from Balinski and Young without stating it separately.

Formalization scope

Populations are p : Fin n → ℕ with IsPop p ($n>0$ and every $p_i>0$); house sizes carry 0 < H. A solution is one Lean function Solution := ∀ {n}, (Fin n → ℕ) → ℕ → (Fin n → ℕ) defined on vectors of every length. $\mathcal A(p,H)$ quantifies over such families, exactly as in the paper; a per-$p$ sequence of apportionments would be a different object. House monotonicity is axiom (c) with three house sizes; the one-step form is Proposition 8, a milestone. LP points with $L$ seats are x : Fin n → Fin L → ℝ. Seats are 0-indexed, so column $t$ is seat $t+1$, and the quota bounds at column $t$ use $t+1$. Floors and ceilings are Nat.floor/Nat.ceil of the nonnegative rational quantity computed in $\mathbb R$. $\mathcal E(p,L)$ is Set.extremePoints ℝ (K p L). The minima and maxima defining $k^\star$ and $\Phi$ are sInf/sSup on $\mathbb N$, whose sets are nonempty, and finite where a maximum is taken, wherever they are used. The convention $f(p,0)=0$ is the function ext. The goal compares subsets of $\mathbb R^n$: the image of $\mathcal A(p,H)$ under the cast equals $\{A(x,H)\}$.

The goal must not be read with integer vectors on both sides. Writing $\mathcal A(p,H)=\{y : (y_i:\mathbb R)=A_i(x,H)\text{ for some }x\}$ would silently ignore non-integral $A(x,H)$ and empty the inclusion $\supseteq$ of its content.

A complete development needs:

• total unimodularity and the integrality of polytopes with totally unimodular constraints (Hoffman–Kruskal), partly available in Mathlib through Matrix.IsTotallyUnimodular;
• the finiteness of the extreme points of a polytope;
• a formal proof of the Balinski–Young characterization, including the nonemptiness of $\mathcal L\cap\mathcal U$ along the construction.

The first two are reusable well beyond apportionment. Proofs of any milestone are welcome, and so are proofs of the cited Balinski–Young theorem and of the properties of $\Phi$ the paper uses ($\Phi(p,H)\ge H$, and the finiteness and nonemptiness of the sets in its recursion).

Selected references

• J. Cembrano, J. Correa, U. Schmidt-Kraepelin, A. Tsigonias-Dimitriadis, V. Verdugo, New Combinatorial Insights for Monotone Apportionment, arXiv:2410.23869v1, 2024; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2410.23869
• M. Balinski, H. P. Young, Quotatone apportionment methods, Mathematics of Operations Research 4(1):31–38, 1979. https://doi.org/10.1287/moor.4.1.31
• M. Balinski, H. P. Young, The quota method of apportionment, The American Mathematical Monthly 82(7):701, 1975.
• M. Balinski, H. P. Young, Fair Representation: Meeting the Ideal of One Man, One Vote, Brookings Institution Press, 2010.
• J. W. Still, A class of new methods for congressional apportionment, SIAM Journal on Applied Mathematics 37(2):401–418, 1979.
• P. Gölz, D. Peters, A. D. Procaccia, In this apportionment lottery, the house always wins, Proceedings of the 23rd ACM Conference on Economics and Computation (EC), 2022.
• A. Ghouila-Houri, Caractérisation des matrices totalement unimodulaires, C. R. Acad. Sci. Paris 254:1192–1194, 1962.

Motivation

A finite game can be split into simpler pieces. Candogan, Menache, Ozdaglar and Parrilo (Math. Oper. Res. 36 (2011)) showed that the space of finite games is the direct sum of potential, harmonic and nonstrategic games: potential games have pure equilibria and well-behaved learning dynamics, harmonic games generalize matching pennies, and nonstrategic games do not affect anyone's incentives. The decomposition is used to approximate a game by the closest potential game and to transfer equilibrium and dynamics results from the potential component to the original game.

Their decomposition depends on a uniform measure on each strategy set and an unweighted inner product. As a result it is not invariant under transformations that leave the strategic content of a game unchanged. The most basic such transformation is duplicating a strategy: giving a player a second, payoff-identical copy of one of her strategies. Abdou, Pnevmatikos, Scarsini and Venel (arXiv:1901.06048v2, 2020; Math. Oper. Res. 2022) introduce a weighted family of decompositions, parametrized by a measure vector and a co-measure vector, and show that duplication commutes with it once the weights are transformed accordingly. This mission formalizes that result together with the weighted decomposition it rests on.

Setting

There is a finite set $N$ of players. Player $i$ has a finite strategy set $S^i$; $S=\prod_{i\in N}S^i$ is the set of profiles $s$, $s^{-i}$ is $s$ without player $i$, and $(t^i,s^{-i})$ is $s$ with player $i$'s strategy replaced by $t^i$. A game is a vector $g=(g^i)_{i\in N}$ of payoff functions $g^i:S\to\mathbb R$; the games form a real vector space $\mathcal G$.

A measure vector $\mu=(\mu^i)_{i\in N}$ assigns a strictly positive weight $\mu^i(s^i)$ to every strategy; $\mu(s)=\prod_i\mu^i(s^i)$ is the product measure and $\mu^i(S^i)$ the total mass. A co-measure vector $\gamma=(\gamma^i)_{i\in N}$ assigns to player $i$ a strictly positive function $\gamma^i(s^{-i})$ of the other players' strategies. A game $g$ is

• nonstrategic if each $g^i(s^i,s^{-i})$ does not depend on $s^i$;
• $\mu$-normalized if $\sum_{s^i}\mu^i(s^i)g^i(s^i,s^{-i})=0$ for every $i$ and $s^{-i}$;
• $\gamma$-potential if some $\Psi:S\to\mathbb R$ satisfies $\gamma^i(s^{-i})\big(g^i(t^i,s^{-i})-g^i(s^i,s^{-i})\big)=\Psi(t^i,s^{-i})-\Psi(s^i,s^{-i})$;
• $(\mu,\gamma)$-harmonic if $\sum_i\sum_{t^i}\mu^i(t^i)\gamma^i(s^{-i})\big(g^i(s^i,s^{-i})-g^i(t^i,s^{-i})\big)=0$ for every $s$.

Games carry the inner product $\langle g_1,g_2\rangle_{\mu,\gamma}=\sum_i\mu^i(S^i)\sum_s\mu(s)\gamma^i(s^{-i})^2g_1^i(s)g_2^i(s)$.

Duplication. Collapse each strategy set by a map $\pi^j:S'^j\to S^j$. The extended game is $\check g^j(s')=g^j(\pi(s'))$, the extended co-measure is $\check\gamma^j(s')=\gamma^j(\pi(s'))$, and an extension $\check\mu$ of $\mu$ is any strictly positive measure vector whose mass on each fibre $(\pi^j)^{-1}(a)$ is $\mu^j(a)$. Duplicating $s^i_1$ into $s^i_0,s^i_1$ is the case $S'^i=S^i\cup\{s^i_0\}$, $\pi^i(s^i_0)=s^i_1$, all other maps the identity: then $\check\mu^i(s^i_0)+\check\mu^i(s^i_1)=\mu^i(s^i_1)$.

Formalization targets

Goal: Theorem 3.15

Write $(g_{\text{NS}},g_{\text{P}},g_{\text{H}})$ for the $(\mu,\gamma)$-decomposition of $g$. Then

$$\big(\check g\big)_{(\check\mu,\check\gamma)\text{-NS}}=\check g_{\text{NS}},\qquad \big(\check g\big)_{(\check\mu,\check\gamma)\text{-P}}=\check g_{\text{P}},\qquad \big(\check g\big)_{(\check\mu,\check\gamma)\text{-H}}=\check g_{\text{H}},$$

stated as: a triple of games on $S'$ is a $(\check\mu,\check\gamma)$-decomposition of $\check g$ if and only if it equals the extension of $(g_{\text{NS}},g_{\text{P}},g_{\text{H}})$. Both directions are content: one is uniqueness for the extended weights, the other the invariance of each class.

The weighted decomposition: Theorem 2.11

$$\mathcal G=(\mu\text{-NoG}\cap\gamma\text{-PG})\oplus_{\mu,\gamma}(\mu\text{-NoG}\cap(\mu,\gamma)\text{-HG})\oplus_{\mu,\gamma}\mathsf{NSG},$$

every game having exactly one decomposition and the three classes being pairwise orthogonal. Proposition 2.10 ($\mathcal G=\mu\text{-NoG}\oplus_{\mu,\gamma}\mathsf{NSG}$) and Lemma 3.14 (each class is preserved by extension) are the other main milestones; Lemmas A.1–A.11 and Propositions A.3–A.9 of the appendix are the intermediate steps, in the order of the milestone list.

Significance

The result says that the potential, harmonic and nonstrategic parts of a game are properties of its strategic content and not of the way it is written down, provided the measure is split among copies of a strategy and the co-measure is copied. Duplicate strategies appear whenever a game is derived from an extensive form or a mechanism, so a decomposition that is not invariant under duplication assigns different "closest potential games" to the same strategic situation. The same weighted machinery gives the paper's invariance results for relabellings and scalings and the elimination of duplicates (Theorem 3.19, derived from Theorem 3.15).

All results are proved in the paper. None of them is formalized: the platform has the uniform-weight decomposition of Candogan et al. (Theorem 4.1 of that paper, proved), with an unweighted inner product and a pseudo-inverse-based definition of the projections, but no weighted classes, no co-measures and no statement about duplication. This mission adds the weighted definitions, the weighted decomposition with its uniqueness and orthogonality, and the commutation theorem.

Difficulty

The commutation is an immediate consequence of two facts, and both carry the work. The first is uniqueness of the $(\check\mu,\check\gamma)$-decomposition on the larger profile set: this is Theorem 2.11 itself, whose proof needs the weighted flow operators, their adjoints and the orthogonality of normalized potential and normalized harmonic games under $\langle\cdot,\cdot\rangle_{\mu,\gamma}$. The second is that extension preserves each class, which fails for the obvious guess at the extended co-measure: the definition printed in the paper splits $\gamma^j$ between the two copies, and with that choice a potential game's extension is no longer potential. Only the copied co-measure works. The weights also matter for normalization: without splitting $\mu^i(s^i_1)$ between the copies the extended game is not normalized.

Formalization scope

• Players are a finite type ι, strategy sets finite types S i, profiles ∀ i, S i, and $(t^i,s^{-i})$ is Function.update s i t. A game is ι → (∀ i, S i) → ℝ.
• Measures are point-mass functions μ i : S i → ℝ with strict positivity as a hypothesis; a co-measure γ i is a positive function of the full profile that is invariant under changing coordinate i.
• The standing assumptions $n\ge2$ and $|S^i|\ge2$ are dropped; all statements hold without them.
• The $(\mu,\gamma)$-decomposition is the predicate IsDecomposition μ γ g n p h in the order (nonstrategic, potential, harmonic) of (2.18); no decomposition function is defined, since Theorem 2.11 makes the triple unique.
• Inner products are explicit finite sums: $\langle\cdot,\cdot\rangle_0$ with the unnormalized product measure, $\langle\cdot,\cdot\rangle_{\mu,\gamma}$ with the factor $\mu^i(S^i)$, and $\langle\cdot,\cdot\rangle_1$ on flows with the factor $\tfrac12$. Flows are functions on pairs with a skew-symmetry hypothesis; $\delta^{i*}$ is defined by its explicit formula, and Proposition A.3 states that it is the adjoint.
• Duplication is generalized to arbitrary collapsing maps $\pi$, which covers Definition 3.13 and iterated duplications. The extended co-measure is the copy $\gamma\circ\pi$; the paper's printed sum version makes Lemma 3.14 and Theorem 3.15 false, and the copy is what its proof uses.
• Lemma A.11 is stated for every solution of the normal equation $\delta^*\delta\varphi=\delta^*D(g)$, together with existence of a solution, instead of through the Moore–Penrose pseudo-inverse.

A statement asserting only that the extended triple is a $(\check\mu,\check\gamma)$-decomposition of $\check g$ would be Lemma 3.14 and not the goal: the goal also excludes every other decomposition.

The weighted classes, inner products and flow operators are reusable for the paper's other invariance results (relabelling, pseudo-translations, scalings, elimination of duplicates) and for weighted versions of the closest-potential-game problem. Proofs of any milestone are welcome; the appendix lemmas are independent finite linear-algebra statements.

Selected references

• J. Abdou, N. Pnevmatikos, M. Scarsini, X. Venel, Decomposition of Games: Some Strategic Considerations, arXiv:1901.06048v2, 2020; Mathematics of Operations Research 47(1), 2022. https://arxiv.org/abs/1901.06048v2
• O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, Mathematics of Operations Research 36(3), 474–503, 2011. https://doi.org/10.1287/moor.1110.0500
• D. Monderer, L. S. Shapley, Potential Games, Games and Economic Behavior 14(1), 124–143, 1996. https://doi.org/10.1006/game.1996.0044

Searching a tree with unreliable directions

Search games model a Searcher looking for an object or a person whose location is chosen adversarially: a lost hiker, a mine, a hidden explosive device, a fugitive. In the classic search game on a tree, a Hider stands still at a point of a tree network, and a Searcher starts from the root and moves at unit speed. The payoff is the time to find the Hider. Gal (1979) solved this game for every tree. Its value is the total length $\mu$ of the tree, and an optimal Searcher randomizes over depth-first searches.

In practice, searchers often get hints: a witness who saw the hiker turn left, a sensor reading, a dog that picks one trail. Such hints are useful but fallible. Alpern and Lidbetter (arXiv:2303.13378, Operations Research, 2025) model this by a signal at each branching point. The signal points to the branch containing the Hider and is correct with a known probability $p>\tfrac12$. They solve the resulting game exactly on every binary tree. The value, the optimal Hider distribution and the optimal Searcher strategy are all given in closed form by a recursion on the tree.

Timeline. Gal (1979) solved the game without signals on trees, with value $\mu$. Biased depth-first strategies of the Searcher were introduced in other contexts by Alpern (2010) and by Alpern and Lidbetter (2014). Alpern and Lidbetter (2025) solved the game with signals of accuracy $p$, which as $p\to\tfrac12$ reduces to Gal's.

The game $G(Q,O,p)$

A rooted tree $(Q,O)$ is a finite tree whose arcs have positive lengths, with a distinguished root $O$. Write $\mu=\mu(Q)$ for its total length and $d(O,v)$ for the distance from the root to a node $v$. Every node other than the root has degree three (a branch node) or one (a leaf node). The root has degree one or two, and in the second case it is also a branch node. At a branch node $j$, the part of the tree beyond $j$ splits into two branches $Q_1$ and $Q_2$.

The Hider picks a leaf node. The Searcher performs a depth-first search from $O$ at unit speed. On her first arrival at a branch node $j$ on the way to the Hider she receives a signal, either 1 or 2, naming the branch that contains the Hider. It is correct with probability $p$ and wrong with probability $q=1-p$, where $\tfrac12<p\le1$. She then chooses which branch to search first, as a function of the signal. There are four such actions: $[1,1]$ and $[2,2]$ ignore the signal, $[1,2]$ follows it, and $[2,1]$ does the opposite. If she enters the wrong branch first she searches all of it and returns, which costs twice its length. The payoff $T$ is the time until she reaches the Hider. The Hider maximizes $T$ and the Searcher minimizes its expectation.

The mean depth of $Q$ with respect to a probability distribution $\lambda$ on its leaf nodes $L$ is

$$D(Q,O,\lambda)=\sum_{v\in L}\lambda(v)\,d(O,v).$$

The Hider distribution $\bar\lambda_Q$ is defined by recursion on the tree. On a single arc it is the point mass at its leaf. At a root of degree one it is the distribution of the subtree. At a branch root with branches $Q_1,Q_2$ of lengths $\mu_1,\mu_2$, call $Q_1$ the favored branch if $D_{Q_1}\ge D_{Q_2}$, where $D_{Q_i}=D(Q_i,\bar\lambda_{Q_i})$. Then

$$\bar\lambda(v)=\frac{p\mu_1}{p\mu_1+q\mu_2}\,\bar\lambda_{Q_1}(v)\ \ (v\in Q_1),\qquad \bar\lambda(v)=\frac{q\mu_2}{p\mu_1+q\mu_2}\,\bar\lambda_{Q_2}(v)\ \ (v\in Q_2).$$

Write $D_Q=D(Q,O,\bar\lambda_Q)$. At a branch node with favored branch $Q_1$, the favoring bias is

$$\beta=\frac{(p-q)(D_{Q_1}-D_{Q_2})}{2(p\mu_1+q\mu_2)}.$$

Formalization targets

Goal: Theorem 7

For every rooted tree with positive arc lengths and every $\tfrac12<p\le1$:

1. the value of $G(Q,O,p)$ is

$$V(Q)=2q\mu+(p-q)D_Q;$$

2. $\bar\lambda$ is an optimal Hider strategy;
3. the Searcher strategy that, at every branch node, searches the favored branch first with probability $\beta$ and otherwise follows the signal is optimal.

All three parts are stated, for every tree and every $p$ in the model's range. Nothing is fixed to a special tree or a special $p$.

Milestones

• $V(Q)=\ell+V(Q')$ at a root of degree one (proof of Theorem 7, p. 10).
• Proposition 6: $D_Q=\ell+D_{Q'}$ at a degree-one root, and $D_Q=\dfrac{p\mu_1D_{Q_1}+q\mu_2D_{Q_2}}{p\mu_1+q\mu_2}$ at a branch root with $Q_1$ favored.
• Table 1: at a branch root, the game has the value of a $2\times4$ matrix game whose entries are the lengths and values of the two branches (pp. 10–11).
• "Follow" dominates "opposite": the two columns differ by $(2\mu_2(2p-1),\,2\mu_1(2p-1))$ (p. 11).
• Lemma 2: the game has a value, and it is at most $\mu$.

What the result gives

The theorem gives a complete closed-form solution of a search game with imperfect information, on every tree. The value interpolates between Gal's $\mu$ (as $p\to\tfrac12$) and the mean depth $D_Q$ (at $p=1$). It quantifies how much a signal of accuracy $p$ is worth to the Searcher. It also shows that always following the signal is almost never optimal: the Searcher should sometimes go to the favored branch without looking at the signal. The paper derives explicit formulas for penultimate nodes (Corollary 8), monotonicity of the value in $p$ (Proposition 9) and the value on trees of constant depth (Corollary 10) from it.

The result is proved in the paper. To our knowledge no part of it has a machine-checked proof, and Gal's theorem for the game without signals is not formalized either. This mission produces a formal model of depth-first search games on weighted trees together with the full solution of the signal game. The model consists of trees as an inductive type, leaves and branch nodes as finite types, and the expected search time of a pure strategy.

Where the difficulty lies

The natural induction on the tree has to compare games of different sizes. At a branch root, the Searcher's pure strategies on the whole tree are combinations of a root action and arbitrary pure strategies on both branches. Reducing this game to the $2\times4$ matrix of Table 1 requires an argument that optimal play in the branches can be composed with the root choice in both directions. A Hider strategy must be shown to guarantee the value against every combination, not only against strategies of the β-form. The mixing weights of the Hider distribution also depend on mean depths that are themselves defined through the distribution, so the induction must carry the identity of Proposition 6 alongside the value. Solving the $2\times4$ game then needs the sign of the slope $(p-q)(D_{Q_1}-D_{Q_2})$ and Lemma 2's bound $V\le\mu$ on each branch. A Hider distribution proportional to lengths, which is optimal without signals, is not optimal here.

Formalization scope

Trees are an inductive type RTree with constructors for a single arc, an arc leading to a subtree, and a fork with two branches. This also admits interior nodes of degree two and forks whose branches start with a fork, which is the paper's own conversion of arbitrary trees to binary trees by arcs of length zero. Every arc has positive length. Signals and branches are booleans, and an action is a map from signals to the branch searched first. A pure Searcher strategy assigns an action to every branch node. The payoff is the expected search time. Signals off the path to the Hider do not matter, so it is computed from the marginal law of each signal on the path, and no joint law is assumed. Mixed strategies are probability vectors over all pure strategies. Value and optimality are the published matrix-game notions ZeroSumLP.DantzigExt.MatrixGame (min-max and max-min strategies of a finite zero-sum game). On a tie $D_{Q_1}=D_{Q_2}$ branch 1 is favored, and then $\beta=0$.

Neither the value nor the mean depth is defined by the formulas being proved. The value is the matrix-game value of the expected-time matrix. The mean depth is the sum of Definition 3, not the recursion of Proposition 6. The Hider's optimality must hold against every pure Searcher strategy.

A complete development needs finite sums over the leaves of a tree, the expected-time recursion, minimax for the $2\times4$ game, and the induction of Theorem 7. The tree model and the fact that a finite game's value composes over subtrees can be reused for other search games on trees. Contributions to any milestone, or to Gal's theorem as a by-product, are welcome.

Selected references

• S. Alpern, T. Lidbetter, Search for an Immobile Hider on a Binary Tree with Unreliable Locational Information, Operations Research, 2025; arXiv:2303.13378v2 (2024). https://arxiv.org/abs/2303.13378
• S. Gal, Search games with mobile and immobile hider, SIAM Journal on Control and Optimization 17(1), 99–122, 1979. https://doi.org/10.1137/0317009
• S. Alpern, Search games on trees with asymmetric travel times, SIAM Journal on Control and Optimization 48(8), 5547–5563, 2010.
• S. Alpern, T. Lidbetter, Searching a variable speed network, Mathematics of Operations Research 39(3), 697–711, 2014.

Public occupancy as an observation

A data structure can hide each stored share individually while revealing their joint value through its visible layout. This distinction matters when a ledger publishes both a collection of shares and the markers identifying which cells were filled by genuine insertions. The GBFPlus protocol records cross-domain transfers in ledger attestations and uses a shared word containing an adjacent-domain identifier. Alexander Richard Towell's note identifies an allowed singleton snapshot in which its occupied cells reveal that identifier directly. The note also gives a sufficient occupied-count certificate for recovering an aggregate from a larger batch. These are the two results targeted here. Towell, v1.0.0

The observer in that setting is a reader of a permissioned ledger. Public visibility means visibility to such a reader, not unrestricted Internet access. The source protocol's construction, publication rules and adjacent-domain recovery checks provide the context; the contribution is limited to the particular metadata and view analyzed in the note. Qin et al., GBFPlus

A finite honest insertion history

A snapshot is an array of $m$ cells. Each cell is either empty or occupied by a $\lambda$-bit word. An occupied all-zero word is distinguishable from an empty cell. Public parameters include the share count $\kappa$, with $1\le\kappa\le m$, and the identifier width $\ell$, with $0<\ell<\lambda$.

A row consists of a set $S_i$ of exactly $\kappa$ distinct positions, a $(\lambda-\ell)$-bit prefix $P_i$ and an $\ell$-bit adjacent-domain identifier $N_i$. Its target is their concatenation $T_i=P_i\Vert N_i$. The array starts empty. A successful insertion reserves an empty selected cell, retains existing occupied words, fills the other empty selected cells with free words, and sets the reserved cell to the residual required by the target. If every selected cell is already occupied, the insertion fails and leaves the array unchanged. These operations follow the construction preceding the note's two propositions. Towell, Section 2

An honest history is a finite sequence of attempts satisfying those rules at every step. Its successful rows and count $c$ are derived from that sequence; an independently asserted integer is not substituted for $c$. Let $O$ be the final occupied set, $w=|O|$, and $Z_j$ its occupied words. The public recovery statistic is

$$R(Z)=\operatorname{suffix}_{\ell}\!\left(\bigoplus_{j\in O}Z_j\right).$$

The statistic takes the snapshot and public widths. It does not take a secret prefix, query token, selected support or insertion history as an input.

Formalization targets

The goal is Proposition 1, singleton disclosure: for every honest history with exactly one successful row,

$$c=1\quad\Longrightarrow\quad R(Z)=N_1.$$

It quantifies over every admitted position set, prefix, pivot and free-share realization. The Lean statement names the sole row by requiring that the derived successful-row list is its singleton list. Towell, Proposition 1

The supporting milestones are:

1. Honest-history invariants: final occupancy equals the union of successful supports; every successful row still XORs to its original target; admissible failed insertions leave the state unchanged.
2. Disjoint-support certificate: the equality $w=c\kappa$ implies that the successful supports are pairwise disjoint. The support lemma also includes the empty history, where pairwise disjointness is vacuous.
3. Proposition 2, aggregate disclosure: for an honest history,

$$c\ge1\ \text{and}\ w=c\kappa \quad\Longrightarrow\quad R(Z)=\bigoplus_{i=1}^{c}N_i.$$

The positive-count condition is retained in this proposition. Its conclusion is an aggregate, not recovery of the individual identifiers or their multiset. Towell, Proposition 2 and its proof

What the formalization adds

The singleton identity identifies an adjacent-domain identifier from a complete share set exposed by occupancy. The larger-batch certificate establishes a narrower aggregate observation when the public occupied count matches the authentic successful count times the share count. It does not characterize every possible disclosure and does not estimate how often the certificate occurs. A deployment interpretation still needs the source's visibility and publication premises. Towell, Sections 1–2

Both propositions already have written proofs in the archived preprint. The accompanying source supplement provides finite computational checks. The remaining work here is to verify their universal statements from an explicit insertion model and preserve that construction-to-statement connection. The draft model has compiled concrete examples, including the published seven-cell array and an occupied zero word; the four theorem items remain open formal obligations. No new mathematical discovery or independent human proof review is claimed.

Where care is needed

The risk lies in changing what constitutes a snapshot or an honest insertion. Treating a zero word as empty changes the occupancy count. Allowing later writes to replace occupied shares can invalidate earlier row equations. Supplying an unrelated count can make the certificate appear applicable when the claimed aggregate is wrong. Assuming all final row equations as part of the definition of honesty would also remove the construction obligation that the mission is intended to check.

The recovery function must remain independent of hidden row data even though the theorem's conclusion refers to the identifier that was inserted. The model must admit genuine executions, including singleton, disjoint and overlapping histories, and must distinguish a legitimate full-support failure from an arbitrary skipped insertion.

Formalization scope

The shared namespace is GBFPlus.OccupancyDisclosure. A configuration stores positive prefix and suffix widths; their sum is $\lambda$. Words are pairs of finite coordinate vectors over $\mathbb Z/2\mathbb Z$. Componentwise addition is XOR, and concatenation places the prefix coordinates before the suffix coordinates. Cells use optional words, so occupancy is represented independently of payload value. Supports are finite sets of valid cell indices with exact cardinality $\kappa$; successful occurrences retain their multiplicity in an ordered list.

Free words and valid pivots are explicit inputs. Universal quantification covers each realization; no probability distribution is needed for these identities. Honest histories are checked transition by transition from the empty state, without assuming the conclusions. The model uses Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474.

Ledger read access, authentic publication, genuine occupancy and timeout rules admitting singleton release are external premises of the source interpretation. The formalization does not model cryptographic position derivation, authentication, ledger execution, the separate data-identifier privacy game, publisher identification, full paths, scan costs or a complete repair. Contributions closing the stated obligations or extracting reusable finite-share and occupancy lemmas are welcome. Alexander Richard Towell supplies the source research and direction; substantial OpenAI Codex assistance in model construction, checks and proposal preparation is disclosed. Independent AI read-backs accompany the draft items and do not substitute for human review.

Selected references

• Alexander Richard Towell, Adjacent-Domain Disclosure from Public Occupancy in GBFPlus, archival preprint v1.0.0, 20 October 2026. DOI 10.5281/zenodo.23497466.
• S. Qin, Y. Zhou, W. Dai, Y. Sun and W. Qiang, Privacy-Preserving On-Chain Attestation for Cross-Domain Data Flows via GBFPlus, Entropy 28 (2026), 947. DOI 10.3390/e28090947.

Motivation

Quantum hypothesis testing is one of the most basic tasks in quantum information theory and has fundamental links with quantum communication and estimation theory. In this paper, we establish a formula that characterizes the decay rate of the minimal Type-II error probability in a quantum hypothesis test of two Gaussian states given a fixed constraint on the Type-I error probability. This formula is a direct function of the mean vectors and covariance matrices of the quantum Gaussian states in question. We give an application to quantum illumination, which is the task of determining whether there is a low-reflectivity object embedded in a target region with a bright thermal-noise bath. For the asymmetric-error setting, we find that a quantum illumination transmitter can achieve an error probability exponent stronger than a coherent-state transmitter of the same mean photon number, and furthermore, that it requires far fewer trials to do so. This occurs when the background thermal noise is either low or bright, which means that a quantum advantage is even easier to witness than in the symmetric-error setting because it occurs for a larger range of parameters. Going forward from here, we expect our formula to have applications in settings well beyond those considered in this paper, especially to quantum communication tasks involving quantum Gaussian channels.

This mission is the statement-level formalization of Gaussian hypothesis testing and quantum illumination (arXiv:1608.06991v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Compatible ordinary diagonalization and Gibbs-matrix equivalence (Appendix A, (A4)–(A13), PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

10 results of the paper are not stated yet, because the library lacks an interface they need:

• Theorem 1, (10), Appendix C and D: Independent relative entropy variance of full n-mode Gaussian density operators, including singular rho (hard)
• Unnumbered expansion (1)–(2): Optimal IID quantum testing error and its separable Gaussian second-order expansion (hard)
• Coherent-state formulas (15)–(16): Returned coherent thermal/displaced-thermal states and independent D,V (hard)
• Quantum-illumination expansion (17)–(18): Actual quantum-illumination returned pair and large-NS D,V remainders (hard)
• Quantum-illumination expansion (19)–(20): Actual quantum-illumination pair and large-NB D,V remainders (hard)
• Qualitative claim and Figure 1: Quantified parameter ranges and finite-copy comparison for far fewer trials (source-ambiguity)
• Fourth quadratic moment (14), Appendix B: Ordered unbounded fourth quadratic moment on the Gaussian oscillator domain (hard)
• Proposition 2, (D1): Independent V and its equality to the grouped symplectic expression (hard)
• Lemma 3, (E14): Independent two-mode relative entropy variance and reduced grouped extension (hard)
• Lemma 4, corrected (E24): Independent Gaussian operator relative entropy and corrected E24 (hard)

Selected references

• Gaussian hypothesis testing and quantum illumination, arXiv:1608.06991v2, https://arxiv.org/abs/1608.06991v2

Motivation

Online platforms, social networks and marketplaces run randomized experiments (A/B tests) to estimate the effect of a new feature. The standard analysis assumes that one unit's treatment does not affect another unit's outcome. On a network this fails: a treated user changes what their friends see, a treated seller changes what competing sellers sell. The resulting interference biases the naive difference-in-means estimator, often by more than the effect being measured.

Two classical answers sit at opposite ends of a trade-off. The difference-in-means (DM) estimator ignores interference: its variance is small, but its bias is first order in the interference strength. The Horvitz–Thompson (HT) estimator removes the bias by importance weighting over each unit's whole neighbourhood, at a variance exponential in the degree. Peng, Ye and Zheng (arXiv:2503.02271v1, ACM EC 2025) propose the Differences-in-Neighbors (DN) estimator, which sits in between: its bias is second order in the interference strength, and its variance is polynomial in the degree. DN extends the Differences-in-Q estimator for Markovian interference of Farias et al. (2022) to general interference graphs.

This mission formalizes DN's bias bound, Theorem 1 of the paper, and the steps of its proof.

Setting

There are $N$ units. Interference is an undirected graph $G$ without self-loops: $\mathcal N_i$ is the set of neighbours of unit $i$, and $d = \max_i |\mathcal N_i|$ is the maximum degree. A treatment vector is $z \in \{0,1\}^N$, and unit $i$ has a potential outcome function $f_i : \{0,1\}^N \to \mathbb R$, with observed outcome $Y_i = f_i(z)$.

Assumption 1 (neighborhood interference). $f_i(z)$ depends only on $z_i$ and on $(z_j)_{j \in \mathcal N_i}$. The paper assumes this throughout.

The target is the average treatment effect

$$\mathrm{ATE} = \frac1N \sum_{i=1}^N \bigl(f_i(\vec 1) - f_i(\vec 0)\bigr),$$

the average difference between global treatment and global control. The conditional outcome functions $f^1_i$, $f^0_i$ are unit $i$'s outcome when its own treatment is $1$ or $0$, as a function of the other treatments.

The design draws $z_i$ i.i.d. Bernoulli$(p)$, $0 < p < 1$. The DN estimator is

$$\mathrm{ATE}_{\mathrm{DN}} = \frac1N \sum_{i=1}^N \Bigl(\frac{z_i}{p} - \frac{1 - z_i}{1 - p}\Bigr)\Bigl(\sum_{j \in \mathcal N_i} Y_j\, \xi_j + Y_i\Bigr), \qquad \xi_j = \frac{z_j(1-p)}{p} + \frac{(1 - z_j)p}{1 - p}.$$

Smoothness is measured by second-order finite differences. For $h : \{0,1\}^N \to \mathbb R$ and units $j, k$,

$$\Delta_{jk} h(z) = h(z^{(z_j=1,z_k=1)}) - h(z^{(z_j=0,z_k=1)}) - h(z^{(z_j=1,z_k=0)}) + h(z^{(z_j=0,z_k=0)}),$$

where $z^{(z_j=a,z_k=b)}$ is $z$ with entries $j, k$ set to $a, b$. The function $h$ is $\epsilon$-smooth if $|\Delta_{jk} h(z)| \le \epsilon$ for all $z$, $j$, $k$.

The proof uses the multilinear extension $F(w) = \sum_{z} \prod_j \bigl(z_j w_j + (1 - z_j)(1 - w_j)\bigr) h(z)$, the expectation of $h(Z)$ when the $Z_j$ are independent Bernoulli$(w_j)$.

Formalization targets

Goal: Theorem 1 (p. 9)

Under Assumption 1 and the Bernoulli$(p)$ design, if $f^1_i$ and $f^0_i$ are $\epsilon$-smooth for every unit $i$, then

$$\bigl|\mathrm{ATE} - \mathbb E[\mathrm{ATE}_{\mathrm{DN}}]\bigr| \le d^2 \epsilon.$$

Milestones (proof of Theorem 1, §3, §3.3)

The proof has no numbered lemmas. The milestones are its displayed claims, in the order the proof uses them:

1. Credit assignment (5): $\mathrm{ATE}_{\mathrm{DN}} = \frac1N \sum_i \bigl(\eta_i + \xi_i \sum_{j \in \mathcal N_i} \eta_j\bigr) Y_i$ with $\eta_j = z_j/p - (1 - z_j)/(1 - p)$.
2. First partial derivative: $\partial F/\partial w_j = \mathbb E[h(Z) \mid Z_j = 1] - \mathbb E[h(Z) \mid Z_j = 0]$.
3. Propensity weights: $\mathbb E[f^1_i(Z)] = \mathbb E[(Z_i/p) Y_i]$, $\mathbb E[f^0_i(Z)] = \mathbb E[((1 - Z_i)/(1 - p)) Y_i]$, and $\mathbb E[f^a_i(Z) \mid Z_j = b] = \mathbb E\bigl[\frac{\mathbf 1\{Z_i = a\}}{\Pr(Z_i = a)} \frac{\mathbf 1\{Z_j = b\}}{\Pr(Z_j = b)} Y_i\bigr]$.
4. Unbiasedness for the first-order approximation: $\mathbb E[\mathrm{ATE}_{\mathrm{DN}}]$ equals the node average of the first-order Taylor approximations of $F^1_i(1) - F^0_i(0)$ around $p$.
5. Second partial derivatives: $\partial^2 F/\partial w_j \partial w_k = \mathbb E[\Delta_{jk} h(Z)]$ for $j \neq k$, and $\partial^2 F/\partial w_j^2 = 0$.
6. Taylor remainder (corrected): the error of the first-order approximation to $F^a(a)$ is $\frac12 (a - p)^\top H^a(p')(a - p)$ for some $p'$ between $(p, \dots, p)$ and $(a, \dots, a)$.
7. Remainder bound: $\bigl|\sum_{j \neq k \in \mathcal N_i} (a - p)^2\, \mathbb E_{p'}[\Delta_{jk} f^a_i(Z)]\bigr| \le d^2 \epsilon$.

Milestone 6 corrects the paper. The page states the remainder without the factor $\frac12$ of Taylor's theorem, which is false: a unit with two neighbours and $f^1(z) = z_1 z_2$ at $p = \frac12$ has error $\frac14$, while $(a - p)^\top H (a - p) = \frac12$. With the $\frac12$ restored, milestones 6 and 7 bound each treatment's error by $\frac12 d^2 \epsilon$, and Theorem 1's $d^2\epsilon$ is their sum.

Significance

Theorem 1 is the main bias guarantee for DN. Specialized to the paper's outcome model with interference magnitude $\delta$ (Corollary 1), it gives bias $O(d^2 \delta^2)$, compared with $\Theta(d\delta)$ for DM. Together with the variance bound $O(d^4/N)$ of Theorem 2, it places DN strictly between DM and HT in the bias–variance trade-off, and it covers the Markovian interference models of Farias et al. as a special case of the graph.

The proof also shows how DN is derived: DN is the unbiased propensity-weighted estimate of a first-order Taylor expansion of the multilinear extension. Higher-order expansions give higher-order estimators with the same analysis.

As far as a search of Prove2Me shows, no network-interference model, neighbourhood potential-outcome framework or DN-type estimator has been formalized. The platform's experiment-design items are temporal (Markovian or switchback) interference models. The paper's result is proved on paper; it has not been machine-checked. The mission also states one correction (the factor $\frac12$ above).

Difficulty

Most of the proof is exact finite algebra: the credit-assignment identity, the propensity-weight identities and unbiasedness are rearrangements of sums over $\{0,1\}^N$ using independence. The analytic step is the Taylor remainder. $F$ is a polynomial in $N$ variables, and Taylor's theorem must be applied along the diagonal segment from $(p, \dots, p)$ to $(a, \dots, a)$. The second derivative along that segment must then be identified with the off-diagonal Hessian entries $\mathbb E_{p'}[\Delta_{jk} h]$. One natural shortcut, bounding each Hessian entry separately and summing over all of $\{0,1\}^N$, loses the restriction to $j, k \in \mathcal N_i$. That restriction is where Assumption 1 enters, and it is what yields $d^2$ rather than $N^2$. Without Assumption 1 the theorem is false: on the empty graph with two units and $f_1(z) = z_2$, the ATE is $\frac12$, $\mathbb E[\mathrm{ATE}_{\mathrm{DN}}] = 0$, and $d = \epsilon = 0$.

Formalization scope

• Units are a finite type ι with $N$ = Fintype.card ι, and treatments are ι → Bool. The graph is a Mathlib SimpleGraph, with $\mathcal N_i$ = G.neighborFinset i and $d$ = G.maxDegree.
• Outcomes are f : ι → (ι → Bool) → ℝ. Assumption 1 is the predicate NeighborhoodInterference G f. It is a hypothesis of the goal and is omitted from milestones whose statements hold without it.
• Expectations are finite sums. mlExt h w is the multilinear extension, and bernExp p h = mlExt h (p, …, p) is the expectation under the design. Conditional expectations given $Z_j = b$ set coordinate $j$ to $b$ (Function.update), which is exact by independence.
• $f^a_i$ is condOutcome f i a, the function $z \mapsto f_i(z \text{ with } z_i := a)$ on the whole vector. Under Assumption 1 it depends only on $z_{\mathcal N_i}$.
• $\epsilon$-smoothness quantifies all $z$ and all $j, k$, as printed (so $\Delta_{jj} \equiv 0$ forces $\epsilon \ge 0$). The hypotheses $0 < p < 1$ make the weights $1/p$ and $1/(1-p)$ meaningful.
• The estimator is (3) exactly, with the factor $1/N$ and the correction $\xi_j$, for general $p$. It is not the $p = \frac12$ form (4).

Two formalizations would make the goal a different theorem and are ruled out. In the first, the expectation is taken at a single fixed treatment vector instead of under the Bernoulli design. In the second, $\epsilon$-smoothness is imposed on $f_i$ itself instead of on $f^1_i$ and $f^0_i$: that also constrains the pairs $(i, k)$, which are not second-order interference terms.

The development needs only Mathlib: finite sums over ι → Bool, HasDerivAt, and Taylor's theorem in one variable (taylor_mean_remainder_lagrange). Lemmas about multilinear extensions of functions on the Boolean cube are reusable beyond this mission. Proofs of any milestone are welcome, as are the variance bound (Theorem 2) and the clustered estimator results (Theorems 3–4) as follow-up statements.

Selected references

• T. Peng, N. Ye, A. Zheng, Differences-in-Neighbors for Network Interference in Experiments, ACM EC 2025; arXiv:2503.02271v1, 2025. https://arxiv.org/abs/2503.02271v1
• V. F. Farias, A. A. Li, T. Peng, A. Zheng, Markovian Interference in Experiments, NeurIPS 2022. https://arxiv.org/abs/2206.02371
• J. Ugander, B. Karrer, L. Backstrom, J. Kleinberg, Graph Cluster Randomization: Network Exposure to Multiple Universes, KDD 2013. https://arxiv.org/abs/1305.6979
• P. M. Aronow, C. Samii, Estimating Average Causal Effects Under General Interference, with Application to a Social Network Experiment, Annals of Applied Statistics 11(4), 2017. https://doi.org/10.1214/16-AOAS1005