% The Watermark and Double Ladder Theorems -- LaTeX source for the Hexagon preprint server. % Written by hand on 14 October 2026 from: The Watermark Theorem v8, The Double Ladder Theorem v4, % The Double Ladder Theorem -- a pencil proof v2, and the two Lean certificates v2 % (Zenodo 10.5281/zenodo.23062530). The proof printed here is the integral route that was formalized in Lean. \documentclass[11pt]{article} \usepackage[T1]{fontenc} \usepackage{lmodern} \usepackage[a4paper,margin=2.6cm]{geometry} \usepackage{amsmath,amssymb,amsthm} \usepackage{enumitem} \usepackage{url} \usepackage[hidelinks,pdfusetitle]{hyperref} \hypersetup{pdfauthor={Rafael Amichis Luengo},pdftitle={The Watermark and Double Ladder Theorems},pdfsubject={The discriminant group of the Neron-Severi lattice of a Fermat surface of prime degree}} \setlist{itemsep=0.2em,topsep=0.3em} \newtheorem{theorem}{Theorem} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \newcommand{\Z}{\mathbb{Z}} \newcommand{\Q}{\mathbb{Q}} \newcommand{\F}{\mathbb{F}} \newcommand{\C}{\mathbb{C}} \newcommand{\Pp}{\mathbb{P}} \newcommand{\NS}{\operatorname{NS}} \newcommand{\pb}{\operatorname{pb}} \newcommand{\fib}{\operatorname{fib}} \newcommand{\aug}{\operatorname{aug}} \newcommand{\SAT}{\mathrm{SAT}} \newcommand{\one}{\mathbf{1}} \emergencystretch=2em \begin{document} \begin{center} {\LARGE\bfseries The Watermark and Double Ladder Theorems\par} \medskip {\large The discriminant group of the N\'eron--Severi lattice of a Fermat surface of prime degree\par} \bigskip {\large Rafael Amichis Luengo\par} \smallskip {\small Madrid, Spain $\cdot$ tretoef@gmail.com $\cdot$ 14 October 2026\par} \end{center} \begin{abstract} Let $S_m\subset\Pp^3$ be the complex Fermat surface $x_0^m+x_1^m+x_2^m+x_3^m=0$ of prime degree $m\ge 5$. Its N\'eron--Severi lattice $\NS(S_m)$ is generated by the classes of the $3m^2$ lines on $S_m$ (Sch\"utt--Shioda--van Luijk, Degtyarev). We prove that \[ |\operatorname{disc}\NS(S_m)| = m^{3(m-3)^2}\qquad\text{(the Watermark Theorem)}, \] which answers, for prime degree, the determinant question asked by Shioda in 1987, and we determine the discriminant group itself: \[ \NS(S_m)^\ast/\NS(S_m)\;\cong\;\begin{cases}(\Z/m)^{3m^2-24m+59}\times(\Z/m^2)^{3m-16}, & m\ge 7,\\ (\Z/5)^{10}\times\Z/25, & m=5\end{cases} \] (the Double Ladder Theorem). The transcendental lattice of $S_m$ has the same discriminant group. Both proofs work with the explicit integer intersection matrix $G$ of the lines and use only elementary lattice arithmetic: the action of $G$ on functions pulled back along the $m+1$ pencils of directions of $(\Z/m)^2$, an explicit sublattice of $\ker G$ of index $m^{12}$, and two index computations for the order; an integer identity $GYG=6m^2G$ for the exponent, and a factorization of $G$ modulo $m$ through twelve one-variable ``shadows'' for the number of cyclic factors of order $m^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 $G$ 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. \end{abstract} \section{Introduction} The N\'eron--Severi lattice of the Fermat surface has been a test case for the theory of algebraic cycles since Shioda's work on Fermat varieties \cite{Sh79,AS83,Sh87}. Let $m\ge 5$ be prime and let $S_m\subset\Pp^3(\C)$ be the Fermat surface of degree $m$. It contains exactly $3m^2$ lines. For $m\le 4$ or $\gcd(m,6)=1$ their classes span $\NS(S_m)\otimes\Q$ \cite{Sh82} (see \cite[\S3]{SSvL}), and for $\gcd(m,6)=1$ they generate $\NS(S_m)$ over $\Z$: Sch\"utt, Shioda and van Luijk proved this for $m\le 100$ \cite{SSvL}, and Degtyarev for every such $m$ \cite{Deg}. For prime $m\ge5$ the rank is $\rho(S_m)=3(m-1)(m-2)+1$ \cite{Sh82,AS83}. At the end of \cite{Sh87} (\S7, pp.~133--134) Shioda asked whether $|\det\NS| = m^{3(m-3)^2}$ for the Fermat surface of prime degree $m$: Question~7.2 in characteristic $p\equiv 1\pmod m$, and Question~7.4, formula (7.10), for the complex surface. Sch\"utt, Shioda and van Luijk computed the determinant of the intersection form on their basis of lines for every odd $m\le 81$ and found $m^{3(m-3)^2}$ \cite[end of \S4]{SSvL}. In 2015 Shioda still used the formula as expected, inside Conjecture~23 of \cite{Sh15}. Aljovin, Movasati and Villaflor computed by machine the elementary divisors of the lattice of the lines for $3\le m\le 14$ \cite[Table~1]{AMV}; for $m=5,7,11,13$ their rows are \[ 1^{26}\,5^{10}\,25,\qquad 1^{48}\,7^{38}\,49^{5},\qquad 1^{96}\,11^{158}\,121^{17},\qquad 1^{120}\,13^{254}\,169^{23}, \] whose products are $m^{3(m-3)^2}$. We did not find a proof of the formula for general prime $m$, nor a description of the group for general $m$, in the literature that we read (\S\ref{sec:history}). \begin{theorem}[The Watermark Theorem]\label{thm:A} For every prime $m\ge5$, the lattice $V$ spanned by the classes of the $3m^2$ lines of $S_m$, with the intersection form, is free of rank $3(m-1)(m-2)+1$ and the Gram matrix of every $\Z$-basis of $V$ has determinant $m^{3(m-3)^2}$. Hence $|\operatorname{disc}\NS(S_m)|=m^{3(m-3)^2}$. \end{theorem} \begin{theorem}[The Double Ladder Theorem]\label{thm:B} For every prime $m\ge7$, \[ V^\ast/V\;\cong\;(\Z/m)^{3m^2-24m+59}\times(\Z/m^2)^{3m-16}, \] and $V^\ast/V\cong(\Z/5)^{10}\times\Z/25$ for $m=5$. Here $V^\ast=\operatorname{Hom}(V,\Z)$, and $V\subset V^\ast$ through the form. \end{theorem} Since $V=\NS(S_m)$, Theorem~\ref{thm:B} is the discriminant group of the N\'eron--Severi lattice; Theorem~\ref{thm:A} gives its order. The sign of the determinant in Theorem~\ref{thm:A} is $+$: the form has signature $(1,\rho-1)$ and $\rho-1=3(m-1)(m-2)$ is even.\footnote{The row $(2,7)$ of \cite[Table~1]{AMV} (arXiv:1711.02628v2) prints the sign $-$; the signature argument and a direct computation of the determinant both give $+7^{48}$.} The four rows of \cite[Table~1]{AMV} quoted above are Theorem~\ref{thm:B} at $m=5,7,11,13$. \begin{corollary}\label{cor:T} For every prime $m\ge5$ the transcendental lattice $T_m=\NS(S_m)^\perp\subset H^2(S_m,\Z)$ has rank $(m-1)(m-3)^2$ and $T_m^\ast/T_m\cong V^\ast/V$; in particular $|\operatorname{disc}T_m|=m^{3(m-3)^2}$. \end{corollary} \begin{proof} $H^2(S_m,\Z)$ is torsion free and unimodular, since $S_m$ is simply connected (Lefschetz) and by Poincar\'e duality, and $\NS(S_m)=H^2(S_m,\Z)\cap H^{1,1}$ is a primitive sublattice, so the discriminant groups of $\NS(S_m)$ and of its orthogonal complement are isomorphic \cite[Prop.~1.6.1]{Nik}. The second Betti number of a smooth surface of degree $m$ in $\Pp^3$ is $m^3-4m^2+6m-2$, and $m^3-4m^2+6m-2-(3m^2-9m+7)=(m-1)(m-3)^2$. \end{proof} \paragraph{The proofs.} Everything is proved for an explicit integer matrix $G$ of size $3m^2$, defined in \S\ref{sec:config}; that $G$ is the intersection matrix of the lines is the classical configuration, proved in \S\ref{sec:geometry}. Theorem~\ref{thm:A} is proved in \S\S\ref{sec:pencils}--\ref{sec:proofA}. The kernel $K$ of $G$ contains an explicit sublattice $\SAT$ with $mK\subseteq\SAT$ and $[K:\SAT]=m^{12}$ (the number $12$ is a count of relations modulo $m$, Lemma~\ref{lem:C}); and $A=\Z^{3m^2}$ contains an explicit sublattice $F$, the orthogonal direct sum of $N_0$ and $3(m-2)$ blocks, whose image in $V$ has index $m^{3(m^2+m+2)/2-12}$. Theorem~\ref{thm:B} is proved in \S\ref{sec:proofB}: the order is Theorem~\ref{thm:A}, the exponent divides $m^2$ by an explicit integer identity $GYG=6m^2G$, and the rank of $G$ modulo $m$ is $12(m-3)$ (and $26$ at $m=5$). \paragraph{Lean.} The lattice statements of Theorems~\ref{thm:A} and~\ref{thm:B}, for the matrix $G$ of \S\ref{sec:config}, are checked in Lean~4 with Mathlib (\S\ref{sec:lean}). The geometric identification of \S\ref{sec:geometry}, the equality $V=\NS(S_m)$ \cite{SSvL,Deg} and Corollary~\ref{cor:T} are not formalized. \paragraph{Earlier versions.} Both theorems were first stated and proved in June 2026 by a different route, through the characters of $(\Z/m)^3$, trace lattices and a large determinant \cite{WM,DL}. Four steps of the June proof of Theorem~\ref{thm:B} were confirmed by computation at three or four primes and not written for general $m$; the proof printed here does not use them. The proof printed here is the integral route, without characters, along which the theorems were formalized in Lean; every step is written for general $m$. \paragraph{Notation.} Throughout, $m\ge5$ is prime, $\F_m=\Z/m$, and $P=\F_m^2$; its elements are written $(k,l)$. For a function $u:\F_m\to\Z$ write $\Sigma u=\sum_{x\in\F_m}u(x)$; $Z_0$ is the group of $u$ with $\Sigma u=0$, free of rank $m-1$. For a commutative ring $R$ and $u:\F_m\to R$ put $u^{\pm}(x)=u(x\pm1)$; for $c\in\F_m$, $\delta_c:\F_m\to\Z$ is the indicator of $c$. \section{The configuration and the lattice}\label{sec:config} The set of \emph{lines} is $I=\{0,1,2\}\times P$, so $|I|=3m^2$; the first coordinate is the \emph{family}. Let $A=\Z^I$ and define the symmetric matrix $G\in\Z^{I\times I}$ by the following entries, for lines $p=(j,k,l)$ and $q=(j',k',l')$: \begin{itemize} \item same family ($j=j'$): $G_{pp}=2-m$; for $(k,l)\neq(k',l')$, $G_{pq}=1$ if $k=k'$ or $l=l'$, and $0$ otherwise; \item families $0$ and $1$ ($j=0$, $j'=1$): $G_{pq}=1$ if $k-l=k'-l'$, else $0$; \item families $1$ and $2$ ($j=1$, $j'=2$): $G_{pq}=1$ if $k+l=k'+l'$, else $0$; \item families $0$ and $2$ ($j=0$, $j'=2$): $G_{pq}=1$ if $k'-l'=k+l+1$, else $0$; \item the remaining entries by symmetry, $G_{qp}=G_{pq}$. \end{itemize} All equalities are in $\F_m$. Let $K=\ker G\subseteq A$ and $V=A/K$, with the form induced by $B(x,y)=x^{\mathsf T}Gy$; it is well defined because $G$ is symmetric. The group $V$ is torsion free (if $cx\in K$ with $c\neq0$ then $x\in K$), hence free. For $j\in\{0,1,2\}$ let $N_j\in A$ be the indicator of family $j$, and $\one=N_0+N_1+N_2$. For $x\in A$ write $x_j:P\to\Z$ for its restriction to family $j$ and $\aug(x_j)=\sum_{p\in P}x_j(p)$. \paragraph{Rows of $G$.} The row of $G$ at $p=(j,k,l)$ has $2-m$ at $p$, $1$ at the $2(m-1)$ lines of family $j$ that share $k$ or $l$ with $p$, and, in each other family $j'$, the value $1$ exactly on an \emph{incidence set} $S_{j'}(p)\subset P$: \[ \begin{array}{lll} \text{family of }p & & \\ 0: & S_1(p)=\{k'-l'=k-l\}, & S_2(p)=\{k'-l'=k+l+1\},\\ 1: & S_0(p)=\{k'-l'=k-l\}, & S_2(p)=\{k'+l'=k+l\},\\ 2: & S_0(p)=\{k'+l'=k-l-1\}, & S_1(p)=\{k'+l'=k+l\}. \end{array} \] Each incidence set is a ``$-$ set'' $\{k'-l'=c\}$ or a ``$+$ set'' $\{k'+l'=c\}$; it has $m$ points. \begin{lemma}\label{lem:N} $GN_j=m\one$ for every $j$, and $G\one=3m\one$. \end{lemma} \begin{proof} At a line of family $j$ the row sum over family $j$ is $(2-m)+2(m-1)=m$. At a line of another family the row meets family $j$ in an incidence set, of $m$ points. \end{proof} \section{The geometry}\label{sec:geometry} This section identifies $G$ with the intersection matrix of the lines on $S_m$ and $V$ with $\NS(S_m)$. It is not used in \S\S\ref{sec:pencils}--\ref{sec:proofB}. Put $\varepsilon=e^{\pi i/m}$ and $\zeta=\varepsilon^2=e^{2\pi i/m}$, so that $\varepsilon^m=-1$. For $(a,b)\in\F_m^2$ the following lines lie on $S_m$: \[ \begin{array}{lll} \text{family }0: & x_0=\varepsilon\zeta^a x_1, & x_2=\varepsilon\zeta^b x_3;\\ \text{family }1: & x_0=\varepsilon\zeta^a x_2, & x_1=\varepsilon\zeta^b x_3;\\ \text{family }2: & x_0=\varepsilon\zeta^a x_3, & x_1=\varepsilon\zeta^b x_2. \end{array} \] For instance on a line of family $0$, $x_0^m+x_1^m=(\varepsilon^m+1)x_1^m=0$ and likewise $x_2^m+x_3^m=0$. These are the $3m^2$ lines of $S_m$ \cite{SSvL}; the line of family $j$ with parameters $(a,b)$ is the line $(j,a,b)\in I$. \begin{proposition}\label{prop:geom} The intersection number of the lines $(j,a,b)$ and $(j',c,d)$ on $S_m$ is the entry of $G$. \end{proposition} \begin{proof} By adjunction a line $L$ on $S_m$ has $L^2=-2-K_{S_m}\cdot L=-2-(m-4)=2-m$. Two distinct lines on a smooth surface meet in at most one point, transversally, so their intersection number is $1$ if they meet and $0$ otherwise; they meet if and only if their four linear equations have a common non-zero solution. Two lines of one family meet if and only if they share $a$ or $b$: for instance the lines of family $0$ with the same $a$ and different $b$ meet at $(\varepsilon\zeta^a:1:0:0)$, and if $a\ne a'$ and $b\ne b'$ the equations force $x=0$. For families $0$ and $1$, with parameters $(a,b)$ and $(c,d)$, a common point has $x_3\neq0$ (otherwise all coordinates vanish) and $x_0=\varepsilon\zeta^a x_1=\varepsilon^2\zeta^{a+d}x_3$, $x_0=\varepsilon\zeta^c x_2=\varepsilon^2\zeta^{c+b}x_3$; so the lines meet if and only if $a-b=c-d$. In the same way families $1$ and $2$, with $(c,d)$ and $(e,f)$, meet if and only if $c+d=e+f$. For families $0$ and $2$, with $(a,b)$ and $(e,f)$, again $x_3\neq0$ and $x_0=\varepsilon\zeta^a x_1=\varepsilon^2\zeta^{a+f}x_2=\varepsilon^3\zeta^{a+f+b}x_3$ and $x_0=\varepsilon\zeta^e x_3$, so the lines meet if and only if $\varepsilon^2\zeta^{a+b+f}=\zeta^e$, that is, $e-f=a+b+1$. These are the entries of $G$; the $+1$ of the last case is $\varepsilon^2=\zeta$. \end{proof} \begin{corollary}\label{cor:VNS} The lattice spanned by the classes of the lines in $H^2(S_m,\Z)$, with the intersection form, is isometric to $V$. For prime $m\ge5$ it is $\NS(S_m)$. \end{corollary} \begin{proof} The classes of the lines span $\NS(S_m)\otimes\Q$ for $\gcd(m,6)=1$ \cite{Sh82} (see \cite[\S3]{SSvL}), $H^2(S_m,\Z)$ is torsion free, as $S_m$ is simply connected, and the intersection form on $\NS(S_m)$ is non-degenerate (Hodge index theorem). So a combination $x\in A$ of lines has class $0$ if and only if it pairs to zero with every line, that is, $Gx=0$, by Proposition~\ref{prop:geom}. Hence the lattice of the lines is $A/\ker G=V$ with the form of $G$. For $\gcd(m,6)=1$ the lines generate $\NS(S_m)$ \cite{SSvL,Deg}. \end{proof} The proof of Proposition~\ref{prop:geom} was also checked by computer: for $m=5,7,11$ the lines were built numerically and every pair of distinct lines was tested for a common point (rank of a $4\times4$ complex matrix); all $2\,775$, $10\,731$ and $65\,703$ such pairs agree with $G$ (the diagonal entries $2-m$ come from adjunction), and the same test with $k+l-1$ in place of $k+l+1$ in the last case disagrees on $250$, $686$ and $2\,662$ pairs. \section{Pencils and pullbacks}\label{sec:pencils} For $t\in\F_m$ let $\pi_t(k,l)=k+tl$, and let $\pi_\infty(k,l)=l$. These are the $m+1$ \emph{pencils}: the linear forms on $P$ up to scalars. We call $\pi_0=k$ and $\pi_\infty=l$ the \emph{axis} pencils, $\pi_{1}=k+l$ and $\pi_{-1}=k-l$ the \emph{overlap} pencils, and the $m-3$ others the \emph{live} pencils. For a family $j$, a pencil $\pi$ and $u:\F_m\to\Z$, the \emph{pullback} $\pb_j^\pi(u)\in A$ is $u\circ\pi$ on family $j$ and $0$ elsewhere. For $y:P\to\Z$ the \emph{fibre sums} are $\fib_\pi(y)(v)=\sum_{\pi(p)=v}y(p)$. (The names R.1, R.2 and C given below to three lemmas are those of the Lean project, \S\ref{sec:lean}.) \begin{lemma}\label{lem:indep} Let $\pi\neq\pi'$ be pencils and $u,v:\F_m\to\Z$. Then $\sum_{p\in P}u(\pi(p))v(\pi'(p))=(\Sigma u)(\Sigma v)$ and $\sum_{p\in P}u(\pi(p))v(\pi(p))=m\sum_x u(x)v(x)$. In particular every fibre of $\pi$ meets every fibre of $\pi'$ in exactly one point. \end{lemma} \begin{proof} Two non-proportional linear forms on $\F_m^2$ give a bijection $p\mapsto(\pi(p),\pi'(p))$ of $P$ onto $\F_m^2$; every fibre of one pencil has $m$ points. \end{proof} \begin{lemma}[Lemma R.1]\label{lem:R1} For every $y:P\to\Z$ and every family $j$, \[ m\cdot y\big|_{\text{family }j} \;=\;\sum_{\pi}\pb_j^\pi\big(\fib_\pi(y)\big)-\Big(\sum_{p}y(p)\Big)N_j , \] the sum running over the $m+1$ pencils (here $y|_{\text{family }j}\in A$ is $y$ on family $j$ and $0$ elsewhere). \end{lemma} \begin{proof} At $(j,p)$ the right side is $\sum_\pi\sum_{\pi(q)=\pi(p)}y(q)-\sum_q y(q)$. A point $q\neq p$ lies on the same fibre as $p$ for exactly one pencil, the one containing the direction $q-p$; the point $p$ does so for all $m+1$. So the double sum is $(m+1)y(p)+\sum_{q\ne p}y(q)$. \end{proof} \begin{lemma}[$G$ on pullbacks]\label{lem:G} Let $u\in Z_0$. \begin{enumerate}[label=(\alph*)] \item Axis pencils: $G\,\pb_j^{\pi_0}(u)=G\,\pb_j^{\pi_\infty}(u)=0$ for every $j$. \item Live pencils: $G\,\pb_j^{\pi_t}(u)=-m\,\pb_j^{\pi_t}(u)$ for $t\notin\{0,1,-1\}$ and every $j$. \item Overlap pencils: \begin{align*} G\,\pb_0^{\pi_{-1}}(u)&=-m\,\pb_0^{\pi_{-1}}(u)+m\,\pb_1^{\pi_{-1}}(u), & G\,\pb_1^{\pi_{-1}}(u)&=-m\,\pb_1^{\pi_{-1}}(u)+m\,\pb_0^{\pi_{-1}}(u),\\ G\,\pb_1^{\pi_{1}}(u)&=-m\,\pb_1^{\pi_{1}}(u)+m\,\pb_2^{\pi_{1}}(u), & G\,\pb_2^{\pi_{1}}(u)&=-m\,\pb_2^{\pi_{1}}(u)+m\,\pb_1^{\pi_{1}}(u),\\ G\,\pb_0^{\pi_{1}}(u)&=-m\,\pb_0^{\pi_{1}}(u)+m\,\pb_2^{\pi_{-1}}(u^-), & G\,\pb_2^{\pi_{-1}}(u)&=-m\,\pb_2^{\pi_{-1}}(u)+m\,\pb_0^{\pi_{1}}(u^+). \end{align*} \end{enumerate} \end{lemma} \begin{proof} Let $v=\pb_j^\pi(u)$ and look at $(Gv)(q)$. \emph{Lines $q=(j,k,l)$ of family $j$.} If $\pi$ is an axis pencil, say $\pi=\pi_0$, the entry is $(2-m)u(k)+(m-1)u(k)+\sum_{k'\neq k}u(k')=\Sigma u=0$; likewise for $\pi_\infty$. If $\pi=\pi_t$ with $t\neq0$, the row $\{k'=k\}$ and the column $\{l'=l\}$ each meet every fibre of $\pi$ once, so with $x=\pi(k,l)$ the entry is $(2-m)u(x)+2(\Sigma u-u(x))=-mu(x)$. \emph{Lines $q$ of another family.} The entry is the sum of $u\circ\pi$ over an incidence set $S$. On a $-$ set $\{k'-l'=c\}$, $\pi_t$ takes the values $(1+t)l'+c$, a bijection onto $\F_m$ unless $t=-1$; on a $+$ set $\{k'+l'=c\}$, $\pi_t$ takes the values $(1-t)k'+tc$, a bijection unless $t=1$; $\pi_0=k'$ and $\pi_\infty=l'$ are bijections on both kinds. A bijection gives $\Sigma u=0$. In the two remaining cases ($\pi_{-1}$ on a $-$ set, $\pi_1$ on a $+$ set) $\pi$ is constant on $S$ and the entry is $m\,u(\text{value})$. Reading the value off the table of incidence sets gives the six formulas; for example, for $v=\pb_0^{\pi_1}(u)$ and $q=(2,k,l)$ the set is $S_0(q)=\{k'+l'=k-l-1\}$, so the entry is $m\,u(k-l-1)=m\,u^-(k-l)$; for $v=\pb_2^{\pi_{-1}}(u)$ and $q=(0,k,l)$ it is $S_2(q)=\{k'-l'=k+l+1\}$, giving $m\,u^+(k+l)$. \end{proof} The three \emph{overlap pairs} are $(\pb_0^{\pi_{-1}},\pb_1^{\pi_{-1}})$, $(\pb_1^{\pi_1},\pb_2^{\pi_1})$ and $(\pb_0^{\pi_1},\pb_2^{\pi_{-1}})$, the last one with a shift by one. \section{The sublattice SAT of the kernel}\label{sec:SAT} \begin{definition} Let $R$ be a commutative ring. A \emph{datum} over $R$ consists of functions $a_j,b_j:\F_m\to R$ ($j=0,1,2$), $w_0,w_1,w_2:\F_m\to R$, and scalars $\varepsilon_1,\varepsilon_2\in R$. It is \emph{admissible} if each of the nine functions $a_j,b_j,w_i$ has sum zero; the admissible data form a free $R$-module $\mathrm{Src}_R$ of rank $9(m-1)+2=9m-7$. The map $s_R:\mathrm{Src}_R\to R^I$ sends a datum to the vector with values \[ \begin{array}{ll} (0,k,l)\mapsto a_0(k)+b_0(l)+w_0(k-l)+w_2(k+l)+\varepsilon_1,\\ (1,k,l)\mapsto a_1(k)+b_1(l)+w_0(k-l)+w_1(k+l)+\varepsilon_2-\varepsilon_1,\\ (2,k,l)\mapsto a_2(k)+b_2(l)+w_1(k+l)+w_2(k-l-1)-\varepsilon_2 . \end{array} \] Put $\SAT=s_\Z(\mathrm{Src}_\Z)\subseteq A$. \end{definition} In terms of pullbacks, $s_\Z$ of a datum is \begin{multline*} \sum_j\big(\pb_j^{\pi_0}(a_j)+\pb_j^{\pi_\infty}(b_j)\big)+\big(\pb_0^{\pi_{-1}}+\pb_1^{\pi_{-1}}\big)(w_0)+\big(\pb_1^{\pi_1}+\pb_2^{\pi_1}\big)(w_1)\\ +\pb_0^{\pi_1}(w_2)+\pb_2^{\pi_{-1}}(w_2^-)+\varepsilon_1(N_0-N_1)+\varepsilon_2(N_1-N_2). \end{multline*} \begin{lemma}\label{lem:SATK} $\SAT\subseteq K$. \end{lemma} \begin{proof} By Lemma~\ref{lem:G}(a), $G$ kills the axis pullbacks. For the first overlap pair, Lemma~\ref{lem:G}(c) gives \[G\big(\pb_0^{\pi_{-1}}+\pb_1^{\pi_{-1}}\big)(w_0)=(-m+m)\,\pb_0^{\pi_{-1}}(w_0)+(m-m)\,\pb_1^{\pi_{-1}}(w_0)=0,\] and likewise for the second. For the third, $G\pb_0^{\pi_1}(w_2)=-m\pb_0^{\pi_1}(w_2)+m\pb_2^{\pi_{-1}}(w_2^-)$ and $G\pb_2^{\pi_{-1}}(w_2^-)=-m\pb_2^{\pi_{-1}}(w_2^-)+m\pb_0^{\pi_1}(w_2)$, since $(w_2^-)^+=w_2$; the sum is $0$. Finally $G(N_0-N_1)=G(N_1-N_2)=0$ by Lemma~\ref{lem:N}. \end{proof} \begin{lemma}[Lemma C: the count of relations]\label{lem:C} The kernel of $s_{\F_m}:\mathrm{Src}_{\F_m}\to\F_m^I$ has dimension $12$; hence its image has dimension $9m-19$. \end{lemma} \begin{proof} Let $\Theta$ be an admissible datum over $\F_m$ with $s_{\F_m}(\Theta)=0$, so that the three displayed functions of $(k,l)$ vanish identically. For $\Phi:P\to\F_m$ put $(\square\Phi)(k,l)=\Phi(k+1,l+1)-\Phi(k+1,l)-\Phi(k,l+1)+\Phi(k,l)$, and for $w:\F_m\to\F_m$ put $(\Delta^2w)(z)=w(z+2)-2w(z+1)+w(z)$. The operator $\square$ kills functions of $k$ alone, of $l$ alone, and constants, and a direct computation gives $\square[w(k-l)]=-(\Delta^2w)(k-l-1)$ and $\square[w(k+l)]=(\Delta^2w)(k+l)$. Applying $\square$ to the three identities gives, for all $k,l$: \begin{gather*} (\Delta^2w_2)(k+l)=(\Delta^2w_0)(k-l-1),\qquad (\Delta^2w_1)(k+l)=(\Delta^2w_0)(k-l-1),\\ (\Delta^2w_1)(k+l)=(\Delta^2w_2)(k-l-2). \end{gather*} Since $m$ is odd, $(k,l)\mapsto(k+l,k-l)$ is a bijection of $P$, so each of these says that both sides are one and the same constant. Hence $\Delta^2w_0=\Delta^2w_1=\Delta^2w_2=2c$ for one $c\in\F_m$. As $\Delta^2(x^2)=2$, the function $w_i-cx^2$ has zero second difference, so its first difference is a constant $\alpha_i$ and $w_i(x)=cx^2+\alpha_ix+\beta_i$ for all $x\in\F_m$. With these $w_i$ the cross terms cancel, $(k-l)^2+(k+l)^2=2k^2+2l^2$ and $(k+l)^2+(k-l-1)^2=2k^2+2l^2-2k+2l+1$, so each identity reads $a_j(k)+b_j(l)=p_j(k)+q_j(l)$ with explicit quadratic polynomials $p_j,q_j$. Its solutions are exactly $a_j=p_j+t_j$, $b_j=q_j-t_j$ with $t_j\in\F_m$ (put $l=0$, then $k=0$). Conversely every such choice is admissible: a quadratic function on $\F_m$ has sum zero, because $\sum_x1=m$, $\sum_xx=m(m-1)/2$ and $\sum_xx^2=(m-1)m(2m-1)/6$ vanish in $\F_m$ ($\gcd(m,6)=1$). So the kernel is the image of the injective linear map from $\F_m^{12}$ sending $(c,\alpha_0,\alpha_1,\alpha_2,\beta_0,\beta_1,\beta_2,\varepsilon_1,\varepsilon_2,t_0,t_1,t_2)$ to the datum just described. Injectivity: $c,\alpha_i,\beta_i$ are read off the $w_i$, $t_j$ off $a_j(0)$, and $\varepsilon_1,\varepsilon_2$ are coordinates of the datum. \end{proof} \begin{remark} At $m=3$ the count drops to $11$ because $\sum_{x\in\F_3}x^2\neq0$; this is one of the places where $m\ge5$ is used. \end{remark} \begin{lemma}\label{lem:lift} Reduction modulo $m$ maps $\mathrm{Src}_\Z$ onto $\mathrm{Src}_{\F_m}$, and $s_{\F_m}(\Theta\bmod m)=s_\Z(\Theta)\bmod m$ for $\Theta\in\mathrm{Src}_\Z$. \end{lemma} \begin{proof} The second statement holds because reduction is a ring map. For the first, lift a sum-zero $f:\F_m\to\F_m$ to any $y:\F_m\to\Z$; $m$ divides $\Sigma y$, and $y-(\Sigma y)\,\delta_0$ is a sum-zero lift of $f$ (it changes $y$ only at $0$, by a multiple of $m$). The scalars $\varepsilon_1,\varepsilon_2$ lift trivially. \end{proof} \section{The kernel}\label{sec:K} \begin{lemma}[Lemma R.2]\label{lem:R2} For $x\in K$: $\aug(x_0)+\aug(x_1)+\aug(x_2)=0$, and $m$ divides each $\aug(x_j)$. \end{lemma} \begin{proof} By Lemma~\ref{lem:N}, $0=N_0^{\mathsf T}Gx=(GN_0)^{\mathsf T}x=m\sum_px(p)$, which is the first statement. For the second, let $y$ be the indicator of the fibre $\{\pi_t=c\}$ of family $0$, so that $my=\pb_0^{\pi_t}(m\delta_c-1)+N_0$ with $m\delta_c-1\in Z_0$. By Lemmas~\ref{lem:G} and~\ref{lem:N}: \begin{align*} Gy&=2N_0+N_1+N_2-my && (t\notin\{0,\pm1\}),\\ Gy&=2N_0+N_1+mz-my && (t=1),\\ Gy&=2N_0+N_2+mz'-my && (t=-1), \end{align*} with $z,z'\in A$ fibre indicators. Pairing with $x\in K$ gives $0=y^{\mathsf T}Gx$, hence, with $s_j=\aug(x_j)$: $2s_0+s_1+s_2\equiv0$, $2s_0+s_1\equiv0$ and $2s_0+s_2\equiv0\pmod m$. A live pencil exists because $m\ge5$. Subtracting, $s_1\equiv s_2\equiv0$ and $2s_0\equiv0$, so $s_0\equiv0$ as $m$ is odd. \end{proof} \begin{lemma}[the census of the kernel]\label{lem:census} Let $x\in K$ and write $f_{j,\pi}=\fib_\pi(x_j)$. Then $f_{j,\pi_t}$ is constant for every $j$ and every live $t$, and the functions $f_{0,\pi_{-1}}-f_{1,\pi_{-1}}$, $f_{1,\pi_1}-f_{2,\pi_1}$ and $v\mapsto f_{0,\pi_1}(v)-f_{2,\pi_{-1}}(v+1)$ are constant. \end{lemma} \begin{proof} For every $w\in A$, $x^{\mathsf T}Gw=(Gx)^{\mathsf T}w=0$, and $x^{\mathsf T}\pb_j^\pi(u)=\sum_vu(v)f_{j,\pi}(v)$. A function $f:\F_m\to\Z$ with $\sum_vu(v)f(v)=0$ for every $u\in Z_0$ is constant (take $u=\delta_a-\delta_b$). Apply this with $w=\pb_j^{\pi_t}(u)$ for live $t$, and with $w=\pb_0^{\pi_{-1}}(u)$, $\pb_1^{\pi_1}(u)$, $\pb_0^{\pi_1}(u)$, using Lemma~\ref{lem:G}; in the last case $\sum_zu(z-1)f_{2,\pi_{-1}}(z)=\sum_vu(v)f_{2,\pi_{-1}}(v+1)$. \end{proof} \begin{proposition}\label{prop:mK} $mK\subseteq\SAT$. \end{proposition} \begin{proof} Let $x\in K$, put $\mu_j=\aug(x_j)/m\in\Z$ (Lemma~\ref{lem:R2}, which also gives $\mu_0+\mu_1+\mu_2=0$), and $\tilde f_{j,\pi}=f_{j,\pi}-\mu_j$; since $\Sigma f_{j,\pi}=\aug(x_j)$, each $\tilde f_{j,\pi}$ has sum zero. By Lemma~\ref{lem:R1}, \[ m\cdot x_j\big|_{\text{family }j}=\sum_\pi\pb_j^\pi(\tilde f_{j,\pi})+(m+1)\mu_jN_j-m\mu_jN_j=\sum_\pi\pb_j^\pi(\tilde f_{j,\pi})+\mu_jN_j . \] By Lemma~\ref{lem:census}, $\tilde f_{j,\pi_t}$ is constant with sum zero, hence $0$, for every live $t$; and the three overlap differences, constant with sum zero, vanish: $\tilde f_{0,\pi_{-1}}=\tilde f_{1,\pi_{-1}}$, $\tilde f_{1,\pi_1}=\tilde f_{2,\pi_1}$, $\tilde f_{2,\pi_{-1}}=\tilde f_{0,\pi_1}^-$. Hence $mx=s_\Z(\Theta)$ for the admissible datum $\Theta$: $a_j=\tilde f_{j,\pi_0}$, $b_j=\tilde f_{j,\pi_\infty}$, $w_0=\tilde f_{0,\pi_{-1}}$, $w_1=\tilde f_{1,\pi_1}$, $w_2=\tilde f_{0,\pi_1}$, $\varepsilon_1=\mu_0$, $\varepsilon_2=-\mu_2$ (note $\varepsilon_2-\varepsilon_1=\mu_1$). \end{proof} \section{The sublattice $F$ and two indices}\label{sec:F} Let $F\subseteq A$ be spanned by $N_0$ and by the $3(m-2)$ \emph{blocks} $\pb_j^{\pi_t}(Z_0)$ for $j\in\{0,1,2\}$ and $t$ live, together with $\pb_0^{\pi_{-1}}(Z_0)$, $\pb_1^{\pi_1}(Z_0)$ and $\pb_0^{\pi_1}(Z_0)$ (one member of each overlap pair). \begin{lemma}\label{lem:Fgram} Distinct blocks are $B$-orthogonal, and $N_0$ is $B$-orthogonal to every block. Inside a block, $B(\pb u,\pb v)=-m^2\sum_xu(x)v(x)$; and $B(N_0,N_0)=m^3$. \end{lemma} \begin{proof} By Lemma~\ref{lem:G}, $G$ applied to a block vector is $-m$ times it, plus, for the three overlap members, $m$ times a pullback along an overlap pencil of another family: of family $1$ along $\pi_{-1}$, of family $2$ along $\pi_1$, and of family $2$ along $\pi_{-1}$. None of these three is a block of $F$, so that term pairs with a block of $F$ either through disjoint supports or through two different pencils of one family, which gives $(\Sigma u)(\Sigma v)=0$ by Lemma~\ref{lem:indep}. Two blocks of one family and different pencils are orthogonal for the same reason, and blocks of different families have disjoint supports. Inside a block, Lemma~\ref{lem:indep} gives $-m\cdot m\sum_xu(x)v(x)$. Finally $B(N_0,w)=(GN_0)^{\mathsf T}w=m\sum_pw(p)$, which is $0$ on pullbacks of sum-zero functions, and $m\cdot m^2$ for $w=N_0$. \end{proof} \begin{corollary}\label{cor:FK} $F\cap K=0$, and $F$ is free of rank $3(m-2)(m-1)+1$. \end{corollary} \begin{proof} Write $x\in F$ as $cN_0+\sum_\beta\pb(u_\beta)$, one term per block. If $x\in K$ then $0=B(x,\pb(u_\beta))=-m^2\sum u_\beta^2$, so every $u_\beta=0$, and $0=B(x,N_0)=cm^3$. The same argument shows that the blocks and $N_0$ are independent; each block is isomorphic to $Z_0$ because $\pi$ is surjective. \end{proof} Let $L_{\mathrm{fam}}\subseteq\Z^P$ be spanned by the constant $1$ and all $u\circ\pi$, $u\in Z_0$, $\pi$ a pencil; and let $L\subseteq A$ consist of the $x$ with $x_j\in L_{\mathrm{fam}}$ for every $j$. \begin{lemma}\label{lem:Lfam} $[\Z^P:L_{\mathrm{fam}}]=m^{(m^2+m+2)/2}$, hence $[A:L]=m^{3(m^2+m+2)/2}$. \end{lemma} \begin{proof} The $(m+1)(m-1)+1=m^2$ vectors $(\delta_x-\delta_0)\circ\pi$ ($x\neq0$, $\pi$ a pencil) and $1$ span $L_{\mathrm{fam}}$. By Lemma~\ref{lem:indep} their Gram matrix for the standard inner product is block diagonal: inside one pencil it is $m(I+J)$ of size $m-1$, with determinant $m^{m-1}\cdot m$; and $\langle1,1\rangle=m^2$. The Gram determinant is $(m^m)^{m+1}m^2=m^{m^2+m+2}\neq0$; so the vectors form a basis, and the index of the lattice they span is the square root of the Gram determinant ($m^2+m$ is even). \end{proof} \begin{lemma}\label{lem:FSAT} $F+\SAT=L$, and $F\cap\SAT=0$. \end{lemma} \begin{proof} Both $F$ and $\SAT$ lie in $L$. Conversely $L$ is spanned by the vectors $\pb_j^\pi(u)$, $u\in Z_0$, and $N_0,N_1,N_2$. Live blocks lie in $F$; axis pullbacks lie in $\SAT$; for an overlap pair, one member lies in $F$ and the sum of the pair lies in $\SAT$ (with a datum having one non-zero $w_i$; for the third pair, the vector $\pb_2^{\pi_{-1}}(v)$ is reached with $w_2=v^+$). Finally $N_0\in F$, and $N_0-N_1$, $N_1-N_2\in\SAT$. The intersection is $0$ because $F\cap K=0$ and $\SAT\subseteq K$. \end{proof} \begin{proposition}\label{prop:ranks} $\SAT$ and $K$ are free of rank $9m-7$, and $[K:\SAT]=m^{12}$. \end{proposition} \begin{proof} By Lemmas~\ref{lem:Lfam} and~\ref{lem:FSAT}, $F\oplus\SAT$ has finite index in $A$, so $\operatorname{rank}\SAT=3m^2-\operatorname{rank}F=9m-7$. Since $\SAT\subseteq K$ and $F\cap K=0$, also $9m-7\le\operatorname{rank}K\le3m^2-\operatorname{rank}F=9m-7$. By Proposition~\ref{prop:mK}, $K/\SAT$ is killed by $m$, so $[K:\SAT]=|K/mK|/|\SAT/mK|=m^{9m-7}/|\SAT/mK|$. Since $K=\ker G$, $K\cap mA=mK$, so $K/mK$ embeds in $A/mA=\F_m^I$; it maps $\SAT/mK$ onto the reduction of $\SAT$ modulo $m$, which by Lemma~\ref{lem:lift} is the image of $s_{\F_m}$, of dimension $9m-19$ (Lemma~\ref{lem:C}). Hence $[K:\SAT]=m^{(9m-7)-(9m-19)}=m^{12}$. \end{proof} \begin{corollary}\label{cor:index} $[A:F+K]=m^{3(m^2+m+2)/2-12}$. \end{corollary} \begin{proof} $L=F+\SAT\subseteq F+K\subseteq A$. The map $K\to(F+K)/(F+\SAT)$ is onto with kernel $K\cap(F+\SAT)=\SAT$: if $k=f+s$ then $f=k-s\in F\cap K=0$. So $[F+K:L]=[K:\SAT]=m^{12}$, and $[A:F+K]=[A:L]/m^{12}$. \end{proof} \section{Proof of the Watermark Theorem}\label{sec:proofA} $V=A/K$ is free of rank $3m^2-(9m-7)=3(m-1)(m-2)+1$ (\S\ref{sec:config} and Proposition~\ref{prop:ranks}). The quotient map $\varphi:A\to V$ is injective on $F$ (Corollary~\ref{cor:FK}) and $V/\varphi(F)\cong A/(F+K)$, so $\varphi(F)$ is a sublattice of full rank and index $N=m^{3(m^2+m+2)/2-12}$ (Corollary~\ref{cor:index}). Let $c$ be the basis of $\varphi(F)$ formed by $\varphi(N_0)$ and, for each block, the images of $\pb(\delta_x-\delta_0)$, $x\neq0$. By Lemma~\ref{lem:Fgram} its Gram matrix is block diagonal, with $3(m-2)$ blocks $-m^2(I+J)$ of size $m-1$ and the block $(m^3)$; since $m-1$ is even, \[ \det\mathrm{Gram}_c=\big(m^{2(m-1)}\cdot m\big)^{3(m-2)}\cdot m^3=m^{3(m-2)(2m-1)+3}. \] For any basis $b$ of $V$, $\mathrm{Gram}_c=M^{\mathsf T}\mathrm{Gram}_bM$ with $|\det M|=N$, so \[ \det\mathrm{Gram}_b=m^{3(m-2)(2m-1)+3-3(m^2+m+2)+24}=m^{3m^2-18m+27}=m^{3(m-3)^2}. \] With Corollary~\ref{cor:VNS} this proves Theorem~\ref{thm:A}. \qed \section{Proof of the Double Ladder Theorem}\label{sec:proofB} By Theorem~\ref{thm:A}, $D=V^\ast/V$ is a finite group of order $m^{3(m-3)^2}$. Its structure is fixed by two more facts: its exponent divides $m^2$ (\S\ref{sec:exp}), and the rank of $G$ modulo $m$ (\S\ref{sec:rank}). \subsection{The exponent}\label{sec:exp} For a pencil $\pi$ let $P_\pi\in\Z^{I\times I}$ be the block-diagonal matrix with $(P_\pi)_{pq}=1$ if $p,q$ lie in one family and $\pi(p)=\pi(q)$, and $0$ otherwise. Put \[ Y=P_{\pi_0}+P_{\pi_\infty}+3P_{\pi_{-1}}+3P_{\pi_1}-6m\,I . \] \begin{lemma}\label{lem:GYG} $GYG=6m^2G$. \end{lemma} \begin{proof} By Lemma~\ref{lem:R1} (applied to the indicator of one point), $\Q^I$ is spanned by the pullbacks $\pb_j^\pi(u)$, $u\in Z_0$, and the vectors $N_j$; we check the identity on these. By Lemma~\ref{lem:indep}, $P_\pi\pb_j^{\pi'}(u)$ is $m\,\pb_j^\pi(u)$ if $\pi'=\pi$ and $0$ otherwise, and $P_\pi N_j=mN_j$. So $Y$ acts by $-5m$ on axis pullbacks, by $-3m$ on overlap pullbacks, by $-6m$ on live pullbacks, and by $2m$ on the $N_j$. Now use Lemma~\ref{lem:G}. Axis: both sides vanish. Live: $(-m)(-6m)(-m)=-6m^3=6m^2\cdot(-m)$. Each overlap pair spans a $G$-stable plane on which $G=mE$, $E=\begin{pmatrix}-1&1\\1&-1\end{pmatrix}$ (for the third pair use the vectors $\pb_0^{\pi_1}(u)$ and $\pb_2^{\pi_{-1}}(u^-)$), and $Y=-3m$; as $E^2=-2E$, $mE(-3m)mE=6m^3E=6m^2\cdot mE$. On the span of $N_0,N_1,N_2$, $G=mJ_3$ (Lemma~\ref{lem:N}) and $Y=2m$; as $J_3^2=3J_3$, $mJ_3\cdot 2m\cdot mJ_3=6m^3J_3$. \end{proof} The proof shows that $G$ is diagonalizable over $\Q$ with eigenvalues $0,-m,-2m,3m$, so its minimal polynomial is $x(x+m)(x+2m)(x-3m)$; and $Y$ acts as $6m^2/\lambda$ on the $\lambda$-eigenspace for every $\lambda\neq0$; the integer $6$ is the least common denominator of $m^2/\lambda$ over $\lambda\in\{-m,-2m,3m\}$. \begin{corollary}\label{cor:exp} $m^2V^\ast\subseteq V$: the exponent of $D$ divides $m^2$. \end{corollary} \begin{proof} A functional on $V$ is given by a vector $f\in\Z^I$ orthogonal to $K=\ker G$; as $G$ is symmetric, $f=Gy$ with $y\in\Q^I$. By Lemma~\ref{lem:GYG}, $6m^2f=GYGy=G(Yf)$, which is the functional of the class of the integer vector $Yf$. So $6m^2V^\ast\subseteq V$. The order of $D$ is a power of $m$ and $\gcd(6,m)=1$, so $m^2V^\ast\subseteq V$. \end{proof} \subsection{The rank of $G$ modulo $m$}\label{sec:rank} Use the four pencils $\pi_0,\pi_\infty,\pi_{-1},\pi_1$ (that is, $k$, $l$, $k-l$, $k+l$). For each family $j$ and each of them let $\mathrm{push}_{j,\pi}:\F_m^P\to\F_m^{\F_m}$ be the fibre sum, and let $S:\F_m^I\to U=(\F_m^{\F_m})^{12}$ collect these twelve \emph{shadows}. Let $\Gamma$ be the symmetric matrix on $U$ that pairs each of the six axis slots $(j,\pi_0),(j,\pi_\infty)$ with itself by the identity, pairs $(0,\pi_{-1})$ with $(1,\pi_{-1})$ and $(1,\pi_1)$ with $(2,\pi_1)$ by the identity, and pairs $(0,\pi_1)$ with $(2,\pi_{-1})$ by the shift (the value $v$ of the first slot with the value $v+1$ of the second). Then $\Gamma^2=I$. \begin{lemma}\label{lem:shadow} $G=S^{\mathsf T}\Gamma S-mI$ over $\Z$ (with $S$ and $\Gamma$ read as integer matrices). Hence $G\equiv S^{\mathsf T}\Gamma S\pmod m$ and $\operatorname{rank}_{\F_m}(G\bmod m)=\dim W-\dim(W\cap W^{\perp_\Gamma})$, where $W=\operatorname{im}S$ and $W^{\perp_\Gamma}=\{w:\langle\Gamma w,W\rangle=0\}$. \end{lemma} \begin{proof} The entry of $S^{\mathsf T}\Gamma S$ at two lines of one family is $[k=k']+[l=l']$ (only the axis slots pair inside a family), which is $2$ on the diagonal; at a line of family $0$ and one of family $1$ it is $[k-l=k'-l']$; at families $1,2$ it is $[k+l=k'+l']$; at families $0,2$ it is $[k'-l'=k+l+1]$. Subtracting $mI$ gives $G$. For the rank: $S^{\mathsf T}\Gamma Sx=0$ if and only if $\Gamma Sx\perp W$, i.e. $Sx\in W\cap W^{\perp_\Gamma}$, so $\dim\ker=\dim\ker S+\dim(W\cap W^{\perp_\Gamma})$. \end{proof} \begin{lemma}\label{lem:W} $\dim W=12m-18$. The annihilator $R$ of $W$ (for the standard pairing) has dimension $18$; family by family it is spanned by the elements placing $c_\pi x^s$ in the slot $(j,\pi)$, with $s\in\{0,1,2\}$ and $\sum_\pi c_\pi\pi^s=0$ as a form on $P$. \end{lemma} \begin{proof} $W=\bigoplus_jW_j$. A tuple $(h_\pi)_\pi$ of functions annihilates $W_j$ if and only if $\sum_\pi h_\pi(\pi(k,l))=0$ as a function on $P$. Write each $h_\pi$ as a polynomial of degree $\le m-1$; the sum is a polynomial of total degree $\le m-1$, which vanishes as a function on $\F_m^2$ if and only if it vanishes as a polynomial, i.e. if and only if $\sum_\pi c_{\pi,s}\pi^s=0$ for each $s$, where $c_{\pi,s}$ is the coefficient of $x^s$ in $h_\pi$. For $3\le s\le m-1$ the four forms $\pi^s$ are linearly independent: writing $\pi=ak+bl$, the coefficient of $k^tl^{s-t}$ in $\pi^s$ is $\binom st a^tb^{s-t}$, the binomial coefficients are units ($sm-2$, that is, the only one for which $\sum_xx^4\ne0$ in $\F_m$ enters the count. The integer $6$ in Lemma~\ref{lem:GYG} is harmless exactly because $\gcd(m,6)=1$, the hypothesis under which the lines generate $\NS(S_m)$. \end{remark} \section{Verification in Lean}\label{sec:lean} The lattice statements of Theorems~\ref{thm:A} and~\ref{thm:B} are proved in Lean~4 \cite{Lean} with the Mathlib library \cite{Mathlib}, toolchain \texttt{leanprover/lean4:v4.28.0}. The Lean definitions of the lines, of $G$ (as the case analysis of \S\ref{sec:config}), of $K=\ker G$, of $V=A/K$ with the induced form, and of $D=V^\ast/V$ (the dual of $V$ modulo the range of the form) are printed verbatim in the two certificates \cite{WMLean,DLLean} and compared there, line by line, with the June papers \cite{WM,DL}, whose definitions are those of \S\ref{sec:config}. The final theorems are: \begin{itemize} \item \texttt{Watermark.watermark\_theorem}: for every prime $m\ge5$,\\ $V$ is free of rank $3(m-1)(m-2)+1$, and for every $\Z$-basis $b$ of $V$ the Gram determinant is $m^{3(m-3)^2}$; \item \texttt{DoubleLadder.\allowbreak double\_ladder\_theorem}: for every prime $m\ge7$,\\ $D\cong(\Z/m)^{3m^2-24m+59}\times(\Z/m^2)^{3m-16}$ as abelian groups; \item \texttt{DoubleLadder.double\_ladder\_five}: $D\cong(\Z/5)^{10}\times\Z/25$ at $m=5$. \end{itemize} They depend only on the axioms \texttt{propext}, \texttt{Classical.choice} and \texttt{Quot.sound}; the project contains no \texttt{sorry}, no \texttt{admit} and no \texttt{native\_decide}. The Lean proof follows \S\S\ref{sec:pencils}--\ref{sec:proofB} with a few differences of detail recorded in the certificates: for instance, the inclusion $\SAT\subseteq K$ is proved there for every $m\ge1$ by a direct computation, the relations of Lemma~\ref{lem:W} are identified by mixed second differences instead of polynomials, and the structure of $D$ is obtained from $|D|$ and $|D/mD|$ instead of a Smith form. The Lean proofs were written by the system Aristotle (Harmonic) \cite{Aristotle} from statements and proofs prepared by the author, then compiled and checked again on the author's machine, including a clean rebuild of the whole project. The project, the certificates and the logs are in the Zenodo record \cite{WMDLZenodo} and the repository \url{https://github.com/tretoef-estrella/watermark-theorem}. Not formalized: the geometry of \S\ref{sec:geometry} (Mathlib has no complex algebraic surfaces and no singular cohomology of them), the equality $V=\NS(S_m)$, which is cited \cite{SSvL,Deg}, and Corollary~\ref{cor:T}, which uses the unimodularity of $H^2(S_m,\Z)$ and \cite{Nik}. \section{What was known before, and what is new}\label{sec:history} We read in the original \cite{Sh87,SSvL,Deg,Sh15,AMV}; a search cannot prove that nothing else exists, it records what we looked at. \begin{itemize} \item Shioda \cite{Sh87}, \S7, pp.~133--134, asks for the determinant only (Questions~7.2 and 7.4, prime $m$). In ``Added in proof'' he notes that the discriminant divides a power of $m$ for every $m$. Theorem~\ref{thm:A} answers (7.10) for prime $m\ge5$, and \cite{Deg} answers (7.11) (the lines span $\NS$). \item Sch\"utt, Shioda and van Luijk \cite[end of \S4]{SSvL}: for every odd $m\le81$ the Gram determinant of their rational basis $\mathcal B$ of lines is $m^{3(m-3)^2}$, by computer, ``with exponent as conjectured''; $\mathcal B$ spans $\NS(S_m)$ when $\gcd(m,6)=1$ and $m\le100$ \cite[Theorem~1.1]{SSvL}. \item Shioda \cite[\S6.5, Conjecture~23]{Sh15} still uses the formula as expected in 2015, for every $m$ prime to $6$; the present paper proves it for prime $m$ only. \item Aljovin, Movasati and Villaflor \cite[Table~1]{AMV}: the elementary divisors for $3\le m\le14$, by machine; for prime $m$ these are the rows quoted in \S1, that is, Theorem~\ref{thm:B} at $m=5,7,11,13$. They give no formula for general $m$. \end{itemize} New here, as far as we could determine: the proof of the formula $m^{3(m-3)^2}$ for every prime $m\ge5$; the structure of the discriminant group for every prime $m\ge5$, with the explanation of the exceptional value at $m=5$; and the verification of both lattice statements in Lean. The determinant of the lattice of linear cycles of Fermat varieties of prime degree in every even dimension is treated, by other methods and modulo cited results, in \cite{WMEven}. \section*{Use of AI} This work was developed with extensive use of AI systems: Claude (Anthropic) for exploration, computation, writing and auditing, and Aristotle (Harmonic) for writing the Lean proofs. The text of this paper was read before release by a separate reader, also an AI system; its report led to corrections in Lemma~\ref{lem:lift} and \S\ref{sec:history} and to changes of presentation, which were applied and checked again, without a second reading. The statements, the choice of what to claim and the responsibility for errors are the author's. The work has not been refereed by a human expert. \begin{thebibliography}{99} \bibitem{AMV} E.~Aljovin, H.~Movasati, R.~Villaflor, \emph{Integral Hodge conjecture for Fermat varieties}, J. Symbolic Comput. \textbf{95} (2019), 177--184. arXiv:1711.02628. \bibitem{AS83} N.~Aoki, T.~Shioda, \emph{Generators of the N\'eron--Severi group of a Fermat surface}, in: Arithmetic and Geometry, Vol.~I, Progr. Math. \textbf{35}, Birkh\"auser, Boston (1983), 1--12. \bibitem{Aristotle} Harmonic, \emph{Aristotle}, \url{https://aristotle.harmonic.fun}. \bibitem{Deg} A.~Degtyarev, \emph{Lines generate the Picard groups of certain Fermat surfaces}, J. Number Theory \textbf{147} (2015), 454--477. arXiv:1305.3073. \bibitem{DL} R.~Amichis Luengo, \emph{The Double Ladder Theorem}, version 4 (30 September 2026), in \cite{WMDLZenodo}. \bibitem{DLLean} R.~Amichis Luengo, \emph{The Double Ladder Theorem --- Lean certificate}, version 2 (30 September 2026), in \cite{WMDLZenodo}. \bibitem{Lean} L.~de~Moura, S.~Ullrich, \emph{The Lean 4 theorem prover and programming language}, in: Automated Deduction --- CADE 28, Lecture Notes in Comput. Sci. \textbf{12699}, Springer (2021), 625--635. \bibitem{Mathlib} The mathlib Community, \emph{The Lean mathematical library}, in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM (2020), 367--381. \bibitem{Nik} V.~V.~Nikulin, \emph{Integral symmetric bilinear forms and some of their applications}, Math. USSR Izv. \textbf{14} (1980), 103--167. \bibitem{SSvL} M.~Sch\"utt, T.~Shioda, R.~van Luijk, \emph{Lines on Fermat surfaces}, J. Number Theory \textbf{130} (2010), no.~9, 1939--1963. arXiv:0812.2377. \bibitem{Sh79} T.~Shioda, \emph{The Hodge conjecture for Fermat varieties}, Math. Ann. \textbf{245} (1979), 175--184. \bibitem{Sh82} T.~Shioda, \emph{On the Picard number of a Fermat surface}, J. Fac. Sci. Univ. Tokyo Sect. IA Math. \textbf{28} (1982), no.~3, 725--734. \bibitem{Sh87} T.~Shioda, \emph{Some observations on Jacobi sums}, in: Galois Representations and Arithmetic Algebraic Geometry, Adv. Stud. Pure Math. \textbf{12}, Kinokuniya / North-Holland (1987), 119--135. \bibitem{Sh15} T.~Shioda, \emph{Mordell--Weil lattice of higher genus fibration on a Fermat surface}, J. Math. Sci. Univ. Tokyo \textbf{22} (2015), 443--468. \bibitem{WM} R.~Amichis Luengo, \emph{The Watermark Theorem}, 4 June 2026, with the version note of 30 September 2026, in \cite{WMDLZenodo}. \bibitem{WMDLZenodo} R.~Amichis Luengo, \emph{The Watermark and Double Ladder Theorems (Verified in Lean)}, Zenodo (2026), doi:10.5281/zenodo.23062530. \bibitem{WMEven} R.~Amichis Luengo, \emph{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. \bibitem{WMLean} R.~Amichis Luengo, \emph{The Watermark Theorem --- Lean certificate}, version 2 (30 September 2026), in \cite{WMDLZenodo}. \end{thebibliography} \end{document}