Rumor Spreading on the Complete Graph
1 The model
Fix \(n \ge 2\) and let \(V = \{ 0,1,\dots ,n-1\} \) be the vertex set of the complete graph \(K_n\).
A round configuration is a function \(\omega \colon V \to V\) with \(\omega (v) \ne v\) for all \(v\). Let \(R_n\) denote the (finite) set of round configurations; it carries the uniform probability measure, i.e. every node picks a uniformly random target among the other \(n-1\) nodes, independently of all other nodes.
For an informed set \(I \subseteq V\) and a round configuration \(\omega \in R_n\), the next informed set is
(Only informed nodes actually transmit; letting all nodes draw a target and ignoring the choices of uninformed nodes is an equivalent and formalization-friendlier convention.)
Fix a horizon \(T \in \mathbb {N}\) and a start vertex \(v_0 \in V\). The sample space is \(\Omega = R_n^{\, T}\) (uniform measure, i.e. i.i.d. uniform rounds). For \(\omega = (\omega _0,\dots ,\omega _{T-1}) \in \Omega \) define \(I_0(\omega ) = \{ v_0\} \) and \(I_{t+1}(\omega ) = \mathrm{step}(I_t(\omega ), \omega _t)\) for \(0 \le t {\lt} T\). We write \(m_t = |I_t|\) and \(U_t = n - m_t\) for the numbers of informed and uninformed nodes. Since \(\Omega \) is finite, all probabilities are finite ratios and all expectations are finite sums; “conditioning on \(I_t\)” means partitioning \(\Omega \) according to the first \(t\) coordinates. In the formalization, a trajectory is simply a List of round configurations and \(\mathrm{run}\ I\ l\) folds step over the list \(l\).
Two trivial but load-bearing facts, both immediate from Definition 2:
\(I_t(\omega ) \subseteq I_{t+1}(\omega )\) for all \(t\) and all \(\omega \); hence \(m_t\) is non-decreasing and \(U_t\) is non-increasing in \(t\), pointwise on \(\Omega \).
\(|I_{t+1}(\omega ) \smallsetminus I_t(\omega )| \le |I_t(\omega )|\); equivalently \((\mathrm{step}(I,\omega )).\mathrm{card} \le 2\, I.\mathrm{card}\).
2 Main theorem
Throughout, \(\log \) denotes the natural logarithm.
Let \(n \ge 2\), let \(v_0 \in V\), and set
Then \(\Pr \bigl[\, I_T = V \, \bigr] \; \ge \; 1 - \frac{2}{n}\). In particular all nodes are informed after \(O(\log n)\) rounds with high probability.
The constants are deliberately crude: the proof is organized to minimize the analytic toolkit, not the round count. The sharp answer is \(\log _2 n + \log n + o(\log n)\) (Frieze–Grimmett [ 1 ] , Pittel [ 2 ] ). Replacing \(2/n\) by \(n^{-\alpha }\) for any fixed \(\alpha \ge 1\) only changes the constants in \(T_1, T_2\).
The proof has two phases, glued by Lemma 4:
Growth phase (Section 7): while \(m_t \le n/2\), each round multiplies \(m_t\) by \(\ge 9/8\) with probability \(\ge 1/8\); an exponential-moment bound for adaptive trials shows that after \(T_1\) rounds, \(m_{T_1} {\gt} n/2\) except with probability \(\le 1/n\).
Saturation phase (Section 8): once \(m_t \ge n/2\), the expected number of uninformed nodes contracts by a factor \(2/3\) per round; after \(T_2\) further rounds Markov’s inequality gives \(U_T = 0\) except with probability \(\le 1/n\).
3 Finite uniform probability
All randomness in this development is uniform over finite types, so instead of measure theory or PMF we work with plain finite sums. The definitions and their basic laws are those of the shared dynamics library (Dynamics.Uniform), which also identifies them with Mathlib’s finite expectation Finset.expect and with the independent product of uniform distributions (Dynamics.Bridge).
For a finite type \(\alpha \) and \(f \colon \alpha \to \mathbb {R}\), \(\mathrm{avg}(f) := \bigl(\sum _{a} f(a)\bigr) / |\alpha |\) is the expectation of \(f\) under the uniform distribution on \(\alpha \).
For a finite type \(\alpha \), \(\mathrm{expList}\ \alpha \ T\ F\) is the expectation of a functional \(F\) of a trajectory of \(T\) i.i.d. uniform draws from \(\alpha \), defined by recursion on \(T\): the head draw is averaged out first, i.e. \(\mathrm{expList}\ \alpha \ 0\ F = F(\, []\, )\) and \(\mathrm{expList}\ \alpha \ (T{+}1)\ F = \mathrm{avg}\bigl(a \mapsto \mathrm{expList}\ \alpha \ T\ (l \mapsto F(a :: l))\bigr)\). This makes “conditioning on the first round” a definitional unfolding rather than a measure-theoretic construction.
\(\mathrm{avg}\) and \(\mathrm{expList}\) are monotone, additive, and homogeneous, and constants pass through unchanged. These pointwise inequalities pushed through \(\mathrm{avg\_ le\_ avg}\) / \(\mathrm{expList\_ le\_ expList}\) are the only form in which Markov’s inequality and union bounds are used below (Lemmas 16 and 17); they are not separately formalized lemmas.
\(\mathrm{expList}\ \alpha \ T\ F\) equals the uniform average of \(F\) over all length-\(T\) sequences of draws, i.e. over the product probability space \(\mathrm{Fin}\ T \to \alpha \) of \(T\) i.i.d. uniform rounds. This confirms that the recursive definition of Definition 9 is the textbook object.
4 Elementary inequalities
We write \(x := \tfrac {1}{n-1}\), so \(0 {\lt} x \le 1\) for \(n \ge 2\).
For all real \(y \ge -1\) (we only use \(y\in [-1,1]\)) and \(m \in \mathbb {N}\): \((1+y)^m \ge 1 + my\). Equivalently, with \(y = -x\): \(1 - mx \le (1-x)^m\).
For \(0 \le x \le 1\) and \(m \in \mathbb {N}\):
and consequently \(mx/2 \le 1-(1-x)^m\) whenever \(mx \le 1\).
For \(0 \le x \le 1\) and \(m \in \mathbb {N}\): \((1-x)^m \le \dfrac {1}{1+mx}\).
For \(x {\gt} 0\): \(1 - \tfrac 1x \le \log x\). (The formalization only needs this left inequality, applied at \(x = 9/8,\ 16/15,\ 3/2\), together with Mathlib’s numeric bound \(\log 2 {\lt} 0.6931471808\).)
Let \(\Omega \) be a finite nonempty set with the uniform measure, \(f \colon \Omega \to \mathbb {R}\) with \(f \ge 0\), and \(a {\gt} 0\). Then \(\Pr [f \ge a] \le \mathbb {E}[f]/a\). In particular, if \(f\) takes values in \(\mathbb {N}\), then \(\Pr [f \ne 0] \le \mathbb {E}[f]\).
Let \(f \colon \Omega \to \mathbb {R}\) with \(0 \le f \le b\) pointwise, \(b {\gt} 0\), and let \(0 {\lt} a {\lt} b\). Then \(\Pr [f \ge a] \ge \dfrac {\mathbb {E}[f] - a}{b}\). (As with Lemma 16, the formalization does not isolate this as a named lemma: each use site supplies its own pointwise bound and pushes it through \(\mathrm{avg\_ le\_ avg}\), e.g. in the proof of Lemma 20.)
5 One-round estimates
Fix an informed set \(I\) with \(|I| = m \ge 1\) and let \(\omega \in R_n\) be a uniform round configuration. All statements in this section concern this single round; by independence of the rounds they apply verbatim to the conditional law of round \(t\) given \(I_t = I\).
For any fixed \(u \notin I\),
The Lean proof is the only place where a probability is computed rather than estimated: it counts round configurations avoiding \(u\) on \(I\) via an explicit equivalence to a product of subtypes and Fintype.card_pi.
Let \(N(\omega ) = |\mathrm{step}(I,\omega )| - m\) be the number of newly informed nodes. The formalization gives the exact formula
from which, if \(1 \le m \le n/2\): \(\mathbb {E}_\omega [N] \ge m/4\) (using Lemma 13 and \(n - m \ge n/2\), \(mx \le 1\)).
If \(1 \le m \le n/2\), then \(\Pr _\omega \bigl[\, |\mathrm{step}(I,\omega )| \ge \tfrac {9}{8}\, m\, \bigr] \ge \tfrac 18\).
If \(m \ge n/2\), then for every fixed \(u \notin I\), \(\Pr _\omega [u \notin \mathrm{step}(I,\omega )] = (1-x)^m \le \tfrac 23\), and consequently, with \(U' := n - |\mathrm{step}(I,\omega )|\), \(\mathbb {E}_\omega [U'] \le \tfrac 23(n-m)\).
6 Adaptive Bernoulli trials
A round is good if it multiplies the informed set by \(\ge 9/8\), or if the informed set already exceeds \(n/2\):
\(\mathrm{goodCount}\) counts the good rounds along a trajectory. By Lemma 20 (applied when \(m_t \le n/2\); trivial otherwise), \(\Pr [X_t = 1 \mid \omega _0,\dots ,\omega _{t-1}] \ge \tfrac 18\) for every prefix, since \(\omega _t\) is independent of the prefix and \(\mathrm{expList}\) conditions on it definitionally.
For every \(T\) and every nonempty \(I\),
over \(T\) rounds started at \(I\). (This specializes the textbook “\(\mathbb {E}[s^G] \le (1-p(1-s))^T\) for adaptive \(\{ 0,1\} \)-trials with per-step success probability \(\ge p\)” at \(p = 1/8\), \(s = 1/2\); the formalization proves the specialized statement directly by induction on \(T\) rather than the general one, since only this instance is needed. The ensuing tail bound \(\Pr [G {\lt} L] \le 2^{L}(15/16)^{T}\) — via \(s^{L}\Pr [G{\lt}L] \le \mathbb {E}[s^G]\) — is likewise not isolated as a separate lemma; it is proved inline inside Lemma 25 (phase1).
7 Growth phase
Let \(L \in \mathbb {N}\) satisfy \((9/8)^L {\gt} n/2\). If the informed set never exceeds \(n/2\) up to time \(T_1\), then along that trajectory \(m_{T_1} \ge (9/8)^{\mathrm{goodCount}} \cdot m_0\): every good round multiplies \(m_t\) by \(\ge 9/8\) and every round is non-decreasing (Lemma 4), so \(\mathrm{goodCount} \ge L\) would force \(m_{T_1} {\gt} n/2\), a contradiction — hence \(\mathrm{goodCount} {\lt} L \Rightarrow m_{T_1} \le n/2\) is impossible to rule out only via the deterministic growth bound stated here.
If \((9/8)^L \ge n\), then after \(T_1\) rounds the informed set is still \(\le n/2\) with probability at most \(2^{L}\, (15/16)^{T_1}\).
With \(L = \left\lceil 9 \log n \right\rceil + 1\) we have \((9/8)^L \ge n\) (numeric_A), and with \(T_1 = \left\lceil 117 \log n \right\rceil + 23\) we have \(2^{L}(15/16)^{T_1} \le 1/n\) (numeric_B), using \(\log \tfrac 98 \ge \tfrac 19\), \(\log \tfrac {16}{15} \ge \tfrac 1{16}\) and \(\log 2 {\lt} 0.6932\). Combined with Lemma 25: \(\Pr [m_{T_1} \le n/2] \le 1/n\). The clean statement to formalize is that any \(L, T_1\) satisfying these two numeric inequalities work; the values above merely exhibit admissible ones.
8 Saturation phase
Let \(A = \{ m_{T_1} {\gt} n/2\} \) (an event determined by the first \(T_1\) coordinates). Then for every \(s \ge 0\), \(\mathbb {E}\bigl[\, U_{T_1 + s}\, \mathbf{1}_A \, \bigr] \le (2/3)^{s}\, n\), by induction on \(s\) using Lemma 21 at each step (monotonicity keeps \(m_{T_1+s} {\gt} n/2\) on \(A\)).
With \(T_2 = \left\lceil 6 \log n \right\rceil \): \(\Pr [\, U_T \ge 1 \text{ and } A \, ] \le n\, (2/3)^{T_2} \le 1/n\). (\(U_T\) is \(\mathbb {N}\)-valued, so Markov applied to \(U_T \mathbf{1}_A\) and Lemma 27 give the first inequality; \((2/3)^{T_2} n \le 1/n\) — numeric_C — follows from \(\log \tfrac 32 \ge \tfrac 13\) and \(T_2 \ge 6\log n\).)
9 Proof of the main theorem
Let \(\mathrm{prNotAllInformed}(n,v_0,T)\) be the probability that some node is still uninformed after \(T\) rounds started at \(v_0\). For all \(L, T_1, T_2\) with \((9/8)^L \le n\):
Failure requires either phase 1 to fail (informed set still \(\le n/2\) after \(T_1\) rounds, Lemma 25) or phase 2 to leave an uninformed node on the complementary event, controlled by Lemma 27 via Markov.
With \(T_1 = \left\lceil 117\log n \right\rceil + 23\), \(T_2 = \left\lceil 6\log n \right\rceil \), \(T = T_1+T_2\), Theorem 6 follows from Lemma 29, Lemma 26 and Corollary 28:
10 PULL and PUSH–PULL
We now treat the two other protocols of Karp, Schindelhauer, Shenker and Vöcking [ 3 ] , driven by the same random calls: in a round configuration \(\omega \in R_n\) every node \(v\) calls \(\omega (v)\). In PULL the caller learns the rumor from its callee; in PUSH–PULL the rumor travels in both directions along every call. As for PUSH, partners are chosen among the other \(n-1\) nodes (KSSV allow self-calls; only constants change), and the round count is a crude \(O(\log n)\) instead of the sharp \(\log _3 n + O(\log \log n)\) of [ 3 , Thm. 2.1 ] .
\(\mathrm{pullStep}(I,\omega ) = I \cup \{ v : \omega (v) \in I\} \) and \(\mathrm{pushPullStep}(I,\omega ) = \mathrm{step}(I,\omega ) \cup \mathrm{pullStep}(I,\omega )\); trajectories fold these steps over a list of i.i.d. uniform rounds, and the failure probabilities are the probabilities that some node is still uninformed after \(T\) rounds started from \(\{ v_0\} \).
With the same calls, the PUSH–PULL informed set contains the PUSH and the PULL informed sets after every number of rounds.
The calls \(\omega (v)\), \(v \in V\), of a uniform round are independent, each uniform among the other \(n-1\) nodes; in particular a caller \(v \notin I\) calls into \(I\) with probability \(|I|/(n-1)\).
Let \(m = |I|\) and \(u = n - m\). From a single informed node a PULL round informs nobody with probability \((1 - \frac1{n-1})^{n-1}\). After one PULL round, \(\mathbb {E}|I'| = m + u\, \frac{m}{n-1}\) and \(\mathbb {E}[n - |I'|] = \frac{u(u-1)}{n-1} \le \frac{u^2}{n}\) (quadratic shrinking). After one PUSH–PULL round, \(\mathbb {E}[n - |I'|] = \frac{u(u-1)}{n-1}\bigl(1 - \frac1{n-1}\bigr)^{m}\).
Let \(f(I,a) \supseteq I\) be a spreading step driven by i.i.d. uniform rounds \(a\). Suppose that from every nonempty \(I\) a round is good (\(|f(I,a)| \ge \frac98 |I|\), or \(|I| {\gt} n/2\)) with probability at least \(1/8\), and that for \(|I| \ge n/2\) the expected number of uninformed nodes contracts by \(2/3\). Then after \(\left\lceil 160 \log n \right\rceil \) rounds from \(\{ v_0\} \), some node is uninformed with probability at most \(2/n\). The proof is the PUSH proof of Sections 6–9, which uses no other property of \(\mathrm{step}\).
A PULL round is good with probability at least \(1/8\), and for \(|I| \ge n/2\) it contracts the expected uninformed count by \(2/3\).
The contraction follows from \(\frac{u(u-1)}{n-1} \le \frac23 u\) for \(u \le n/2\). For good rounds, let \(X\) be the number of uninformed callers that call into \(I\), so \(|I'| = |I| + X\). By Lemma 32, \(\mu = \mathbb {E}X = \frac{(n-m)m}{n-1} \ge \max (m/2, 1/2)\) for \(m \le n/2\) and, the calls being pairwise independent, \(\mathbb {E}X^2 \le \mu + \mu ^2\). A round that is not good has \(X {\lt} m/8 \le \mu /4\), so pointwise \(X \le \mu /4 + X^2/(2t) + (t/2)\, \mathbf1[\text{good}]\) with \(t = 4(1+\mu )/3\); taking expectations gives \(\Pr [\text{good}] \ge \frac{3\mu }{4t} \ge 3/16\) (a Paley–Zygmund bound). Unlike PUSH, the reverse Markov argument of Lemma 20 does not apply, since a PULL round can inform many more than \(|I|\) new nodes.
Let \(n \ge 2\) and \(v_0 \in V\). After \(\left\lceil 160 \log n \right\rceil \) rounds of PULL, or of PUSH–PULL, started from \(\{ v_0\} \), all nodes are informed with probability at least \(1 - 2/n\).
11 The Lean formalization
The argument above is fully formalized in the accompanying repository (library RumorSpread, namespace RumorPush); the build contains no sorry and the main theorem depends only on the three standard axioms (propext, Classical.choice, Quot.sound). File structure (dependency order): Bounds.lean (Section 4), Dynamics.Uniform of the shared dynamics library (Section 3), Model.lean (Section 1), OneRound.lean (Section 5), Growth.lean (Sections 6–7), Saturation.lean (Section 8), Main.lean (main theorem and numeric lemmas), Equivalence.lean (Theorem 11). PULL and PUSH–PULL (Section 10): PullFoldl.lean and PullModel.lean (Definition 30, Lemma 31), PullIndep.lean (Lemma 32), PullOneRound.lean (Lemma 33), PullPhases.lean (Lemma 34), PullGood.lean (Lemma 35), PullMain.lean and PullPushPull.lean (Theorem 36).