Mathlib prerequisites scoping: class field towers and Golod-Shafarevich (follow-up to #20516)

[rjwalters]

Background

Follow-up to #20516 (acceptance criterion #4b).

The OpenAI 2026-05-20 construction reportedly disproving Erdős's unit-distance conjecture (#20516) relies on infinite class field towers, guaranteed to exist by the Golod–Shafarevich theorem when the class group's ℓ-rank exceeds a bound depending on the discriminant. Formalizing this construction in Lean 4 / Mathlib (see #20576) requires the following infrastructure, which may or may not already exist in Mathlib.

This issue scopes which prerequisites exist, which are partially formalized, and which are entirely missing.

Scope

For each of the following Mathlib areas, audit the current state and report:

1. Algebraic number theory basics: NumberField, RingOfIntegers, Mathlib.NumberTheory.NumberField.*
2. Class group: ClassGroup, finiteness, ℓ-torsion subgroups
3. Class field theory: Hilbert class fields, idele class groups, Artin reciprocity
4. Class field towers: explicit definition and infinitude criteria
5. Golod–Shafarevich theorem: pro-ℓ groups, inequalities on generators and relations, application to class field towers
6. Dirichlet's unit theorem: rank of unit groups in rings of integers
7. Embeddings: complex / real embeddings of number fields, Minkowski embedding into ℝⁿ

Acceptance Criteria

• Audit table produced: for each item above, classify as complete, partial, missing, or out-of-scope.
• For missing items, estimate effort (lines, person-weeks).
• For partial items, list specific lemmas/definitions still needed.
• Cross-reference any in-progress Mathlib PRs working on these topics.
• Final report attached as a comment with markdown table.

Notes

• This is a scoping issue, not a formalization issue. Output is a written audit, not Lean code.
• The Mathlib PR tracker (https://github.com/leanprover-community/mathlib4/pulls) and the Mathlib4 documentation are primary sources.
• Useful starting points: Mathlib.NumberTheory.ClassNumber.*, Mathlib.NumberTheory.NumberField.Units.*.

Test Plan

• Audit report posted as a comment on this issue.
• Each item has a state and (where applicable) a Mathlib file path or PR reference.
• Estimates are provided for missing prerequisites.

Affected Files

• This issue itself (comment with the audit report).
• No code changes in this repo. Findings will inform planning for Lean formalization of OpenAI 2026 unit-distance lower-bound construction (follow-up to #20516) #20576.

[rjwalters]

Companion to #20576 (Lean formalization). Parent: #20516.

[rjwalters]

Curator enrichment (scope clarification, references, estimates)

This is a scoping/audit issue — the deliverable is a written report (markdown table posted as a comment), not Lean code. It is well-formed and concrete enough for a researcher/scout to pick up. Adding pointers and estimates below.

Recommended workflow

1. Clone mathlib4 (or use the deployed docs at https://leanprover-community.github.io/mathlib4_docs/) and grep each subtree listed in Scope.
2. Cross-reference open PRs on https://github.com/leanprover-community/mathlib4/pulls using keywords (class field, Hilbert class field, Golod, Shafarevich, idele, Artin reciprocity).
3. Produce the audit as a single markdown comment on this issue with the schema below.

Suggested audit table schema

#	Topic	Mathlib path(s)	State	Missing lemmas / Notes	Effort estimate
1	NumberField / RingOfIntegers	...	complete/partial/missing/oos	...	n/a or X person-weeks

Starting points by item

1. NumberField / RingOfIntegers — Mathlib/NumberTheory/NumberField/Basic.lean, Mathlib/NumberTheory/NumberField/Embeddings.lean. Expected: complete.
2. Class group — Mathlib/NumberTheory/ClassNumber/{Basic,AdmissibleAbs,Finite,FunctionField,NumberField}.lean. ClassGroup K, finiteness (ClassGroup.fintype) present. ℓ-torsion subgroups (AddCommGroup.torsionBy / Submonoid.torsion) generic in Mathlib/GroupTheory/Torsion.lean — composing with ClassGroup likely needs a small adapter. Expected: partial.
3. Class field theory — Hilbert class fields, idele class groups, Artin reciprocity. As of late-2025 Mathlib has local class field theory work in progress (Mathlib/NumberTheory/LocalClassFieldTheory/*) and partial idele content under Mathlib/NumberTheory/NumberField/Adele.lean / IsAdmissible. Global Artin reciprocity is widely expected to be missing or only fragmentarily present — verify by searching for ArtinReciprocity, HilbertClassField, IdeleClassGroup.
4. Class field towers — explicit definition (the sequence $K = K_0 \subseteq K_1 \subseteq \ldots$ where $K_{i+1}$ is the Hilbert class field of $K_i$) and infinitude criteria. Almost certainly missing; depends on item 3.
5. Golod–Shafarevich — pro-$\ell$ groups, generator/relation inequality $r \ge \tfrac14 d^2$ (or refinements), application to class field towers. Search Mathlib/GroupTheory/, Mathlib/Topology/Algebra/Group/Profinite.lean. Expected: missing (this is the deepest gap).
6. Dirichlet's unit theorem — Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean (rank, regulator, fundamental units). Expected: complete or near-complete — verify the precise statement of NumberField.Units.rank_modTorsion.
7. Embeddings / Minkowski — Mathlib/NumberTheory/NumberField/Embeddings.lean, Mathlib/NumberTheory/NumberField/CanonicalEmbedding/*, Mathlib/NumberTheory/NumberField/Discriminant/*. Expected: complete for the canonical embedding; Minkowski lattice / convex-body theorem present in Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean.

Search commands a curator/researcher can run

# In a mathlib4 checkout:
rg -l "HilbertClassField|ArtinReciprocity|IdeleClassGroup|ClassFieldTower" Mathlib/
rg -l "Golod|Shafarevich|proL|Pro.*Group" Mathlib/
rg "structure ClassGroup|def ClassGroup" Mathlib/NumberTheory/
gh pr list --repo leanprover-community/mathlib4 --search "class field" --state all --limit 30
gh pr list --repo leanprover-community/mathlib4 --search "Golod" --state all --limit 30

Estimated total effort for a single auditor

• Reading + grepping Mathlib: 4–8 hours
• Triaging open PRs and writing the table: 2–4 hours
• Realistic single-sitting deliverable: 1 person-day

This is bounded scope; no Lean compilation required.

Why this is loom:curated (not loom:triage)

• Concrete deliverable (markdown audit table) defined in acceptance criteria.
• Clear list of 7 items to audit.
• No code changes required; no build risk.
• Researcher/scout can pick this up without further design discussion.

Suggested additional label

Consider adding epic:mathlib since the deliverable directly informs which Mathlib contributions would be needed; leaving that to the human approver.