B5: the local reciprocity bundle for `ℚ₂` #

This file states the paper's local class field theory input (leaf B5) as a single bundled axiom: the existence of the arithmetic local reciprocity map rec and the unramified coordinate ν_ur, satisfying the norm-residue property together with the two normalizations that the paper fixes in Lemma 3.5 / equation (13).

Everything here is a statement (definitions + one axiom + stress tests); nothing about reciprocity is proved (that is local CFT, absent from Mathlib — see docs/mathlib-cft-survey.md, §B5). The axiom asserts that the reciprocity data exists; the stress tests below derive the paper's equation (13) from it, so a human reviewer can check the bundle reproduces the paper's orientation/valuation rows without trusting the proof of reciprocity itself.

The bundle (paper Lemma 3.5, eq. (13); Prop. 1.1) #

LocalReciprocity packages continuous homomorphisms

rec : ℚ₂ˣ →* G_{ℚ₂}^{ab} (dense image), and
ν_ur : G_{ℚ₂}^{ab} →* Multiplicative ℤ₂ (continuous, surjective),

subject to the three clauses of the plan (docs/orchestration/formalization-plan.md, §B5):

(a) norm residue. For every finite abelian L/ℚ₂ inside ℚ̄₂, the induced map ℚ₂ˣ → Gal(L/ℚ₂) (i.e. rec followed by the abelianized restriction restrictAb) is surjective with kernel exactly the norm subgroup N_{L/ℚ₂}(Lˣ) (normSubgroup). This is the class-formation reciprocity of NSW [1] (7.1.1)/(7.1.5) (finite-level Gal(L/ℚ₂) ≅ ℚ₂ˣ / N Lˣ), and is aligned with the finite-level shape of the Oxford ClassFieldTheory project blueprint (this repo's ClassFieldTheory git dependency).
(b) unramified normalization. ν_ur ∘ rec = −v₂ (nu_ur_rec). Equivalently ν_ur(rec 2) = −1: rec sends the uniformizer 2 to arithmetic Frobenius, while ν_ur is normalized so that geometric Frobenius = arithmetic⁻¹ has coordinate +1 (paper's standing convention, line "νur is normalized geometrically"; Lemma 3.5 proof). Reproduces ν_ur(ā,s̄,ȳ) = (−2,1,0) of (13).
(c) cyclotomic orientation. χ_cyc ∘ rec = (·)⁻¹ on units (chiCyc_rec_unit) and χ_cyc(rec 2) = 1 (chiCyc_rec_uniformizer: the uniformizer acts trivially on the totally ramified ℚ₂(μ_{2^∞})/ℚ₂). Here χ_cyc is Mathlib's own cyclotomicCharacter … 2 (§clause (c) is a convention check against the real cyclotomic character, not an abstract one). Reproduces χ_D(ā,s̄,ȳ) = (−1,1,(−3)⁻¹) of (13), because χ_D = χ_cyc for a local Demushkin group.

Convention table (the #1 human-review target) #

rec — Lean object LocalReciprocity.rec — arithmetic: rec(2) = arithmetic Frobenius; rec a continuous hom into G^{ab} with dense image
ν_ur — Lean object LocalReciprocity.nu_ur — geometric: ν_ur(geom. Frob) = +1, so ν_ur(arith. Frob) = −1; target Multiplicative ℤ₂
v₂ — Lean object GQ2.v2 — Padic.valuation, so v₂(2) = 1, v₂(unit) = 0; clause (b) is ν_ur∘rec = −v₂
χ_cyc — Lean object GQ2.chiCyc / chiCycAb — Mathlib cyclotomicCharacter (AlgebraicClosure ℚ₂) 2 : g ↦ (ζ ↦ ζ^{χ(g)}); values in ℤ₂ˣ
G^{ab} — Lean object GQ2.AbsGalQ2ab — Mathlib absoluteGaloisGroupAbelianization ℚ₂ = G ⧸ closure⁅G,G⁆ (topological abelianization)
x^g, [x,y] — (inherited) — x^g = g⁻¹xg, [x,y] = x⁻¹y⁻¹xy (paper's standing conventions)

Soundness note (a real trap, cf. the Nat.card bug). ν_ur must target a profinite group (ℤ₂), never ℤ: G^{ab} is compact, and a continuous hom from a compact group to discrete ℤ is forced trivial — so clause (b) with target ℤ would be inconsistent (the axiom would prove False). Targeting Multiplicative ℤ₂ (with −v₂ embedded via ℤ ↪ ℤ₂) is what makes the bundle consistent.

Deviations flagged for review.

Injectivity of rec (true in the literature) is not asserted; it follows from clause (a) as L ranges over all finite abelian extensions (⋂_L N_{L/ℚ₂}Lˣ = 1). We keep the bundle minimal.
ν_ur, χ_cyc and the per-L restrictions are stated on the topological abelianization G^{ab}; rec lands there (its image is abelian). χ_cyc/restrictAb factor Mathlib's full-group chiCyc/restrictNormalHom through G^{ab} (chiCycAb_toAb, restrictAb_toAb).

References: [1] Neukirch–Schmidt–Wingberg, Cohomology of Number Fields, 2nd ed., (7.1.1)/(7.1.5) (class formation ⇒ local reciprocity); [7] Serre, Local Fields, Ch. XI–XIII. Paper: Turturean, Lemma 3.5, eq. (13); Prop. 1.1.

Note: the axiom GQ2.localReciprocity itself lives in GQ2/Foundations/Axioms.lean; this file holds the bundle definition and the axiom-free, bundle-parametrized stress tests.

B5: the local reciprocity bundle for ℚ₂ #

The bundle (paper Lemma 3.5, eq. (13); Prop. 1.1) #

Convention table (the #1 human-review target) #

The abelianized absolute Galois group and the maps out of it #

The 2-adic cyclotomic character on G_{ℚ₂} and its abelianization #

The 2-adic valuation on ℚ₂ˣ #

Norm subgroups and the abelianized restriction to a finite layer #

Embedding ℤ₂ˣ and the uniformizer into ℚ₂ˣ #

The reciprocity bundle #

Stress tests: the bundle reproduces the paper's equation (13) #

Paper-tag ledger (auto-generated by paperforge; do not edit) #

B5: the local reciprocity bundle for `ℚ₂` #

The 2-adic cyclotomic character on `G_{ℚ₂}` and its abelianization #

The 2-adic valuation on `ℚ₂ˣ` #

Embedding `ℤ₂ˣ` and the uniformizer into `ℚ₂ˣ` #