2607.20408v1 / README.md
all files
# Reproduction report: *Extreme values of quadratic Dirichlet L-functions*
## Verdict
**Partial.** The central analytic estimate has not been formalized, so this is
not a reproduction of Theorem 1.1. All Lean declarations in `Repro/` compile
without proof placeholders or project-specific postulates. The strongest
capstone theorem proved here is conditional on the proposition
`GRHImpliesPaperResonanceMoments`; that proposition is the missing novel
analytic core of equations (3.2)--(3.8), not an admissible “deep external
theorem” shortcut.
The run also found two literal errors in the paper. Neither currently gives a
counterexample to Theorem 1.1, because both appear repairable, but the proof as
printed is not correct without repairs.
## The paper's claim
Let \(\mathcal F\) be the fundamental discriminants and let
\(\chi_d=(d/\cdot)\) be the real primitive quadratic character modulo
\(\lvert d\rvert\). Assuming GRH, the paper claims
\[
\max_{\substack{X<|d|\le 2X\\d\in\mathcal F}}
\left|L\!\left(\tfrac12,\chi_d\right)\right|
\ge
\exp\!\left((1+o(1))
\sqrt{\frac{\log X\,\log_3 X}{\log_2 X}}\right).
\]
`ExtremeValues.HasExtremeLowerBound` gives the phrase
“\(\ge\exp((1+o(1))S(X))\)” the standard unambiguous lower-bound meaning:
for every real \(c<1\), the inequality with \(\exp(cS(X))\) holds eventually.
This avoids encoding an informal \(o(1)\) as arbitrary data.
## Files
- `Repro/QuadraticCharacters.lean`
bundles \(n\mapsto J(n\mid q)\) as a genuine
`DirichletCharacter ℂ q`, proves its pointwise Jacobi-symbol specification,
proves it is quadratic, connects it to quadratic reciprocity for
\(q\equiv1\pmod4\), and defines its actual mathlib analytic continuation
`jacobiLFunction`.
- `Repro/ExtremeValues.lean`
defines fundamental discriminants, the iterated-log scale, finite
resonance witnesses, shell suprema, and proves the complete
weighted-average step from a resonance moment inequality to an extreme
value.
- `Repro/CentralClaim.lean`
restricts to positive odd fundamental discriminants
\(q>1,\ q\) squarefree, \(q\equiv1\pmod4\). This positive-density subfamily
avoids the paper's parity error. It defines GRH explicitly for these
mathlib L-functions and states the precise missing moment proposition.
- `Repro/PaperErrors.lean`
gives kernel-checked witnesses for the product-sign error and for the fact
that \(\chi_{-4}\) is odd and therefore has the odd gamma factor.
- `Repro/Audit.lean`
prints the assumptions of the important declarations.
- `Repro/parity_check.py`
independently evaluates the two approximate-functional-equation weights
at \(d=-4\), using only Python's standard library.
## Semantic checks
### Fundamental discriminants
`IsFundamentalDiscriminant d` uses the standard elementary classification:
1. \(d\equiv1\pmod4\) and \(|d|\) is squarefree; or
2. \(d=4m\), \(m\equiv2\) or \(3\pmod4\), and \(|m|\) is squarefree.
The development proves such a discriminant is nonzero and proves that every
positive squarefree \(q\equiv1\pmod4\) belongs to this class.
### Quadratic characters and L-functions
Mathlib already provides Jacobi symbols, Dirichlet characters, analytic
continuation of Dirichlet L-functions, gamma factors, and their functional
equations. It does not bundle a general Jacobi symbol as a Dirichlet character.
`jacobiCharacterInt` fills that gap directly:
\[
\chi_q(n)=J(n\mid q).
\]
The construction proves multiplicativity, vanishing at non-units, the exact
value on natural arguments, and quadraticity. For odd \(n\) and
\(q\equiv1\pmod4\), quadratic reciprocity proves
\(J(n\mid q)=J(q\mid n)\). Thus the repaired positive odd subfamily uses an
actual mathlib L-function attached to the standard quadratic character, not a
free numerical function.
`positiveOddCentralNorm` is zero outside this subfamily and is
\[
\left|L\!\left(\tfrac12,\chi_q\right)\right|
\]
inside it. A lower bound for this zero-padded subfamily is stronger than the
same lower bound after maximizing over all fundamental discriminants.
## What is completely proved
For any real-valued family `value : ℤ → ℝ`, a `ResonanceWitness` consists of:
- a finite set of fundamental discriminants in \(X<|d|\le2X\);
- nonnegative weights with positive total mass; and
- the moment inequality
\[
T\sum_d w_d\le\sum_d w_d\,\mathrm{value}(d).
\]
`ResonanceWitness.exists_value_ge` proves that some supported \(d\) has
`value d ≥ T`. `extreme_lower_bound_of_resonance` upgrades eventual witnesses
at every \(c<1\) to `HasExtremeLowerBound` for the shell supremum. This is the
fully formal content of the paper's equation (3.1), including finiteness and
nonempty-mass details.
The capstone theorem
`extreme_values_of_quadratic_dirichlet_L` proves the repaired central
lower-bound statement from these two disclosed hypotheses:
1. `GRHForPositiveOddQuadratic`;
2. `GRHImpliesPaperResonanceMoments`.
The second is not counted as an allowed external theorem in the verdict,
because it is precisely the paper's new resonance calculation.
## Missing analytic core
Closing `GRHImpliesPaperResonanceMoments` requires formal versions of all of:
1. the central approximate functional equation, including positivity,
parity-correct gamma weights, exponential decay, the small-argument
expansion, and justified interchange of sums;
2. the GRH-dependent mean estimate for quadratic characters, with its
dependence on squarefree and square parts, plus partial summation for the
\(d\)-dependent weight;
3. the sharp asymptotic construction for squarefree GCD sums, including the
largest-prime-factor property used in the Rankin truncation;
4. the uniform error calculation producing
\(E\ll X^{3/4+\varepsilon}N^{2+\varepsilon}\);
5. the asymptotic comparison after setting \(N=X^{1/4-\alpha}\).
Mathlib has the analytic continuation and functional equation for Dirichlet
L-functions, but none of items 1--3 in the required strength. A permitted
tooling-only GitHub search found generic Kronecker-character and analytic
number theory experiments but no formalized quadratic mean theorem,
approximate functional equation with these bounds, or sharp squarefree GCD-sum
asymptotic. The generic Kronecker bridge found in that search itself exposes
periodicity modulo \(|d|\) as a hypothesis, so importing it would not remove
the gap.
## Errors found in the paper
### 1. Lemma 2.1 uses the wrong parity for negative discriminants
The theorem maximizes over \(X<|d|\le2X\), so it includes \(d<0\). Such
\(\chi_d\) are odd. Nevertheless Lemma 2.1 uses
\[
\frac{\Gamma(1/4+s/2)}{\Gamma(1/4)}
\]
and writes \(n/\sqrt d\). The displayed formula is the even-character formula.
For \(d<0\), it must use \(|d|\) and
\(\Gamma(3/4+s/2)/\Gamma(3/4)\).
`PaperErrors.chiNegFour_odd` proves in Lean that the character attached to
\(d=-4\) is odd. `PaperErrors.chiNegFour_gammaFactor` then proves from
mathlib's standard Dirichlet functional equation that its gamma factor is
`Gammaℝ (s + 1)`, not `Gammaℝ s`.
The numerical script uses the identity
\[
\omega_a(\xi)=Q(a,\pi\xi^2)
\]
for the regularized upper incomplete gamma function. For \(d=-4\), 100 terms
give
```text
paper-even-weight RHS: 0.18901770464767276
correct odd-weight RHS: 0.66769145718960932
difference: -0.47867375254193656
```
The correct value agrees with the standard central value
\(\beta(1/2)\). This is a concrete failing case of Lemma 2.1 as printed.
A plausible repair is to split signs and use the two parity weights, or to
work only with positive discriminants. This development takes the latter
route, but the needed restricted-family character mean remains unproved.
### 2. The Euler product for \(g_2\) has the wrong sign
The paper defines
\[
g_2(n)=\sum_{q\mid n}\frac{\mu(q)^2}{q^{1/2+\varepsilon}}.
\]
Its Euler product has factors \(1+p^{-1/2-\varepsilon}\), but the next display
prints \(1-p^{-1/2-\varepsilon}\). At \(n=2,\varepsilon=1/2\), the definition
is \(3/2\) while the printed product is \(1/2\).
`PaperErrors.g2_product_sign_counterexample` checks this counterexample
exactly over \(\mathbb Q\).
Replacing the minus by a plus preserves a subexponential upper bound of the
kind later needed, so this error alone does not refute Theorem 1.1.
## Approaches attempted
1. **Direct all-discriminant formalization.** Mathlib has Dirichlet analytic
continuation but lacks fundamental discriminants and a general Kronecker
character. The negative-discriminant parity error also makes the paper's
stated approximate functional equation unusable verbatim.
2. **Build the character theory locally.** The Jacobi character was bundled
and verified successfully. Extending this to all signed fundamental
discriminants would still leave the analytic estimates untouched.
3. **Parity-split repair.** Restricting to positive odd fundamental
discriminants repairs Lemma 2.1 and is strong enough for the original
maximum. It requires a GRH mean estimate in this restricted family, which
is not available.
4. **Abstract resonance factorization.** The finite weighted-average and
shell-maximum layers were isolated and fully proved. Expanding the cited
inputs into the claimed moment inequality still requires the five analytic
items listed above.
5. **Library/project search.** Local mathlib and permitted generic Lean
projects were searched for GRH character means, approximate functional
equations, Kronecker characters, and sharp GCD sums. The structural
character code was reproducible locally; the decisive analytic theorems
were absent.
6. **Counterexample audit.** The two literal errors were checked formally and,
for the parity issue, numerically. Both admit plausible repairs, so there
is no established counterexample to Theorem 1.1 itself.
No remaining route avoids developing substantial new analytic number theory
in Lean. Assuming the moment proposition would assume the paper's principal
new argument, so the run stops with a partial rather than reproduced verdict.
## Verification
From the repository root:
```bash
lake build Repro
lake env lean Repro/ExtremeValues.lean
lake env lean Repro/QuadraticCharacters.lean
lake env lean Repro/CentralClaim.lean
lake env lean Repro/PaperErrors.lean
lake env lean Repro/Audit.lean
python3 Repro/parity_check.py
```
`Repro/Audit.lean` reports only `propext`, `Classical.choice`, and
`Quot.sound`, the standard logical principles already used throughout
mathlib. There are no project-specific assumptions in the checked proofs.