Gauge fee-split conservation (proven)

Proven · Aristotle / Lean 4

Gauge fee-split conservation

Machine-checked: lottery / burn / voters BPS sum to 100%, and floor residuals stay on an onchain lane — never an unpaid dust bucket.

Verdict

6900 + 961 + 2139 = 10000. Burn is 9.61%; voters/protocol are 21.39% (do not swap). ShareOFT fees residual to burn; vault-share distribute residual to voters. Both paths conserve L + B + P = F.

Plain claim

Every trade fee is split 69% jackpot / 9.61% burn / 21.39% voters. Those three BPS add to 100%. Creator treasury lane is off (creatorShareBps = 0) and omitted. Integer flooring does not create an unpaid dust wallet.

Worked example (F = 69_000)

Path	Residual to	Jackpot	Burn	Voters	Sum
ShareOFT fees	burn	47,610	6,631	14,759	69,000
Vault-share distribute	voters	47,610	6,630	14,760	69,000

Formula (onchain model)

6900 + 961 + 2139 = 10000

-- ShareOFT (_splitShareOftAmount / previewDistribution)
L = ⌊F · 6900 / 10000⌋
P = ⌊F · 2139 / 10000⌋
B = F − L − P

-- Vault-share (_distributeVaultShares)
B = ⌊F · 961 / 10000⌋
L = ⌊F · 6900 / 10000⌋
P = F − B − L

What Lean proved

Aristotle project 28ab1f5d-2e57-4131-86d2-128ba0f458ab builds with no sorry / admit:

• lanes_sum_maxBps
• shareOft_conservation / shareOft_example
• vault_conservation / vault_example
• Residual bounds (shareOft_B_bounded, vault_P_bounded) and no-dust restatements

Where it lives in code

• CreatorGaugeController — _splitShareOftAmount / previewDistribution / _distributeVaultShares
• Operator notes: docs/audits/aristotle/gauge-fee-split/

Read next

• Jackpot payout — same 6900 number, different base
• GaugeController
• All Lean targets

Scope note

Creator treasury lane (creatorShareBps) is omitted because launch default is 0. Do not treat this as a proof that an enabled creator lane still conserves without a fourth residual rule.