Once a round has started an election or been closed, it never starts one again

Proved

OpenSearchPreVote.round_starts_once

by pitimespi · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

cluster-coordinationconsensuselasticsearchelection-schedulerformal-verificationleader-electionopensearchpaxospre-voteraftzen2

For every election strategy es, requester response lr, response resp, sender and round r with r.electionStarted = true ∨ r.isClosed = true: handling the response does not call startElection ((r.handlePreVoteResponse es lr resp sender).2.1 = false), and the resulting round again has electionStarted = true or isClosed = true. Hence, with round_start_quorum (after a call that calls startElection, the round has electionStarted = true) and because close sets isClosed, a round calls startElection at most once along any sequence of steps, and never after it is closed (Java's compareAndSet on electionStarted, PVC:272).

Preamble

import Definitions.Def_OpenSearchPreVote
open OpenSearchCoordination OpenSearchPreVote

Formal statement

theorem OpenSearchPreVote.round_starts_once {V : Type} (es : ElectionStrategy) (lr resp : PreVoteResponse)
    (sender : DiscoveryNode) (r : PreVotingRound V) (h : r.electionStarted = true ∨ r.isClosed = true) :
    (r.handlePreVoteResponse es lr resp sender).2.1 = false ∧
    ((r.handlePreVoteResponse es lr resp sender).1.electionStarted = true ∨
      (r.handlePreVoteResponse es lr resp sender).1.isClosed = true) := by sorry

Source

OpenSearch b2a54ba5c0defba3d1d20423e911d4bf920bab19: PreVoteCollector (state line 79, start 111-115, update 128-131, handlePreVoteRequest 133-163, PreVotingRound 175-300, handlePreVoteResponse 225-279, close 296-299): https://github.com/opensearch-project/OpenSearch/blob/b2a54ba5c0defba3d1d20423e911d4bf920bab19/server/src/main/java/org/opensearch/cluster/coordination/PreVoteCollector.java#L66-L301; Coordinator (updateMaxTermSeen lines 560-581, startElection 583-602, nodeMayWinElection 628-633, getPreVoteResponse 873-879, handleJoin 1267-1299, startElectionScheduler 1567-1618, the preVoteCollector.update calls 516, 653, 777, 801, 839, 1157): https://github.com/opensearch-project/OpenSearch/blob/b2a54ba5c0defba3d1d20423e911d4bf920bab19/server/src/main/java/org/opensearch/cluster/coordination/Coordinator.java#L560-L633; ElectionSchedulerFactory (settings lines 85-115, constructor check 133-143, nonNegative 159-161, toPositiveLongAtMost 169-172, scheduleNextElection 195-241): https://github.com/opensearch-project/OpenSearch/blob/b2a54ba5c0defba3d1d20423e911d4bf920bab19/server/src/main/java/org/opensearch/cluster/coordination/ElectionSchedulerFactory.java#L62-L254; ElectionStrategy.isElectionQuorum (lines 68-88): https://github.com/opensearch-project/OpenSearch/blob/b2a54ba5c0defba3d1d20423e911d4bf920bab19/server/src/main/java/org/opensearch/cluster/coordination/ElectionStrategy.java#L68-L88; the messages PreVoteRequest.java and PreVoteResponse.java in the same directory; CoordinationState (handleStartJoin, handleJoin) as transcribed by the OpenSearchCoordination mission

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5 (independent sub-agent, blind: Lean code + auditor instructions only)

Read-back: `OpenSearchPreVote.round_starts_once`

Notions used

Rounds. A pre-voting round $r$ has five fields: a cluster state, a local node, a list of (sender, response) pairs, and Booleans $r.\mathrm{electionStarted}$ and $r.\mathrm{isClosed}$ .

The handler. $\mathrm{handlePreVoteResponse}(es, lr, r, resp, \mathit{sender})$ returns a triple (new round, start flag, max-term argument). The cases, in order:

If $r.\mathrm{isClosed}$ : $(r, \mathrm{false}, \text{none})$ .
If $resp$ is fresher than $r$ 's cluster state: $(r, \mathrm{false}, \text{some } resp.\mathrm{currentTerm})$ . "Fresher" means a larger last accepted term, or an equal term and a larger last accepted version than the state's version-or-metadata-version.
Otherwise let $r_1$ $r_{1}$ be $r$ $r$ with the list updated: the new entry in front, and earlier entries from an equal sender removed. $r_1$ $r_{1}$ has $r$ $r$ 's flags.
- If the votes of $r_1$ are not an election quorum, or $r_1.\mathrm{electionStarted}$ is true: $(r_1, \mathrm{false}, \ldots)$ .
- Otherwise: $(r_1 \text{ with electionStarted} := \mathrm{true}, \mathrm{true}, \ldots)$ .

1. Declaration

Binders and hypothesis.

$V$ : an implicit type;
$es$ : an election strategy;
$lr, resp$ : pre-vote responses;
$\mathit{sender}$ : a discovery node;
$r$ : a round over $V$ ;
$h$ : $r.\mathrm{electionStarted} = \mathrm{true} \vee r.\mathrm{isClosed} = \mathrm{true}$ .

Conclusion. Write $(r', b, m) = \mathrm{handlePreVoteResponse}(es, lr, r, resp, \mathit{sender})$ . Then

b = \mathrm{false} \;\wedge\; \big(r'.\mathrm{electionStarted} = \mathrm{true} \vee r'.\mathrm{isClosed} = \mathrm{true}\big).

If the round has already started an election or has been closed, then handling any response does not signal an election start, and the resulting round has still started an election or is still closed.

2. What is not constrained

No reachability hypothesis. $r$ is arbitrary, and $es$ , $lr$ , $resp$ and $\mathit{sender}$ are arbitrary.
A weak form. The conclusion keeps only the disjunction. It does not say which flag holds afterwards. By the definition, each flag is in fact preserved individually: a closed round is returned unchanged, and a started round stays started in every branch. The theorem states only the weaker disjunctive form.
Other fields. The conclusion says nothing about $r'$ 's other fields. In particular, the list of a started but open round can still grow. It says nothing about $m$ .
Only the handler. The theorem covers only $\mathrm{handlePreVoteResponse}$ . $\mathrm{close}$ is not mentioned (it trivially keeps $\mathrm{isClosed}$ true). The theorem is a single-step statement; it does not itself assert anything about sequences of steps.
Vacuity. None. The hypothesis is satisfiable by any closed or started round.

3. Plain-language summary

Once a round has started an election or been closed, handling one more pre-vote response never starts an election again. The round remains started or closed.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by pitimespi · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph