Decentralized Finance (DeFi) has revolutionized financial markets by enabling complex asset-exchange protocols without trusted intermediaries. Automated Market Makers (AMMs) are a central component of DeFi, providing the core functionality of swapping assets of different types at algorithmically computed exchange rates. Several mainstream AMM implementations are based on the constant-product model, which ensures that swaps preserve the product of the token reserves in the AMM -- up to a \emph{trading fee} used to incentivize liquidity provision. Trading fees substantially complicate the economic properties of AMMs, and for this reason some AMM models abstract them away in order to simplify the analysis. However, trading fees have a non-trivial impact on users' trading strategies, making it crucial to develop refined AMM models that precisely account for their effects. We extend a foundational model of AMMs by introducing a new parameter, the trading fee $φ\in(0,1]$, into the swap rate function. Fee amounts increase inversely proportional to $φ$. When $φ= 1$, no fee is applied and the original model is recovered. We analyze the resulting fee-adjusted model from an economic perspective. We show that several key properties of the swap rate function, including output-boundedness and monotonicity, are preserved. At the same time, other properties - most notably additivity - no longer hold. We precisely characterize this deviation by deriving a generalized form of additivity that captures the effect of swaps in the presence of trading fees. We prove that when $φ< 1$, executing a single large swap yields strictly greater profit than splitting the trade into smaller ones. Finally, we derive a closed-form solution to the arbitrage problem in the presence of trading fees and prove its uniqueness. All results are formalized and machine-checked in the Lean 4 proof assistant.

翻译：去中心化金融（DeFi）通过实现无需可信中介的复杂资产交换协议，彻底改变了金融市场。自动化做市商（AMMs）是 DeFi 的核心组成部分，提供了按算法计算汇率交换不同类型资产的核心功能。几种主流的 AMM 实现基于恒定乘积模型，该模型确保交换操作保持 AMM 中代币储备量的乘积不变——但需扣除用于激励流动性提供的**交易费**。交易费极大地复杂化了 AMM 的经济特性，因此一些 AMM 模型将其抽象掉以简化分析。然而，交易费对用户的交易策略具有重要影响，这使得开发能够精确考虑其影响的精细化 AMM 模型变得至关重要。我们通过向交换率函数中引入一个新参数——交易费 $φ\in(0,1]$，扩展了一个基础的 AMM 模型。费用金额与 $φ$ 成反比增加。当 $φ= 1$ 时，不收取费用，恢复为原始模型。我们从经济学角度分析了由此产生的费用调整模型。我们证明了交换率函数的几个关键性质，包括输出有界性和单调性，得以保留。同时，其他性质——最显著的是可加性——不再成立。我们通过推导一种广义的可加性形式来精确刻画这种偏差，该形式捕捉了存在交易费时交换操作的影响。我们证明了当 $φ< 1$ 时，执行一次大额交换比将交易拆分为多次小额交换能产生严格更大的利润。最后，我们推导了存在交易费时套利问题的闭式解，并证明了其唯一性。所有结果均在 Lean 4 证明助手中进行了形式化和机器验证。