Add roadmap: Chebotarev density theorem

[roed-math]

Dependencies: This roadmap depends on Number-Field Arithmetic #191, Arithmetic Dirichlet Series #192, and Global Number Fields #245. It should be reviewed and merged after those supplier PRs. The inherited supplier order includes #192; #188 → #244 → #189 → #191 → #245.

Summary

This roadmap develops Chebotarev density and qualitative prime counting from the portfolio's canonical Frobenius and analytic interfaces. It builds Frobenius prime sets for conjugacy classes, the cyclotomic and abelian cases, fixed-field reduction to the general Dirichlet-density theorem, Frobenius von Mangoldt coefficients, ϑ_C, ψ_C, and π_C, and qualitative natural-density Chebotarev.

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

Ownership

It consumes the sole finite-level Frobenius and Artin carrier from #191, generic density and Tauberian tools from #192, and ray/congruence counting from Global Number Fields. It owns Chebotarev prime sets and qualitative Dirichlet- and natural-density/counting theorems. It does not own generic density, Hecke L-functions, zero-free regions, or effective error terms.

Port history and prior art

This is a clean port of roed-math/TauCetiRoadmap#18, rebased onto upstream main. It combines corrected material extracted from the former L-functions roadmap with the dedicated architecture and permitted density formalization recorded in #181, targeting Mathlib's current IsArithFrobAt and NumberField.Set.HasDirichletDensity APIs. AINTLIB's Dirichlet-density Chebotarev development is identified in the README as prior art, and the roadmap now names the Dirichlet-primes-in-arithmetic-progressions density corollary obtained by comparison with Mathlib. The non-normative PROVENANCE.md is omitted; detailed source and licensing records remain private.

Human review priorities

• conjugacy-class rather than chosen-Frobenius semantics;
• normalization by the all-prime Dirichlet sum;
• the prime-power test Frob(𝔭)^j ∈ C, including the cyclic degree-four guard;
• the fixed-field restriction direction, exceptional set, exact fibre cardinality, and cyclotomic linear-disjointness crossing;
• the Dirichlet primes-in-arithmetic-progressions corollary and complete ψ → ϑ → π qualitative summit.

Validation

• lake -Kjobs=1 build TauCetiRoadmap.Chebotarev.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, including licensing records, is maintained privately. No unlicensed or unconfirmed external code was copied into this roadmap.

[CBirkbeck]

I think if we remove the PROVENANCE.md then we should put in the readme some notes about where the code comes from (I guess this is true in the other roadmaps). For example the dirichlet version of Chebotarev is all in AINTLIB. Also, I couldn't see it mentioned but we should also add the corollary that gives the density for Dirichlets primes in AP theorem.

[roed-math]

GPT-5.6 Sol: Addressed in 81e4db4. The README now identifies AINTLIB's Dirichlet-density Chebotarev development as prior art and points to Mathlib's Dirichlet-primes-in-arithmetic-progressions theorem. Suggested.lean now exports the corresponding density corollary, using Mathlib's NumberField.Set.HasDirichletDensity carrier.

[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 #191, #192 and #245.

The route is deliberately independent of class field theory and Artin L-functions, uses the fixed-field / cyclotomic-crossing reduction, and keeps conjugacy classes rather than chosen Frobenius elements. The counting carriers and the local-to-global tower formulas are carefully pinned.

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 #249

Roadmap: Chebotarev density theorem

Head reviewed: 81e4db42f1ab241394721b2605082b93a0cf36ec

PR #249 — Chebotarev density theorem

Verdict

No new mathematical changes requested. The roadmap should remain stacked after #191, corrected #192, and corrected #245. The nonabelian reduction is now stated at the right conjugacy-class level.

What I checked

1. Prime-set carrier

The primary object is a set of unramified height-one primes whose Frobenius conjugacy class is the target class. No chosen prime above 𝔭 appears in the definition.

2. Arithmetic Frobenius convention

The roadmap consumes the unique convention from Number-Field Arithmetic and does not invert Frobenius in the density theorem.

Cyclotomic tests compare

$$\zeta_m\longmapsto\zeta_m^{N\mathfrak p}.$$

3. Abelian case

The abelian proof is routed through ray-class/character data and generic Dirichlet-series tools. It must retain its explicit nonvanishing-at-one argument; it cannot infer prime distribution merely from counting all ideals in ray classes.

The current roadmap names this analytic step rather than treating uniform ideal counting as prime counting.

4. Fixed-field reduction

For an element g in the target conjugacy class, the fixed field of the cyclic subgroup ⟨g⟩ is used. The roadmap tracks:

• restriction of primes;
• the exceptional ramified set;
• residue-degree-one primes;
• exact fibre cardinalities;
• the centralizer/conjugacy factor.

This is the essential nonabelian argument.

5. Degree-above-one primes

Primes of residue degree greater than one contribute a density-zero/error term when moving between the fixed field and the base. The relevant estimate is consumed from the analytic supplier.

6. Prime powers

The Frobenius von Mangoldt coefficient tests

$$\operatorname{Frob}_{\mathfrak p}^{\,j}\in C$$

for the j-th prime power. It does not incorrectly replace this by Frob∈C.

The cyclic degree-four example is a useful guard: powers can enter or leave a conjugacy class.

7. Dirichlet versus natural density

Dirichlet density is proved first. The ψ→ϑ→π summit uses the Tauberian boundary input and removes higher prime powers before claiming natural density.

Natural density is not inferred formally from Dirichlet density.

8. Cyclotomic crossing

The linear-disjointness and restriction maps are named when translating to rational primes in arithmetic progressions. This prevents an incorrect one-to-one identification of prime ideals and rational primes.

9. Scope

No effective error term, zero-free region or Artin L-function is claimed here. Those remain downstream.

Dependency warning

The roadmap is only as complete as the ray-class and analytic suppliers. In particular:

• #245 must provide the exact ray-class/Hecke-character carriers and the geometric count without the order-theory error;
• #192 must correct its weight carrier;
• the abelian nonvanishing theorem must remain explicit in #249 or be imported from #248.

This is a dependency condition, not a new mathematical objection to #249's present architecture.

Sources checked

• J. Neukirch, Algebraic Number Theory, Chapter VII.
• J.-P. Serre, Topics in Galois Theory.
• Classical fixed-field proofs of Chebotarev.
• The existing AINTLIB Dirichlet-density formalization as prior art.

Disposition

Approve after its three suppliers.

[roed-math]

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

No review request outstanding — a one-line build fix, pushed as 1a8eda1, found by building the whole portfolio in one dependency-complete checkout. No milestone or statement changes.

Layer 4's cyclotomicCharacterWeight returned ArithmeticDirichletSeries.IdealWeight, a declaration the accepted #192 does not have: its carrier is MultiplicativeIdealWeight. Lean reports it as an unknown identifier, so this file did not elaborate against the merged supplier at all. Renamed, and the ramified-prime vanishing statement now applies the weight through the supplier's CoeFun rather than through a .toFun projection that does not exist either. The contract table in README.md follows.

Verification. In the dependency-complete stack, lake build TauCetiRoadmap.Chebotarev.Suggested is green. git diff --check passes.

Merge order. Unchanged: #192 (merged), #191 and #245 → this.

[CBirkbeck]

Verdict

Request changes.

The cyclotomic → abelian crossing → general fixed-field route is a good proof architecture. The remaining issue is that the crossing field is not guaranteed to have the degree used in the argument, and the weighted crossing is much less formal than the roadmap currently suggests.

1. The auxiliary cyclotomic extension needs two disjointness conditions

The roadmap chooses a prime q with

[
L\cap K(\zeta_q)=K
]

and then treats

[
\operatorname{Gal}(K(\zeta_q)/K)
]

as having order q-1.

The displayed intersection only gives disjointness of L/K from K(\zeta_q)/K. It does not imply

[
K\cap\mathbf Q(\zeta_q)=\mathbf Q.
]

Without the latter, [K(\zeta_q):K] can be a proper divisor of q-1.

A clean choice is a rational prime q unramified in K and L, outside the finite exceptional set. Every nontrivial subfield of Q(ζ_q) is ramified at q, so then
K ∩ Q(ζ_q)=Q. The roadmap needs an exact theorem producing such a q with the additional congruence conditions used in the crossing argument.

2. State the theorem which produces the auxiliary prime

“Choose a sufficiently large prime” hides:

• infinitude of primes in the required congruence class;
• avoidance of the ramified primes of K and L;
• the cyclotomic intersection argument;
• any size inequality used to separate group-theoretic fibres.

This should be one named arithmetic lemma with all conditions in its conclusion.

3. The weighted crossing for ψ_C is not the same as the prime-set crossing

The set-theoretic fixed-field argument compares unramified prime ideals and Frobenius classes. The logarithmic derivative counts prime powers:

[
\sum_{\mathfrak p,m}
1_{\mathrm{Frob}_{\mathfrak p}^m\in C}
\log N\mathfrak p.
]

Under extension and contraction, residue degrees and powers interact. The roadmap needs separate lemmas for:

• primes with residue degree one;
• higher residue-degree primes;
• ramified primes;
• prime powers with m>1;
• the error contributed by all discarded terms.

Only after those estimates can the weighted asymptotic be transferred. It should not be described as a formal corollary of the prime-set crossing.

4. Keep the Frobenius convention visible in the Artin-character reduction

The roadmap correctly uses arithmetic Frobenius. The character expansion and the fixed-field restriction must preserve that convention. In particular, every restriction formula should say whether it sends Frobenius to a power determined by residue degree. This is a common inverse/power error and deserves a worked example in a tower.

5. Separate qualitative and effective statements

The current roadmap should end with the qualitative asymptotic and density. Error terms belong to Zeros of L-functions. The interface should make this boundary exact rather than carrying optional “effective” placeholders.

What is good

The corrected prime-power coefficients, the regularization
[
-L_1'/L_1-\frac1{s-1},
]
the ramified Euler correction, and the use of a nonzero-prime subtype should remain. The general fixed-field fibre count is also the right finite group statement.

Recommendation

Add the full auxiliary-prime theorem and a genuine weighted-crossing package. With those in place, the proof architecture is sound.

[roed-math]

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

Addressed in 7fcc3c0. Both gaps were real, and a third turned up.

1–2. The auxiliary prime. You are right that L ∩ K(ζ_q) = K gives only disjointness and not [K(ζ_q):K] = q − 1. exists_auxiliaryPrime now carries every condition in its conclusion: N < q, q ≡ 1 (mod n), n ∣ q − 1, q unramified in K and in L, and irreducibility of cyclotomic q K — the ambient-field-free form of K ∩ ℚ(ζ_q) = ℚ. 7.2 derives the degree in the stated order, and 7.3 now proves L ∩ K(ζ_q) = K from totally-ramified-meets-unramified rather than assuming it. The ⚠ carries the witness K = ℚ(√5), L = K(√2), q = 5 with its subfield lattice, pinned in Lean.

3. The weighted crossing. ϑ_C moved to 11.2 (Layer 12 consumes it, so its old position was a forward reference), and 11.3 states the four discard estimates separately — prime powers j ≥ 2, residue degree ≥ 2, a finite prime set, and their sum. 12.3 gives the exact residue-degree-one contraction, with the ⚠ that no ψ-level identity exists: for m ≥ 2 the fibre is supported on classes w with wᵐ = σ, not on C — in a cyclic quintic a prime with Frobenius g³ feeds the g fibre.

4. Frobenius convention. Two convention rows separate shrinking the top field (no power) from raising the base (power f(𝔓/𝔭)), with the tower ℚ ⊂ ℚ(√−7) ⊂ ℚ(ζ₇) at p = 3 worked out so both misreadings are rejected, discharged by decide.

5. Boundary with #253. There were no "optional effective" placeholders to drop, so instead the boundary is made exact: the five carriers #253 consumes and the two theorems it rederives are named, with three explicit consequences.

A false theorem found while doing this. fixedFieldExceptionalPrimes was ramifiedPrimes E L, which makes frobeniusPrimeSet_preimage_fixedField false: a prime 𝔓 can be unramified in L/E while 𝔭 ramifies in L/K. Witness K = ℚ, L = ℚ(∛2, ζ₃), σ = (1 2) so E = ℚ(∛2), p = 2: e(Q/2) = 3, e(𝔓/2) = 3, e(Q/𝔓) = 1. Now the primes above ramifiedPrimes K L. Layers 8 and 9 are also swapped so the fibre count precedes the crossing that consumes it.

One question for you. ADS states the prime ideal theorem only conditionally, but this roadmap needs ψ_K(x) ~ x and π_K(x) ~ x/log x. Both are derived internally as the trivial-Galois-group case of Layer 12.2 rather than importing a boundary package, and 12.2 and 14 say so. If you would rather Chebotarev depend on LFunctions for this, those are the two places to change.
Open for the maintainers: whether Chebotarev should derive ψ_K(x) ~ x and π_K(x) ~ x/log x internally (as it now does, from the trivial-Galois case of Layer 12.2) or import them from LFunctions. Layers 12.2 and 14 are the two places to change.

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.

[roed-math]

🤖 Claude Opus 5, on David Roe's behalf — resolving the question my previous comment left open.

Decision: the prime ideal theorem inputs stay derived internally. ψ_K(x) ~ x and π_K(x) ~ x/log x remain the trivial-Galois-group case of Layer 12.2, as committed. Reasons: no roadmap exports the unconditional statement (ArithmeticDirichletSeries states it only against a boundary package), so importing would be citing a theorem that does not exist; and the derivation here is one specialization of a limit this roadmap proves anyway, not a second development. Layers 12.2 and 14 record the decision, so if LFunctions later exports an unconditional prime ideal theorem, those are the two places that switch to consuming it.

[CBirkbeck]

Current head: 7fcc3c0408703ccde38db324ba3faa24924d29fa

Verdict

Approve after the stated arithmetic and $L$-function suppliers land.

The cyclotomic-crossing proof is now specified carefully enough to be implemented without silently assuming a false linear-disjointness statement.

What I checked

The auxiliary-prime theorem now produces all of the properties used later:

• a congruence $q\equiv1\pmod{f^r}$;
• avoidance of a prescribed bound;
• unramifiedness in the relevant number fields;
• irreducibility of $\Phi_q$ over the base field, hence the full cyclotomic degree;
• the second intersection $L\cap K(\zeta_q)=K$ as a theorem derived from ramification.

This fixes the earlier counterexample in which $L\cap K(\zeta_q)=K$ held but the cyclotomic degree over $K$ was too small.

The group-theoretic crossing is also explicit:

• tagged elements are those whose order is divisible by the fixed residue degree;
• their exact count in a cyclic group is proved;
• the lower bound tends to the desired constant only after the auxiliary level grows;
• the fixed-field step uses the relative Frobenius power correctly;
• the exceptional contraction set consists of all primes above the original ramified set.

The weighted argument no longer treats the von Mangoldt crossing as a formal consequence of the prime-set crossing. Prime powers, residue-degree $>1$ terms, ramified primes and the two sides of the contraction are estimated separately.

The qualitative/effective boundary is now clean. This roadmap proves density and asymptotic prime counting without an error term. The Zeros roadmap owns effective estimates on the same named carriers.

I found no remaining mathematical correction to request.