The Cyclotomic Route to Fermat's Last Theorem, Formalized Past the Regular Case

We formalize the classical cyclotomic route to Fermat's Last Theorem in Lean 4, past the regular case, as an engine uniform in the exponent. Regularity, p ∤ h, is replaced by a separate criterion for each case. Case II (p ∣ xyz) uses Vandiver's condition p ∤ h⁺ through Washington's Theorem 9.5, discharged by a small-witness certificate: an auxiliary prime ℓ ≡ 1 (mod p) below p² − p, whose test both proves the condition and supplies the arithmetic the descent consumes. Case I (p ∤ xyz) uses the Cauchy–Genocchi criterion p ∤ Bp−3, or a Sophie Germain auxiliary prime where that residue vanishes. One certificate per exponent yields FermatLastTheoremFor p, Mathlib's own definition, for every prime between 17 and 1000 and for both known Wolstenholme primes, 16843 and 2124679. The same engine reduces full FLT, with no modularity input, to two hypotheses uniform in p, both classically open: an effective small-witness form of Vandiver's conjecture, and a Germain auxiliary for every exponent. The theorem itself is already machine-checked by the modular route (Peng et al., 2026); what the cyclotomic route adds is a different argument, sharing no mathematics with it above Mathlib and flt-regular, and an exact statement of where it stops. Every declaration the libraries build is sorry-free, with each compiler-trust axiom named and audited, and sibling libraries re-derive every prime between 17 and 200 by pure kernel reduction. Section 8 describes the AI drafting of the Lean text and the resulting trust model. Lean 4 source: six libraries at https://github.com/batchatco (topic flt-vandiver), release tag afm-v2. 31 pages.