Post-boost win chance (proven)

Proven · Aristotle / Lean 4

Post-boost win-chance pipeline

Machine-checked: personal boost, gauge add, and USD multiplier never push final win chance above the hard cap.

Verdict

Final PPM is always min(scaled, maxWinChance). With neutral boost (10,000 BPS), zero gauge, and unit USD multiplier, final equals min(base, max) — and equals base when base is already under the cap.

Plain claim

Personal boost (up to 2.5×), optional gauge add, and USD multiplier can raise odds — but the final chance is always capped. Neutral boost leaves the base chance unchanged.

Worked example

base	covered boost	gauge	multiplier	max	final
40,000 PPM (4%)	1.0× (10,000 BPS)	0	1.0×	15%	4%
40,000	2.5×	0	1.0×	15%	10%
40,000	2.5×	0	1.0×	5%	5% (cap binds)

Formula (onchain model)

boosted = ⌊base · coveredBps / 10_000⌋ + gaugePPM
scaled  = ⌊boosted · usdMultiplierBps / 10_000⌋
final   = min(scaled, maxWinChancePPM)

coveredBps comes from the proven Curve 2.5× blend ∈ [10,000, 25,000].

What Lean proved

Aristotle project 5d0e6454-fa61-4503-b438-250c771ec84d builds with no sorry / admit:

• final_le_maxWinChance
• final_eq_min_base (neutral parameters)
• boosted_mono_coveredBps
• scaled_eq_boosted_of_unit_multiplier
• final_eq_base (base ≤ max + neutral parameters)

Where it lives in code

• LotteryManager4626._applyBoost then multipliers / cap
• Operator notes: docs/audits/aristotle/post-boost-pipeline/

Read next

• Base win chance
• Curve 2.5× boost
• VRF fairness
• All Lean targets

Scope note

This model takes coveredBps as an input in range; it does not re-prove Curve working-balance algebra (already proven separately).