Jackpot payout fraction (proven)

Proven · Aristotle / Lean 4

Jackpot payout fraction

Machine-checked: a winner receives 69% of each vault’s jackpot reserve — not 69% of fees twice.

Verdict

payout(R) = ⌊R · 6900 / 10000⌋ never exceeds R, and payout + left = R. The constant 6900 matches fee lotteryShareBps numerically but scales a different base (reserve vs incoming fee).

Plain claim

A winner receives 69% of each vault’s jackpot reserve. Fee routing already filled the reserve; payout takes 69% of what is sitting there.

Worked example

Reserve R	Payout (69%)	Left in reserve
10,000	6,900	3,100
0	0	0
Three vaults at 10,000 each	20,700 total	9,300 total left

Formula (onchain model)

payout(R) = ⌊R · 6900 / 10000⌋
left(R)   = R − payout(R)

What Lean proved

Aristotle project 0837752f-e2f3-4eb3-b5e1-f63c14b64615 builds with no sorry / admit:

• payout_le / payout_add_leftover
• payout_mono
• payout_10000 / payout_zero
• totalPayout_eq_sum_map / totalPayout_le_sum
• rewardBps_independent_of_lotteryShareBps (numeric equality only)

Where it lives in code

• LotteryManager rewardPercentage = 6900
• Operator notes: docs/audits/aristotle/jackpot-payout/

Read next

• Gauge fee-split — same 6900 on fee amounts
• LotteryManager
• All Lean targets

Scope note

This is independent of fee-split lottery BPS even though both use 6900. Confusing the two bases would double-count the 69% story in product copy.