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.

Order: covered boost ∈ [1.0, 2.5] from the Curve kernel, then gauge add, then USD multiplier, then min(scaled, maxWinChance). Neutral boost leaves base unchanged. Worked numbers are the table below. Product blend (not live): Lottery personal boost v2. Live LM stays 1.0×. Next: VRF fairness.

Worked example

base	covered boost	multiplier	max	final
40,000 PPM (4%)	1.0× (10,000 BPS)	1.0×	15%	4%
40,000	2.5×	1.0×	15%	10%
40,000	2.5×	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× kernel ∈ [10,000, 25,000]. Product coverage blend (v2, not live): Lottery personal boost v2.

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/

Post-boost win-chance pipeline

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