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.

翻译：许多自动化做市商可以通过其交易轨道的几何结构来理解——这些轨道是通过交换从一个状态可达的另一状态集合。在主流设计中，这种几何结构由一个简洁的闭式不变量刻画，例如Uniswap中的常数乘积$xy$或Balancer中的加权几何均值$x^w y^{1-w}$。本文通过从三个基本假设推导这些形式来解释其成因：有效性不变性（交换保持状态有效性）、帕累托效率（轨道上无状态弱支配另一状态）和单位不变性（测量单位变化不改变机制）。这些条件共同迫使双资产AMM的每个交易轨道均为加权几何均值$x^w y^{1-w}$的水平集。将此公理成对应用可将分类推广至$n$资产池：轨道为$\prod_i x_i^{w_i}$的水平集，其中正权重$w_i$之和为$1$。施加代币重标对称性可确定权重，在双资产情形恢复常数乘积形式$xy$，在一般情形恢复$\prod_i x_i$。正文提供了直观的证明梗概，并讨论了手续费与流动性操作。论文附有完整证明和Lean 4形式化验证。