Aristotle proofsCurve 2.5× boost (proven)

Curve 2.5× boost (proven)

Proven · Aristotle / Lean 4

Curve 2.5× personal boost

Machine-checked: lottery personal boost stays between 1.0× and 2.5×, and only the covered fraction of that uplift applies to a trade.

Verdict

The corrected Curve working-balance model is sound for the stated rules. Raw boost is bounded to 10,000–25,000 BPS (1.0×–2.5×). Coverage blending never exceeds the raw boost. Full 2.5× requires ve share ≥ LP share on the trade.

Plain claim

Holding ve4626 can raise your lottery odds by up to 2.5× versus a tokenless baseline — never more under this model.

Personal boost stays at 1.0× until it is armed. Product lock: v2 is documented, not live. This Lean page proves the Curve kernel bounds. The locked product formula is Lottery personal boost v2. Live LM boostManager stays unset (identity 1.0×).

Product blend (2026-09-04): coverage is locked 4626 USD, Curve l is swapEff, D = 100_000, consume window is one UTC day at 1× veUSD. Lean proves the kernel stays in [1.0, 2.5] and coverage never exceeds raw boost. Mix is 1 + (boost - 1) × cover outside Curve. Worked numbers are the table below. Next: post-boost pipeline.

New to these roles? Follow ve4626 → ve33 / veLottery before reading the formula.

Worked example

Situation	Result
No eligible ve	1.0× (neutral — 10,000 BPS)
Full ve match + full Share coverage	2.5× (25,000 BPS)
Full ve match but only half Share coverage	Uplift is half of the way from 1.0× to 2.5× → 1.75×

Coverage blend (same shape Lean proved):

effectiveBPS = 10_000 + ⌊(rawBoost − 10_000) · coverageBPS / 10_000⌋

Example: rawBoost = 25_000, coverageBPS = 5_000 (50%) → effectiveBPS = 17_500 (1.75×).

Formula (onchain model)

tokenlessWorking = ⌊0.4 · l⌋
working          = min(tokenlessWorking + ⌊⌊0.6 · L⌋ · ve / Ve⌋, l)
rawBoost         = clamp(⌊working · 10_000 / tokenlessWorking⌋, 10_000, 25_000)

coverageBPS      = ⌊min(shareUSD, swapUSD) · 10_000 / swapUSD⌋
effectiveBPS     = 10_000 + ⌊(rawBoost − 10_000) · coverageBPS / 10_000⌋

Where l is covered skin this trade, L is pool size (creator Share supply USD), ve / Ve are effective veLottery and live total ve power.

Do not confuse:

Ratio	Range	Meaning
`working / l`	0.4 → 1.0	Fraction of position that “works”
`working / (0.4 · l)`	1.0 → 2.5	Quoted boost vs tokenless baseline

Zero position, zero tokenless working, or zero coverage → neutral 10,000 BPS.

What Lean proved

New to this section? Start with the Aristotle introduction (what Lean, Aristotle, and “no sorry” mean).

Aristotle project 46f81830-e389-4fe4-b03d-63bd050d8b0b builds with no sorry / admit. Core lemmas include:

Boost stays in [1.0, 2.5] (curveBoost_mem_Icc, rawBoost_*)
Full 2.5× iff ve share ≥ LP share (curveBoost_full_iff)
Closed form min(5/2, 1 + (3/2)·r) (curveBoost_eq_min_r)
working ≤ l; coverage and effective BPS bounds
Boost is antitone in total Ve (larger total ve → weaker personal share)

Shipping delta checks (oracle window, covered floor, LM coverage blend) were also confirmed against the same project.

Where it lives in code

ve4626BoostManager.calculateBoostForPosition — raw Curve multiplier
LotteryManager4626._applyBoost — coverage blend into win chance
Foundry: ve4626BoostManager.t.sol, LotteryManager4626.Hardening.t.sol

Curve 2.5× personal boost

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