From Swap Axioms to Weighted Geometric Means: A Characterization of AMMs
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.