基于Lean 4的AMM费用机制形式化方法

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