Proposition 3(1), p. 22 — additivity: buying αx and then (1 − α)x from a constant product pool costs the same as buying x at once

Proved

CPAMMFlaws.Properties.proposition_3_1

by mikedeng1 · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

automated-market-makingconstant-productp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let a constant product pool hold $X>0$ units of token $A$ and $Y>0$ units of token $B$ , let $0<x<X$ and $0<\alpha<1$ . Buying $\alpha x$ units first, and then $(1-\alpha)x$ units from the pool left by the first trade, $(X-\alpha x,\;Y+y(\alpha x,X,Y))$ , costs exactly as much as buying $x$ units in one trade:

p^{\mathrm{cmm}}(\alpha x,X,Y)+p^{\mathrm{cmm}}\bigl((1-\alpha)x,\;X-\alpha x,\;Y+y(\alpha x,X,Y)\bigr)=p^{\mathrm{cmm}}(x,X,Y),

where $y(\alpha x,X,Y)=p^{\mathrm{cmm}}(\alpha x,X,Y)$ .

So splitting an order in time does not change its total cost on a constant product pool.

Formalization Note $X>0$ , $Y>0$ are the deposits of §II.C, not printed in the proposition. The pool after the first trade is written in the printed form $Y+p^{\mathrm{cmm}}(\alpha x,X,Y)$ .

Preamble

import Mathlib
import Definitions.Def_CPAMMFlaws_Properties_Setting

Formal statement

namespace CPAMMFlaws.Properties

theorem proposition_3_1 (X Y x α : ℝ) (hX : 0 < X) (hY : 0 < Y)
    (hx : 0 < x) (hxX : x < X) (hα : 0 < α) (hα1 : α < 1) :
    pcmm (α * x) X Y + pcmm ((1 - α) * x) (X - α * x) (Y + pcmm (α * x) X Y) =
      pcmm x X Y := by sorry

end CPAMMFlaws.Properties

Source

Park, The Conceptual Flaws of Constant Product Automated Market Making, working paper dated June 8, 2021, p. 22, Proposition 3(1)

Human review

Endorsed by Shuze Chen · Oct 16, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph