Formalization makes you re-derive every step, and now and then a step turns out to want a different argument than the one on the page. Working through the time analysis of the time- and space-optimal exact-majority population protocol of Doty, Eftekhari, Gąsieniec, Severson, Stachowiak, and Uznański (FOCS 2021) in Lean, one case of one lemma was like that. It is a small point, the kind that even careful papers leave for the reader to fill in; the theorem is solid and the fix is short. But it is a pretty illustration of how a proof assistant changes what counts as “obvious,” so it is worth writing down.

The setting

In this protocol $n$ agents each hold an opinion and a small numeric bias. The bias is a signed dyadic value: an agent at exponent $-j$ carries weight $2^{-j}$. Over the run, the population concentrates its majority-opinion mass around a single dominant exponent $-\ell$. Write, for the majority opinion,

where $\lvert A_{-j}\rvert$ is the number of majority-opinion main agents at exponent $-j$ and $\lvert M\rvert$ is the total number of main agents. A later phase needs a guaranteed supply of “reserve” agents sampled at the dominant level, and to arrange it the analysis proves a dichotomy about where the majority sits.

The structural input it has to work with — call it the confinement theorem — gives two facts at the end of the spreading phase:

so almost all majority agents are within three consecutive levels; and a lower bound on the majority mass,

in units of $\lvert M\rvert\,2^{-\ell}$, where the weights $1,\tfrac12,\tfrac14$ are exactly the dyadic weights of levels $-\ell,-(\ell+1),-(\ell+2)$.

The step that wants more care

The lemma’s second case takes the top level to be lightly populated, $x\le 0.19$, and aims to conclude that the next level carries the slack:

The natural way to argue this is to ask how small the mass could be if $y$ were only $0.59$, and the quick estimate places the remaining majority agents at exponent $-(\ell+2)$, the lightest of the three levels. That gives a mass of about $0.3975$, below the required $0.4$, which would force $y>0.59$.

The subtlety is in where the remainder is allowed to sit. The case hypothesis only says $x\le 0.19$; it still permits up to $0.19\lvert M\rvert$ agents to remain at the top level $-\ell$, where each contributes weight $1$, not $\tfrac14$. If those heavy agents are present, the mass lower bound is comfortably met with a much smaller $y$, so the estimate above does not by itself pin $y$ down.

A configuration to keep in mind

Take

Both hypotheses of the confinement theorem hold:

yet neither branch of the dichotomy does: $x=0.19\not>0.19$ and $y=0.064\not>0.59$. So the dichotomy in this form asks for a little more than the two stated facts supply on their own.

It is worth checking whether some other result from the spreading phase secretly caps the third level $z$ and rescues the quick argument. The nearby constants there bound a dyadic mass rather than a count, and the spreading dynamics tend to push mass downward into level $-(\ell+2)$, so a count cap on $z$ is not what that phase provides. Re-deriving the bound from only the stated lemmas leads back to the same place.

The repair: the theorem is fine

The dichotomy was a means to an end — a lower bound on a pool of compatible reserves. That pool need not rest on a single heavy level; it can draw on the union of the top two. And the clean premise for a two-level pool is not a count dichotomy but a weighted inequality, which does follow directly from the mass bound. Allowing a small slack $0.002$ for mass above $-\ell$ and placing the untracked remainder no higher than $-(\ell+2)$,

and a line of algebra gives

This is a genuine consequence of the confinement theorem, and it is exactly what a two-level reserve argument needs. Pairing it with the union of reserves sampled at $-\ell$ and $-(\ell+1)$ produces a linear floor on compatible reserves — a smaller constant than a single-level bound would give, which makes the drain phase run a constant factor longer, but the asymptotics are untouched. The optimal $O(\log n)$ stabilization time stands; only one case of one lemma changes shape. The configuration above is consistent with all of this: $3(0.19)+0.064 = 0.634 \ge 0.592$, as any real configuration must be.

Why the formalization surfaced it

Reading at speed, the mass estimate looks fine and one moves on; the assumption about where the remainder sits is easy to grant silently. A proof assistant grants nothing silently. When the Lean development tried to derive the dichotomy from the lemmas actually in hand, the goal would not close — not for want of a stronger tactic, but because the implication needs a premise the inputs do not give at that generality. That refusal is the signal. The protocol is sound, the headline theorem is correct, and the adjustment is small; what mechanization contributed was the steady insistence that each case really follow from what comes before it. That is most of what formalizing a beautiful proof feels like: not finding it wrong, but being made to say, precisely, why each step is right.