From Swap Axioms to Weighted Geometric Means: A Characterization of AMMs Björn Assmann∗
Ulan Degenbaev†
arXiv:2604.16898v1 [cs.DC] 18 Apr 2026
April 21, 2026
Abstract Many automated market makers can be understood through the geometry of their trading orbits, the sets of states reachable from one another through swaps. In prominent designs, this geometry is captured by a simple closed-form invariant such as the constant product xy in Uniswap or a weighted geometric mean xw y 1−w in Balancer. This paper explains why these forms arise by deriving them from three basic assumptions: validity invariance (swaps preserve the validity of states), Pareto efficiency (no state on an orbit weakly dominates another), and unit invariance (changing measurement units does not change the mechanism). Together, these force every trading orbit of a two-asset AMM to be a level set of a weighted geometric mean xw y 1−w . Applied the axioms extend Q pairwise, i the classification to n-asset pools: orbits are level sets of i xw with positive weights wi i summing to 1. Imposing token-relabeling symmetry thenQpins down the weights, recovering the constant-product form xy in the two-asset case and i xi in general. The main text provides an intuitive proof sketch and discusses fees and liquidity operations. Complete proofs and a machine-checked Lean 4 formalization accompany the paper.
1
Introduction
Automated market makers (AMMs) are on-chain mechanisms that execute token swaps without an order book. In a two-token pool, the reserve pair of token balances determines which swaps are feasible and at what prices. The constant-product AMM popularized by Uniswap [10] and the weighted geometric-mean AMM used by Balancer [4] are the canonical examples, but they sit inside a much larger design space of possible reserve-based trading mechanisms. This raises a natural question: can one derive the familiar invariant curves from simple assumptions on the swap rule itself? In this paper we study this question for AMMs with positive reserves and unrestricted swaps. Rather than postulating an invariant function from the outset, we focus on the trading orbits, which are the sets of reserve states reachable from one another by swaps. We impose three structural requirements: swaps must preserve the validity of states (validity invariance), no reserve state on a trading orbit may strictly dominate another coordinatewise (Pareto efficiency) and the trading rule must be invariant under independent rescaling of the units used to measure each asset (unit invariance). Two-asset classification. In the two-asset case, these three requirements are already highly restrictive. Our main theorem shows that every trading orbit must be a weighted geometric-mean curve xw y 1−w = k ∗ †
[email protected] [email protected]
1
for some w ∈ (0, 1) and k > 0. The weighted geometric-mean AMMs are therefore not merely examples but forced by the axioms. The constant-product case appears as the special case w = 1/2. Multi-asset extension. The classification extends to n-asset AMMs. Given such an AMM, each pair (i, j) of reserves defines a two-token restriction: the intersection of a global trading orbit with the coordinate slice obtained by freezing all reserves except xi and xj . If every such restriction of the AMM satisfies Q wi the two-asset axioms, then every global trading orbit is a level set of a weighted product i xi with positive weights wi summing to 1. The argument reduces to showing that a subset of Rn whose every coordinate 2-slice is an affine line of negative slope must itself be a hyperplane with positive normal. Proof method. Our proof is geometric and elementary. The key step is to pass to log reserves (u, v) = (log x, log y), where token-wise rescaling becomes translation. This turns the orbit structure into a translation-invariant geometry in R2 , reducing the problem to a classification of additive subgroups and their cosets subject to Pareto monotonicity: the subgroup must be a line through the origin, and every orbit a parallel translate of it. Exponentiating back yields the weighted geometric-mean form. The same log-coordinate passage applies to the n-asset case, with hyperplanes playing the role of lines. Formalization. We formalize the main theorem and its multi-asset extension in Lean 4. The machine-checkable proofs give confidence in our arguments and show that foundational results in DeFi mechanism design can be expressed and verified in a modern theorem prover. Related work. Much of the CFMM literature takes a specified AMM mechanism, trading function, or invariant as given and studies the resulting pricing, arbitrage behavior, oracle properties, or liquidity-provider outcomes (see, e.g., [2, 1, 8]). Our paper reverses this perspective. Rather than postulating an invariant and analyzing its consequences, we ask which orbit geometries are compatible with a swap mechanism satisfying a small number of basic axioms. The closest conceptual relative is Lee [7], who studies general state-transition market systems from an order-theoretic viewpoint and proves abstract existence and uniqueness results for increasing invariants. In that framework, arbitrage-freeness is equivalent to the existence of an increasing invariant, while completeness is equivalent to uniqueness up to monotone reparameterization. Another paper close in spirit is [6], which shows that market makers satisfying axioms on valid trades admit a potential-function representation. Our result is complementary. In the present two-asset setting, it is more explicit and constructive. Instead of establishing the existence of some representing invariant for a broad class of systems, we work directly with primitive swap operations and show that validity invariance, Pareto efficiency, and unit invariance under token-wise rescaling force the trading orbits themselves to be weighted geometric-mean curves (xw y 1−w = k). Imposing token-relabeling symmetry further yields the constant-product form (xy = k). Thus, in our setting, the invariant family is not assumed and then analyzed, nor obtained indirectly through a general representation theorem; it is derived directly from structural axioms by an elementary geometric argument. Where existing Lean developments for AMMs verify properties of a given CFMM design [9, 5], our formalization verifies a structural classification result for the family of designs allowed by the axioms.
2
Contributions. In summary, the main contributions are the following: 1. State a minimal set of natural assumptions on the swap operation of a two-asset AMM. 2. Show that these assumptions force the trading orbits to be weighted geometric-mean curves. 3. Extend the main theorem to multi-asset AMMs. 4. Characterize how fees and liquidity operations interact with the orbit geometry. 5. Formalize the main theorem and the multi-asset extension in Lean 4. Overview. Section 2 defines the minimal model and the three assumptions. Section 3 gives an intuitive, picture-driven proof sketch and extends the result to arbitrarily many assets. Section 4 discusses how fees and liquidity operations interact with the orbit geometry. Section 5 discusses the Lean formalization. Appendix A contains the complete proofs.
2
Model
2.1
Definitions
An automated market maker (AMM) pool manages reserves of two tokens, X and Y . Traders swap assets by depositing one token and withdrawing the other. While real-world deployments track additional metadata such as fee accumulators, liquidity-provider shares, or tick ranges, we focus on an idealized model in which the reserve balances alone determine the state. This abstraction isolates the geometric structure of trading orbits. Definition 2.1 (State). A state is a pair s = (x, y) ∈ R2 representing the reserves of tokens X and Y in the AMM pool. The valid state space is S := {(x, y) ∈ R2 | x > 0, y > 0}. We allow the primitive swap maps to be defined on all of R2 , not just on S. This is convenient because the orbit relation below is defined as the symmetric closure of one-step swaps. Validity will then be enforced by an axiom stating that swaps preserve validity status. Definition 2.2 (Swap primitives). • X(s, dx) denotes the post-swap state obtained by inputting dx ≥ 0 units of token X into the pool, • Y (s, dy) denotes the post-swap state obtained by inputting dy ≥ 0 units of token Y into the pool. Bookkeeping defines output maps yout and xout through X(s, dx) = (x + dx, y − yout (s, dx)),
Y (s, dy) = (x − xout (s, dy), y + dy),
where s = (x, y). Thus yout (s, dx) is the amount of token Y paid out when dx units of token X are input at state s, and similarly for xout (s, dy). We ignore fees in the axiomatic development that follows. This isolates the structural constraints imposed by the axioms; the interplay of fees and liquidity operations with the orbit geometry is treated in Section 4. A single swap gives a one-step state transition. We first define adjacency by a single primitive swap and then take the transitive closure. Definition 2.3 (Adjacency). For states s, t, write s ↔ t if one can be obtained from the other by a single primitive swap, meaning there exists δ ≥ 0 such that t = X(s, δ)
or t = Y (s, δ)
or 3
s = X(t, δ)
or
s = Y (t, δ).
This relation is symmetric by construction. Definition 2.4 (Orbit relation). Define s ∼ t if there exist states s = s0 , s1 , . . . , sn = t such that si−1 ↔ si for all i = 1, . . . , n. For a valid state s ∈ S, its trading orbit is [s] := {t ∈ S : t ∼ s}. Thus two valid states lie in the same trading orbit precisely when they can be connected by a finite chain of primitive swaps. The question of the paper is: what geometric shape can these orbits have?
2.2
Assumptions
The abstract swap maps X and Y do not yet specify how outputs depend on reserves and inputs. To obtain structure we impose three assumptions. Our first assumption states that a primitive swap preserves the validity status of a state. Equivalently, valid states remain valid under swaps, and invalid states never become valid through a single swap. Assumption 2.5 (Validity invariance). For every state s ∈ R2 and every dx, dy ≥ 0, X(s, dx) ∈ S ⇐⇒ s ∈ S,
Y (s, dy) ∈ S ⇐⇒ s ∈ S.
Assumption 2.5 ensures that validity is constant along every adjacency edge, and hence along every orbit: a valid state and an invalid state can never lie in the same orbit. Our second assumption is an internal no-free-lunch condition. Within a trading orbit, one should not be able to move to a state with weakly more of both reserves. Definition 2.6 (Pareto order). Write t ⪰ s if t.x ≥ s.x and t.y ≥ s.y. Assumption 2.7 (Pareto efficiency). For all valid states s, t ∈ S, if s ∼ t and t ⪰ s, then t = s. This condition is numeraire-free: it compares reserve vectors directly and does not refer to any external price oracle or valuation map. Our third assumption formalizes invariance under the choice of measurement units. Changing from ETH to wei, or from dollars to cents, rescales the recorded balances but should not alter the economic mechanism. Assumption 2.8 (Unit invariance). For any a, b > 0 define Ta,b (x, y) = (ax, by). For every valid state s ∈ S and all dx, dy ≥ 0, X(Ta,b s, a dx) = Ta,b X(s, dx),
Y (Ta,b s, b dy) = Ta,b Y (s, dy).
In diagram form (shown for the X-swap): s
Ta,b
X(·, dx)
X(s,dx)
Ta,b (s) X(·, a dx)
Ta,b X(s,dx)
Ta,b
In practice, on-chain arithmetic uses finite precision, so unit invariance holds only approximately. Our model works over the reals and treats it as exact. This isolates the structural constraints that unit invariance imposes on trading orbits. Taken together, Assumptions 2.5–2.8 force a remarkably rigid orbit geometry.
4
Theorem 2.9 (Orbit classification). Consider a two-asset AMM in the setting above, satisfying validity invariance, Pareto efficiency, and unit invariance. Then there exists w ∈ (0, 1) such that the trading orbits in S are exactly the level sets of Φ(x, y) := xw y 1−w . Full proof in Appendix A. Remark 2.10. Conversely, any AMM whose orbits are level sets of xw y 1−w for some w ∈ (0, 1) satisfies the three axioms. Hence Theorem 2.9 is in fact a characterization. The weight w reflects the relative role of the two assets and is left free by the axioms. If we further require that relabeling the two tokens does not change the orbit structure, the weight is pinned down. Corollary 2.11 (Token symmetry forces constant product). Under the hypotheses of Theorem 2.9, additionally assume token relabeling symmetry: swapping the labels of X and Y preserves the orbit relation. Then w = 12 and every orbit satisfies xy = const. Full proof in Appendix A. The next section explains why the assumptions lead to weighted geometric-mean curves, and extends the classification to multi-asset pools.
3
Derivation of Weighted Geometric Means
This section presents a high-level derivation of the main result: under the three assumptions of Section 2, the trading orbits of a two-asset AMM are exactly the level sets of a weighted geometric mean xw y 1−w . Section 3.5 extends the classification to multi-asset pools. We emphasize the key ideas and geometric intuition, deliberately omitting technical details in favor of readability. Readers seeking complete proofs should consult Appendix A, while those interested in full machine-checked rigor can find the Lean formalization in Section 5. We restate the theorem here for convenience. Theorem 3.1 (Orbit classification (Theorem 2.9 restated)). Consider a two-asset AMM in the setting of Section 2, satisfying validity invariance, Pareto efficiency, and unit invariance. Then there exists w ∈ (0, 1) such that the trading orbits in S are exactly the level sets of Φ(x, y) := xw y 1−w . We first analyze the orbit through (1, 1) in four steps (Figure 1), and then extend the argument to arbitrary orbits.
5
3.1
The orbit through (1, 1) y
v
(0, 0)
u lo
g-
(1, 1)
or
bi t
orbit [s]
[s]
x (a) Decreasing curve by Pareto efficiency.
(b) Switch to log space.
y
v
(0, 0)
u v=
(1, 1)
xc y = const
−c
u
x (d) Switch back to the original space.
(c) Linearity from unit invariance.
Figure 1: Derivation of the weighted geometric-mean invariant. Step (a): Pareto efficiency. Consider the orbit through (1, 1). Pareto efficiency requires that no state on the orbit dominates another: if s1 = (x1 , y1 ) and s2 = (x2 , y2 ) lie on the same orbit with x1 < x2 , then y1 > y2 . The orbit is therefore a strictly decreasing curve (Figure 1a). Step (b): Switch to log space. Unit invariance acts multiplicatively: rescaling (x, y) 7→ (ax, by). Define the log map ℓ(x, y) := (log x, log y); the state (1, 1) maps to the origin (0, 0). In log coordinates, rescaling becomes a translation (u, v) 7→ (u + log a, v + log b), which is much easier to analyze. The orbit through (0, 0) is again a strictly decreasing curve (Figure 1b). We lift the orbit relation to log space: z ≈ z ′ ⇐⇒ ℓ−1 (z) ∼ ℓ−1 (z ′ ). Unit invariance makes this relation translation-invariant: if z ≈ z ′ , then z + δ ≈ z ′ + δ for all δ ∈ R2 (Lemma A.6). Step (c): Linearity from unit invariance. Let H := {h ∈ R2 | h ≈ 0} be the log-orbit of the origin. Translation invariance gives H an additive subgroup structure: 0 ∈ H; h ∈ H ⇒ −h ∈ H; h1 , h2 ∈ H ⇒ h1 + h2 ∈ H. But H is also a strictly decreasing curve by Pareto efficiency. An additive subgroup compatible with the strict monotonicity imposed by Pareto efficiency must be a straight line through the origin, since any genuine bend would contradict closure under addition; see Appendix A for the precise argument. We conclude that H is a line v = −c u with c > 0 (Figure 1c). Step (d): Return to reserve space. Exponentiating v = −cu gives log y = −c log x, i.e., c xc y = const (Figure 1d). Reparameterizing as w = 1+c ∈ (0, 1) yields the weighted geometric w 1−w mean x y = const.
6
3.2
Extend to all orbits
v J
z1
H
−z1
0
z2
u
z2 − z1
Figure 2: Any orbit J is parallel to H. Translating by −z1 moves z1 ∈ J to the origin and z2 to z2 − z1 . Since translation preserves ≈, we get z2 − z1 ∈ H, so J is a translate of H. Consider the log orbit J of an arbitrary valid state. We show that J is a line parallel to H. Take any two points z1 , z2 ∈ J, so that z1 ≈ z2 . By Lemma A.6, translating the entire space by −z1 shifts z1 to the origin and z2 to z2 − z1 . Since translation preserves the orbit relation, 0 ≈ (z2 − z1 ), which means (z2 − z1 ) ∈ H. Thus, the difference between any two points in J always lies in H. Because H is a line through the origin, J must be a parallel translate of H: J = z0 + H for any fixed z0 ∈ J. Applying this argument to every orbit reveals a clean geometric picture: all trading orbits in log space are parallel lines with the same slope −c (Figure 2). Different orbits differ only by their intercept. Exponentiating back to reserve space, each line cu + v = const becomes xc y = const, and reparameterizing as w = c/(1 + c) gives xw y 1−w = const on every orbit.
3.3
Role of the Axioms
The three axioms play distinct roles in the argument. Validity invariance keeps the orbit relation internal to the positive state space, so that trading orbits are genuinely geometric objects in S and can be transported to log space. Pareto efficiency forces each orbit to be a strictly decreasing tradeoff curve rather than a higher-dimensional region; without it, one can have mechanisms whose symmetrized trading orbits fill the entire positive quadrant. Unit invariance is what rigidifies these decreasing curves into weighted geometric-mean level sets: in log coordinates it becomes translation invariance, which turns the orbit through (1, 1) into an additive subgroup of R2 , and Pareto efficiency then forces that subgroup to be a line. Thus Pareto efficiency and unit invariance drive the classification, while validity invariance ensures that the classification is taking place on the intended positive-reserve state space.
3.4
Derivation of Constant Product
Token symmetry is the principle that relabeling the two assets should not change the mechanism. Assumption 3.2 (Token relabeling symmetry). Let τ (x, y) = (y, x). For all valid states s, t, s∼t
⇐⇒
τ (s) ∼ τ (t). 7
Corollary 3.3 (Constant Product). Assume the hypotheses of Theorem 2.9 and token relabeling symmetry (Assumption 3.2). Then w = 21 and every orbit satisfies xy = const. Proof. In log space, τ acts as coordinate swap (u, v) 7→ (v, u). A line v = −cu + d is sent to u = −cv + d, equivalently v = −(1/c)u + d/c. Token symmetry requires the orbit partition to be invariant under this swap, so the slope parameter must satisfy c = 1/c, hence c = 1. Therefore √ c w = 1+c = 12 , and Φ(x, y) = xy, so xy is constant on orbits.
3.5
Extension to Multiple Assets
The two-asset classification extends to pools with arbitrarily many tokens. Given a multi-asset AMM, restricting any of its global trading orbits to a coordinate 2-slice (fixing all reserves except a chosen pair (i, j)) yields a two-token restriction, i.e. the intersection of the global orbit with the slice. The global orbit structure is determined by local conditions on these restrictions: if every Q wi two-token restriction of the AMM satisfies the two-asset axioms, then a single invariant xi governs all trades, and conversely. We now make this precise. A state is a vector s = (x1 , . . . , xn ) ∈ Rn with valid state space S = {s ∈ Rn : xi > 0 for all i}. For each pair of distinct tokens (i, j), a swap primitive Xij (s, dx) inputs dx ≥ 0 units of token i and returns token j: ij (xi , xj ) 7→ xi + dx, xj − yout (s, dx) , with all other reserves unchanged. Adjacency and orbits extend from the two-asset case (Definitions 2.3–2.4), with the orbit relation generated by all pairwise swaps. Definition 3.4 (Coordinate two-token slice). For a valid state p ∈ S and a pair 1 ≤ i < j ≤ n, define Πij (p) := {x ∈ Rn : xk = pk for all k ̸= i, j}. Definition 3.5 (Two-token (i, j) restriction). For a valid state p ∈ S and a pair 1 ≤ i < j ≤ n, the two-token (i, j) restriction through p is the two-asset AMM on the slice Πij (p) whose swap primitives are the (i, j)-swaps Xij and Xji of the global AMM. Its trading orbit through p is [p]ij := [p] ∩ Πij (p). Theorem 3.6 (Multi-asset orbit classification). The trading orbits of an n-asset AMM are exactly the level sets of a weighted product Φ(x1 , . . . , xn ) =
n Y
i xw i ,
wi > 0,
P
i wi = 1,
i=1
if and only if, for every valid state p ∈ S and every pair 1 ≤ i < j ≤ n, the two-token restriction [p]ij , viewed in the coordinates (xi , xj ), satisfies the two-asset axioms (Assumptions 2.5–2.8). Proof sketch. The idea is to pass to log coordinates ui = log xi , where weighted products become affine equations and the geometry of the orbit slices becomes linear. Q i Backward direction. If the global orbits are level sets of Φ(x) = i xw i , then in log coordinates they are affine hyperplanes w1 u1 + · · · + wn un = const. Intersecting such a hyperplane with a coordinate slice Πij (p) gives an affine line in the (ui , uj )plane with slope −wi /wj < 0 (since wi , wj > 0). Exponentiating back, each two-token restriction i wj [p]ij is a weighted geometric-mean curve xw i xj = const, so by Theorem 2.9 it satisfies the two-asset axioms. 8
Forward direction. Conversely, assume every two-token restriction [p]ij satisfies the two-asset axioms. Then by the two-asset classification, every such slice is a weighted geometric-mean curve in (xi , xj ), hence a line of negative slope in log coordinates. Thus every coordinate 2-slice of every log-orbit is a negative-slope affine line. The key geometric fact, proved in Lemma A.18, is that a subset of Rn with this property must P itself be an affine hyperplane a1 u1 + · · · + an un = d with all coefficients ai > 0.QSetting wi = a / k ak and exponentiating back, each orbit is a level Pi wi set of a weighted product i xi with i wi = 1. Since parallel log-hyperplanes share the same normal, the same weights work for every orbit. u3
orbit
plane
w v12 u1
u2
v13
v23
Figure 3: Three-asset AMM in log space, showing the orbit through the origin (corresponding to the state (1, 1, 1)). The pairwise swap directions v12 , v13 , v23 (red) all lie in a common plane. The weight vector w (green) P is normal to this plane. Every other orbit is a parallel translate of this plane, characterized by wi ui = const. Corollary 3.7 (Multi-asset constant product). Under the hypotheses of Theorem 3.6, if additionally the orbit structureQis invariant under every permutation of tokens, then wi = 1/n for all i and the orbits satisfy ni=1 xi = const. Q i In practice, the invariant Φ = xw i defines admissible trades: a state transition from s to t is a valid fee-free trade whenever Φ(t) = Φ(s). This includes pairwise swaps, but also multi-token trades such as depositing several tokens and withdrawing one, or rebalancing across multiple tokens in a single transaction. A trade routed through an intermediate token (e.g., swapping X1 for X2 via X3 ) is a chain of pairwise swaps and therefore also preserves Φ.
4
Extension to Fees and Liquidity Operations
Theorems 2.9 and 3.6 classify fee-free swap orbits. Real-world AMMs also include trading fees and liquidity operations. These do not invalidate the geometric picture; rather, the partition of the state space into trading orbits provides a natural reference frame: swaps move along orbits, while fees and liquidity operations move the state across them. Fees. In many AMMs, trading fees are charged on the input token. For an X-in trade of gross size dx ≥ 0 with fee rate ϕ ∈ [0, 1), only (1 − ϕ) dx is used for pricing, while the remainder ϕ dx is retained in the pool reserves. Thus a fee-paying swap can be viewed as a fee-free swap with effective input (1 − ϕ) dx along the current orbit, followed by a one-sided reserve injection (x, y) 7→ (x + ϕ dx, y), which moves the state across orbits. This matches Uniswap v2, where the output dy satisfies (x + (1 − ϕ) dx)(y − dy) = xy, 9
while the full input dx is added to the X-reserve. Note that the order matters: reversing it, by injecting the fee first and then swapping on the shifted orbit, yields a different output. Liquidity operations. Proportional liquidity addition or removal scales the state as (x, y) 7→ (λx, λy) with λ > 0. Since Φw (λx, λy) = λ Φw (x, y), such operations move the state between orbits. In log space this becomes the diagonal translation (u, v) 7→ (u + log λ, v + log λ). More generally, an asymmetric reserve scaling (x, y) 7→ (λx x, λy y) changes the invariant by the factor λxw λy1−w : Φw (λx x, λy y) = λxw λy1−w Φw (x, y). This includes single-sided reserve additions as a special case. In summary: fee-free swaps preserve trading orbits, retained input-token fees induce transverse drift across orbits, and proportional liquidity operations produce diagonal translations in log space, hence moving the state across orbits.
5
Lean Formalization
The results of this paper have been formalized and machine-checked in Lean 4, using Mathlib for the underlying real analysis. The source code is available at [3]. For this project, the role of Lean was not only to certify the final proofs, but also to help shape the paper itself. Because the paper develops an axiomatic classification theorem, this was particularly valuable. The formalization made it transparent which assumptions were genuinely needed, helped us formulate them more precisely, and provided a reliable environment for testing variations of the theory. In an informal development, it is easy to retain assumptions that were useful in an earlier proof attempt or that simply feel natural. In Lean, by contrast, every theorem is proved under an explicit list of hypotheses, so weakening the setup immediately reveals which later steps break and which do not. This helped us reduce the number of assumptions in the final presentation. For example, an earlier version of the project included an additional path-independence type assumption, but the formalization showed that it was not needed for the main classification result. More generally, once a compiling development was in place, it became easy to experiment with modified assumptions and alternative proof structures while keeping full control over the dependency structure of the argument. The formalization also led to greater precision in the formulation of the axioms. Several statements that sound clear informally had to be made fully explicit once encoded in Lean. A representative example is the treatment of validity and adjacency. At an informal level, one might simply say that swaps “preserve validity” and fold validity directly into the definition of adjacency. In the formal development, however, we adopted a more careful design choice. We modeled validity as a separate predicate on states, while adjacency records only the existence of a primitive swap. This made clear that the validity assumption is best formulated in a way that guarantees that validity is preserved along swap chains, rather than being left implicit in the definition of the orbit relation.
6
Conclusion
The main takeaway is that a minimal set of natural assumptions already forces a very rigid orbit geometry. In the two-asset case, validity invariance, Pareto efficiency, and unit invariance force the trading orbits of a fee-free AMM to be weighted geometric-mean curves xw y 1−w = const, with constant product recovered under token symmetry. The same perspective extends to the multi-asset setting: once every two-token restriction satisfies the two-asset axioms, the global trading orbits are forced to be level sets of a weighted
10
Q i product i xw i with positive weights wi summing to 1. Beyond these classification results themselves, the Lean formalization was valuable in identifying a minimal set of assumptions and in guiding the argument toward simpler and more robust proofs.
References [1] Guillermo Angeris, Akshay Agrawal, Alex Evans, Tarun Chitra, and Stephen Boyd. Constant Function Market Makers: Multi-Asset Trades via Convex Optimization, 2021. arXiv: 2107.12484. [2] Guillermo Angeris and Tarun Chitra. Improved Price Oracles: Constant Function Market Makers, 2020. arXiv:2003.10001. [3] Björn Assmann and Ulan Degenbaev. Lean 4 Formalization of AMM Axioms. GitHub repository, 2025. URL: https://github.com/bjoernek/amm-axioms-lean. [4] Balancer Labs. Balancer: A Non-Custodial Portfolio Manager, Liquidity Provider, and Price Sensor. Protocol whitepaper, 2019. URL: https://docs.balancer.fi/whitepaper.pdf. [5] Marco Dessalvi, Massimo Bartoletti, and Alberto Lluch-Lafuente. A Formal Approach to AMM Fee Mechanisms with Lean 4, 2026. arXiv:2602.00101. [6] Rafael Frongillo, Maneesha Papireddygari, and Bo Waggoner. An Axiomatic Characterization of CFMMs and Equivalence to Prediction Markets. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024), volume 287 of Leibniz International Proceedings in Informatics (LIPIcs), pages 51:1–51:21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPIcs.ITCS.2024.51. [7] Roger Lee. All AMMs are CFMMs. All DeFi Markets Have Invariants, 2023. arXiv: 2310.09782. [8] Jason Milionis, Ciamac C. Moallemi, Tim Roughgarden, and Anthony Lee Zhang. Automated Market Making and Loss-Versus-Rebalancing, 2022. arXiv:2208.06046. [9] Daniele Pusceddu and Massimo Bartoletti. Formalizing Automated Market Makers in the Lean 4 Theorem Prover, 2024. arXiv:2402.06064. [10] Uniswap Labs. Uniswap V2 Core. Protocol whitepaper and documentation, 2020. URL: https://uniswap.org/whitepaper.pdf.
11
A
Full Mathematical Proofs
A.1
Basic properties of orbits
Lemma A.1 (Orbit relation is an equivalence relation). The relation ∼ of Definition 2.4 is an equivalence relation on R2 . Proof. Reflexivity holds by the zero-step chain s ∼ s. Symmetry holds because adjacency ↔ is symmetric by Definition 2.3. Transitivity holds by concatenating chains. Lemma A.2 (Adjacency preserves validity). Under Assumption 2.5, if s ↔ t, then s ∈ S ⇐⇒ t ∈ S. Proof. By Definition 2.3, an adjacency step has one of the forms t = X(s, δ), t = Y (s, δ), s = X(t, δ), or s = Y (t, δ) with δ ≥ 0. In each case, the equivalence follows directly from Assumption 2.5. Lemma A.3 (Orbit relation preserves validity). Under Assumption 2.5, if s ∼ t, then s ∈ S ⇐⇒ t ∈ S. In particular, if s ∈ S, then every state in the trading orbit [s] is valid. Proof. Apply Lemma A.2 along a finite adjacency chain from s to t.
A.2
Consequences of unit invariance
Lemma A.4 (Unit scaling maps orbits to orbits). Under Assumption 2.8, if s ∼ t and s, t ∈ S, then Ta,b s ∼ Ta,b t for all a, b > 0. Proof. It suffices to check one adjacency step. If t = X(s, δ), then Assumption 2.8 gives Ta,b t = Ta,b X(s, δ) = X(Ta,b s, aδ), so Ta,b s ↔ Ta,b t. The case t = Y (s, δ) is analogous. If the step is written in reverse, symmetry of ↔ handles it. Concatenating along a finite chain yields the claim. Define the logarithmic coordinate map ℓ : S → R2 ,
ℓ(x, y) := (log x, log y).
Lemma A.5 (Unit scaling becomes translation in log space). For all a, b > 0 and all s ∈ S, ℓ(Ta,b s) = ℓ(s) + (log a, log b). Proof. Immediate from log(ax) = log x + log a and log(by) = log y + log b. Since ℓ is a bijection S → R2 , its inverse is ℓ−1 (u, v) = (eu , ev ). Lift the orbit relation to R2 by declaring, for z, z ′ ∈ R2 , z ≈ z′
:⇐⇒
ℓ−1 (z) ∼ ℓ−1 (z ′ ).
Lemma A.6 (Translation invariance of ≈). Under Assumption 2.8, if z ≈ z ′ , then z + δ ≈ z′ + δ
for all δ ∈ R2 .
Proof. Write δ = (α, β) and set a = eα , b = eβ . Then ℓ−1 (z + δ) = Ta,b ℓ−1 (z) and likewise for z ′ . By Lemma A.4, orbit-equivalence is preserved under Ta,b . 12
A.3
Structure of log-orbits
Let 0 = (0, 0) ∈ R2 and define the ≈-orbit of the origin, H := {h ∈ R2 | h ≈ 0}. Translation invariance implies that every lifted orbit is a coset of H. Lemma A.7 (H is an additive subgroup). H is an additive subgroup of (R2 , +). Proof. We have 0 ∈ H by reflexivity. If h ∈ H, then h ≈ 0, and translating by −h yields 0 ≈ −h, hence −h ∈ H. If h1 , h2 ∈ H, then h1 ≈ 0 and h2 ≈ 0. Translating h1 ≈ 0 by h2 gives h1 + h2 ≈ h2 , and since h2 ≈ 0, transitivity yields h1 + h2 ≈ 0. Thus h1 + h2 ∈ H. Lemma A.8 (Every lifted orbit is a coset of H). For z, z ′ ∈ R2 , z ≈ z′
z − z ′ ∈ H.
⇐⇒
Hence each ≈-orbit has the form z0 + H. Proof. If z ≈ z ′ , translate by −z ′ to get z − z ′ ≈ 0, so z − z ′ ∈ H. Conversely, if z − z ′ ∈ H, then z − z ′ ≈ 0; translating by z ′ gives z ≈ z ′ . Lemma A.9 (H is the graph of a strictly decreasing partial function). For each u ∈ R there is at most one v ∈ R such that (u, v) ∈ H. Moreover, if (u1 , v1 ), (u2 , v2 ) ∈ H and u1 < u2 , then v1 > v2 . Proof. Since (u, v) ∈ H means ℓ−1 (u, v) ∼ (1, 1), the claim is exactly Theorem A.11 applied to the orbit of (1, 1). Lemma A.10 (H has full domain). For every u ∈ R there exists v ∈ R such that (u, v) ∈ H. Proof. First assume u ≥ 0. Set dx := eu − 1 ≥ 0,
t := X((1, 1), dx).
By Assumption 2.5, the state t is valid. Its first coordinate is tx = 1 + (eu − 1) = eu . Hence ℓ(t) = (u, log ty ), and since t is obtained from (1, 1) by a single swap, we have ℓ(t) ∈ H. Now let u < 0. By the positive case, there exists v such that (−u, v) ∈ H. Since H is a subgroup, also (u, −v) = −(−u, v) ∈ H.
A.4
Consequences of Pareto efficiency
Theorem A.11 (Orbits are strictly decreasing graphs). Fix a valid state s ∈ S. Then there exists a unique function fs : projx ([s]) → R such that (x, y) ∈ [s]
⇐⇒
y = fs (x),
and fs is strictly decreasing on its domain. Proof. Uniqueness at fixed x: if (x, y1 ), (x, y2 ) ∈ [s] and y2 ≥ y1 , then (x, y2 ) ⪰ (x, y1 ). By Assumption 2.7, they must be equal, so y1 = y2 . Strict decrease: if (x1 , y1 ), (x2 , y2 ) ∈ [s] with x1 < x2 and y2 ≥ y1 , then (x2 , y2 ) ⪰ (x1 , y1 ), again contradicting Assumption 2.7. 13
Lemma A.12 (H lies in the anti-diagonal region). Every element of H satisfies uv ≤ 0. Equivalently, H ⊆ {(u, v) ∈ R2 : uv ≤ 0}. Proof. Let (u, v) ∈ H. Then (eu , ev ) ∼ (1, 1). If u > 0 and v > 0, then (eu , ev ) ≻ (1, 1), contradicting Assumption 2.7. If u < 0 and v < 0, then (1, 1) ≻ (eu , ev ), again contradicting Assumption 2.7. Hence the coordinates cannot have the same nonzero sign, so uv ≤ 0. Lemma A.13 (Subgroups in the anti-diagonal region are linear). Let G be a nontrivial additive subgroup of R2 such that G ⊆ {(u, v) ∈ R2 : uv ≤ 0}. Assume moreover that for every u ∈ R there exists v ∈ R with (u, v) ∈ G, and that for each fixed u there is at most one such v. Then there exists c > 0 such that G = {(u, v) ∈ R2 : v = −c u}. Proof. We first show that G contains no two linearly independent vectors. Suppose for contradiction that h1 = (u1 , v1 ) and h2 = (u2 , v2 ) are linearly independent elements of G. Since G = −G, replacing vectors by their negatives if necessary, we may assume both lie in the closed fourth quadrant, so u1 , u2 ≥ 0,
v1 , v2 ≤ 0.
If one vector lies on an axis, say h1 = (u1 , 0) with u1 > 0, then h2 must have v2 < 0 (otherwise the two vectors are linearly dependent). For n large enough, nh1 − h2 = (nu1 − u2 , −v2 ) has both coordinates positive, contradicting G ⊆ {uv ≤ 0}. Hence we may assume u1 , u2 > 0,
v1 , v2 < 0.
Because h1 and h2 are linearly independent, the ratios |v1 |/|v2 | and u1 /u2 are unequal. After relabeling, assume |v1 | u1 < . |v2 | u2 Choose n ∈ N so large that the interval |v1 | u1 n ,n |v2 | u2 contains an integer m. Then for z := nh1 − mh2 ∈ G we have z1 = nu1 − mu2 > 0,
z2 = nv1 − mv2 = −n|v1 | + m|v2 | > 0.
Thus z lies in the open first quadrant, contradicting G ⊆ {uv ≤ 0}. Therefore G contains no two linearly independent vectors, so span(G) is one-dimensional. Hence G is contained in a line L through the origin. By the full-domain assumption, there exists some element of G with nonzero first coordinate, so L is not vertical. Therefore L has the form L = {(u, v) ∈ R2 : v = κu} 14
for some κ ∈ R. Since for every u ∈ R there exists (u, v) ∈ G and G ⊆ L, the uniqueness assumption forces v = κu. Hence G = L. Finally, because every nonzero element of G satisfies uv ≤ 0, the slope must be non-positive. It cannot be zero, because then G would be the u-axis, contradicting the existence of a unique v for every u together with nontriviality and the anti-diagonal constraint. So κ < 0. Writing κ = −c with c > 0 gives G = {(u, v) ∈ R2 : v = −c u}.
Theorem A.14 (The subgroup H is a line of negative slope). There exists c > 0 such that H = {(u, v) ∈ R2 : v = −c u}. Proof. Apply Lemma A.13 to G = H. The subgroup property is Lemma A.7. The anti-diagonal property is Lemma A.12. Existence of some v for each u is Lemma A.10. Uniqueness of v at fixed u is Lemma A.9. Theorem A.15 (Log-orbits are parallel lines with negative slope). There exists a constant c > 0 such that every ≈-orbit is a translate of the line {(u, v) ∈ R2 : v = −c u}. Equivalently, the linear functional L(u, v) := c u + v is constant on every lifted orbit. Proof. By Theorem A.14, the orbit of the origin is the line H = {(u, v) : v = −c u} for some c > 0. By Lemma A.8, every lifted orbit is a coset of H, hence an affine line parallel to it. On such a coset the functional L(u, v) = cu + v is constant.
A.5
Proof of the main theorem and symmetry corollary
Theorem A.16 (Weighted-product characterization of orbits). There exist constants c > 0 and w ∈ (0, 1), with c , w= 1+c such that for all valid states s = (x1 , y1 ) and t = (x2 , y2 ), s∼t
⇐⇒
1−w 1−w xw = xw . 1 y1 2 y2
Equivalently, the trading orbits are exactly the level sets of the weighted geometric mean Φw (x, y) := xw y 1−w . Proof. By Theorem A.15, there exists c > 0 such that every lifted orbit in log space is a translate of the line H = {(u, v) ∈ R2 : v = −c u}. Equivalently, if we define L(u, v) := c u + v, then two points of R2 lie in the same lifted orbit if and only if they have the same L-value. 15
Let s = (x1 , y1 ) and t = (x2 , y2 ) be valid states, and write ℓ(s) = (log x1 , log y1 ),
ℓ(t) = (log x2 , log y2 ).
Then s∼t
⇐⇒
ℓ(s) ≈ ℓ(t)
⇐⇒
L(ℓ(s)) = L(ℓ(t)).
Since L(ℓ(s)) = c log x1 + log y1 = log(xc1 y1 ), and similarly for t, this is equivalent to xc1 y1 = xc2 y2 . Now set w :=
c ∈ (0, 1). 1+c
Because all quantities are positive, raising both sides to the power 1/(1 + c) preserves equivalence, so c/(1+c) 1/(1+c) c/(1+c) 1/(1+c) xc1 y1 = xc2 y2 ⇐⇒ x1 y1 = x2 y2 . That is, 1−w 1−w xw = xw . 1 y1 2 y2
Thus s∼t
⇐⇒
Φw (s) = Φw (t),
so the trading orbits are exactly the level sets of Φw . Corollary A.17 (Constant-product characterization (Corollary 2.11 restated)). Under Assumption 3.2 (token relabeling symmetry), for all valid states s = (x1 , y1 ) and t = (x2 , y2 ), s∼t
⇐⇒
x1 y1 = x2 y2 .
Equivalently, the trading orbits are exactly the level sets of Φ(x, y) := xy. Proof. By Theorem A.16, there exists c > 0 such that lifted orbits are affine lines of slope −c, equivalently c 1−w 1−w s ∼ t ⇐⇒ xw = xw , w= . 1 y1 2 y2 1+c Token relabeling symmetry implies that swapping coordinates preserves the orbit relation. In log space, swapping coordinates sends a line v = −c u + d to the line u = −c v + d, equivalently 1 d v =− u+ . c c Hence the orbit partition is preserved when slope −c is replaced by slope −1/c. Since the orbit partition is unchanged, we must have 1 c= . c
16
Because c > 0, it follows that c = 1, and therefore w=
c 1 = . 1+c 2
Substituting into Theorem A.16 yields s∼t
⇐⇒
1/2 1/2
x1 y1
1/2 1/2
= x2 y2 .
Since all quantities are positive, this is equivalent to x1 y1 = x2 y2 . Thus the trading orbits are exactly the level sets of xy.
A.6
Proof of the multi-asset theorem and symmetry corollary
Lemma A.18 (Negative-slope slices imply hyperplane). Let S ⊆ Rn be nonempty. Assume that for every point p ∈ S and every pair 1 ≤ i < j ≤ n, the coordinate 2-slice S ∩ Πij (p),
Πij (p) := {x ∈ Rn : xk = pk for all k ̸= i, j},
is an affine line of negative slope in the (xi , xj )-coordinates. Then S is an affine hyperplane of the form a1 x1 + · · · + an xn = d with a1 , . . . , an > 0. Proof. Fix any p ∈ S. We first show that S is the graph of a function f : Rn−1 → R. Existence. Let (u1 , . . . , un−1 ) ∈ Rn−1 be given. Starting from p, we perform n − 1 moves: at step i, walk along the (xi , xn )-slice of the current point until the i-th coordinate equals ui . This is possible because the slice is a line of nonzero slope. The move changes only coordinates xi and xn , so coordinates set in earlier steps are preserved. After n − 1 steps, the first n − 1 coordinates of the resulting point are u1 , . . . , un−1 . Hence there exists un ∈ R such that (u1 , . . . , un−1 , un ) ∈ S. Uniqueness. If (u1 , . . . , un−1 , vn ), (u1 , . . . , un−1 , wn ) ∈ S, they share their x1 -coordinate and lie on the same (x1 , xn )-slice; since that slice is a line of nonzero slope, vn = wn . Therefore S = {(x1 , . . . , xn−1 , f (x1 , . . . , xn−1 )) : (x1 , . . . , xn−1 ) ∈ Rn−1 } for a uniquely determined function f : Rn−1 → R. Fix any i ∈ {1, . . . , n − 1} and any values x̄k ∈ R for k ∈ {1, . . . , n − 1} \ {i}. The graph of the one-variable restriction xi 7→ f (x̄1 , . . . , xi , . . . , x̄n−1 ) is exactly the (xi , xn )-slice of S through any of its points (all coordinates xk with k ∈ / {i, n} being held at x̄k ). By hypothesis this slice is an affine line, hence the restriction is affine. Thus f is affine in each variable separately, hence multi-affine: X Y f (x1 , . . . , xn−1 ) = cI xk , I⊆{1,...,n−1}
with cI ∈ R and the empty product equal to 1. 17
k∈I
We claim that all mixed terms vanish. Fix 1 ≤ i < j ≤ n − 1 and any values x̄k ∈ R for k ∈ {1, . . . , n − 1} \ {i, j}. The resulting two-variable restriction has the form g(u, v) = αuv + βu + γv + δ, where the coefficients α, β, γ, δ depend on the frozen values x̄k ; in particular X Y α = c{i,j}∪T x̄k . T ⊆{1,...,n−1}\{i,j}
k∈T
Its level sets g(u, v) = z0 are exactly the corresponding (xi , xj )-slices of S. By hypothesis each such level set is an affine line of negative slope. If α ̸= 0, then g(u, v) = z0 is a (possibly degenerate) hyperbola, which cannot be a single affine line; this contradicts the hypothesis. Hence α = 0 for every choice of the x̄k . Since α is a polynomial in these variables, all its coefficients vanish, i.e. c{i,j}∪T = 0 for every T ⊆ {1, . . . , n − 1} \ {i, j}. Since this holds for every pair i < j, every coefficient cI with |I| ≥ 2 vanishes. Hence f is affine: f (x1 , . . . , xn−1 ) = b1 x1 + · · · + bn−1 xn−1 + d for suitable b1 , . . . , bn−1 , d ∈ R. Therefore S = {(x1 , . . . , xn ) ∈ Rn : xn = b1 x1 + · · · + bn−1 xn−1 + d}, so S is an affine hyperplane. Finally, if all coordinates except xi , xn are fixed, then the corresponding slice is given by xn = bi xi + constant, hence has slope bi . By hypothesis this slope is negative, so bi < 0 for all i < n. Rewriting the equation of the hyperplane as (−b1 )x1 + · · · + (−bn−1 )xn−1 + xn = d, and setting ai := −bi
(1 ≤ i ≤ n − 1),
an := 1,
we obtain S = {x ∈ Rn : a1 x1 + · · · + an xn = d} with a1 , . . . , an > 0, as claimed. Lemma A.19 (Hyperplane implies negative-slope slices). Let S ⊆ Rn be an affine hyperplane of the form a1 x1 + · · · + an xn = d with a1 , . . . , an > 0. Then for every point p ∈ S and every pair 1 ≤ i < j ≤ n, the coordinate 2-slice S ∩ Πij (p),
Πij (p) := {x ∈ Rn : xk = pk for all k ̸= i, j},
is an affine line of negative slope in the (xi , xj )-coordinates. Proof. Fix p ∈ S and 1 ≤ i < j ≤ n. On the slice Πij (p) every coordinate except xi and xj equals the corresponding coordinate of p, so the hyperplane equation reduces to X ai xi + a j xj = d − ak pk =: c. k̸=i,j
Solving for xj gives xj = −
ai c xi + , aj aj
which describes an affine line in the (xi , xj )-plane with slope −ai /aj < 0, since ai , aj > 0. 18
Theorem A.20 (Multi-asset orbit classification (Theorem 3.6 restated)). The trading orbits of an n-asset AMM are exactly the level sets of a weighted product Φ(x1 , . . . , xn ) =
n Y
i xw i ,
wi > 0,
P
i wi = 1,
i=1
if and only if, for every valid state p ∈ S and every pair 1 ≤ i < j ≤ n, the two-token restriction [p]ij , viewed in the coordinates (xi , xj ), satisfies the two-asset axioms (Assumptions 2.5–2.8). Q i Proof. Backward direction. Suppose the orbits are level sets of Φ = xw i . In log coordinates ui = log xi , each orbit is the hyperplane w1 u1 + · · · + wn un = const with all wi > 0. By Lemma A.19, every coordinate 2-slice of this hyperplane is a line of negative slope. Exponentiating back, for every valid state p and every pair (i, j), the restricted orbit [p]ij is a weighted geometric-mean curve w
j i xw i xj = const
in the (xi , xj )-plane, so it satisfies the two-asset axioms by Theorem 2.9. Forward direction. Suppose that for every valid state p and every pair (i, j), the two-token restriction [p]ij satisfies the two-asset axioms. Fix a valid state s and consider its orbit O. Pass to log coordinates ui = log xi and let S = ℓ(O) be the corresponding log-orbit. For any point p ∈ S and any pair 1 ≤ i < j ≤ n, the coordinate 2-slice S ∩ Πij (p) is exactly the log-orbit of the two-token restriction obtained by fixing all reserves except (xi , xj ) at the values determined by p. By hypothesis this restriction satisfies the two-asset axioms, so by Theorem 2.9 its orbit is a level set of xai x1−a for some a ∈ (0, 1). In log coordinates this is a line j of negative slope. Since every 2-slice of S is a line of negative slope, Lemma A.18 gives S = {u ∈ Rn : a1 u1 + · · · + an un = d} P with all a > 0. Setting w = a / i i i k ak and exponentiating back, the orbit of s is the level set of Q wi xi . Since this holds for every orbit, and the weights are determined by the hyperplane normal Q i (which is the samePfor all parallel orbits), the trading orbits are exactly the level sets of Φ = xw i with wi > 0 and wi = 1. Corollary A.21 (Multi-asset constant product (Corollary 3.7 restated)). Under the hypotheses of Theorem 3.6, if additionally the orbit structure Q is invariant under every permutation of tokens, then wi = 1/n for all i and the orbits satisfy ni=1 xi = const. Q wi P Proof. By Theorem 3.6, the orbits are level sets of xi with wi > 0 and wi = 1. A Q wi Q wσ(i) xi to xi permutation σ of the tokens sends the invariant . If the orbit structure is invariant under every such permutation, the two invariants must define the P same level sets, which forces wσ(i) = wi for all σ and all i. Hence all weights are equal, and wi = 1 gives wi = 1/n.
19