Foundational corpus mapping FC09 Neukirch

Status: Sweep II complete. C01–C07 complete.

Canonical catalogue: FC09 — Neukirch, Algebraic Number Theory.

Pinned project baseline: Mathlib db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0. Current Mathlib was refreshed 2026-09-07 to 71a80585ee495fc24472fd0eaffc89d94e4fd8d6; declarations first appearing after the project pin are revision-specific reference-port routes unless an importable package route is independently justified.

Every canonical unit receives exactly one Sweep-II route: mathlib, project-existing, package-import, reference-port, or unmatched. Project source is searched first, followed by pinned/current Mathlib, open/current work, and targeted external Lean discovery. Strict bundle semantics apply throughout.

Provenance contract for FC09 C01

Chapter 1. Algebraic Integers FC09

Provenance contract for FC09 C02

Chapter 2. Valuations FC09

Provenance contract for FC09 C03

Chapter 3. Riemann-Roch Theory FC09

Provenance contract for FC09 C04

Chapter 4. Abstract Class Field Theory FC09

Provenance contract for FC09 C05

Chapter 5. Local Class Field Theory FC09

Provenance contract for FC09 C06

Chapter 6. Global Class Field Theory FC09

Provenance contract for FC09 C07

Chapter 7. Zeta Functions and L-series FC09