The 3-Majority Dynamics on the Complete Graph
1 The model
Fix \(n \ge 1\) and let \(V = \{ 0,1,\dots ,n-1\} \) be the set of agents, each holding one of two opinions, \(1\) (“red”) or \(0\) (“blue”). Write \(I \subseteq V\) for the set of agents currently holding opinion \(1\).
A round configuration is a function \(r \colon V \to V \times V \times V\) assigning to every agent \(v\) an ordered triple of samples, each drawn independently and uniformly from \(V\), with replacement (an agent may sample itself, or the same agent twice — harmless, since a majority of three Boolean values is always well defined). Let \(R_n = V^{3V}\) denote the (finite) set of round configurations, with the uniform probability measure.
For an opinion-\(1\) set \(I \subseteq V\) and \(r \in R_n\),
Each agent independently samples \(3\) agents and adopts the majority of their current opinions.
Fix a horizon \(T \in \mathbb {N}\) and an initial set \(I_0 \subseteq V\). The sample space is \(\Omega = R_n^{\, T}\) with the uniform (i.i.d.) measure. For \(r = (r_0,\dots ,r_{T-1}) \in \Omega \) define \(I_{t+1} = \mathrm{step}(I_t, r_t)\). We write \(X_t = |I_t|\) and \(U_t = n - X_t\). In the formalization, a trajectory is a List of round configurations and \(\mathrm{run}\ I\ l\) folds step over the list \(l\).
For a fixed round \(r\), the map \(I \mapsto \mathrm{step}(I,r)\) is monotone: \(I \subseteq I'\) implies \(\mathrm{step}(I,r) \subseteq \mathrm{step}(I',r)\); iterating over a trajectory, \(\mathrm{run}\) is monotone in the same sense. This is purely combinatorial (no probability involved).
Unlike the push protocol, where the analogous monotonicity (Lemma 4 there) is load-bearing throughout, here the per-round probabilistic estimates below (Lemmas 25, 28, etc.) are instead stated and proved directly for any set \(I\) satisfying a hypothesis on \(|I|\), using monotonicity of the real polynomial \(p\) of Section 4 on \([0,1]\) rather than a reference-embedding argument via Lemma 4. Lemma 4 is recorded because it is the exact analogue of the push protocol’s structural fact, but it is not otherwise used by the chain of lemmas leading to the main theorem.
2 Main theorem
Throughout, \(\log \) denotes the natural logarithm.
Let \(n\) be such that \(\log n \ge 30\) (in particular \(n \ge 2\)), let \(I_0 \subseteq V\) with \(|I_0| \ge \tfrac 35 n\), and set
Then \(\Pr [\, I_T = V \, ] \; \ge \; 1 - \dfrac {500}{n}\).
As in the push protocol’s write-up, the threshold \(\log n \ge 30\) and the constant \(500\) are deliberately crude: the proof is organized to keep every inequality an easy direct computation, not to be sharp. Reaching this modest, two-digit threshold on \(\log n\) (rather than an astronomically large one) relies on two ingredients in Section 5: a degree-\(11\) instance of the generic exponential-vs-power bound (Lemma 18), and a log-log bound tangent at a reference point near the threshold itself rather than at the fixed point \(e\) (Lemma 20). It is known (Doerr–Goldberg–Minder–Sauerwald–Scheideler 2011; Becchetti–Clementi–Natale–Pasquale–Silvestri, SODA 2015) that an initial imbalance of only \(\Theta (\sqrt{n\log n})\) already suffices for \(O(\log n)\)-round consensus w.h.p.; reaching that sharp threshold requires tracking the process on the scale of its own standard deviation throughout, a substantially more delicate multi-scale argument. Here a constant-fraction initial imbalance keeps every step to a single, reusable Chernoff bound (Section 6) applied at a handful of explicit parameters.
The proof has two phases, as in the push protocol, but for a structurally different reason: growth (Section 7), where the opinion-\(1\) fraction self-amplifies from \(60\% \) to \(75\% \); and saturation (Section 8), where the last dissenting agents are eliminated in three stages. Because the process is not monotone in the round index, both phases need the Chernoff bound of Section 6 — unlike the push protocol, where only saturation needed a (much weaker) expectation argument.
3 Finite uniform probability and independence
As in the push protocol, all randomness is uniform over finite types, so instead of measure theory or PMF we work with plain finite sums.
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 \).
Exactly as in the push protocol: \(\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), so conditioning on the first round is a definitional unfolding.
\(\mathrm{avg}\) and \(\mathrm{expList}\) are monotone, additive, homogeneous, and constants pass through unchanged; \(\mathrm{expList}\) over a concatenated horizon splits as a nested \(\mathrm{expList}\) (expList_append), used to glue phases in Section 9.
New relative to the push protocol, since that development only ever averaged over a single uniform draw at a time. For finite types \(\beta ,\delta \) and \(g \colon \beta \to \mathbb {R}\), \(h\colon \delta \to \mathbb {R}\): \(\mathrm{avg}(p \mapsto g(p_1)h(p_2)) = \mathrm{avg}(g)\, \mathrm{avg}(h)\) over the product \(\beta \times \delta \) (avg_mul_prod), with marginal consequences avg_fst_mul/avg_snd_mul. Iterating over a \(\mathrm{Fin}\ n\)-indexed product (avg_prod_pi): for \(f \colon \mathrm{Fin}\ n \to \gamma \to \mathbb {R}\),
over \(x \colon \mathrm{Fin}\ n \to \gamma \) — the discrete, measure-theory-free form of “coordinate projections on a product space are independent,” with a one-coordinate marginal corollary (avg_eval). This is exactly the independence fact that lets the \(n\) agents’ per-round updates be combined into a single concentration bound (Section 6).
4 The majority map
Write \(x = X_t/n \in [0,1]\) for the opinion-\(1\) fraction, and \(\mathrm{ind}(I)\) for the real-valued membership indicator of \(I\), so \(\mathrm{avg}(\mathrm{ind}(I)) = |I|/n\).
For \(a,b,c \in \{ 0,1\} \): \(\mathbf1[a+b+c\ge 2] = ab+bc+ac-2abc\). Applied pointwise to the three samples of a fixed agent, this expresses the majority indicator as a polynomial in the three membership indicators.
\(Y_{\mathrm{maj}}(I,v,s) \in \{ 0,1\} \) is \(1\) iff a majority of the sample triple \(s\) lies in \(I\) (independent of \(v\), kept as a function of \(v\) to match the shape the Chernoff bound of Section 6 expects). Then \(|\mathrm{step}(I,r)| = \sum _v Y_{\mathrm{maj}}(I,v,r(v))\) (card_step_eq_sum): the per-agent, \(\{ 0,1\} \)-valued decomposition that Section 6’s tail bounds need.
Conditionally on a fixed \(I\) with \(|I|=m\), the next count \(X_{t+1} = |\mathrm{step}(I,r)|\) satisfies
proved exactly (no approximation) via Lemma 12, Definition 13 and the independence toolkit of Lemma 11 (each pairwise/triple product of membership indicators over distinct coordinates of the product space \(\mathrm{Tgt3}\ n\) factors by avg_mul_prod).
\(Y_{\mathrm{dis}} := 1 - Y_{\mathrm{maj}}\), the complementary per-agent dissent contribution, so \(n - |\mathrm{step}(I,r)| = \sum _v Y_{\mathrm{dis}}(I,v,r(v))\) with mean \(n - n\, p(x)\) (sum_avg_Y_dis); by the algebraic identity \(1-p(x) = (1-x)^2(1+2x)\) this is the quantity controlled in Section 8.
The algebraic identities for \(p\) used throughout below — \(p(x)-x = x(1-x)(2x-1)\), \(1-p(x) = (1-x)^2(1+2x)\), and the growth/saturation regional bounds \(p(\tfrac 12+\beta )-\tfrac 12 \ge \tfrac 54\beta \) for \(0\le \beta \le \tfrac 14\) and \(u(3-2u)\le \tfrac 58\) for \(0\le u\le \tfrac 14\) — are not isolated as separate Lean lemmas: each use site (growth_round, saturation_round_closed, saturation_mean_quad) re-derives the specific polynomial inequality it needs inline via ring/nlinarith, in the same spirit as the push protocol’s reverse-Markov bound, which is also not isolated as its own named lemma.
5 Elementary inequalities
For \(\tfrac 12 \le x \le 1\): \((x-1)-(x-1)^2 \le \log x\). (Mathlib’s crude linear bound \(\log x \ge x-1\) is false for \(x{\lt}1\) and, worse, plugging the correct one-sided bound \(1-\tfrac 1x\le \log x\) into the Chernoff exponent \(k-\mu -k\log (k/\mu )\) gives exactly \(0\) when \(k/\mu \to 1\) — useless. This quadratic correction, derived from Mathlib’s degree-\(3\) Taylor lower bound for \(\exp \) by elementary algebra, is what makes the growth-phase Chernoff bound (Lemma 25) bite.)
For \(x\ge 0\) and any \(k\in \mathbb {N}\): \(x^k/k! \le \exp (x)\) — the single degree-\(k\) term of the Taylor truncation, extracted by dropping every other (nonnegative, since \(x\ge 0\)) term of the sum. The cubic case \(k=3\) (exp_ge_cube) is the special case used by Lemma 17. Choosing \(k\) large enough relative to a given lower bound on \(\log n\) lets \(n\) be shown to dominate any fixed polynomial in \(\log n\) using only a modest such lower bound (Stage 2b, Lemma 35, and the final numeric bound Lemma 40) — a single low-degree truncation, such as the cubic case alone, would instead force \(\log n\) to be astronomically large.
For \(L{\gt}0\) and any reference point \(c{\gt}0\): \(\log L \le \log c - 1 + L/c\), from the crude bound \(\log t \le t - 1\) applied to \(t = L/c\); tight at \(L=c\) (equality there), unlike a bound tangent at a single globally-fixed point, so choosing \(c\) near the \(L\) actually in play gives a far sharper bound. Also records \(\exp (3)\ge 20\) (cubing the standard \(10\)-digit lower bound on \(e\)), used to instantiate \(c=\exp (3)\) below.
For \(\log x{\gt}0\): \(\log \log x \le 2 + (\log x)/20\), from Lemma 19 tangent at the reference point \(c=\exp (3)\approx 20.09\) (so \(\log c = 3\) exactly), combined with \(\exp (3)\ge 20\) to replace \(1/\exp (3)\) by the cruder but rational \(1/20\). Far tighter, once \(\log x\) is more than a few units above \(e\), than a bound tangent at the fixed point \(c=e\) (the crude bound \(\log t\le t-1\) applied directly at \(t=(\log x)/e\)) — exactly the regime Lemma 35 needs. Used only inside Lemma 35’s numeric estimate.
6 An elementary Chernoff bound
The only concentration tool used in the whole development, and the only place beyond elementary combinatorics where real exponentials appear.
Let \(Y_1,\dots ,Y_n \colon \gamma \to \{ 0,1\} \) be the per-agent contributions on the product space \(\mathrm{Fin}\ n \to \gamma \) (one independent draw of \(\gamma \) per agent), with \(\mu =\sum _i\mathrm{avg}(Y_i)\) and \(X(x) := \sum _i Y_i(x_i)\). Then for every real \(t\) (no sign restriction):
Proved via the independence toolkit (Lemma 11) applied to \(x \mapsto \prod _i \exp (tY_i(x_i))\), and the elementary bound \(1+y\le e^y\) (Mathlib’s Real.add_one_le_exp) at each factor.
In the setting of Lemma 21: for \(t\ge 0\) and any \(k\), \(\Pr [X\ge k] \le \exp (\mu (e^t-1)-tk)\) (avg_tail_ge, Markov applied to \(\exp (tX)\)); symmetrically for \(t\le 0\), \(\Pr [X\le k] \le \exp (\mu (e^t-1)-tk)\) (avg_tail_le).
Plugging \(t=\log (k/\mu )\) into Lemma 22: for \(k\ge \mu {\gt}0\),
and symmetrically for \(0{\lt}k\le \mu \), \(\Pr [X\le k] \le \exp (k-\mu -k\log (k/\mu ))\) (avg_tail_le_log). Both closed forms are mean-scaled: the exponent depends on the true \(\mu \) directly, not on a crude worst-case range/variance proxy, which matters late in the saturation phase once few at-risk agents remain (Lemma 35). Two generalized variants take only an upper bound \(\mu _{\mathrm{ub}}\ge \mu \) (avg_tail_ge_log_le, used by the saturation phase) or a lower bound \(\mu _{\mathrm{lb}} \le \mu \) (avg_tail_le_log_ge, used by the growth phase) on the true mean — monotonicity of the exponent in \(\mu \) at the optimal \(t\) makes both directions sound, and this is the form each phase actually needs, since the exact mean depends on \(x=|I|/n\) while the phases only assume an inequality on \(|I|\).
7 Growth phase
Set \(\beta _j = \tfrac 1{10}(1.1)^j\) for \(j=0,\dots ,10\); \(\beta _0=0.1\) (the hypothesis \(X_0\ge 0.6n\)) and \(\beta _{10}{\gt}0.25\).
\(\mathrm{growthBias}(j) := \tfrac 1{10}(\tfrac {11}{10})^j\), the deterministic bias target after \(j\) growth rounds; monotone, \(\le \tfrac 14\) for \(j\le 9\), and \({\gt}\tfrac 14\) at \(j=10\).
Starting from opinion-\(1\) fraction \(\ge \tfrac 12+\beta \) (\(\tfrac 1{10}\le \beta \le \tfrac 14\)), the probability of failing to reach the next bias target (guaranteed growth factor \(\tfrac {11}{10}\), comfortably below the true drift factor \(\tfrac 54\) from Lemma 14) is at most \(\exp (-n/10^7)\). Proved by computing a lower bound \(\mu _{\mathrm{lb}} = n(\tfrac 12+\tfrac 54\beta )\) on the true mean via monotonicity of \(p\) on \([\tfrac 12+\beta ,1]\) (an inline nlinarith computation, not a separate lemma), then applying the lower-tail bound avg_tail_le_log_ge at \(k=n(\tfrac 12+\tfrac {11}{10}\beta )\), and bounding the resulting exponent using Lemma 17.
Starting from bias \(\mathrm{growthBias}(i)\), after \(j\) further rounds (with \(i+j\le 10\)) the probability of failing to reach \(\mathrm{growthBias}(i+j)\) is at most \(j\exp (-n/10^7)\), by induction on \(j\) via the \(\mathrm{expList}\)-conditioning idiom (mirroring the push protocol’s Main.lean).
Starting from opinion-\(1\) fraction \(\ge \tfrac 35\), after \(10\) rounds the opinion-\(1\) fraction exceeds \(\tfrac 34\), except with probability \(\le 10\exp (-n/10^7)\).
8 Saturation phase
Write \(U_t = n-X_t\). By Lemma 27, \(U_{10}\le n/4\) except with probability \(\le 10\exp (-n/10^7)\). Getting \(U_t\) all the way to exactly \(0\) needs three stages, since a fixed-ratio Chernoff bound needs the mean itself to be \(\Omega (\log n)\) for a polynomially-small per-round failure probability.
Given a reference dissent bound \(U_t\le M\le n/4\) and any target \(k\ge \tfrac 58M\) (an upper bound \(\mu _{\mathrm{ub}}=\tfrac 58M\) on the true one-round mean, via \(1-p(x)=(1-x)^2(1+2x)\le \tfrac 58(1-x)\) for \(x\ge \tfrac 34\)), the probability the next dissent count exceeds \(k\) is at most \(\exp (k-\tfrac 58M-k\log (k/(\tfrac 58M)))\) (saturation_round_closed); the same conclusion holds for any directly-supplied upper bound \(\mu _{\mathrm{ub}}\) on the true mean (saturation_round_generic, used by Stage 2b where the quadratic estimate below is the tight one).
For any dissent bound \(U_t\le M\le n\), the true one-round mean is at most \(3M^2/n\) (the crude bound \(1-p(x)\le 3(1-x)^2\), dropping the \(\tfrac 58\) refinement). Used both by Stage 2b and by Stage 2c (at \(M=10\)).
Lemma 28’s exponent, simplified via Mathlib’s quadratic-tight Padé bound for \(\log \) (Real.le_log_one_add_of_nonneg) to the closed form \(-\lambda ^2/(k+\tfrac 58M)\), \(\lambda =k-\tfrac 58M\).
Guaranteed contraction factor \(0.7\) (vs. the true \(\tfrac 58\)): failure probability \(\le \exp (-M/250)\).
\(\mathrm{satAfter}(n,M,i) := \max (500\log n,\ (0.7)^i M)\), the target dissent bound after \(i\) Stage 2a rounds, clamped below at the floor \(500\log n\); written in closed form (not recursively) so shifts by one round agree definitionally on the unclamped branch.
Starting from a dissent bound \(M\) (\(500\log n\le M\le n/4\)), offset \(i\) rounds in, the probability the dissent count exceeds \(\mathrm{satAfter}(n,M,i+j)\) after \(j\) further rounds is at most \(j\, n^{-2}\), by induction on \(j\) via the same \(\mathrm{expList}\)- conditioning idiom as Lemma 26, with the tail direction flipped (dissent shrinking rather than opinion-\(1\) count growing).
With \(T_{2a}(n) := \left\lceil 6\log n \right\rceil \): starting from any dissent bound \(\le n/4\), after \(T_{2a}(n)\) rounds the dissent count exceeds the floor \(500\log n\) with probability at most \(T_{2a}(n)\cdot n^{-2}\).
Provided \(\log n\ge 30\): whenever \(U_t\le 500\log n\), \(\Pr [U_{t+1}{\gt}10] \le \exp (-\log n) = 1/n\). One round, jumping from the \(\Theta (\log n)\) floor directly to the fixed constant \(10\): since the mean is already tiny (\(\Theta ((\log n)^2/n)\)), this single round has an astronomically small failure probability once \(n\) is large enough to beat the relevant polynomial in \(\log n\), which a degree-\(11\) instance of Lemma 18, combined with the tighter tangent-line bound of Lemma 20, already secures at this modest threshold.
Whenever \(U_t\le 10\): \(\Pr [U_{t+1}\ge 1] \le 300/n\), via ordinary Markov applied to the nonnegative-integer \(U_{t+1}\) (\(\mathbb {E}[U_{t+1}]\le 300/n\) by Lemma 29 at \(M=10\)) — no concentration needed for the very last step.
9 Proof of the main theorem
\(T_{2a}(n)+2\) rounds, from \(U_t\le n/4\) to exactly \(U=0\), with total failure probability \(\le T_{2a}(n)\cdot n^{-2} + \exp (-\log n) + 300/n\).
For \(\log n\ge 30\) and \(|I_0|\ge \tfrac 35n\): over \(10+(T_{2a}(n)+2)\) rounds,
by gluing Lemma 27 (growth) to Lemma 38 (saturation), exactly as the push protocol’s prNotAllInformed_le glues its own two phases.
With \(T = 10+(T_{2a}(n)+2)\), Theorem 6 (majority3_consensus_whp) follows from Theorem 40 by \(\Pr [I_T=V] = 1-\Pr [I_T\ne V] \ge 1-500/n\).
10 The Lean formalization
The argument above is fully formalized (no sorry) in the accompanying repository (library ThreeMajority, namespace ThreeMajority). File structure (dependency order): Prob.lean (Section 3: the same finite-uniform avg/expList machinery as rumor_spread/RumorSpread/Prob.lean, copied since the two Lean projects are independent packages, plus the new independence toolkit avg_prod_pi and friends), Model.lean (Section 1), Bounds.lean (Section 5), Chernoff.lean (Section 6), OneRound.lean (Section 4), Growth.lean (Section 7), Saturation.lean (Section 8), Main.lean (Section 9 and the main theorem). Design constraint preserved from rumor_spread: no measure theory, no PMF/ENNReal, no Mathlib ProbabilityTheory kernels — everything is finite sums, plus Real.exp/Real.log where the Chernoff bound genuinely needs them (structurally central here, unlike the push protocol, where Real.exp appears only in a numeric side lemma).