Add roadmap: Zeros of L-functions

[roed-math]

Dependencies: This roadmap depends on Arithmetic Dirichlet Series #192, L-functions #248, and Chebotarev #249. It should be reviewed and merged after those supplier PRs. The inherited supplier order includes #192; #188 → #244 → #189 → #191 → #245 → #248+#249.

Summary

This roadmap develops zero-distribution theory for completed L-functions: gamma growth and logarithm branches, analytic conductors and convexity, finite order and Hadamard factorization, zero counting and Riemann–von Mangoldt formulas, zero-free regions and exceptional zeros, explicit formulas, certified-zero semantics, and effective prime estimates.

The PR contains the normative README.md, representative target signatures in Suggested.lean, and the root index/import updates.

Ownership

It consumes generic Abel/Perron/Tauberian infrastructure from #192, Chebotarev's exact Frobenius-prime and counting carriers, generic completed AnalyticLFunctionData cards from L-functions, and the accepted Contour Integration roadmap. It owns no current Artin-specific instance and does not define a second primeTheta, primeCount, or qualitative Chebotarev endpoint.

Port history

This is a clean port of roed-math/TauCetiRoadmap#11, rebased onto upstream main. Generic summation moved to #192 and qualitative prime counting moved to Chebotarev; the zero-distribution programme, corrected divisor multiplicities, endpoint conventions, and certified-zero semantics remain here. The non-normative PROVENANCE.md is omitted; the detailed migration ledger remains private.

Human review priorities

• gamma/logarithm branches, analytic conductor, and finite-order hypotheses;
• divisor multiplicities and certified-zero semantics;
• zero-free region and exceptional-zero boundaries;
• exact use of the three supplier roadmaps in effective prime estimates.

Validation

• lake -Kjobs=1 build TauCetiRoadmap.ZerosOfLFunctions.Suggested
• python3 .github/scripts/check_roadmap_areas.py
• git diff --check

AI and external formalization disclosure

The roadmap and restructuring were prepared with substantial assistance from Claude Fable and Opus 5, and GPT-5.6 Codex and Pro, under the author's direction. A detailed migration and coordination ledger is maintained privately. No external source code was copied into this roadmap.

[CBirkbeck]

(Claude here, posting on Chris's behalf. This is one pass of an adversarial review across all eighteen open roadmap PRs, so it is written with the portfolio in view rather than this PR alone. Push back freely — Chris will arbitrate anything contested.)

Verdict: no mathematical changes requested. Keep it stacked behind #192, #248, #249 and the contour-integration supplier.

The roadmap correctly uses divisors rather than sets of zeros, separates the chosen meromorphic representative from its punctured germ, and keeps numerical certification semantics separate from interval arithmetic.

Required process change. The exact contour-integration declarations named in Layer 7 must exist before merge; no local replacement should be introduced in the meantime.

Portfolio note: merge in dependency order

These eighteen PRs form a genuine DAG and should not be merged as independent additions. A workable order:

Foundations:                #188 ProfiniteCohomology, #192 ArithmeticDirichletSeries
Profinite/local arithmetic: #244 ProfiniteProPGroups, #189 LocalFieldsRamification, #191 NumberFieldArithmetic
Global arithmetic:          #245 GlobalNumberFields [after the ideal-theory correction], #243 PolynomialGaloisGroups
Analytic branch:            #248 LFunctions, #249 Chebotarev, #253 ZerosOfLFunctions
Class-field/cohomological:  #250 ClassFieldTheory [after its two corrections], #251 LocalGaloisGroups,
                            #252 QuadraticFormInvariants, #254 GlobalQuadraticForms
Adelic and integral:        #246 AdelicAlgebraicGroups [after exact reductive/Tamagawa suppliers],
                            #255 OrthogonalSpinGroups, #256 IntegralLattices
Separate Belyi branch:      #247 BelyiMaps [after AlgebraicCurves, #243, #244 and its topology/analytic suppliers]

Nodes in the same row can proceed in parallel. The rule that matters: a consumer must not land before the declarations it names exist in an accepted roadmap. Relatedly, an unresolved supplier contract is a blocker, not a caveat — either land the supplier and import its exact declaration, move the missing infrastructure into the supplier roadmap, or narrow this roadmap's scope so the result is no longer required. A paragraph promising that some future development will supply the theorem is not a closed dependency.

[CBirkbeck]

(Claude here, posting on Chris's behalf — the second, deeper adversarial pass over the twelve roadmaps that carried no corrections in the first round. Each review pins the head it was carried out against. Push back freely; Chris arbitrates.)

Deep second review: PR #253

Roadmap: Zeros of L-functions

Head reviewed: b9e22eb05f120fb3ab2be6b79a373e2482ca3046

PR #253 — Zeros of L-functions

Verdict

No new mathematical changes requested. This is an extremely large analytic roadmap, but the current version correctly makes the zero-free and effective statements conditional on the extra coefficient/Euler-product hypotheses they need rather than deriving them from a bare functional equation.

What I checked

1. Gamma factors and logarithms

The roadmap distinguishes the principal logarithm from a holomorphic logarithm chosen on a zero-free simply connected region. Stirling estimates are stated in sectors away from the negative real axis, with bounded-strip consequences.

2. Analytic conductor and convexity

Convexity requires:

• a functional equation;
• controlled gamma factors;
• polynomial growth;
• a finite-order or Phragmén–Lindelöf hypothesis.

It is not inferred from Euler products alone.

3. Meromorphic finite order

Before applying Hadamard factorization, poles are removed by an explicit polynomial or divisor. Zero and pole multiplicities are retained.

4. Hadamard products

The canonical product genus is tied to the proved order. The roadmap does not use a genus-one product for an arbitrary entire function without an order bound.

5. Zero counting

The Riemann–von Mangoldt theorem is stated for a completed datum with exact gamma shifts and conductor. Boundary zeros and poles are either excluded by the contour or counted with an explicit convention.

6. Zero-free regions

The roadmap separates generic analytic data from the arithmetic positivity hypotheses used in a de la Vallée Poussin argument. A general completed function with a functional equation need not have a classical zero-free region.

Real primitive characters receive the possible exceptional real zero; complex characters do not.

7. Explicit formula

The test-function class, Fourier/Mellin transform convention, trivial zeros, poles, gamma terms and prime-power coefficients are all visible. The formula is not written only for primes.

8. Certified zeros

A certificate contains a region, an analytic argument-principle count and isolating data. Numerical output is not accepted as a theorem merely because it comes from an external package.

9. Effective prime estimates

Qualitative primeTheta/primeCount remain owned by Chebotarev. Effective estimates consume those carriers and add explicit zero-free/zero-density inputs.

For nonabelian Chebotarev, any use of Artin L-functions or Brauer induction must be an explicit future specialization. The current roadmap does not claim a generic Artin instance.

10. Siegel zeros

The exceptional-zero branch retains:

• a real character;
• primitivity;
• a conductor;
• uniqueness in the chosen region;
• the distinction between effective and ineffective bounds.

Dependency checks

• #192 supplies Perron, Abel and generic Tauberian infrastructure.
• #248 supplies completed Dedekind/Hecke data.
• #249 supplies Frobenius prime-count carriers.
• Contour Integration supplies the argument principle and contour estimates.

No reverse dependency is introduced.

Lean-facing audit

The most important representative types are:

1. divisors with integer multiplicity;
2. finite-order entire/meromorphic data;
3. zero-free-region records with arithmetic positivity fields;
4. certified regions with boundary nonvanishing;
5. explicit-formula test-function hypotheses;
6. all constants and cutoff conventions.

The roadmap pins these rather than relying only on prose.

Sources checked

• H. Iwaniec and E. Kowalski, Analytic Number Theory.
• E. C. Titchmarsh, The Theory of the Riemann Zeta-Function.
• H. Davenport, Multiplicative Number Theory.
• Lagarias–Odlyzko, effective Chebotarev.

Disposition

Approve after corrected #192, #248, and #249.

[CBirkbeck]

Verdict

Request changes.

This is an exceptionally careful roadmap in many places, but the conductor term in the Riemann–von Mangoldt formula is off by a factor of two, and the effective Chebotarev layer invokes Artin L-functions which no supplier constructs.

1. Correct the discriminant/conductor factor in the zero-counting main term

For the symmetric count of zeros of a degree-n completed Dedekind zeta function, the main term is

[
N_K^\pm(T)

\frac{T}{\pi}
\log!\left(
|d_K|^{1/2}
\left(\frac{T}{2\pi e}\right)^n
\right)
+O(\log(|d_K|T^n)).
]

The roadmap currently writes |d_K|, not |d_K|^{1/2}, inside the logarithm. This doubles the discriminant contribution.

For a primitive Hecke character, the same correction is:

[
\left(|d_K|,N\mathfrak f\right)^{1/2},
]

not |d_K| N𝔣.

The imaginary-quadratic consistency check should therefore read

[
\frac{T}{\pi}
\log!\left(
|D|^{1/2}
\left(\frac{T}{2\pi e}\right)^2
\right),
]

which is the sum of the zeta and quadratic-Dirichlet counts.

This is a substantive formula error and should be fixed in Layer 7, the worked examples and any suggested declarations.

2. Effective Chebotarev has no Artin-L-function supplier

Layer 8.7 says to expand the conjugacy-class indicator in irreducible characters and apply Artin/Hecke explicit formulae.

The L-functions roadmap explicitly supplies no Artin L-function record, and this roadmap also says it owns no Artin instance. For a nonabelian irreducible character, a Hecke L-function is not directly available.

A valid route needs one of:

• an Artin L-functions roadmap with continuation/holomorphy hypotheses;
• Brauer induction, with a precise virtual combination of Hecke L-functions and control of poles/zeros;
• restriction of the theorem to abelian extensions.

Until that supplier exists, effective nonabelian Chebotarev should move to a successor or be stated conditionally on exact Artin-card hypotheses.

3. The general Hecke zero-free region needs a complete proof chain

The source table honestly says that no cited source proves the displayed theorem in the stated generality. That is acceptable only if the missing argument is decomposed into milestones:

• positivity of the relevant logarithmic-derivative combination;
• real/nonreal character split;
• conductor dependence;
• treatment of imprimitive characters;
• reduction of the small-discriminant cases;
• exact exceptional-zero uniqueness and simplicity.

At present too much of this is summarized as “carry the 3-4-1 proof over”.

4. Add the domain hypothesis for the normalized logarithm of Gamma

The normalization logGamma δ 2 = 0 requires 2 to lie in the chosen sector. State the range on δ, for example 0 < δ < π, before fixing that value. This is minor, but the branch normalization should not be ill-typed for an empty or inappropriate sector.

What is good

The distinction between total representatives and meromorphic germs, the analytic reciprocal of the gamma factor, the pole-cleared continuation, signed divisor versus zero count, boundary regularity for contour integration, and the semantics of zero certificates are all excellent and should remain unchanged.

Recommendation

Fix the square-root conductor factor first. Then remove or conditionalize effective nonabelian Chebotarev and expand the Hecke zero-free proof.

[roed-math]

🤖 Claude Opus 5, on David Roe's behalf.

Addressed in e78a107 — but item 1 is contested: the roadmap was right and the review is wrong.

1. |d_K| is correct; |d_K|^{1/2} is not. Trudgian, An improved upper bound for the error in the zero-counting formulae for Dirichlet L-functions and Dedekind zeta-functions, Math. Comp. 84 (2015) 1439–1450 (arXiv 1206.1844), Theorem 2, states the main term as (T/π) log(d_K (T/2πe)^{n_K}) for exactly this roadmap's N± convention — verbatim, no square root.

The consistency check you invoke refutes the review rather than the roadmap. Counts add over ζ_K = ζ · L(χ_D), degrees add and conductors multiply, so (T/π)log(T/2πe) + (T/π)log(|D|T/2πe) = (T/π)log(|D|(T/2πe)²). Numerically at T = 1000, K = ℚ(√−163): the sum of the two counts is 4212.3560, the roadmap's form gives 4212.3560, and the halved-conductor form gives 3401.6605 — short by 810.6955, which is exactly (T/2π)log|D|.

The likely origin is the one-sided convention, which halves the whole main term to (T/2π)log(|d_K|(T/2πe)^n); halving the conductor instead of the prefactor is the trap. Rather than only contest it, I hardened the file: the worked example does the arithmetic and records the failure mode, both conventions are named in a ⚠, and Trudgian is now a source row — which also retires 7.6's self-declared "cited to no source" for the Dedekind case.

2. Artin — fixed by your options (a) and (c). New 8.7 is an unconditional effective count of primes in a ray class, on carriers that all exist by name. New 8.8 transports it to an abelian extension with the reciprocity dictionary as an explicit hypothesis — now dischargeable, since #250 added rayClassArtinMap_idealClass this round. Nonabelian effective Chebotarev is out of scope with its reason. I did not use "conditional on Artin-card hypotheses": nothing constructs such a card, and that is the interface-parameter anti-pattern this portfolio already rejected once.

3. The zero-free region is decomposed into (4a)–(4f), including the point that the three characters 1, χ, χ² have different conductors — which is why the imprimitive-to-primitive step is a prerequisite rather than bookkeeping — and that Re b = −∑_ρ Re(1/ρ) is not available for a non-real χ and must come from the functional equation. Three are named theorems.

4. The gamma sector was already hypothesised in Lean; only the prose omitted it. Both endpoints now have reasons.

Also fixed in passing: the ADS dependency row cited ArithmeticDirichletSeries.idealVonMangoldt, which does not exist.

Verification. The whole portfolio was built in one dependency-complete checkout — all sixteen open roadmap branches merged together, at their final state — and is green: lake build, 8798 jobs, exit 0, zero errors, 43 roadmap targets. This PR's own GitHub build check stays red on its unmerged supplier imports until they land, which is the merge order the portfolio note already asks for.

[CBirkbeck]

Current head: e78a1073248c187414890feb3b276a13ca850975

Verdict

Approve after the L-functions and contour-integration suppliers land.

The current revision is mathematically much stronger than the first one. The zero-free and explicit-formula arguments are now decomposed into named analytic steps, and the normalization of the zero count is correct.

A normalization point I checked explicitly

For the one-sided Dedekind-zeta zero count, the roadmap uses
$$
N_K(T)

\frac{T}{2\pi}
\log!\left(
|d_K|\left(\frac{T}{2\pi e}\right)^{[K:\mathbf Q]}
\right)
+O!\left(\log(|d_K|T^{[K:\mathbf Q]})\right).
$$

This is the standard formula in the convention counting positive ordinates. It is equivalently
$$
\frac{T}{\pi}
\log!\left(
|d_K|^{1/2}
\left(\frac{T}{2\pi e}\right)^{[K:\mathbf Q]/2}
\right)
+O(\cdots).
$$
Thus the present conductor coefficient and gamma coefficient are consistent; the earlier objection obtained by inserting a square root while leaving the rest of the logarithm unchanged would be wrong.

What I checked

The generic complex analysis is now separated from the arithmetic instances:

• gamma estimates with a fixed logarithm branch;
• order and finite-order predicates;
• Jensen zero counts;
• canonical products indexed by the divisor support;
• an entire logarithm for a nonvanishing entire function;
• Hadamard factorization with explicit convergence modes.

The family-specific steps no longer claim that a general analytic record has a zero-free region. The roadmap identifies exactly where positivity of Euler-product coefficients, the 3-4-1 inequality and the functional equation are used.

The Hecke zero-free region is especially careful:

• the three characters are first presented at one common modulus;
• imprimitive Euler factors are removed with a finite correction;
• real and non-real characters are treated separately;
• the relation between the Hadamard constants for $\chi$ and $\chi^{-1}$ replaces a false “reality” argument for non-real characters;
• the small-conductor range is isolated as a separate finiteness step.

The explicit formula records:

• all residues, including the order at zero;
• the exact trivial-zero multiplicities;
• the positive part of the divisor rather than the signed divisor in the zero sum;
• the test-function class and absolute summability;
• the exceptional-zero term in the prime ideal theorem.

The effective Chebotarev endpoint is restricted to the abelian/ray-class setting and is stated on the carriers supplied by the qualitative Chebotarev roadmap.

I found no remaining mathematical correction to request.