Base win chance (proven)

Proven · Aristotle / Lean 4

Base win chance ($1 → 0.0004%)

Machine-checked: eligible swap USD scales win chance linearly in PPM until the pre-boost ceiling.

Verdict

Every $1 of eligible swap USD adds 4 PPM (0.0004%) of win chance until the default pre-boost ceiling of 40,000 PPM (4%) at $10k. Larger trades stay capped.

Plain claim

Every $1 of eligible swap USD adds 4 PPM (0.0004%) of win chance, until the pre-boost ceiling (default 4% at $10k).

Worked example

Trade	PPM	Chance
$1	4	0.0004%
$100	400	0.04%
$1,000	4,000	0.4%
$10,000	40,000	4% (ceiling)
$20,000	40,000	still 4%

Formula (onchain model)

Solidity uses USDC 1e6 units (swapAmountUSD):

winChancePPM = min(⌊swapAmountUSD / 250_000⌋, baseCeilingPPM)

Default baseCeilingPPM = 40_000. So $1 → 1_000_000 / 250_000 = 4 PPM.

Lean proves the same table with dollar labels via the equivalent encoding min(⌊usdDollars · 1_000_000 / 250_000⌋, c).

What Lean proved

New to this section? Start with the Aristotle introduction.

Aristotle project fedb2c3c-b7a9-41bc-bd53-5a105964042f builds with no sorry / admit. Core lemmas:

Table examples (winChancePPM_1 … winChancePPM_20000)
Always ≤ ceiling (winChancePPM_le_ceiling)
Monotone in USD (winChancePPM_monotone)
4 PPM = 4/1_000_000 = 0.0004% as a rational (ppm_four_eq_fraction)
Conversion identity usd · 1_000_000 / 250_000 = usd · 4 (conv_eq)

Where it lives in code

LotteryManager4626.calculateWinChance
Operator notes: docs/audits/aristotle/base-win-chance/

Base win chance ($1 → 0.0004%)

Plain claim​

Worked example​

Formula (onchain model)​

What Lean proved​

Where it lives in code​

Read next​

Plain claim

Worked example

Formula (onchain model)

What Lean proved

Where it lives in code

Read next