Lemma
Definition
LAMPORT, P. 7 — §2.1If $\mathbf{B1}(\mathcal{B})$, $\mathbf{B2}(\mathcal{B})$, and $\mathbf{B3}(\mathcal{B})$ hold, then for any $B, B' \in \mathcal{B}$:
$\big((B_{\text{qrm}} \subseteq B'_{\text{vot}}) \wedge (B'_{\text{bal}} > B_{\text{bal}})\big) \Rightarrow (B'_{\text{dec}} = B_{\text{dec}})$
If a quorum of votes for $B$ is included in the votes of $B'$ and $B'$ has a higher ballot number, then the decree chosen by $B'$ must be the same as the decree of $B$.
Proof Via Contradiction
-
Choose $C \in \Psi(B, B)$ such that $C_{\mathrm{bal}} = \min\{
B'_{\mathrm{bal}} : B' \in \Psi(B, B) \}$.
Proof: $C$ exists because $\Psi(B, B)$ is nonempty and finite. -
$C_{\mathrm{bal}} > B_{\mathrm{bal}}$.
Proof: By step 1 and the definition of $\Psi(B, B)$. -
$B_{\mathrm{vot}} \cap C_{\mathrm{qrm}} = \emptyset$.
Proof: By $B2(B)$ and the hypothesis that $B_{\mathrm{qrm}} \subseteq B_{\mathrm{vot}}$. -
$\mathrm{MaxVote}(C_{\mathrm{bal}}, C_{\mathrm{qrm}},
B)_{\mathrm{bal}} \ge B_{\mathrm{bal}}$.
Proof: By steps 2, 3 and the definition of $\mathrm{MaxVote}(C_{\mathrm{bal}}, C_{\mathrm{qrm}}, B)$. -
$\mathrm{MaxVote}(C_{\mathrm{bal}}, C_{\mathrm{qrm}}, B) \in
\mathrm{Votes}(B)$.
Proof: By step 4 (which implies that $\mathrm{MaxVote}(C_{\mathrm{bal}}, C_{\mathrm{qrm}}, B)$ is not a null vote) and the definition of $\mathrm{MaxVote}(C_{\mathrm{bal}}, C_{\mathrm{qrm}}, B)$. -
$\mathrm{MaxVote}(C_{\mathrm{bal}}, C_{\mathrm{qrm}},
B)_{\mathrm{dec}} = C_{\mathrm{dec}}$.
Proof: By step 5 and $B3(B)$. -
$\mathrm{MaxVote}(C_{\mathrm{bal}}, C_{\mathrm{qrm}},
B)_{\mathrm{dec}} = B_{\mathrm{dec}}$.
Proof: By step 6, step 1, and the definition of $\Psi(B, B)$. -
$\mathrm{MaxVote}(C_{\mathrm{bal}}, C_{\mathrm{qrm}},
B)_{\mathrm{bal}} > B_{\mathrm{bal}}$.
Proof: By step 4, since steps 7 and $B1(B)$ imply $\mathrm{MaxVote}(C_{\mathrm{bal}}, C_{\mathrm{qrm}}, B)_{\mathrm{bal}} = B_{\mathrm{bal}}$. -
$\mathrm{MaxVote}(C_{\mathrm{bal}}, C_{\mathrm{qrm}}, B) \in
\mathrm{Votes}(\Psi(B, B))$.
Proof: By steps 7, 8, and the definition of $\Psi(B, B)$. -
$\mathrm{MaxVote}(C_{\mathrm{bal}}, C_{\mathrm{qrm}},
B)_{\mathrm{bal}} < C_{\mathrm{bal}}$.
Proof: By definition of $\mathrm{MaxVote}(C_{\mathrm{bal}}, C_{\mathrm{qrm}}, B)$. -
Contradiction.
Proof: By steps 9, 10, and 1.
Simplified Proof
- Let's Assume a counterexample exists: There’s a valid ballot C which comes after a valid ballot with a different decree. Let Ψ(B, B) be the set of all such later ballots.
- Given Constraint B2 Ballot C quorum includes the quorum of Ballot B and will be able to use MaxVote to find said vote
- $\text{MaxVote}(Cbal, Cqrm, \mathcal{B})$ selects the largest prior vote in $C’$s quorum. By B3, C must adopt the decree of that vote.
- Observe the conflict: The vote chosen by MaxVote is either in $B’$s votes (so it has decree B_dec) or is null. Either way, C cannot legitimately choose a different decree than B.
- Contradiction arises: Our assumption that $C$ picks a different decree is impossible, because the rules force it to pick $B’$s decree. Ψ(B, B) can only be empty.