Nothing new under the sum: A formal model of fast Fourier algorithms. - William Scarbro; Sanjay Rajopadhye (J. Log. Algebraic Methods Program., 2026)