Lemma 2, p. 15 — the constant product invariant (X − x)(Y + y) = XY holds exactly when y = p^cmm(x, X, Y) = xY/(X − x)

Proved

CPAMMFlaws.Properties.lemma_2

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$ , and let $x<X$ be the quantity of $A$ traded ( $x>0$ a buy, $x<0$ a sale). Then:

for every real $y$ , the pool stays on its constant product curve,

(X-x)(Y+y)=XY \iff y=p^{\mathrm{cmm}}(x,X,Y)=\frac{xY}{X-x};

after the trade the pool holds

Y+p^{\mathrm{cmm}}(x,X,Y)=\frac{XY}{X-x}

units of $B$ .

This is the bridge between the pricing rule $(X-x)(Y+y)=c=XY$ of §II.C and the closed form (3) used in every later computation, together with the paper's description of the pool after the trade.

Formalization Note The page allows demand $x\in(-\infty,X]$ ; at $x=X$ no $y$ satisfies the invariant, so the lemma is stated for $x<X$ . $X>0$ , $Y>0$ are the deposits of §II.C. Part 2 is the sentence after the lemma: "After the trade, the contract contains $X-x$ units of token $A$ , and $XY/(X-x)$ units of $B$ ."

Preamble

import Mathlib
import Definitions.Def_CPAMMFlaws_Properties_Setting

Formal statement

namespace CPAMMFlaws.Properties

theorem lemma_2 (X Y x : ℝ) (hX : 0 < X) (hY : 0 < Y) (hxX : x < X) :
    (∀ y : ℝ, (X - x) * (Y + y) = X * Y ↔ y = pcmm x X Y) ∧
      Y + pcmm x X Y = X * Y / (X - x) := by sorry

end CPAMMFlaws.Properties

Source

Park, The Conceptual Flaws of Constant Product Automated Market Making, working paper dated June 8, 2021, p. 15, Lemma 2, (3), and the sentence after it; invariant from §II.C, p. 14

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