Lehmer: source and evidence

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Included manuscript sections

• appendix_operator.tex
• appendix_workbook.tex

Read the typeset paper

1 \chapter{Definitions and conventions}\label{app:definitions}
2 
3 The following conventions fix the object under discussion and the translations between its arithmetic, geometric and local descriptions. They are part of the claim. Changing a coefficient shift, the Vandermonde orientation or a Frobenius convention changes the formulas that a computation must verify.
4 
5 \section{The coefficient and its local parameters}
6 The normalized form is
7 \[
8 \Delta(q)=q\prod_{m\ge1}(1-q^m)^{24}
9          =\sum_{n\ge1}\tau(n)q^n,\qquad \tau(1)=1.
10 \]
11 All coefficient indices in this book are positive integers. A stored value at index zero is a programming sentinel unless a displayed formula explicitly introduces the coefficients of $\Delta/q$. For the latter coefficients, $f_m=\tau(m+1)$ and $f_0=1$.
12 
13 At a prime $p$, the default local parameters are $a=\tau(p)$ and $b=p^{11}$. The scalar recurrence has $T_0=1$, $T_1=a$ and $T_r=aT_{r-1}-bT_{r-2}$ for $r\ge2$. Thus $T_r=\tau(p^r)$. A construction that permits an arbitrary integer $a$ states that change explicitly. Such a recurrence need not be the local sequence of $\Delta$.
14 
15 The symbol $T_k(p)$ in the trace-formula chapter denotes a Hecke operator on the weight-$k$ cusp-form space. It is an operator, whereas $T_r$ in a scalar recurrence is an integer or an integer polynomial. The weight $k$ and the exponent $r$ serve different roles.
16 
17 The valuation $v_\ell(x)$ is the exponent of $\ell$ in a nonzero rational number $x$, with $v_\ell(0)=\infty$. The quadratic character used in the radial extraction is
18 \[
19 \chifive(d)=
20 \begin{cases}
21 0&5\mid d,\\
22 1&d\equiv1,4\pmod5,\\
23 -1&d\equiv2,3\pmod5.
24 \end{cases}
25 \]
26 The character value and the tenth power in the scaling formula are both essential.
27 
28 \section{Packets, content and the coefficient shift}
29 Coordinates have indices $0,1,2,3,4$. A shell is
30 \[
31 \Vn=\left\{v\in\Z^5:
32 v_i\equiv i\pmod5,\quad
33 \sum_i v_i=0,\quad
34 \sum_i v_i^2=10n\right\}.
35 \]
36 The standard orientation is
37 \[
38 D(v)=\prod_{0\le i<j\le4}(v_i-v_j),\qquad W(v)=D(v)/288.
39 \]
40 The identity is $\tau(n)=\sum_{v\in\Vn}W(v)$. No absolute values occur in that sum. Distinct residue classes ensure that no Vandermonde factor is zero. Integrality of $W$ is proved separately from the core identity.
41 
42 The corresponding five-core partition has size $n-1$. In particular, the coefficient at $n=1$ corresponds to the empty partition. The involution is $J(v)_i=-v_{-i\bmod5}$. A $J$-orbit may contain one or two packets, and its mass is the sum of their weights.
43 
44 The content of a packet is the positive gcd of its five coordinates. Content-one packets are primitive. Multiplication followed by the prescribed residue reindexing gives
45 \[
46 \tau(n)=\sum_{g^2\mid n}\chifive(g)g^{10}R(n/g^2),
47 \qquad
48 R(n)=\sum_{d^2\mid n}\mu(d)\chifive(d)d^{10}\tau(n/d^2).
49 \]
50 The boundary values are $R(1)=1$ and $R(p)=\tau(p)$. At a prime shell the only possible content is one, so the extraction has not created a new prime coefficient.
51 
52 \section{Three polynomial operations}
53 The ordinary hyperplane Laplacian is $\Delta_H$. The conjugated operator $\mathcal L$ is characterized by $\Delta_H(DQ)=D\mathcal LQ$. Harmonicity of $DQ$ means $\mathcal LQ=0$. It does not mean that $Q$ itself is harmonic.
54 
55 A universal null is a polynomial $Q$ for which
56 \[
57 \sum_{v\in\Vn}W(v)Q(v)=0
58 \]
59 for every positive $n$. A shell-null polynomial satisfies that equation only at a specified shell. A polynomial interpolating prescribed values on a shell need satisfy neither condition. The difference between these three operations is responsible for several of the obstruction results.
60 
61 For a universal null, replacing $W(v)$ by $W(v)(1+Q(v))$ preserves the shell total. A sign conclusion requires real corrected weights and at least one strict nonzero contribution. There is no order relation on complex weights. The all-polynomial content theorem assumes a finite symmetric polynomial and makes no claim for arbitrary infinite series or nonsymmetric functions.
62 
63 \section{Local and global conventions}
64 For $\ell\ne p$, the arithmetic-Frobenius convention in the integral $\ell$-adic representation gives the characteristic polynomial
65 \[
66 X^2-\tau(p)X+p^{11}.
67 \]
68 The cohomological conventions in the filtered-module discussion are stated there separately. An abstract trace-zero filtered module and a representation realizing it are local objects. A comparison identifying its normalized Frobenius trace with the actual coefficient $\tau(p)$ is additional mathematical data.
69 
70 The fixed-modulus survivor theorem concerns the actual joint finite image, including the cyclotomic factor. It does not assume that its constituent images are independent. Its quantifiers are
71 \[
72 \text{for every fixed }M,\quad \text{there exist suitable actual primes }p.
73 \]
74 The prime may change with $M$. The theorem does not supply one prime for every modulus.
75 
76 \input{appendix_operator.tex}
77 \input{appendix_workbook.tex}
78 
79 \chapter{External theorem contracts}\label{app:sources}
80 
81 This edition checks the specific theorem statements used in the argument. The check is targeted, not an exhaustive review of the literature or a certification of novelty. The sixteen source contracts below are recorded with versions, locators, access outcomes and limitations in the companion evidence. The bibliography supplies the corresponding primary or author-hosted references.
82 
83 The source-dependent input and the project argument should be read together. For example, a vector-valued harmonic theta theorem does not by itself prove the scalar sign-line descent used here. That descent is developed in the main text. Similarly, a trace formula computes an exact difference, but its existence does not exclude a zero difference.
84 
85 \section{Classical coefficient structure}
86 \paragraph{S01: Lehmer's original reduction.}
87 Lehmer's 1947 paper is the historical reference for the least-zero prime reduction and the multiplicative structure \cite{Lehmer}. The original scan was not text-readable through the checked access route, so this edition does not claim to have freshly reconstructed its original proof. The necessary coefficient identities are separately checked in readable modern primary sources, and the prime-power zero criterion is proved in the main text.
88 
89 \paragraph{S06: Deligne's bound and normalization.}
90 The modular representation and purity inputs give $|\tau(p)|\le2p^{11/2}$ \cite{DeligneModular,DeligneWeil}. The modular paper's representation construction and the Weil theorem supply different parts of this implication. Their Frobenius conventions require translation. This upper bound includes zero and is never used as a positive lower bound.
91 
92 \paragraph{S07: classical congruences.}
93 Serre's 1967/68 exposition supplies the checked modulo-$691$ identity and the modulo-$23$ prime classification \cite{SerreCongruences}. The latter excludes $p=23$. Representation existence is still conjectural in the relevant passage of that early exposition. The existence input in this book therefore uses the later established representation statement.
94 
95 \paragraph{S10: a cited historical computation.}
96 Derickx, van Hoeij and Zeng establish the strict historical range
97 \[
98 n<816212624008487344127999
99 \]
100 in their checked 2014 version, Corollary~1.2 \cite{DHZ}. The endpoint is not asserted to be a zero. This source-certified range was not rerun for the present edition and is not presented as the latest record.
101 
102 \paragraph{S11: scoped contemporary context.}
103 The checked 2026 version supplies a contemporary formulation and readable classical recurrence and parity statements \cite{TauContext2026}. Only those classical introductory inputs are used. The 2025 submission titled as a proof was withdrawn \cite{Withdrawn2025}. Its title is not accepted as evidence of a theorem. No exhaustive current-status or priority claim follows from this targeted check.
104 
105 \paragraph{S16: readable classical leaves.}
106 Balakrishnan, Craig and Ono provide the modulo-$5$ congruence at equation~(1.2), the multiplicativity and recurrence statements at Theorem~2.2, and the direct odd-square parity argument in Section~3 of the checked 2020 version \cite{BCO}. These are the exact leaves used here. This edition has not audited the paper's separate integral-point or omitted-value arguments.
107 
108 \section{Convolutions and trace moments}
109 \paragraph{S12: the Hurwitz moment normalization.}
110 Lygeros and Rozier's 2010 primary paper gives the trace moments and Catalan inversion used in Chapter~5 \cite{LRTrace}. The class-number function includes imprimitive forms with its specified weights. The $t=0$ term has a half-weight in the zeroth moment. The integral normalization is $6H$. Removing any of these qualifications would change the rows of the inverse system.
111 
112 \paragraph{S14: Niebur's convolution.}
113 The universal formula is checked in the primary paper of Moriya and Smyth, Section~7, rather than inferred from finite coefficient agreement \cite{MoriyaSmyth}. The original 1975 Niebur proof was inaccessible through the checked route \cite{Niebur}. The attribution is retained with that access limitation. The size and divisibility alternatives remain compatible with a prime zero.
114 
115 \paragraph{S15: differential equations.}
116 Fonseca records the normalized Ramanujan differential relations used in the polynomial computation \cite{Fonseca}. The project-specific $S_4$ cancellation is verified algebraically in the main text and by an exact symbolic remainder. Modularity and the level-one dimension input for the cusp identity are separate contracts \cite{Stein}. A finite output check is not substituted for the universal algebraic identity.
117 
118 \section{Cores, harmonic theta series and valence}
119 \paragraph{S02: Han's packet identity.}
120 Han's Definition~1.1 and Theorems~1.1--1.2 in the checked first arXiv version provide the five-core specialization and Vandermonde product \cite{Han}. The specialization $t=5$, $z=25$ gives the shell norm $10n$ after the coefficient shift. With the orientation used here, the normalization is $D/288$. The identity permits cancellation and does not imply that its terms have one sign.
121 
122 \paragraph{S13: packet cardinality.}
123 Garvan, Kim and Stanton's Theorem~4 and equation~(5.3) give the five-core count \cite{GKS}. In the present conventions this reads
124 \[
125 a_5(n-1)=\sum_{d\mid n}\chifive(d)\frac nd.
126 \]
127 For a prime different from $5$, the shell cardinality is $p+\chifive(p)$. This is the number of packets, not their weighted sum.
128 
129 \paragraph{S03: harmonic theta modularity.}
130 Ibukiyama and Williams, Section~3.4 of the checked version, give the vector-valued harmonic theta theorem with weight $\nu+r/2$ \cite{IW}. Here the rank is four and the harmonic polynomial is alternating of degree $10+d$. The scalar full-level transformation follows from the separate sign-line descent in Chapter~8. It is not silently imported as part of the general theorem.
131 
132 \paragraph{S04: the valence step.}
133 Stein's author exposition supplies the level-one valence bound and the relevant cusp-form dimensions \cite{Stein}. The vanishing test is applied only after modularity, holomorphy and the weight are established. Vanishing of sufficiently many initial Fourier coefficients then proves that specific modular form is zero. It does not establish an arbitrary polynomial's universal nullness without the modular prerequisites.
134 
135 \section{Global congruences and local realization}
136 \paragraph{S05: the actual compatible representations.}
137 Serre's 1973 exposition gives the established integral rank-two representations and the arithmetic-Frobenius polynomial \cite{SerreBourbaki}. The fixed-modulus proof uses their actual joint finite quotient. It does not require an image classification, surjectivity onto an ambient matrix group, or independence across primes $\ell$.
138 
139 \paragraph{S08: Chebotarev's theorem.}
140 The checked Stevenhagen--Lenstra exposition states the nonempty conjugacy-class theorem and distinguishes natural density \cite{Chebotarev}. In a finite Galois quotient the density is the class size divided by the group size. Complex conjugation supplies the class in the actual image. The theorem is applied separately for each fixed modulus. Nothing in the density formula interchanges the quantified modulus and prime.
141 
142 \paragraph{S09: weak admissibility and admissibility.}
143 The Colmez--Fontaine author manuscript supplies the implication from weak admissibility to admissibility and the $N=0$ crystalline realization in the specified setting \cite{CF}. The constructed rank-two module has equal Hodge and Newton totals and no proper Frobenius-stable rational line. Those checks concern a local object. They do not identify it with the global representation of $\Delta$.
144 
145 \section{Access and attribution limits}
146 The companion source records retain the exact checked versions and successful alternative author-hosted access routes. The two original-proof access limits above are explicit. The book does not label a cached excerpt, a source title, a search result or a historical status field as a completed proof audit.
147 
148 The internal packet transport, nonhomogeneous content argument, interpolation analysis and arithmetic model constructions are reviewed as written arguments. Their correctness is distinct from whether any formulation has appeared elsewhere. This edition makes no historical-priority claim for them and no exhaustive novelty claim.
149 
150 \chapter{Reproduction and evidence boundaries}\label{app:reproduction}
151 
152 The companion archive is a reproducible record of this edition's finite claims. It preserves six recovered research ZIPs and all their original extracted file members. New executions write to separate directories. The present prose and audits determine what this reader claims. Historical labels remain available for comparison without being treated as current validation.
153 
154 \section{What was rerun}
155 Sixteen fresh suites completed. Their version-two execution manifests validate current inputs, scientific results and logs. Thirteen historical scientific outputs agree exactly with the fresh results after removing only elapsed-time metadata fields named \texttt{runtime}, \texttt{runtime\_seconds} and \texttt{seconds}. Three additional suites provide independent coefficient, transfer and large-residue checks.
156 
157 The most direct coefficient check covers every $1\le n\le512$. The triangular recurrence, the defining binomial product and an independent logarithmic-derivative divisor-sum engine agree exactly. All three use integers. This range is distinct from the historical final-arithmetic program's product check through $128$, and from the independent product check in the packet-tree program through $512$.
158 
159 The arithmetic survivor search uses $\tau$ through $10000$ and twenty-four selected moduli. Twenty-two moduli have a matching prime in that bounded search, supplying $22\times32=704$ local recurrence checks. Moduli $11$ and $19$ have no observed witness in that search. This is a search outcome, not a contradiction of the density theorem. Modulus one is included as a trivial case.
160 
161 The synthetic recurrence suite has $256$ moduli, three parameter choices and thirty-two positive exponents, for $24576$ checks. Its value $p=5M-1$ need not be prime. Separately, the $1229$ prime-indexed companion matrices through $10000$ are constructed local models. They are not sampled global Frobenius matrices.
162 
163 \section{Packet and polynomial checks}
164 The five-core suite checks $405$ shell sums and $326585$ packet polynomials, with $308$ prime shell counts. Twenty-five coefficients also agree with an independent hook-partition calculation. The tree suite enumerates all shells through $512$ and the two additional shells $737$ and $2411$, giving $514$ shell sums and $95937$ packets. It checks $3084$ sector partitions and explicit sharp-boundary witnesses at sixty-four depths.
165 
166 The shell at $737$ is a sparse additional witness. The replay does not enumerate every shell from $513$ through $736$. The universal threshold formula rests on the separate lower-bound proof and the symbolic witness families.
167 
168 The retained universal-null suite checks fourteen exact rational sign certificates. Its degree-at-most-sixteen dual at $31$ concerns the seven stored corrections, not all possible corrections. The primitive transport suite checks thirty-six symbolic harmonic certificates, $128$ Mobius identities, $144$ profiles and the stored rational transfer. The independent $31$ calculation obtains coarse, fine and detail ranks $5$, $15$ and $10$ over the rationals and the two prime fields $65537$ and $1000003$, with structural upper bounds.
169 
170 The content obstruction is the exact shell $121$. Its masses are
171 \[
172 -25439104668+25937424601=498319933.
173 \]
174 The computation establishes these integers. The theorem that every finite symmetric universal null conserves each content is a separate proof. Likewise, the interpolation suite's finite orbit checks and two explicit failures do not prove an all-degree fullness theorem.
175 
176 \section{Large modular coefficients}
177 The valuation suite regenerates coefficients at all $13848$ primes through $150000$. Its proposed valuation equalities are tested only on their stated candidate residue classes. Independent Eisenstein convolutions verify the selected counterexample coefficients. The dyadic obstruction uses twelve selected primes through $1032191$, with nineteen fresh modular comparisons.
178 
179 The CRT/NTT computation returns residues modulo $2^{19}$. It is not a reconstruction of those large integer tau coefficients. Within each convolution, however, the integer coefficient is reconstructed before reduction. With
180 \[
181 L=1032191,\qquad M=524288,
182 \]
183 the nonnegative representative bound is
184 \[
185 L(M-1)^2=283725419316756479
186  <998244353\cdot1004535809
187  =1002772198720536577.
188 \]
189 The common transform length $2^{21}$ divides both finite-field multiplicative periods. This bound, primitive-root checks and integer-type limits are part of the computation contract. Modular agreement alone would not justify CRT reconstruction without them.
190 
191 \section{How to reproduce the record}
192 Paths in this section are relative to the extracted project root. The executable entry point is
193 \begin{lstlisting}[basicstyle=\ttfamily\small,breaklines=true]
194 python3 code/run_replays.py --output-root evidence/computation/reproduced
195 \end{lstlisting}
196 The output directory must be fresh. Individual suite names may precede the output option. The tested runtime and dependency versions are recorded in \path{evidence/BUILD_ENVIRONMENT.json}. Each execution records its actual arguments, inputs, result hashes and resource outcomes.
197 
198 The full replay uses a $600$-second wall-clock bound per suite, a $570$-second per-process CPU cap, inherited one-core affinity and a two-million-byte combined log limit. Numerical-library thread caps are cooperative. No address-space cap is claimed. Exact arithmetic programs can consume substantial time or memory outside the recorded ranges.
199 
200 The two readers rebuild with
201 \begin{lstlisting}[basicstyle=\ttfamily\small,breaklines=true]
202 python3 build.py --figures
203 python3 quality_check.py
204 python3 validate_fonts.py
205 \end{lstlisting}
206 Rendering creates immutable snapshots for inspection. Automated checks locate unresolved references, clipped text and font problems. Every final page in this edition also has an individual visual review record tied to the final PDF hash. A fresh rebuild may change PDF metadata, so its layout approval must be tied to its own output rather than copied from this edition.
207 
208 \section{What the evidence does not claim}
209 No scientific replay failed. One inventory collector initially read the wrong schema field, then was corrected. Its failure and correction are recorded rather than hidden as a successful mathematical execution.
210 
211 The recovered project contains written mathematics and exact programs, with no recovered Lehmer proof-assistant source project or compiled certificate. The formal inventory is an inventory and definition audit. It is not a Lean verification of the theorems in this book.
212 
213 Each exact certificate proves its stated finite equality, rank or sign claim. Each range check ends at its stated bound. The universal deductions use the written proofs and the external contracts in Appendix~\ref{app:sources}. The all-prime nonvanishing statement remains open in this work.

Back to source controls

Back to Lehmer: source and evidence