Lean 4를 활용한 AMM 수수료 메커니즘 형식 검증 — DEX Digest