HEXAGONbeta

The Watermark and Double Ladder Theorems: the discriminant group of the Néron–Severi lattice of a Fermat surface of prime degree

A mix of human-written and AI-generated textHuman understanding: some partsmath.AG — Algebraic Geometrymath.NT — Number Theory

Contributed by Rafael Amichis Luengo ↗

Version 1 / Oct 14, 2026 / CC BY 4.0

Abstract

Let Sm⊂P3S_m\subset\mathbb{P}^3 be the complex Fermat surface x0m+x1m+x2m+x3m=0x_0^m+x_1^m+x_2^m+x_3^m=0 of prime degree m≥5m\ge 5. Its Néron–Severi lattice NS(Sm)\mathrm{NS}(S_m) is generated by the classes of the 3m23m^2 lines on SmS_m (Schütt–Shioda–van Luijk, Degtyarev). We prove that ∣disc NS(Sm)∣=m3(m−3)2|\mathrm{disc}\,\mathrm{NS}(S_m)| = m^{3(m-3)^2} (the Watermark Theorem), which answers, for prime degree, the determinant question asked by Shioda in 1987, and we determine the discriminant group itself: NS(Sm)∗/NS(Sm)≅(Z/m)3m2−24m+59×(Z/m2)3m−16\mathrm{NS}(S_m)^*/\mathrm{NS}(S_m)\cong(\mathbb{Z}/m)^{3m^2-24m+59}\times(\mathbb{Z}/m^2)^{3m-16} for m≥7m\ge 7, and (Z/5)10×Z/25(\mathbb{Z}/5)^{10}\times\mathbb{Z}/25 for m=5m=5 (the Double Ladder Theorem). The transcendental lattice of SmS_m has the same discriminant group. Both proofs work with the explicit integer intersection matrix GG of the lines and use only elementary lattice arithmetic: the action of GG on functions pulled back along the m+1m+1 pencils of directions of (Z/m)2(\mathbb{Z}/m)^2, an explicit sublattice of ker⁡G\ker G of index m12m^{12}, and two index computations for the order; an integer identity GYG=6m2GGYG=6m^2G for the exponent, and a factorization of GG modulo mm through twelve one-variable "shadows" for the number of cyclic factors of order m2m^2. The lattice statements of both theorems are checked in the proof assistant Lean 4 with the Mathlib library, with no axiom beyond the three standard ones; the identification of GG with the intersection matrix of the lines is proved by hand and checked by computer. This work has not been refereed by a human expert.

Provenance statement

What a human checked: the author checked and understood the statements, the numbers and the structure of the argument; the proofs were checked line by line only by AI systems and, for the lattice statements, by the Lean kernel. The author, Rafael Amichis Luengo, does not write mathematics. He chose the problem, directed the work and gave ideas in plain words — images — each translated into a precise statement before anything was measured. The formula m^{3(m−3)^2} was found on 4 June 2026, from his image of a pressure test on a tanker («weigh the whole, do not look inside»), in a working exchange with an AI assistant; the attached file HOW_THE_WATERMARK_WAS_FOUND.md tells the story and says what belongs to whom. The proofs and the text were written by instances of Claude (Anthropic) working in separate roles: constructors that proposed and wrote proofs, an auditor that re-derived every step and ran checks with its own code, and a cold reader with no access to the audits. The first proofs (June 2026, through the characters of (Z/m)^3) had steps confirmed only at a few primes; the proof printed here is the integral route along which both theorems were formalized in Lean on 30 September 2026, and every step is written for general m. This text was written on 14 October 2026 and read once by an independent cold reader (also an instance of Claude), whose report found no fatal error and no gap, two errors that do not touch any statement (a lifting sentence in Lemma 14 and a history bullet in §11) and 21 points of presentation; all were applied and checked again, without a second reading. Computations were used as checks, never as steps of a proof. The lattice statements of both theorems (Watermark.watermark_theorem, DoubleLadder.double_ladder_theorem, DoubleLadder.double_ladder_five) were proved in Lean 4 with Mathlib by Aristotle (Harmonic), from pieces written by the author's assistant, then compiled again on the author's machine, including a clean rebuild; no sorry, standard axioms only. The geometry of the lines (that G is their intersection matrix) is proved by hand and checked by computer, not formalized; that the lines generate NS(S_m) is cited [SSvL, Deg]. No human expert has refereed this work. Zenodo record (papers, Lean certificates, Lean project): https://doi.org/10.5281/zenodo.23062530. Repository with the full record: https://github.com/tretoef-estrella/watermark-theorem. This TeX source was written by hand from the earlier versions and the two Lean certificates.
AI provenance filesHOW_THE_WATERMARK_WAS_FOUND.md · 11 KB

Tools used

Anthropic
Claude Code
Lean
LeanVersion v4.28.0
Harmonic
Aristotle
Python Software Foundation
Python

References

  1. E. Aljovin, H. Movasati, R. Villaflor, Integral Hodge conjecture for Fermat varieties , J. Symbolic Comput. 95 (2019), 177--184. arXiv:1711.02628.arXiv
  2. N. Aoki, T. Shioda, Generators of the Néron--Severi group of a Fermat surface , in: Arithmetic and Geometry, Vol. I, Progr. Math. 35 , Birkhäuser, Boston (1983), 1--12.
  3. Harmonic, Aristotle , https://aristotle.harmonic.fun.link
  4. A. Degtyarev, Lines generate the Picard groups of certain Fermat surfaces , J. Number Theory 147 (2015), 454--477. arXiv:1305.3073.arXiv
  5. R. Amichis Luengo, The Double Ladder Theorem , version 4 (30 September 2026), in WMDLZenodo .
  6. R. Amichis Luengo, The Double Ladder Theorem --- Lean certificate , version 2 (30 September 2026), in WMDLZenodo .
  7. L. de Moura, S. Ullrich, The Lean 4 theorem prover and programming language , in: Automated Deduction --- CADE 28, Lecture Notes in Comput. Sci. 12699 , Springer (2021), 625--635.
  8. The mathlib Community, The Lean mathematical library , in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM (2020), 367--381.
  9. V. V. Nikulin, Integral symmetric bilinear forms and some of their applications , Math. USSR Izv. 14 (1980), 103--167.
  10. M. Schütt, T. Shioda, R. van Luijk, Lines on Fermat surfaces , J. Number Theory 130 (2010), no. 9, 1939--1963. arXiv:0812.2377.arXiv
Show all 18 referencesShow fewer references
  1. T. Shioda, The Hodge conjecture for Fermat varieties , Math. Ann. 245 (1979), 175--184.
  2. T. Shioda, On the Picard number of a Fermat surface , J. Fac. Sci. Univ. Tokyo Sect. IA Math. 28 (1982), no. 3, 725--734.
  3. T. Shioda, Some observations on Jacobi sums , in: Galois Representations and Arithmetic Algebraic Geometry, Adv. Stud. Pure Math. 12 , Kinokuniya / North-Holland (1987), 119--135.
  4. T. Shioda, Mordell--Weil lattice of higher genus fibration on a Fermat surface , J. Math. Sci. Univ. Tokyo 22 (2015), 443--468.
  5. R. Amichis Luengo, The Watermark Theorem , 4 June 2026, with the version note of 30 September 2026, in WMDLZenodo .
  6. R. Amichis Luengo, The Watermark and Double Ladder Theorems (Verified in Lean) , Zenodo (2026), doi:10.5281/zenodo.23062530.DOI
  7. R. Amichis Luengo, The Watermark in Every Even Dimension: the Discriminant of the Hodge Lattice of a Fermat Variety of Prime Degree , Zenodo (2026), doi:10.5281/zenodo.23091046.DOI
  8. R. Amichis Luengo, The Watermark Theorem --- Lean certificate , version 2 (30 September 2026), in WMDLZenodo .

Version history

  1. v1Submitted by Rafael Amichis LuengoInitial depositCurrentOct 14, 2026