Dependencies

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{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\).

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\).

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.

\(\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.

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.

\(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.

\(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.

\(\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.

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|\).

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).

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.

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 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.

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).

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.

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 \(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 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.

Under the same hypotheses, the four error terms of Theorem 39 are each bounded by \(O(1/n)\) using Lemma 18 (to show \(n\) dominates the relevant polynomials in \(\log n\) once \(\log n\ge 30\)), giving the single clean bound \(\Pr [I_T\ne V] \le 500/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.

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.

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).

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)\).

\(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\).

Two rounds, from \(U_t\le 500\log n\) to exactly \(U=0\), with total failure probability \(\le \exp (-\log n)+300/n\), by chaining Lemma 35 then Lemma 36 via \(\mathrm{expList}\)-conditioning.

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).

Guaranteed contraction factor \(0.7\) (vs. the true \(\tfrac 58\)): failure probability \(\le \exp (-M/250)\).

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).

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\).

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\)).

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.

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}\).