Can Two Majorities Order Different Sandwiches?

TL;DR

• For exactly five voters, any two groups containing at least three voters must share somebody. That is a mathematical fact, not a benchmark result.
• If each voter signs at most one value in a term, two conflicting values cannot both collect a 3-of-5 certificate; the shared voter would have to sign both.
• I formalized those claims in Lean 4.30.0 and checked every assignment to the model's ten Boolean signature variables using by decide. Lean reports that all four named declarations depend on no axioms.
• The complete proof artifact also contains counterexamples for 2-of-5 quorums and double-signing. It does not prove Raft, liveness, network recovery, preference aggregation, or that any production implementation matches the model.

I originally pitched a simulation as proof

I first proposed this article as a five-node Raft simulation: crash leaders, delay messages, run 1,000 seeded trials, then announce that no two majorities committed different sandwiches. That would have been a useful test harness and a terrible proof.

A simulation can produce a counterexample, measure an implementation, and show what happened in the executions it visited; it cannot establish that a bad execution is impossible across every state allowed by the protocol. One thousand passing seeds only prove that the thousand seeds passed, which is a very expensive way to restate the test log.

The second mistake was quieter. Raft does not collect human lunch preferences and discover the sandwich that society wanted all along; it replicates proposed log entries so servers agree on one history. I had taken the word consensus, added a sandwich election, and accidentally changed the problem.

The fix was to shrink the claim until I could state and prove it exactly:

With five voters, any two groups containing at least three voters intersect. Therefore, if each voter signs at most one value in a term, two conflicting values cannot both receive valid 3-of-5 certificates in that term.

That theorem is smaller than Raft, but it is real. The sandwich remains because formal verification does not require emotional austerity.

A majority is a set, not a feeling

Let the voter set be:

V = {0, 1, 2, 3, 4}

A quorum is any subset of V containing at least three voters. There are 16 possible majority subsets: ten groups of exactly three, five groups of four, and the one group containing everybody.

Suppose order A is a triangular toastie and order B is a long sub. Let Q_A be the voters who signed A, while Q_B contains the voters who signed B. A valid majority certificate means |Q_A| >= 3 or |Q_B| >= 3; a certificate is only evidence that enough voters signed the value, not evidence that the sandwich tastes good or even fits through the office door.

The safety rule is equally small:

For every voter v in this term:
not (v signed A and v signed B)

Under that rule, the two signature sets must be disjoint whenever A and B are conflicting values. If they overlap, the shared voter signed both, so the rule was broken.

This gives the proof a clean shape. First show that two majorities cannot be disjoint; then combine that overlap with the no-double-signing rule. The word term matters because signing A in one term and B in a later term is not the contradiction being modeled here.

Why two 3-of-5 quorums must overlap

The handwritten proof is one paragraph. Assume two majority quorums Q_A and Q_B do not overlap. Each contains at least three voters, so their union would contain at least six distinct voters. The entire universe contains only five voters, which is impossible; therefore Q_A and Q_B share at least one voter.

The same fact appears as a counting inequality:

|Q_A intersect Q_B|
  = |Q_A| + |Q_B| - |Q_A union Q_B|
  >= 3 + 3 - 5
  >= 1

The lower bound is tight. The groups {0, 1, 2} and {2, 3, 4} overlap at exactly voter 2, which means that one computer can become the entire plot.

The proof generalizes in the usual way: if a universe contains n voters and both quorums contain more than n / 2, their sizes add to more than n, so they must overlap. I kept the artifact at five voters because the title, counterexamples, and complete Boolean model all become inspectable without hiding the interesting part behind a library theorem.

What Lean actually checked

The Lean source represents each certificate using five Booleans. A true value means that voter signed the order, and voteCount converts those decisions to natural numbers:

def voteCount (a b c d e : Bool) : Nat :=
  a.toNat + b.toNat + c.toNat + d.toNat + e.toNat

def isMajority (a b c d e : Bool) : Bool :=
  decide (3 ≤ voteCount a b c d e)

There are five signature variables for order A and five for order B, producing 2^10 = 1,024 complete assignments. The overlap function asks whether any voter signed both values:

def overlaps
    (a0 a1 a2 a3 a4 : Bool)
    (b0 b1 b2 b3 b4 : Bool) : Bool :=
  (a0 && b0) || (a1 && b1) || (a2 && b2) ||
  (a3 && b3) || (a4 && b4)

The first theorem universally quantifies over all ten decisions:

theorem majority_quorums_intersect :
    ∀ a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 : Bool,
      isMajority a0 a1 a2 a3 a4 = true →
      isMajority b0 b1 b2 b3 b4 = true →
      overlaps a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 = true := by
  decide

Lean's Decidable type contains either a proof of a proposition or a proof of its negation. According to the official tactic reference, by decide synthesizes that decision procedure, reduces it to the successful isTrue case, and returns the proof it contains; because every variable here is Boolean, the proposition is finite and computable.

This is exhaustive, not random. More importantly, it produces a proof term that Lean checks instead of a CSV containing 1,024 green rows. The distinction is small in runtime and enormous in what the result means: the theorem applies to every assignment admitted by these definitions, while a separate enumerator would only be evidence that its loop and interpretation were implemented correctly.

I also avoided native_decide. Lean's tactic documentation explains that the native variant evaluates through compiled code; it can be dramatically faster, but its proof records compiler trust through Lean.trustCompiler. Ten Booleans are tiny enough that ordinary kernel reduction finishes in roughly a second after the toolchain starts, so adding another trusted component would buy nothing except a more complicated paragraph.

The no-double-signing rule does the work

Quorum intersection alone says the two groups share a voter. It does not say which value that voter signed, whether the voter obeyed a protocol, or whether the voter was a beige computer with two pens.

The second theorem adds the disjointness premise:

theorem conflicting_majority_certificates_are_impossible :
    ∀ a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 : Bool,
      isDisjoint a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 = true →
      isMajority a0 a1 a2 a3 a4 = true →
      isMajority b0 b1 b2 b3 b4 = true →
      False := by
  decide

isDisjoint = true is how this finite model encodes the rule that nobody signed both conflicting values in the term. If both certificates were majorities, the intersection theorem would produce a shared voter; disjointness says no shared voter exists, so the assumptions imply False.

This is the useful safety chain:

majority A + majority B
             |
             v
      the signer sets overlap
             |
             v
  somebody signed A and B
             |
             v
contradiction with one value per voter per term

The threshold and the signing rule are both necessary. Remove either one and the sandwich court immediately becomes corrupt in a way the artifact can exhibit.

Breaking each assumption on purpose

The artifact names two witnesses because a theorem is easier to understand when its guardrails can be kicked.

Two signatures can split cleanly

If the threshold falls from three to two, the groups {0, 1} and {2, 3} are both valid 2-of-5 certificates and share nobody. Voter 4 can remain at lunch pretending not to know any of us.

Lean checks the concrete witness two_of_five_can_split, which states that both two-signature groups meet the smaller threshold and that their signature sets are disjoint. The majority threshold is therefore not decorative; for five voters, a threshold of two does not force intersection.

A double signer can validate both values

Keep the threshold at three, but let voter 2 sign both values. Order A receives {0, 1, 2}, while order B receives {2, 3, 4}; both have valid 3-of-5 signature counts, and the required overlap is exactly the person violating the rule.

The named witness double_signing_allows_two_majorities checks that construction. It does not contradict the impossibility theorem because the two signature sets are not disjoint; this is the counterexample you get after removing the theorem's most important premise.

Together, these witnesses do more than provide negative tests. They show why the proof has its exact shape: a majority threshold forces overlap, while the signing discipline turns that overlap into uniqueness.

No axioms does not mean no assumptions

Lean's #print axioms command reports the axioms used by a declaration, including transitive dependencies. The documentation calls out sorryAx specifically because sorry can inhabit any proposition, which makes a beautifully formatted fake proof remarkably easy.

The artifact prints dependencies for all four named declarations. The saved output is:

'majority_quorums_intersect' does not depend on any axioms
'conflicting_majority_certificates_are_impossible' does not depend on any axioms
'two_of_five_can_split' does not depend on any axioms
'double_signing_allows_two_majorities' does not depend on any axioms

The verifier also rejects sorry, explicit axiom declarations, unsafe, native_decide, sorryAx, and Lean.trustCompiler; it checks the source and output hashes recorded in the machine-readable manifest, then optionally reruns Lean. Those static checks protect the package from an accidental swap, but they are not a substitute for the kernel run, which is why the verifier says so out loud.

"No axiom dependencies" still does not mean "no assumptions." The definitions assume exactly five voters, threshold three, two candidate values, Boolean signature decisions, and one fixed term; the implication assumes conflicting values cannot share a signer. Lean verifies that the conclusion follows from that formal statement, but it cannot inspect a production cluster and confirm that the definitions describe what the code really does.

There is also a trusted base. We trust the Lean kernel to check proof terms, the distributed Lean binary to implement that kernel correctly, and the hardware running it not to flip the one bit that finally settles lunch. Formal verification makes that trust smaller and more explicit; it does not remove physics.

This is not a proof of Raft

The original Raft paper states an Election Safety property: at most one leader can be elected in a given term. Its election argument uses two ingredients that should now look familiar: a candidate needs votes from a majority of the cluster, and each server votes for at most one candidate in a term.

That resemblance is why the quorum lemma matters, but resemblance is not equivalence. This artifact contains none of the following:

• candidate and follower state transitions;
• term advancement or persistent votes;
• RequestVote or AppendEntries messages;
• delayed, duplicated, lost, or reordered delivery;
• leader completeness and log matching;
• commitment rules or state-machine application;
• membership changes, restarts, disks, or implementation code;
• any liveness claim.

A full proof of Raft safety must connect several invariants across those mechanisms. A proof about a production implementation needs another bridge from the formal model to the code, because the world's most correct theorem does not stop an engineer from using >= 2 where the model said >= 3.

The article therefore claims one reusable lemma and one corollary under an explicit signing rule. It does not place a tiny "formally verified" hat on an unverified network stack.

Reproduce the proof

The artifact README pins leanprover/lean4:v4.30.0 in lean-toolchain. After installing Lean through the official setup path, download the artifact directory and run:

cd quorum-sandwich
python verify_artifact.py --run-lean

The verifier first checks the saved package, including these SHA-256 values:

It then invokes Lean on the source, requires exit code 0, and checks that the live output contains the no-axiom line for each declaration. The recorded validation used Lean 4.30.0 for x86_64-unknown-linux-gnu, commit d024af099ca4bf2c86f649261ebf59565dc8c622; the complete environment and proof boundary live in the machine-readable manifest.

Readers can also skip the Python wrapper and run lean QuorumSandwich.lean directly. The wrapper exists to make artifact drift obvious, not to place a second judge above the theorem prover.

Questions a suspicious reader should ask

Is by decide just brute force with better branding?

It is exhaustive computation over a decidable finite proposition, but Lean returns a proof term and the kernel checks it. A normal brute-force script can report that it found no bad case; by decide must construct evidence of the universally quantified proposition as Lean understands it. For ten Booleans, direct reduction is simple enough that there is no reason to use a faster compiler-trusting path.

Why prove exactly five voters instead of all odd cluster sizes?

The general majority-intersection theorem is useful, but the five-voter version makes every modeling choice, witness, and assignment count concrete. The article claims exactly what this artifact checks. A follow-up could formalize the general cardinality result, but silently upgrading a finite theorem into an arbitrary-n claim would repeat the mistake that started this article.

Does the proof choose the correct sandwich?

No. It establishes certificate uniqueness under the stated rule, so two conflicting sandwich values cannot both be validly certified in the same term. It does not define preferences, fairness, taste, allergies, price, or a proposal-selection policy; the theorem can keep the cluster consistent while everybody consistently eats something terrible.

Would a bounded model checker also be useful?

Yes, especially for a state machine with message delivery and failures. Its result would need the explored bounds, symmetry reductions, fairness assumptions, and omitted behavior stated precisely. This artifact uses Lean because the target is a small universal theorem over a fixed finite type, not because model checking is fake.

Conclusion

Any two 3-of-5 majorities share a voter, and if nobody signs two conflicting values in one term, those values cannot both hold valid majority certificates. Lean 4.30.0 checks that statement across all 1,024 assignments in the formal model, reports no axiom dependencies, and accepts the two counterexamples that appear when the threshold or signing discipline is weakened.

That is the whole proof, and the boundary is part of the result: it establishes a quorum-safety lemma instead of Raft, liveness, code correctness, or collective sandwich wisdom. The earlier simulator might still be worth building as an implementation test, but it does not get to wear the proof's little robe.