A Formal Approach to AMM Fee Mechanisms with Lean 4. - Marco Dessalvi; Massimo Bartoletti; Alberto Lluch-Lafuente (FMBC, 2026)