pith. sign in

arxiv: 2604.16898 · v1 · submitted 2026-04-18 · 💻 cs.DC · cs.GT

From Swap Axioms to Weighted Geometric Means: A Characterization of AMMs

Bj\"orn Assmann , Ulan Degenbaev This is my paper

Pith reviewed 2026-05-10 06:54 UTC · model grok-4.3

classification 💻 cs.DC cs.GT
keywords automated market makersAMMsswap axiomsweighted geometric meanstrading orbitsinvariantsconstant productPareto efficiency
0
0 comments X

The pith

Three axioms on swaps force AMM trading orbits to be level sets of weighted geometric means.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper derives the shape of trading orbits in automated market makers directly from three basic rules that any swap mechanism must obey. Validity invariance requires that a swap leaves a pool state either valid or invalid as a whole. Pareto efficiency requires that no swap moves the pool to a state where every participant is at least as well off and at least one is strictly better off. Unit invariance requires that rescaling the units in which asset quantities are measured does not change which states are reachable from which. These three conditions together require that every set of mutually reachable states must coincide exactly with a level set of a weighted geometric mean.

Core claim

Together, validity invariance, Pareto efficiency, and unit invariance force every trading orbit of a two-asset AMM to be a level set of a weighted geometric mean x^w y^{1-w}. Applied pairwise, the axioms extend the classification to n-asset pools: orbits are level sets of prod x_i^{w_i} with positive weights w_i summing to 1. Imposing token-relabeling symmetry then pins down the weights, recovering the constant-product form xy in the two-asset case and prod x_i in general.

What carries the argument

The three axioms of validity invariance, Pareto efficiency, and unit invariance, which together force trading orbits to coincide with level sets of a weighted geometric mean.

If this is right

  • Any two-asset AMM obeying the axioms must have all reachable states lie on a curve x^w y^{1-w} = constant for some fixed w.
  • The same axioms applied to n-asset pools force orbits to be level sets of the weighted product prod x_i^{w_i}.
  • Adding symmetry under token relabeling forces all weights to be equal and recovers the constant-product invariant.
  • The axioms supply a uniform test that any proposed AMM design must pass if it is to use one of these geometric invariants.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Any AMM whose orbits deviate from these forms must violate at least one of the three axioms, for example through fees that break Pareto efficiency.
  • Liquidity operations can be analyzed by checking whether they preserve the same level sets once the axioms are relaxed to include fees.
  • The characterization opens the possibility of constructing new invariants by deliberately relaxing one axiom while keeping the other two.

Load-bearing premise

Every swap operation obeys validity invariance, Pareto efficiency, and unit invariance.

What would settle it

An explicit two-asset swap rule that satisfies all three axioms yet produces a trading orbit that is not a level set of any weighted geometric mean x^w y^{1-w} would falsify the characterization.

Figures

Figures reproduced from arXiv: 2604.16898 by Bj\"orn Assmann, Ulan Degenbaev.

Figure 1
Figure 1. Figure 1: Derivation of the weighted geometric-mean invariant. [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. 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. S… view at source ↗
Figure 3
Figure 3. Figure 3: Three-asset AMM in log space, showing the orbit through the origin (corresponding [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
read the original 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 $x^w 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 $x^w y^{1-w}$. Applied pairwise, the axioms extend the classification to $n$-asset pools: orbits are level sets of $\prod_i x_i^{w_i}$ with positive weights $w_i$ summing to $1$. Imposing token-relabeling symmetry then pins down the weights, recovering the constant-product form $xy$ in the two-asset case and $\prod_i x_i$ 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 0 minor

Summary. The paper claims that three axioms—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)—force the trading orbits of two-asset AMMs to be level sets of the weighted geometric mean x^w y^{1-w}. Pairwise application extends this to n-asset pools, where orbits are level sets of prod x_i^{w_i} with positive weights summing to 1; token-relabeling symmetry then recovers the constant-product form xy (or prod x_i in general). The main text gives an intuitive proof sketch and discusses fees and liquidity operations, with complete proofs and a machine-checked Lean 4 formalization provided.

Significance. If the result holds, it supplies a clean axiomatic foundation for the geometric invariants used in prominent AMMs, showing how basic economic and measurement-invariance properties select weighted geometric means without additional continuity or topological assumptions. The machine-checked Lean 4 formalization is a clear strength: it verifies the central derivation, confirms the absence of circularity, and includes the n-asset extension, lending high confidence to the classification. This work is likely to be useful for analyzing existing designs and motivating new ones in decentralized finance.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive and insightful review. The referee's summary correctly captures the paper's core contribution: deriving weighted geometric means as the unique trading orbits satisfying validity invariance, Pareto efficiency, and unit invariance, with the n-asset extension and symmetry reduction to constant-product forms. We are pleased that the significance of the axiomatic approach and the Lean 4 formalization is recognized, and we appreciate the recommendation to accept.

Circularity Check

0 steps flagged

No significant circularity: axioms derive form via verified proof

full rationale

The paper starts from three explicitly stated, independent axioms (validity invariance, Pareto efficiency, unit invariance) and derives that trading orbits must be level sets of weighted geometric means. The core two-asset and n-asset results are machine-checked in Lean 4, making the derivation self-contained and externally verifiable rather than reducing to a definition, fit, or self-citation chain. No ansatz is smuggled, no parameter is fitted then relabeled as a prediction, and token-relabeling symmetry is an optional additional assumption applied after the main classification. The result does not rename a known empirical pattern but characterizes it from first principles.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 0 invented entities

The claim rests on the three explicitly stated axioms plus standard mathematical background; no free parameters are fitted to data and no new entities are postulated.

axioms (3)
  • domain assumption Validity invariance: swaps preserve the validity of states.
    Stated in the abstract as one of the three basic assumptions.
  • domain assumption Pareto efficiency: no state on an orbit weakly dominates another.
    Stated in the abstract as one of the three basic assumptions.
  • domain assumption Unit invariance: changing measurement units does not change the mechanism.
    Stated in the abstract as one of the three basic assumptions.

pith-pipeline@v0.9.0 · 5540 in / 1328 out tokens · 56751 ms · 2026-05-10T06:54:51.187257+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

10 extracted references · 10 canonical work pages

  1. [1]

    Constant Function Market Makers: Multi-Asset Trades via Convex Optimization, 2021

    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

    work page arXiv 2021

  2. [2]

    Improved price oracles: Constant function market makers.arXiv:2003.10001, 2020

    Guillermo Angeris and Tarun Chitra. Improved Price Oracles: Constant Function Market Makers, 2020.arXiv:2003.10001

    work page arXiv 2020

  3. [3]

    Lean 4 Formalization of AMM Axioms

    Bj¨ orn Assmann and Ulan Degenbaev. Lean 4 Formalization of AMM Axioms. GitHub repository, 2025. URL:https://github.com/bjoernek/amm-axioms-lean

    work page 2025

  4. [4]

    Balancer: A Non-Custodial Portfolio Manager, Liquidity Provider, and Price Sensor

    Balancer Labs. Balancer: A Non-Custodial Portfolio Manager, Liquidity Provider, and Price Sensor. Protocol whitepaper, 2019. URL:https://docs.balancer.fi/whitepaper.pdf

    work page 2019

  5. [5]

    A Formal Approach to AMM Fee Mechanisms with Lean 4, 2026.arXiv:2602.00101

    Marco Dessalvi, Massimo Bartoletti, and Alberto Lluch-Lafuente. A Formal Approach to AMM Fee Mechanisms with Lean 4, 2026.arXiv:2602.00101

    work page arXiv 2026

  6. [6]

    An Axiomatic Characteriza- tion of CFMMs and Equivalence to Prediction Markets

    Rafael Frongillo, Maneesha Papireddygari, and Bo Waggoner. An Axiomatic Characteriza- tion of CFMMs and Equivalence to Prediction Markets. In15th Innovations in Theoretical Computer Science Conference (ITCS 2024), volume 287 ofLeibniz International Proceed- ings in Informatics (LIPIcs), pages 51:1–51:21. Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik...

    work page doi:10.4230/lipics.itcs.2024.51 2024

  7. [7]

    All AMMs are CFMMs

    Roger Lee. All AMMs are CFMMs. All DeFi Markets Have Invariants, 2023. arXiv: 2310.09782

    work page arXiv 2023

  8. [8]

    C., Roughgarden, T., and Zhang, A

    Jason Milionis, Ciamac C. Moallemi, Tim Roughgarden, and Anthony Lee Zhang. Auto- mated Market Making and Loss-Versus-Rebalancing, 2022.arXiv:2208.06046

    work page arXiv 2022

  9. [9]

    Formalizing Automated Market Makers in the Lean 4 Theorem Prover, 2024.arXiv:2402.06064

    Daniele Pusceddu and Massimo Bartoletti. Formalizing Automated Market Makers in the Lean 4 Theorem Prover, 2024.arXiv:2402.06064

    work page arXiv 2024

  10. [10]

    Uniswap V2 Core

    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 onR 2. Proof. Reflexivity holds by the zero-step chain s∼s . Symme...

    work page 2020