VRF win-check fairness (proven)

Proven · Aristotle / Lean 4

VRF decision fairness

Machine-checked: a uniform roll over one million outcomes wins with exactly winChancePPM / 1_000_000.

Verdict

Under uniform randomness over N = 1_000_000 outcomes, the win check (r mod N) < p has probability exactly p / N. A listed 4% chance (p = 40_000) is a real 4% in this model.

Plain claim

If randomness is uniform over one million outcomes, the chance of winning equals winChancePPM / 1_000_000. A 4% listed chance is a real 4% under that model.

Worked example

winChancePPM	Probability
0	0% (never)
40,000	4%
150,000	15%
1,000,000	100% (always)

Formula (onchain model)

win  ⇔  (r mod 1_000_000) < winChancePPM
P(win) = winChancePPM / 1_000_000    when 0 ≤ winChancePPM ≤ 1_000_000

What Lean proved

Aristotle project e1fdf9eb-ab16-46fe-9d75-e02705a934d5 builds with no sorry / admit (Finset counting):

• card_winners — exactly p winners in range N when p ≤ N
• prob_eq — prob p = (p : ℚ) / N
• prob_zero / prob_full
• prob_40000 — prob 40000 = 4 / 100

Where it lives in code

• (randomWords[0] % 1_000_000) < winChancePPM in LotteryManager4626
• Operator notes: docs/audits/aristotle/vrf-fairness/

Read next

• Base win chance
• Post-boost pipeline
• All Lean targets

Scope note

This proves fairness of the comparison under a uniform model of r. It does not verify VRF entropy quality or Chainlink / local VRF wiring.