All missions

Why inspection timing matters

A firm that relies on employees to process transactions can lose money when errors remain undetected. Inspection catches errors, but each inspection costs money, and employees may change their care when they know when an inspection will occur. These effects make the timing of inspections part of a contract design problem, not just a scheduling choice. Kim and Xu study that problem in a continuous-time principal–agent model of operational risk. Their SSRN preprint proves that the ranking of two common inspection policies changes with the cost of inspection: periodic inspection is better at low cost, while random inspection is better at high cost (Proposition 4, p. 17). This mission targets that result in the authors' July 2023 preprint, whose numbering is used throughout.

The comparison matters because neither inspection policy has an unconditional advantage in the model. A periodic schedule fixes the time until the next inspection; a random schedule makes that time uncertain. The agent responds to the schedule through effort, while the firm pays both for inspections and for errors left unresolved. Choosing a policy by its inspection frequency alone therefore misses a change in the agent's response and in the duration of losses. The paper develops both policies' optimal contracts before comparing their payoffs Kim and Xu, §§3–4.

The model

The principal is a firm and the agent is an employee. The firm earns base profit at rate $\mu>0$. The agent chooses a nonnegative effort path $a(t)$, where $t$ is time since the last inspection, at unit cost $c>0$. Errors arrive at aggregate rate $\lambda e^{-a(t)}$, with $\lambda>0$. Each unresolved error causes expected loss $L>0$ per unit time until the next inspection finds and corrects it. The paper begins with several error classes, then uses their aggregate arrival rate $\lambda$ and rate-weighted mean loss $L$ for the remainder of the analysis (7), p. 10.

The firm chooses an inspection frequency $v$, a penalty $P$ charged to the employee per error found, and a wage $w$. Under the random policy $R$, the time $\tau$ between inspections is exponentially distributed with rate $v$; under the periodic policy $D$, it equals $1/v$. The employee chooses a best response to the announced policy and contract. The employee must receive at least the reservation payoff $\bar\pi>0$. Both parties discount future payoffs at rate $r>0$. An inspection costs the firm $K>0$ per cycle. Equations (1) and (3) specify their discounted payoffs; equation (6) gives the firm's reduced payoff when participation binds §3, pp. 8–10.

The standing Assumption 1 is $c<L\lambda/r$ and $L\lambda/r<\bar\mu$, with $\bar\mu=\mu-r\bar\pi$. The first inequality excludes the paper's degenerate no-effort regime; the second ensures that the adjusted base profit exceeds the expected operational loss of the uninspected benchmark (7), p. 10. In the formalization, all six parameters $r,c,\lambda,L,\mu,\bar\pi$ are also positive, as stated in §3.

Formalization targets

The goal is Proposition 4. For fixed model parameters there is one inspection-cost threshold $K_{RD}$, independent of the particular positive cost $K$, such that

$$0<K<K_{RD}\quad\Longrightarrow\quad \Pi_R(S_R^*)<\Pi_D(S_D^*),$$ $$0<K\ \text{and}\ K>K_{RD}\quad\Longrightarrow\quad \Pi_D(S_D^*)<\Pi_R(S_R^*).$$

Here $S_R^*$ and $S_D^*$ are optimal feasible strategies under the respective inspection laws. The paper does not specify which policy is better at $K=K_{RD}$, and the formal goal does not add an equality claim there Proposition 4, p. 17.

The milestones first connect binding participation to the firm's reduced payoff in (6). Lemma 3 identifies constant optimal effort under random inspections and its threshold $\underline v_R$; Lemma 4 identifies the time-dependent effort under periodic inspections and its threshold $\underline v_D$. The two statements in §4.2 then express the firm's reduced payoff through the explicit random branches $\bar V_R,V_R^0$ of (EC.2) and periodic branches $\bar V_D,\underline V_D,V_D^0$ of (EC.4) pp. 10, 13–14 and ec5–ec6. These targets fix the model and its regime changes before solvers address the policy-level optimization.

What the result establishes

The result distinguishes regimes in which a predictable inspection date pays off from regimes in which an uncertain one pays off, after each policy's frequency, penalty, wage and induced effort are optimized. It is a claim about the principal's optimal payoff under complete contracts in the paper's model. It does not assert that either schedule dominates for every fixed frequency or penalty. The strict comparisons matter: they identify a genuine reversal rather than a weak inclusion of one policy's feasible strategies in another's Proposition 4, p. 17.

Kim and Xu proved this proposition in the cited preprint; the open work in this mission is to give its stated model, supporting results and comparison a machine-checked Lean proof. The definitions of inspection laws, achievable payoffs and discounted cycle quantities can also support the paper's separate hybrid-policy comparison and future formal work on continuous-time inspection contracts. The closed-form payoff branches provide testable interfaces between the economic model and the optimization results. The mission does not claim that any of these proofs is already machine checked.

Where the difficulty lies

The direct intuition that unpredictable inspections should always restrain delayed effort fails as a policy comparison. Under a periodic schedule, the employee can increase effort near the known inspection time, but earlier inspection also shortens the time that errors remain costly. The relative effect depends on $K$ and on which effort regime is optimal. An argument based only on the employee's response at a fixed $(v,P)$ cannot determine the ranking of the principal's optimized payoffs. The paper's characterization of each policy includes both effort inducement and error correction modes, with different closed forms and cost thresholds §4.2, pp. 14–15; proof of Proposition 4, pp. ec30–ec33.

Formalization scope

Lean represents an effort path as a real-valued function of time since the last inspection. It is measurable, nonnegative and bounded. The last condition is a disclosed modelling pin: it ensures that the real-valued expected effort and error terms do not acquire Lean's default zero value for a nonintegrable function. The random interval law is Mathlib's exponential measure; the periodic law is a Dirac measure at $1/v$. The error classes are aggregated using $\lambda$ and $L$, and expected errors are $\lambda\int_0^t e^{-a(s)}ds$. This starts at the discounted cycle payoff equations (1) and (3), rather than reconstructing the underlying Poisson and Brownian processes §3 and Appendix EC.4.1.

Feasible principal strategies require $v>0$, $P,w\ge0$, a best-responding agent and the participation constraint. This makes the $1/v$ formulas meaningful. The agent's best-response test sets $w=0$, because wage enters payoff additively and cannot change which effort is optimal. A policy comparison uses achievable payoffs: it asserts an achievable payoff for the better policy exceeding every achievable payoff of the worse policy. That formulation avoids default values of a real supremum over an empty or unbounded set. It also prevents an empty feasible set from satisfying a comparison vacuously. The threshold $K_{RD}$ is quantified before $K$, and the source does not explicitly require it to be positive. Formulas dividing by $P$ are invoked only when $P>c/\lambda$; the zero-penalty case has a separate statement.

This initial mission includes the model, the effort lemmas, the two payoff-regime statements and Proposition 4. Characterizing the globally optimal random and periodic contracts and their comparisons remains welcome solver work; their long closed-form optimization results have not been weakened into easier draft milestones. Reusable contributions include integration facts for the exponential and Dirac laws, best-response characterizations up to almost-everywhere equality, and analytic properties of the payoff branches.

Selected references

• Y. Kim and Y. Xu, Operational Risk Management: Optimal Inspection Policy, SSRN preprint 3491006, version compiled July 2023, SSRN. Published in Management Science, DOI 10.1287/mnsc.2021.00322. The mission cites the preprint's page and result numbering.

Motivation

Machines in production lines deteriorate in ways that are only partly visible. A machine may run in a degraded state that raises costs without announcing itself, and eventually fail in a way that cannot be missed. The decision maker must choose between continuing production, paying for an inspection that reveals the hidden state, and replacing the machine preventively. Models of this kind are partially observable Markov decision processes (POMDPs), and for POMDPs closed-form optimal policies are rare: the value function lives on the space of beliefs and is usually only computed numerically.

H. Zhang and W. Zhang, Analytical Solution to a Partially Observable Machine Maintenance Problem with Obvious Failures (Management Science, 2022; read here as SSRN 2945049, version of 2022-08-21), solve the classical two-state version of this problem completely. Working in the dual "efficient frontier" framework of Zhang (2010), they show that the optimal solution has exactly six possible structures and give each in closed form, with explicit or implicitly characterized thresholds on the replacement and inspection costs.

Setting

A machine is in a hidden state $x\in\{0,1\}$ (good or bad) or in the observable failure state $F$. Each period, if the machine has failed it is replaced correctively at cost $c^F$; otherwise one of three actions is chosen:

• production $P$ costs $0$ in state 0 and $c^P$ in state 1;
• inspection $I$ costs $c^I$ and reveals the current state;
• preventive replacement $R$ costs $c^R$ and resets the machine to state 0.

Production always takes place. From state 0 the machine moves to state 1 with probability $\gamma_0$; from state 1 it fails with probability $\gamma_1$. Write $\bar\gamma_x=1-\gamma_x$, $\mathbf p_0=(\bar\gamma_0,\gamma_0)'$, $\mathbf p_1=(0,\bar\gamma_1)'$, $\mathbf g^P(u_F)=(0,c^P+\beta\gamma_1u_F)'$, $\mathbf g^I(u_F)=(c^I,c^I+\beta\gamma_1u_F)'$ and $\mathbf P^P\mathbf u=(\mathbf p_0'\mathbf u,\mathbf p_1'\mathbf u)'$. Costs are discounted by $\beta$ over an infinite horizon.

A continuation-cost vector $\mathbf u=(u_0,u_1)'$ records the cost of a continuation policy from each hidden state, and $u_F$ the cost after a failure. The expected optimal cost at an (unnormalized) belief $\boldsymbol\pi=(\pi_0,\pi_1)'\ge0$ is $V(\boldsymbol\pi)=\min_{\mathbf u\in U^*}\boldsymbol\pi'\mathbf u$, where $U^*$ is the set of extreme points of the efficient frontier. The pair $(U^*,u^*_F)$ is the fixed point of the dual value iteration (12)–(16). In support-function form, a pair $(W,w_F)$ is mapped to

$$W'(\boldsymbol\pi)=\min\Big\{\boldsymbol\pi'\mathbf g^P(w_F)+\beta W\big((\mathbf P^P)'\boldsymbol\pi\big),\ (\pi_0+\pi_1)\big(c^R+\beta W(\mathbf p_0)\big),\ \boldsymbol\pi'\mathbf g^I(w_F)+\beta\big(\pi_0W(\mathbf p_0)+\pi_1W(\mathbf p_1)\big)\Big\},$$ $$w_F'=c^F+\beta W(\mathbf p_0),$$

the three terms being $P$, $R$ and $I$. A finite set $U$ with a number $u_F$ is the optimal solution for an action set if value iteration from zero terminal costs converges to $\min_{\mathbf u\in U}\boldsymbol\pi'\mathbf u$ for every $\boldsymbol\pi\ge0$ and to $u_F$ after a failure.

The structures are built from two point sequences. The production sequence is $\mathbf u_{i+1}=\mathbf g^P(u_F)+\beta\mathbf P^P\mathbf u_i$. Started on the diagonal at $(u^R,u^R)'$ with $u_F=u^R+c^F-c^R$, the self-consistency equation $u^R=c^R+\beta\mathbf p_0'\mathbf u_m$ has a unique solution $u^R=f(m)$ (31). Started instead at the inspection point (35), it gives $g(m)$ (40).

Formalization targets

Goal: Theorem 2 (pp. 27–28, Table 1)

Let $\theta=\dfrac{c^P+\beta\gamma_1c^F}{1-\beta+\beta(\gamma_0+\gamma_1)}$ and $\hat c=(1+\beta\gamma_0)c^P-\beta\bar\gamma_1(1-\beta+\beta\gamma_0+\beta\gamma_1)c^R+\beta^2\gamma_1\bar\gamma_1c^F$. Under $\{P,I,R\}$:

$$c^R\ge\theta\ \Rightarrow\ [P];\qquad \tfrac{\gamma_0}{\gamma_1}\theta\le c^R<\theta\ \Rightarrow\ R[P],\ IR[P]\ \text{or}\ [PIR]\ \text{by explicit thresholds on }c^I;$$ $$c^R<\min\{\tfrac{\gamma_0}{\gamma_1}\theta,\theta\}\ \Rightarrow\ \exists\,0<\hat c_1\le\hat c_2<c^R:\ [PR],\ I[PR]\ \text{or}\ [PIR]\ \text{as}\ c^I\ge\hat c_2,\ \hat c_1\le c^I<\hat c_2,\ c^I<\hat c_1,$$

with every structure an explicit pair $(U^*,u^*_F)$ from Table 1, and the thresholds characterized implicitly ($\mathbf u^{I\dagger}$ on the frontier of $U^\dagger$ at $c^I=\hat c_2$; $\min f=\min g$ at $c^I=\hat c_1$).

Milestones

Proposition 2 (the fixed-point equations), Proposition 3 (the cost of producing forever), Lemma 1 and Lemma 6 (the two sequences in closed form), Lemma 3 and Lemma 7 (the anchors $f$ and $g$), Proposition 4 (unimodality of $f$), Theorem 1 (the two-action solution: $[P]$, $R[P]$, $[PR]$, with extreme-point exactness) and Lemma 5 (when inspection enters).

Significance

The result. The theorem turns a POMDP into a finite list of explicit policies. Each structure is a periodic plan that needs no belief updating: produce for $m^\dagger$ periods and replace; or inspect every $m^*$ periods and replace only if the machine is found bad. The thresholds tell when inspection is worth its cost, and the comparative statics of $m^\dagger$ and $m^*$ follow from the closed forms. The authors use the solution to justify common maintenance practices.

Formalizing it. The result is proved in the paper (main text §4, proofs in its e-companion, App. A); no part is machine-checked. The proofs of Theorems 1 and 2 argue geometrically from figures of convex curves in the plane ("the curve bends back", "all the points are still extreme points"). A formal development has to turn these into inequalities between piecewise-linear concave functions, and has to prove convergence of value iteration to the stated sets. The implicit thresholds of part (3) were not checked numerically when this mission was planned. Parts (1) and (2) and Theorem 1 were.

Difficulty

Verifying that a candidate set $U$ is a fixed point is not enough: the goal asserts that value iteration from zero converges to it, so uniqueness of the bounded fixed point must be proved (a contraction argument in the supremum norm over the simplex). More importantly, finding the frontier requires knowing which points of the infinite production sequence are extreme, which depends on the location of the anchor relative to the curve $\{\mathbf u_i:i\ge0\}$ (Fig. 5 of the paper, five subcases). The natural induction on $m$ fails because $f$ is not monotone: its least minimizer $m^\dagger$ must be located through the unimodality of the real extension (Proposition 4). In part (3) the thresholds $\hat c_1,\hat c_2$ are defined implicitly, and showing that the three regimes are ordered in $c^I$ requires monotonicity of the whole frontier in $c^I$.

Formalization scope

Everything is defined in the namespace MaintPOMDP.Frontier. Vectors and beliefs are Fin 2 → ℝ (index 0 = good state); beliefs are unnormalized, $\boldsymbol\pi\ge0$. The optimal solution is the limit of the support-function value iteration started from $W\equiv0$, $w_F=0$; "the structure is X" means that this limit equals $\min$ over the points of row X of Table 1, with the failure cost of that row.

Standing assumptions: $0<\beta<1$, $0<c^P<c^I<c^R<c^F$ (p. 14), and $0<\gamma_0<1$, $0<\gamma_1<1$, which the paper never states and which are added (the thresholds divide by $\gamma_1$). The hypothesis $\gamma_0\ne\gamma_1$ is added only to Lemmas 1, 3, 6, 7 and Proposition 4, whose printed formulas divide by $\gamma_1-\gamma_0$; $f$ and $g$ themselves are defined as solutions of the affine anchor equations, so Theorems 1 and 2 cover $\gamma_0=\gamma_1$. Proposition 4 also carries the range of $c^R$ that its proof uses. "$m^\dagger=\arg\min f$" is the least minimizer, and its existence is part of the conclusion. In Theorem 2, the indices $n_R,n_I$ of Table 1 are existential and extreme-point exactness is not asserted for the $I[PR]$ and $[PIR]$ rows (Table 1's $I[PR]$ row conflicts with the paper's Proposition 8). It is asserted in Theorem 1. In part (3) the thresholds are chosen before $c^I$ and the claims hold for every $c^I\in(c^P,c^R)$.

Trivializing readings are ruled out: the value function is the limit of the iterates, not an arbitrary fixed point or a junk limit; identities hold for every belief $\boldsymbol\pi\ge0$, not only at vertices; every frontier set is given by formulas, so no extra points can be slipped in; minimizers are asserted, not assumed; and thresholds involving $\gamma_0/\gamma_1$ are evaluated with $\gamma_1>0$.

A complete development needs convergence of value iteration for a monotone contraction on bounded functions over the cone $\boldsymbol\pi\ge0$, explicit solutions of two-dimensional linear recurrences, and lemmas on lower envelopes of finitely many linear functions in two variables. These are reusable beyond this mission, for other two-state POMDPs. Contributions of any milestone, of the γ0 = γ1 closed forms (App. B), or of a proof of Theorem 1 alone are welcome.

Selected references

• H. Zhang, W. Zhang, Analytical Solution to a Partially Observable Machine Maintenance Problem with Obvious Failures, Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4547 (read as SSRN 2945049, https://ssrn.com/abstract=2945049)
• H. Zhang, Partially Observable Markov Decision Processes: A Geometric Technique and Analysis, Operations Research 58(1), 2010. https://doi.org/10.1287/opre.1090.0697
• R. D. Smallwood, E. J. Sondik, The Optimal Control of Partially Observable Markov Processes over a Finite Horizon, Operations Research 21(5), 1973. https://doi.org/10.1287/opre.21.5.1071
• S. M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9), 1971. https://doi.org/10.1287/mnsc.17.9.587

Motivation

Many quantum algorithms end in a measurement that succeeds only with some probability $a$. Two questions follow: how to raise that probability, and how to learn its value. G. Brassard, P. Høyer, M. Mosca and A. Tapp answered both in Quantum Amplitude Amplification and Estimation (arXiv:quant-ph/0005055, 2000; Contemporary Mathematics 305, 2002). Amplitude amplification generalizes Grover's search (Grover 1996) to an arbitrary algorithm $\mathcal A$ and an arbitrary notion of success. Amplitude estimation combines amplification with the quantum Fourier transform to estimate $a$ with error of order $1/M$ after $M$ applications of $\mathcal A$, where classical sampling needs order $1/M^2$ samples. Quantum counting, quantum Monte Carlo integration (Montanaro 2015) and many quantum speedups for statistics and finance rest on this estimation step.

Timeline:

• 1996: Grover's search algorithm.
• 1997: Brassard and Høyer (arXiv:quant-ph/9704027) introduce the amplification operator $\mathbf Q$ for a general algorithm.
• 1998: Brassard, Høyer and Tapp (arXiv:quant-ph/9805082) give quantum counting.
• 2000: the paper formalized here presents amplification, estimation and counting in a unified form with explicit constants.

Setting

Let $\mathcal H = \mathbb C^\iota$ be a finite-dimensional Hilbert space with computational basis $\{|x\rangle : x\in\iota\}$ and a distinguished zero state $|0\rangle$. A quantum algorithm without measurements is a unitary matrix $\mathcal A$ on $\mathcal H$, and a Boolean function $\chi:\iota\to\{0,1\}$ calls a basis state good when $\chi(x)=1$. Write $|\Psi\rangle=\mathcal A|0\rangle=|\Psi_1\rangle+|\Psi_0\rangle$ for the splitting into the projections onto the good and the bad subspaces. The initial success probability is $a=\langle\Psi_1|\Psi_1\rangle$, the probability that measuring $|\Psi\rangle$ gives a good state, and $\theta_a\in[0,\pi/2]$ is the angle with $\sin^2\theta_a=a$.

The operator $\mathbf S_\chi$ flips the sign of the amplitudes of good states, $\mathbf S_0$ flips the sign of the amplitude of $|0\rangle$, and the amplification operator is

$$\mathbf Q=-\mathcal A\,\mathbf S_0\,\mathcal A^{-1}\,\mathbf S_\chi .$$

For an integer $M\ge1$, the quantum Fourier transform is $F_M:|x\rangle\mapsto\frac1{\sqrt M}\sum_{y=0}^{M-1}e^{2\pi\imath xy/M}|y\rangle$, and the controlled power is $\Lambda_M(U):|j\rangle|y\rangle\mapsto|j\rangle U^j|y\rangle$. The phase state is $|S_M(\omega)\rangle=\frac1{\sqrt M}\sum_y e^{2\pi\imath\omega y}|y\rangle$, and $d(\omega_0,\omega_1)=\min_{z\in\mathbb Z}|z+\omega_1-\omega_0|$ is the circular distance. The algorithm $\mathbf{Est\_Amp}(\mathcal A,\chi,M)$ applies $(F_M^{-1}\otimes I)\,\Lambda_M(\mathbf Q)\,(F_M\otimes I)$ to $|0\rangle\mathcal A|0\rangle$, measures the first register to obtain $y\in\{0,\dots,M-1\}$, and outputs $\tilde a=\sin^2(\pi y/M)$.

Formalization targets

Goal: Theorem 12 (Amplitude Estimation)

For every positive integer $k$, the event

$$|\tilde a-a|\le 2\pi k\frac{\sqrt{a(1-a)}}{M}+k^2\frac{\pi^2}{M^2}$$

has probability at least $8/\pi^2$ when $k=1$, and greater than $1-\frac1{2(k-1)}$ when $k\ge2$. If $a=0$ then $\tilde a=0$ with certainty. If $a=1$ and $M$ is even, then $\tilde a=1$ with certainty.

Milestones, in attack order

1. Lemma 1: $\mathbf Q$ acts on $|\Psi_1\rangle$ and $|\Psi_0\rangle$ by an explicit $2\times2$ matrix.
2. Equations (3)–(5): for $0<a<1$, $|\Psi_\pm\rangle$ are orthonormal eigenvectors of $\mathbf Q$ with eigenvalues $e^{\pm\imath2\theta_a}$.
3. Equation (6): $|\Psi\rangle$ in that eigenbasis.
4. Lemma 7: the error in the angle controls the error in $\sin^2$.
5. Lemma 10: the overlap $|\langle S_M(\omega_0)|S_M(\omega_1)\rangle|^2$.
6. Theorem 11: the exact law of phase estimation and its two tail bounds.
7. Two steps of the proof of Theorem 12 (p. 20): the state after $\Lambda_M(\mathbf Q)$, and the outcome law as an even mixture of two phase-estimation laws.

Further statements from the same development are included as companion targets: the success probability $\sin^2((2m+1)\theta_a)$ after $m$ rounds, Theorem 2 (quadratic speedup), Lemma 5 (the phase-generalized $\mathbf Q$), Theorem 13 (counting) and Corollary 14.

Significance

Theorem 12 is the quantitative core of quantum estimation algorithms. Its error bound scales as $1/M$ in the number of applications of $\mathbf Q$, and that scaling is the quadratic speedup behind quantum counting (Theorem 13), quantum mean estimation, and quantum Monte Carlo methods for option pricing and risk analysis. The exact clauses for $a\in\{0,1\}$ make the estimator usable as a zero-error test for the existence of a good state.

All results here are proved in the paper and widely reproduced in textbooks; none is open. What the mission adds is a machine-checked account with the paper's constants: $8/\pi^2$, the strict tail bound $1-1/(2(k-1))$, and the additive term $k^2\pi^2/M^2$. It also covers every modulus $M\ge1$, not only powers of two, and arbitrary $\mathcal A$ and $\chi$, not only uniform search. Related statements are posed on the platform but unproved:

• QAlgorithms.Nannicini.amplitudeEstimation_error is the special case $k=1$, $M=2^m$, with a bit-string presentation of the algorithm.
• QAlgorithms.Nannicini.groverOperator_eigenstates states (3)–(4) for an abstract reflection.
• QAlgorithms.DeWolf.amplitudeAmplification covers (8) and the $1-a$ half of Theorem 2.

The Grover theorems already proved on the platform treat a single marked item with a uniform start.

Difficulty

The obvious argument has two parts: $\mathbf Q$ rotates a plane by $2\theta_a$, and phase estimation reads off $\theta_a$. Neither part settles the measurement law. The outcome probability is a sum over the second register of the squared amplitudes of an entangled state. Reducing it to two independent phase-estimation laws requires orthonormality of $|\Psi_\pm\rangle$, and that holds only for $0<a<1$. The goal does not assume this: the degenerate cases $a\in\{0,1\}$, where $|\Psi_\pm\rangle$ do not exist, must be handled separately.

On the phase-estimation side, the tail bound for $k\ge2$ must be strict and must hold for every $M\ge1$. The bound $8/\pi^2$ for $k=1$ relies on a minimization over $\Delta\in[0,1/M]$ that needs $M>2$, while the goal has no such hypothesis, so the small cases $M\le2$ need their own argument. Finally, the second eigenphase appears as $1-\theta_a/\pi$, and the matching outcome $M-y$ wraps to $0$ at $y=0$.

Formalization scope

States are vectors $\iota\to\mathbb C$ over a finite type $\iota$ (the paper writes $\chi:\mathbb Z\to\{0,1\}$), operators are matrices, and $\{0,1\}$ is Bool. $\mathcal A$ is assumed unitary and $\mathcal A^{-1}$ is written $\mathcal A^\dagger$. The second register is Fin M with $M\ge1$; $F_M$ is the platform's published Fourier matrix ShorAlgorithms.Shared.fourierMatrix (same sign and normalization as (13)), $F_M^{-1}$ is its conjugate transpose, and $\Lambda_M$ is an explicit matrix on Fin M × ι. The outcome law is the sum over the second register of squared moduli of the final state, and an event's probability is the sum of the outcome probabilities over it. $a$ is computed from $\mathcal A$, $\chi$ and $|0\rangle$, and $\theta_a=\arcsin\sqrt a$. The goal assumes neither $0<a<1$ nor $M>2$, and it keeps the strict inequality for $k\ge2$. The step "after step 2, ignoring global phase" is stated with its phase $-\imath$ written out.

A formalization that takes $a$ or $\theta_a$ as a free parameter, assumes the mixture form of the outcome law, or reasons about $|\Psi_\pm\rangle$ without deriving them from $\mathcal A$ and $\chi$ would make the goal trivial. The statements here do none of these: every quantity is computed from $\mathcal A$, $\chi$, $|0\rangle$ and $M$. The clauses "uses exactly $M$ evaluations of $f$" (Theorem 12) and "requires exactly $\lceil\sqrt N\rceil$ evaluations" (Corollary 14) are not formalized, because the matrix model has no oracle whose calls could be counted. Theorem 13 is stated for any unitary sending $|0\rangle$ to the uniform superposition, which includes $F_N$, as the paper allows on p. 20.

A complete development needs:

• geometric sums of roots of unity;
• the Fejér-kernel identity of Lemma 10;
• the inequality $\sin x\ge 2x/\pi$ on $[0,\pi/2]$;
• a bound on $\sum_{j\ge k}1/j^2$;
• Kronecker-product bookkeeping for two-register states.

The phase-estimation part (Lemma 10, Theorem 11) does not depend on amplification and can be reused by any later formalization of Fourier-based phase estimation. Proofs of individual milestones, and lemmas on Fin M Fourier sums, are welcome.

Selected references

• G. Brassard, P. Høyer, M. Mosca, A. Tapp, Quantum Amplitude Amplification and Estimation, in Quantum Computation and Information, Contemporary Mathematics 305, AMS, 2002, pp. 53–74. arXiv:quant-ph/0005055
• G. Brassard, P. Høyer, An exact quantum polynomial-time algorithm for Simon's problem, ISTCS 1997. arXiv:quant-ph/9704027
• G. Brassard, P. Høyer, A. Tapp, Quantum counting, ICALP 1998. arXiv:quant-ph/9805082
• L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996. arXiv:quant-ph/9605043
• A. Montanaro, Quantum speedup of Monte Carlo methods, Proc. R. Soc. A 471, 2015. arXiv:1504.06987

Motivation

Online platforms run randomized experiments on subjects (users, sessions, orders) that arrive one at a time and must be assigned to a control or a treatment group on arrival, before later subjects are seen. The precision of a treatment-effect estimate depends on how similar the two groups are in their observed covariates. When the groups are badly balanced, the estimator's variance grows, and a large literature on covariate balancing (blocking, rerandomization, matched pairs) addresses this for offline experiments, where all covariates are known in advance.

J. Zhao and Z. Zhou (arXiv:2201.12936, Management Science, 2025) cast the online problem as an online matching problem. The cost of an assignment is the discrepancy, the weight of a minimum-cost perfect matching between the two groups, and they compare three designs against an oblivious adversary that fixes the covariate sequence in advance:

• the clairvoyant matched-pair design;
• the completely randomized design;
• their online pigeonhole design.

For one continuous covariate the pigeonhole design attains $O(T^{1/4}(\log T)^{1/2})$ against $\Theta(T^{1/2})$ for complete randomization. This mission concerns the multi-dimensional result, Theorem 9.

Setting

$T$ subjects arrive in order; $T$ is even. Subject $t$ carries a covariate vector $x_t$ with $q$ discrete coordinates, the $i$-th in a finite set $S_i\subseteq[0,1]$ of size $m_i$, and $p\ge2$ continuous coordinates in $[0,1]$. Distances are Euclidean in $\mathbb R^{q+p}$. An assignment puts each subject in control ($A$) or treatment ($B$).

The discrepancy of a split with $|A|=|B|$ is

$$d_{A,B}=\min_{\sigma:A\to B\text{ bijective}}\ \sum_{t\in A}\lVert x_t-x_{\sigma(t)}\rVert_2 ,$$

the value of the assignment problem (1) of the paper.

The completely randomized design picks $A$ uniformly among the $\binom{T}{T/2}$ subsets of size $T/2$; $\mathrm{ALG}^C(x)$ is the mean of $d_{A,B}$.

A pigeonhole design fixes a partition of the covariate space into pigeonholes. When subject $t$ arrives:

1. if one group already has $T/2$ subjects, $t$ joins the other group;
2. otherwise $t$ joins the group that has fewer subjects in its own pigeonhole, and on a tie a fair coin decides.

Theorem 9 uses the pigeonholes

$$\mathcal P(\mathcal S)=S_1\times\cdots\times S_q\times\Big\{[0,c^{1/p}T^{-\varphi}),\ \dots,\ [1-c^{1/p}T^{-\varphi},1]\Big\}^p ,$$

uniform cells of edge $c^{1/p}T^{-\varphi}$ on each continuous axis, for parameters $\varphi\in(0,1)$ and $c>1$. The expected discrepancy is the mean of $d_{A,B}$ over the design's coins.

Formalization targets

Goal: Theorem 9 (p. 26)

There are $C>0$ and $T_0$, depending only on $p,q,S_1,\dots,S_q,\varphi,c$, such that for every even $T\ge T_0$ and every admissible arrival sequence,

$$\mathbb E[d_{A,B}]\le C\Big(T^{1-\varphi}+T^{(p-1)\varphi}\,\lambda_p(T)\Big),\qquad \lambda_2(T)=(\log T)^{3/2},\quad \lambda_p(T)=1\ (p\ge3).$$

Milestones

1. Lemma EC.1: Hoeffding for a binomial, $\Pr(|H(n)-pn|\le\sqrt{n\log n})\ge1-2/n^2$.
2. Lemma 5, $p=2$: if $T=m^2$ and the subjects occupy each cell of the $m\times m$ grid exactly once, then $\mathrm{ALG}^C(x)=O(T^{1/2}\log T)$.
3. Lemma 5, $p\ge3$: on the full grid of $T=m^p$ cells, $\mathrm{ALG}^C(x)=O(T^{(p-1)/p})$.
4. Balance: every run of a pigeonhole design has $|A|=|B|=T/2$.
5. Component 1: the subjects paired within their pigeonhole before the stopping time $\tau$ contribute at most $\tfrac12c^{1/p}\sqrt p\,T^{1-\varphi}$, on every run.
6. Unmatched subjects: at most one unmatched subject per pigeonhole, $H^0_\tau+H^1_\tau$ at most the number of pigeonholes, and $|H^0_\tau-H^1_\tau|=T-\tau$.
7. Component 2: the remaining subjects contribute $O(T^{(p-1)\varphi}\lambda_p(T))$ in expectation.

Corollary 2 (the case $\varphi=1/p$) is an extra theorem after the goal.

Significance

At $\varphi=1/p$ Theorem 9 gives $O(T^{(p-1)/p})$ for $p\ge3$. This is the order $\Theta(T^{(p-1)/p})$ of the matched-pair design (Theorem 7), which sees all covariates in advance. An online design that commits to each assignment on arrival therefore loses at most a constant factor in dimension $p\ge3$, and at most a $(\log T)^{3/2}$ factor at $p=2$. For the completely randomized design no comparable upper bound is known for general sequences (p. 21). Lemma 5 is the paper's bound for complete randomization on the special family of full grids, and is of independent interest as a random-labelling matching estimate.

The results are proved on paper; none of them has a machine-checked proof, and the platform holds no item on them. A formalization would close the gaps of the printed argument:

• Lemma 5's induction for $p=2$ ends at $\sqrt T(\log T)^{3/2}$ rather than the stated $\sqrt T\log T$.
• Component 2 applies Lemma 5 to unmatched subjects, which occupy distinct cells but do not fill the grid.
• The case $q\ge1$ is argued per discrete support, although the balancing rule acts across supports.

Every statement in the mission is believed true.

Difficulty

The matched part (Component 1) is deterministic: paired subjects share a pigeonhole of diameter $O(T^{-\varphi})$. The difficulty lies in the subjects left over: the unmatched ones and the subjects after $\tau$. Their labels come from coins, but which subjects end up unmatched, and when $\tau$ occurs, depend on the same coins. So the leftover set is not a fixed set with independent fair labels, and the conditional binomial law used on p. ec22 does not hold literally.

A second obstacle is the random-matching estimate itself. Bounding the expected optimal matching between randomly labelled points of a grid at the rates $T^{1/2}\log T$ ($p=2$) and $T^{(p-1)/p}$ ($p\ge3$) is a multi-scale problem of Ajtai–Komlós–Tusnády type. A single-scale count of imbalances per cell gives only $T^{1/2}$ times a power of $T$ that is too large.

Formalization scope

• Subjects are indexed $0,\dots,T-1$; an assignment is a map to Bool (false = control). The covariate space is EuclideanSpace ℝ (Fin q ⊕ Fin p). Admissible sequences have discrete coordinates in $S_i$ and continuous ones in $[0,1]$, with $S_i\subseteq[0,1]$ (the paper's normalisation).
• Discrepancy: an infimum over bijections between the groups. An unbalanced split has the junk value $0$. The designs, the matched set and its complement are balanced on every run, so the junk is never reached.
• Cells: the printed edge $c^{1/p}T^{-\varphi}$ gives a partition only when $c^{-1/p}T^{\varphi}$ is an integer. The formalization uses $m=\lceil c^{-1/p}T^{\varphi}\rceil$ cells per axis of edge $1/m\le c^{1/p}T^{-\varphi}$, with the last cell closed. A pigeonhole is keyed by the exact discrete values and the cell index on each axis. The partition is the printed one, not a quantified family.
• Randomness: the pigeonhole design uses one coin per subject, consulted only on a tie. Its expected discrepancy is the average over all $2^T$ coin vectors, which is exactly the paper's law. The completely randomized design averages over all $\binom{T}{T/2}$ control sets.
• Asymptotics: $O(f(T))$ means $\exists C>0,\exists T_0,\forall T\ge T_0$ even, $\forall x$ admissible. $C$ and $T_0$ are chosen before $T$ and $x$ and depend only on the fixed parameters. $\log$ is the natural logarithm.
• Lemma 5's family $\mathcal X$: $T=m^p$ subjects in $[0,1]^p$, one per cell, stated as injectivity of the cell map.
• Stopping objects: $\tau$ is the first $n$ at which a group holds $T/2$ subjects. Within a pigeonhole the subjects before $\tau$ are paired in arrival order, and the last one is unmatched when their number is odd.
• Corrections to the page: the second cell printed as $[T^{-\varphi},2c^{1/p}T^{-\varphi})$ on p. ec21 is read as $[c^{1/p}T^{-\varphi},2c^{1/p}T^{-\varphi})$. The family's $x'_t\notin\mathbb X$ is read as $x_{t'}\notin\mathbb X$. The bound $H\le\frac1cT^{p\varphi}$ becomes $H\le(\prod_i m_i)\,m^p$ under the ceiling and the discrete supports.

The following formalizations would trivialize the mission and are ruled out:

• a bound on the discrepancy of one run, or of the best run, instead of the average over all coin vectors;
• constants that depend on $T$ or $x$;
• an unbalanced design that exploits the junk value $0$;
• an arbitrary partition in place of the printed grid.

A complete development needs a binomial Hoeffding bound and an exact analysis of the design's recursion (balance, alternation within a pigeonhole before $\tau$). It also needs a multi-scale bound on random bichromatic matchings of grid points. That bound is reusable for Lemma 5 and for matching estimators generally. Contributions on any milestone are welcome, as are proofs of Lemma 5 for arbitrary subsets of grid points, which is what Component 2 needs.

Selected references

• J. Zhao and Z. Zhou, Pigeonhole Design: Balancing Sequential Experiments from an Online Matching Perspective, Management Science, 2025; arXiv:2201.12936v6, 2024. https://arxiv.org/abs/2201.12936
• M. Ajtai, J. Komlós and G. Tusnády, On optimal matchings, Combinatorica 4 (1984) 259–264. https://doi.org/10.1007/BF02579135
• N. Fournier and A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015) 707–738. https://doi.org/10.1007/s00440-014-0583-7
• W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

Motivation

In offline stochastic matching a graph is given in which every edge is present only with some known probability, and the only way to find out is to probe it: a probed edge that turns out to be present must be added to the matching at once. Each vertex may also limit how many of its edges are probed (its patience). The model captures applications in which a proposed match may be refused and an accepted one is binding: organ (kidney) exchange, online dating, advertising, crowdsourcing and ride sharing are the examples the paper lists (pp. 1–2), following Chen, Immorlica, Karlin, Mahdian and Rudra (ICALP 2009) and Bansal, Gupta, Li, Mestre, Nagarajan and Rudra (Algorithmica 2012).

Finding the best probing strategy is computationally hard, so algorithms are compared with a linear-programming relaxation that upper-bounds every strategy (Lemma 1, from Bansal et al.).

Timeline (general graphs with patience, as recorded on p. 2 of the paper).

• 2012: Bansal et al., a $0.25$-approximation.
• 2015: Adamczyk, Grandoni and Mukherjee, $0.269$.
• 2018: Baveja, Chavan, Nikiforov, Srinivasan and Xu, $0.31$.
• 2021–2026: Brubach, Grammel, Ma, MacRury and Srinivasan (arXiv:2106.06892v3; Mathematics of Operations Research, 2025), $0.382$ when every patience is at least $2$. Their algorithm processes the edges in random order and attenuates each probe with an extra coin flip. Version 3 restricts the result to patience at least $2$; earlier versions claimed it for all patience values, and Remark 1 shows why patience $1$ fails.
• Since then Pollner et al. have obtained $0.395$ for general graphs (reference [35] of the paper).

This mission formalizes the per-edge bound behind the $0.382$ result, Theorem 1 of the paper.

Setting

A finite graph $G = (V, E)$ is given. Each edge $e$ is active independently with probability $p_e \in [0,1]$, and each vertex $v$ has a patience $t_v \in \{1, 2, \dots\} \cup \{\infty\}$, the largest number of probes that may be made to edges incident to $v$. Write $\delta(v)$ for the edges incident to $v$.

LP (3). A vector $(y_e)_{e \in E}$ is feasible if

$$0 \le y_e \le 1, \qquad \sum_{e \in \delta(v)} y_e p_e \le 1, \qquad \sum_{e \in \delta(v)} y_e \le t_v \quad (e \in E,\ v \in V).$$

Here $y_e$ is the probability of probing $e$.

Attenuation. An attenuation function $\tilde a : [0,1] \to [0,1]$ assigns to edge $e$ the probability $a(e) = \tilde a(p_e y_e)$. It is effective (Definition 3) if $\tilde a(0) = 1$ and $z \mapsto \ln(1 - x z \tilde a(z))$ is convex on $[0,1]$ for every $x \in (0,1)$. The two functions used here are $\tilde a_{\exp}(z) = e^{-z/2}$ and $\tilde a_{\mathrm{lin}}(z) = 1 - z/2$ (Definition 4 with $\alpha = 1/2$).

Algorithm 1. Draw independent coins $Y_e \sim \mathrm{Bernoulli}(y_e)$ and $A_e \sim \mathrm{Bernoulli}(a(e))$ for every edge, and process the edges in a uniformly random order. When $e$ is processed it is free if both endpoints are unmatched and have made fewer than their patience in probes. If $e$ is free and $Y_e = A_e = 1$, probe $e$; if it is active (coin $P_e \sim \mathrm{Bernoulli}(p_e)$), match it and both endpoints. Finally

$$\beta^* = \int_0^1 \bigl(e^{-2x} + x e^{-2x}\bigr)^2\,dx \approx 0.38278.$$

Formalization targets

Goal: Theorem 1 (p. 9)

If every vertex has patience at least $2$, $y$ is feasible for LP (3), and $\tilde a$ is $\tilde a_{\exp}$ or $\tilde a_{\mathrm{lin}}$, then for every edge $e$

$$a(e) \cdot \Pr[e \text{ is free}] \;\ge\; \beta^*.$$

The probability is over the random order and the coins of Algorithm 1.

Milestones

The milestones are numbered results and displays of the paper, in the order its argument uses them:

1. $\tilde a_{\exp}$ and $\tilde a_{\mathrm{lin}}$ with $\alpha = 1/2$ are effective (Definition 4, p. 9).
2. (7), p. 10: a safe edge (one whose neighbourhood has neither a successful probe nor an exhausted patience before it arrives) is free, so $a(e)\Pr[e \text{ is free}] \ge \tilde a(p_e y_e)\Pr[e \text{ is safe}]$.
3. Lemma 3, p. 11: $\prod_{f \in E_1(r)} (1 - x\,a(f) y_f) \ge e^{-x \sum_{f \in E_1(r)} y_f}$ for an effective attenuation, where $E_1(r)$ is the set of edges at $r$ other than $e$ with $p_f = 1$.
4. Lemma 4, p. 12 (Baveja et al.): $\Pr[\sum_i B_i < t] \ge \Pr[\mathrm{Pois}(\mu) < t]$ for independent Bernoullis with mean sum $\mu < t - 1$.
5. Lemma 5, p. 12: the Chernoff bound $\Pr[\sum_i B_i < (1+\varepsilon)\mu] \ge 1 - e^{-\varepsilon^2 \mu/(2+\varepsilon)}$.
6. Proposition 1, p. 14: $\int_0^1 \lambda\varphi \ge \lambda(z^*)\int_0^1 \varphi$ for $\lambda \ge 0$ non-increasing and $\varphi$ changing sign once, from $+$ to $-$, at $z^*$.
7. (22), p. 15: $\tilde a(y_e)\int_0^1 (e^{-x(2-y_e)} + x e^{-x(2-y_e)})^2\,dx \ge \beta^*$ on $[0,1]$, with equality at $y_e = 0$.

Significance

The result. Equation (4) of the paper writes the expected weight of the algorithm's matching as $\sum_e w_e p_e y_e\, a(e)\Pr[e \text{ is free}]$. Theorem 1 therefore gives at least $\beta^* \sum_e w_e p_e y_e$, and with an optimal LP solution and the LP upper bound of Bansal et al. this is a $0.382$-approximation for stochastic matching on general graphs with patience at least $2$. The bound is per edge, which is the form a random-order contention resolution scheme needs: the same algorithm rounds fractional matchings edge by edge.

Formalizing it. The paper's proof combines a reduction (Lemma 2), the analytic bound of Lemma 3, the tail bounds of Lemmas 4–5, an exchange argument (Lemma 6) resting on a graph construction from another paper, and a case analysis in the patience values that is closed by numerical minimization of explicit integrals over two or three parameters ("we numerically minimize (12)", p. 13; "we numerically verify", p. 15). The margins are thin: the bound $0.3828$ in the last case exceeds $\beta^*$ by about $5 \cdot 10^{-5}$. No part of this argument has a machine-checked proof. A formal proof would certify both the probabilistic reasoning and every numerical step, and would supply a reusable finite model of random-order probing algorithms with patience, of which the platform has none.

Difficulty

The obvious argument bounds $\Pr[e \text{ is free}]$ by a product over the two endpoints of $e$ and applies a Poisson approximation to the number of probes at each endpoint. For an endpoint of patience $2$ that approximation is only valid for arrival times $x < x_c$, a threshold that can be $1/2$, and the bound it gives, about $0.347$ (display (16)), falls below $\beta^*$. Closing that case is what requires the exchange argument of Lemma 6. Beyond it, the remaining cases are optimization problems over the LP mass at each endpoint, which the paper settles by computer and a formal proof must settle by rigorous bounds.

Formalization scope

• The graph is the platform's EdmondsMatching65.Polyhedron.Graph (loopless); the goal adds that the endpoint map is injective, since the paper's edges are pairs $\{u,v\}$. Patience is ℕ∞, with $\infty$ allowed; "minimum patience $2$" is $t_v \ge 2$ at every vertex.
• Standing assumptions: $p_e \in [0,1]$ for every edge; $y$ feasible for LP (3) (which includes $y_e \in [0,1]$).
• Every probability is a finite average: over the $|E|!$ orders of the edges and over the $2^{3|E|}$ outcomes of the coins $Y, A, P$, each weighted by a product of Bernoulli weights. The paper's continuous arrival times induce exactly this uniform order. $\Pr[e \text{ is free}]$ is computed from the run of Algorithm 1 (matched vertices and probe counters, step by step), never from the product formulas of p. 11, which would assume the lemmas being proved.
• The goal is stated for $\tilde a_{\exp}$ and $\tilde a_{\mathrm{lin}}$ with $\alpha = 1/2$. Theorem 1 cites "Definition 3 where $\alpha = 1/2$"; $\alpha$ belongs to Definition 4, and an arbitrary effective function would make the statement false. The third function of Definition 4 is not effective (its $\ln(1 - xz\tilde a(z))$ is concave near $z = 0$ for $x$ close to $1$), so neither the effectiveness milestone nor the goal covers it.
• Lemma 4 prints $e^{-x\mu}$ in the Poisson sum; the statement uses $e^{-\mu}$.
• A formalization that defines "free" without the patience counters or the matched set, one that bounds $\Pr[e \text{ is safe}]$ or the integral (8) instead of $a(e)\Pr[e \text{ is free}]$, or one stated for "some" attenuation function, is a different theorem and does not count.
• Not stated: Lemma 2 (a without-loss-of-generality reduction), Lemma 6 (its hypothesis is a graph built in another paper, with property (18) asserted there), the conditional bounds (8)–(17) and (23)–(25), whose objects live inside the proof, and the numerical values of pp. 13–15. Solvers who need them are welcome to state them as their own lemmas. The paper's proofs are in §3.2, pp. 9–15.
• Reusable beyond this mission: the finite model of Algorithm 1 and its events, Lemma 4 (Bernoulli versus Poisson lower tails), Lemma 5 (a Chernoff bound for independent Bernoullis), and Proposition 1.

Selected references

• B. Brubach, N. Grammel, W. Ma, C. MacRury, A. Srinivasan, Improved Guarantees for Offline Stochastic Matching via New Ordered Contention Resolution Schemes, Mathematics of Operations Research, 2025; arXiv:2106.06892v3 (20 Apr 2026). https://arxiv.org/abs/2106.06892v3
• N. Bansal, A. Gupta, J. Li, J. Mestre, V. Nagarajan, A. Rudra, When LP is the cure for your matching woes: improved bounds for stochastic matchings, Algorithmica 63(4):733–762, 2012 (reference [7] of the paper).
• A. Baveja, A. Chavan, A. Nikiforov, A. Srinivasan, P. Xu, Improved bounds in stochastic matching and optimization, Algorithmica 80(11):3225–3252, 2018 (reference [8]; source of Lemma 4).
• M. Adamczyk, F. Grandoni, J. Mukherjee, Improved approximation algorithms for stochastic matching, ESA 2015, 1–12 (reference [1]).
• N. Chen, N. Immorlica, A. R. Karlin, M. Mahdian, A. Rudra, Approximating matches made in heaven, ICALP 2009, 266–278 (reference [15]).

Opinions on large directed social networks

Linear models of opinion formation go back to DeGroot (DeGroot 1974), in which every individual repeatedly replaces their opinion by a weighted average of the opinions of the people they listen to, and to Friedkin and Johnsen (Friedkin–Johnsen 1990), who added a persistent internal opinion. Fraiman, Lin and Olvera-Cravioto (arXiv:2209.00969v2, Mathematics of Operations Research, 2025) add a random external (media) signal whose law may depend on the individual's attributes, which models selective exposure, and ask what the opinions look like on a large random social network. The answer is the behaviour of a typical individual, a uniformly chosen vertex: its stationary opinion converges in law to the opinion of the root of the network's local weak limit, and the empirical distribution of all stationary opinions converges to the same law. Questions such as consensus or polarization are then questions about one limiting random variable, independent of the particular realization of the network.

This mission formalizes that main result (Theorem 2) together with the fixed-graph stationarity theorem it rests on (Theorem 1).

Setting

A vertex-weighted directed graph on a vertex set $V$ gives each vertex $i$ an in-degree $d_i^-$, an ordered list of inbound neighbours $\ell(i,1),\dots,\ell(i,d_i^-)$ and weights $c(i,r)\in[0,1]$ with $\sum_r c(i,r)=c$ whenever $d_i^->0$. The parameters satisfy $c\in[0,1)$, $d\in(0,1]$, $c+d\le1$. The opinions $R_i^{(k)}\in[-1,1]$ evolve by recursion (1),

$$R_i^{(k+1)}=\sum_{r=1}^{d_i^-}c(i,r)\,R^{(k)}_{\ell(i,r)}+W_i^{(k)}+(1-c-d)R_i^{(k)},\qquad k\ge0,$$

where the external signals $W_i^{(k)}$ are independent, i.i.d. in time given the vertex mark, and bounded by $|W_i^{(k)}|\le d+c-\sum_rc(i,r)$. With the operator $\Delta f(i)=\sum_rc(i,r)f(\ell(i,r))+(1-c-d)f(i)$ this reads $R^{(k+1)}=\Delta R^{(k)}+W^{(k)}$. The stationary vector is $R=\sum_{r\ge0}\Delta^rW^{(r)}$.

The full mark of a vertex is $\mathbf X_i=(\mathbf A_i,Q_i,S_i,D_i^-,C(i,1),C(i,2),\dots)$: a generic attribute, an internal opinion, a stubbornness label, the in-degree and the weights. Marks are compared by the metric

$$\rho(\mathbf x,\tilde{\mathbf x})=\rho'(\mathbf a,\tilde{\mathbf a})+|q-\tilde q|+|s-\tilde s|+|d^--\tilde d^-|+\sum_j|c_j\mathbb 1(d^-\ge j)-\tilde c_j\mathbb 1(\tilde d^-\ge j)|.$$

A random graph sequence $G(V_n,E_n;\mathscr A_n)$ has vertex set $V_n=\{1,\dots,n\}$ and attributes $\mathscr A_n=\{\mathbf Y_i=(\mathbf A_i,Q_i,S_i)\}$; edges and weights are random given the attributes. The conditional expectation $E_n[\cdot]=E[\cdot\mid\mathscr A_n]$ conditions on the attributes only. The in-component of depth $k$ of a vertex $v$ is the set of vertices with a directed path of length at most $k$ to $v$. The sequence admits a strong coupling (Definition 4) with a rooted marked graph $\mathcal G(\boldsymbol{\mathcal X})$ if, for two independent uniform vertices $I_n,J_n$, every depth $k\ge1$ and every $\epsilon>0$, there are two independent copies of $\mathcal G(\boldsymbol{\mathcal X})$ whose depth-$k$ root in-components are, with conditional probability tending to one in probability, isomorphic to those of $I_n$ and $J_n$, with all marks $\epsilon$-close in $\rho$ and the two in-components of $I_n$ and $J_n$ disjoint. The Wasserstein distance is $d_1(\mu,\nu)=\inf\{E|X-Y|:X\sim\mu,Y\sim\nu\}$.

Formalization targets

Goal: Theorem 2

Assume a strong coupling, $d>0$, and a signal kernel $\nu(\mathbf x)$ with $d_1(\nu(\mathbf x),\nu(\tilde{\mathbf x}))\le K\rho(\mathbf x,\tilde{\mathbf x})$. Then there are laws $L_k$ of $(\mathcal R^{(0)},\dots,\mathcal R^{(k)})$ and $L^*$ of $\mathcal R^*$, not depending on $n$, with

$$\max_{0\le r\le k}E\bigl[|R^{(r)}_{I_n}-\mathcal R^{(r)}|\bigm|\mathscr A_n\bigr]\xrightarrow{P}0,\qquad \frac1n\sum_{i=1}^nf(R_i^{(k)})\xrightarrow{P}E f(\mathcal R^{(k)}),$$ $$E\bigl[|R_{I_n}-\mathcal R^*|\bigm|\mathscr A_n\bigr]\xrightarrow{P}0,\qquad \frac1n\sum_{i=1}^nf(R_i)\xrightarrow{P}E f(\mathcal R^*),$$

for every continuous $f$ on $[-1,1]$, and $\mathcal R^{(k)}\Rightarrow\mathcal R^*$ geometrically fast:

$$d_1\bigl(\mathrm{law}\,\mathcal R^{(k)},\mathrm{law}\,\mathcal R^*\bigr)\le(1-d)^k\Bigl(\frac2d+2\Bigr).$$

Milestones

1. $\|\Delta\|_\infty\le1-d$ (proof of Theorem 1, p. 22).
2. Theorem 1 (p. 5): on a fixed locally finite graph, $R^{(k)}\Rightarrow R$ at a geometric rate, with a limit that does not depend on $R^{(0)}$.
3. Theorem 2(1) (p. 8): the fixed-time statement.

A supporting statement of the proposal, not a milestone, is the tail bound $\|R-B^{(k)}\|_\infty\le2\sum_{r>k}(1-d)^r$ for $B^{(k)}=\sum_{r\le k}\Delta^rW^{(r)}$ (proof of Theorem 2, p. 28).

Significance

Theorem 2 reduces the stationary opinion distribution of a large network to a single random variable $\mathcal R^*$ attached to the local limit. When the limit is a marked Galton–Watson tree, $\mathcal R^*$ has an explicit series representation whose mean and variance are computed in closed form later in the paper (the other two missions of this series), and these formulas are what explain consensus and polarization. Strong couplings exist ([Olvera-Cravioto 2022], cited on p. 8 of the paper) for Erdős–Rényi graphs, the Chung–Lu and Norros–Reittu models, the configuration model, stochastic block models and preferential attachment graphs, so the theorem applies to most random graph models used for social networks.

The result is proved in the paper; nothing in it has been formalized. On Prove2Me this is the first statement of a strong coupling, a form of local weak convergence for directed marked graphs, and of a stochastic recursion on a random graph. The definitions of in-components, the coupling event and the strong coupling are reusable for any local-limit statement about directed random graphs, and the contraction and time-reversal milestones are reusable for linear stochastic recursions.

Difficulty

The fixed-graph part is a contraction argument, but the coupled object is not the opinion process itself: $R^{(k)}$ does not converge almost surely, and only its time reversal $B^{(k)}$ does. The main difficulty is Theorem 2. A local limit controls one neighbourhood at a time, while the empirical averages need two uniformly chosen vertices to be asymptotically independent, which a one-vertex limit statement does not give. The errors in weights, signals and initial opinions enter at every vertex of a depth-$k$ neighbourhood, and the statements condition only on the attributes, with edges and weights integrated out. The stationary statement then requires an interchange of $n\to\infty$ and $k\to\infty$ that is uniform in $n$.

Formalization scope

All random objects of the $m$-th model live on one probability space, and the $m$-th graph has $m+1$ vertices (the paper's $G_{m+1}$), so a uniform vertex always exists. Signals are written $W_i^{(k)}=\zeta(\mathbf X_i,U_i^{(k)})$ and initial opinions $R_i^{(0)}=\varphi(\mathbf X_i,V_i)$ with i.i.d. uniforms independent of the graph: this quantile representation is equivalent in law to the paper's conditionally i.i.d. signals. Neighbour indices are 0-based. The conditional quantities given $\mathscr A_n$ are regular conditional distributions given the attribute vector, and "random variables whose distribution does not depend on $\mathscr A_n$" are encoded by fixed limit laws, with the paper's $E[|\cdot|\mid\mathscr A_n]\to0$ read as $d_1$ convergence in probability of the conditional laws, which is equivalent. Theorem 1 is stated on countably many vertices, with its geometric rate given as an explicit bound for 1-Lipschitz test functions of finitely many coordinates.

Disclosed choices: the strong coupling is stated on the given space with measurable events inside the coupling events (the event "an isomorphism exists" need not be measurable), with isomorphisms that preserve the order of inbound neighbours (which the proof uses), and through its second bullet, which implies the first. The paper's conditional independence of weight vectors given $\mathscr A_n$ is not imposed. The strong coupling also requires the depth-$k$ in-components of $I_n$ and $J_n$ to be disjoint on the coupling event: the proof of Theorem 7 uses this, and without it Definition 4 admits a graph whose vertices all listen to a single hub, whose shared signals keep $\frac1n\sum_if(R_i^{(k)})$ random. The page puts no condition on $R^{(0)}$ beyond conditional independence of the signals, but Theorem 2(1) at time $0$ is false then (take $R^{(0)}\equiv(-1)^n$); the statement assumes a $d_1$-Lipschitz initial kernel with the same $K$, which covers the paper's own simulations. The geometric rate uses the constant of the proof.

Trivializing readings are excluded: every tsum is absolutely summable under the hypotheses, conditional laws are regular conditional distributions of measurable random variables, the averages have no division by zero, and the limit laws are forced onto $[-1,1]$ by the convergence, so no integral defaults to $0$. Theorem 7 of the paper (the two-vertex coupling) is not a milestone. Contributions of proofs of any milestone, and of general lemmas on regular conditional distributions and Wasserstein couplings, are welcome.

Selected references

• N. Fraiman, T.-C. Lin and M. Olvera-Cravioto, Opinion dynamics on directed complex networks, Mathematics of Operations Research, 2025; preprint arXiv:2209.00969v2, 2024. https://arxiv.org/abs/2209.00969v2
• M. H. DeGroot, Reaching a consensus, Journal of the American Statistical Association 69 (1974), 118–121. https://doi.org/10.1080/01621459.1974.10480137
• N. E. Friedkin and E. C. Johnsen, Social influence and opinions, Journal of Mathematical Sociology 15 (1990), 193–206. https://doi.org/10.1080/0022250X.1990.9990069
• M. Olvera-Cravioto, Strong couplings for static locally tree-like random graphs, Journal of Applied Probability 59(4) (2022), 1261–1285 (reference [33] of the paper, where the random graph models admitting strong couplings are listed).