nonNegative maps the Java longs exactly two-to-one onto [0, 2^63)

Proved

OpenSearchPreVote.nonNegative_two_to_one

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

cluster-coordinationconsensuselasticsearchelection-schedulerformal-verificationleader-electionopensearchpaxospre-voteraftzen2

For every natural number $v < 2^{63}$ and every integer $n$ with $-2^{63} \le n < 2^{63}$ (a Java long): nonNegative n = v iff $n = v$ , or $n = -v$ when $v > 0$ , respectively $n = -2^{63}$ (Long.MIN_VALUE) when $v = 0$ . Every value in $[0, 2^{63})$ has exactly two preimages among the $2^{64}$ longs, so a uniformly distributed long gives a uniformly distributed nonNegative value. The theorem is the counting statement; no probability is formalized.

Preamble

import Definitions.Def_OpenSearchPreVote
open OpenSearchCoordination OpenSearchPreVote

Formal statement

theorem OpenSearchPreVote.nonNegative_two_to_one (v : Nat) (hv : v < 2 ^ 63) (n : Int)
    (hn : -2 ^ 63 ≤ n ∧ n < 2 ^ 63) :
    nonNegative n = v ↔ n = v ∨ n = (if v = 0 then -2 ^ 63 else -(v : Int)) := 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.nonNegative_two_to_one`

Notions used

$\mathrm{nonNegative}$ . For any integer $n$ ,

\mathrm{nonNegative}(n) = \begin{cases} 0 & \text{if } n = -2^{63},\\ |n| \in \mathbb{N} & \text{otherwise.}\end{cases}

The Lean text -2 ^ 63 parses as $-(2^{63}) = -9223372036854775808$ , which is Java's Long.MIN_VALUE. I confirmed the parse with pp.parens; $(-2)^{63}$ would give the same value anyway, since $63$ is odd.

1. Declaration

Binders and hypotheses.

$v \in \mathbb{N}$ ;
$hv$ : $v < 2^{63}$ ;
$n \in \mathbb{Z}$ ;
$hn$ : $-2^{63} \le n \wedge n < 2^{63}$ , that is, $n$ is in Java's long range.

Conclusion.

\mathrm{nonNegative}(n) = v \iff n = v \;\vee\; n = \begin{cases} -2^{63} & \text{if } v = 0,\\ -v & \text{if } v \neq 0.\end{cases}

Here $v$ on the right is cast to an integer.

Unfolded:

For $v = 0$ , the longs mapped to $0$ are exactly $0$ and $-2^{63}$ .
For $0 < v < 2^{63}$ , the longs mapped to $v$ are exactly $v$ and $-v$ .

In both cases the two candidates are distinct and lie in $[-2^{63}, 2^{63})$ . So every value in $[0, 2^{63})$ has exactly two preimages among the longs, and $\mathrm{nonNegative}$ is exactly two-to-one from the longs onto $[0, 2^{63})$ . That the candidates lie in range is elementary arithmetic and is not itself part of the statement.

2. What is not constrained

Integers outside the long range. $hn$ excludes them, so nothing is said about them. There $\mathrm{nonNegative}$ is just $|n|$ , so the preimage sets differ. For example, $\mathrm{nonNegative}(-2^{63} - 1) = \mathrm{nonNegative}(2^{63} + 1) = 2^{63} + 1$ , which I checked by evaluation.
Values $v \ge 2^{63}$ . $hv$ excludes them. The theorem does not state that no long maps to such a value, although that is true by the definition.
What is not stated. Nothing is said about $\mathrm{toPositiveLongAtMost}$ or about the uniformity of the derived delays, for example the bias introduced by $\bmod$ when the bound does not divide $2^{63}$ .
Vacuity. None. Both hypotheses are satisfiable, for example with $v = 0$ and $n = 0$ .

3. Plain-language summary

Restricted to Java long values, $\mathrm{nonNegative}$ sends exactly $v$ and $-v$ to each $v$ with $0 < v < 2^{63}$ , and exactly $0$ and Long.MIN_VALUE to $0$ . Each value in $[0, 2^{63})$ therefore has exactly two long preimages.

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