The Watermark and Double Ladder Theorems (Verified in Lean)

Two theorems about the lattice V spanned by the 3m² lines of the complex Fermat surface of prime degree m ≥ 5, with the form given by their intersection numbers. The Watermark Theorem. V is a free abelian group of rank 3(m−1)(m−2)+1, and its discriminant is m3(m−3)²; the Gram determinant of every basis is exactly m3(m−3)², with sign +. The Double Ladder Theorem. The discriminant group is V*/V ≅ (Z/m)3m²−24m+59 × (Z/m²)3m−16 for every prime m ≥ 7, and (Z/5)10 × Z/25 for m = 5. For prime m the lines generate the Néron–Severi group (Schütt–Shioda–van Luijk; Degtyarev), so these are the discriminant of NS(S_m) and its discriminant group. Shioda asked in 1987 for the determinant, for prime degree (Questions 7.2 and 7.4). It had been checked by computer for odd m ≤ 81 (Schütt–Shioda–van Luijk), and the elementary divisors were known by computer for m ≤ 14 (Aljovin–Movasati–Villaflor). Both theorems are proved in Lean 4 with Mathlib, in one project, with no sorry and only the standard axioms (propext, Classical.choice, Quot.sound). The Lean proofs were written by Aristotle (Harmonic) from pieces written by the author, and compiled and audited again on the author's machine. Not formalized: that the Lean matrix is the intersection matrix of the lines (proved by hand and checked by computer in the Watermark certificate, §1.4), and that the lines generate the Néron–Severi group (cited). Contents: the two papers; the two Lean certificates; the proof that the Lean formalization of the Double Ladder follows; the story of how the Watermark was found; and the whole GitHub repository as a zip (Lean project, pieces, checks and logs). The same material is in the GitHub repository watermark-theorem. The two papers with their certificates are also in chaise-longue-theorem (folder hodge-fermat-campaign) and in fermat-hodge-primitivity.