**[Classical — B1.]** The absolute Galois group of a `p`-adic local field is *topologically
finitely generated* (in fact by `[K : ℚ_p] + 2` elements).  For `K = ℚ₂` this is the
input `hfgG` that `main_presentation` feeds to `reconstruction`.

Citation: NSW [1], Ch. VII §7.4, Theorem (7.4.1) — for every `p`-adic local field `k`,
`G_k` is generated by `N+2` elements (`N=[k:ℚ_p]`).  This theorem applies at `p=2` and is the
direct source for the statement below.  Jannsen, *Invent. Math.* 70 (1982), Satz 3.2 and
Lemma 3.3, gives the weaker `N+3` bound, which would also suffice.  Verified against the cited
PDFs; the audit copies are not vendored in this repository.

This is a genuine, faithful Lean statement: it is exactly the topological-finite-generation
predicate used throughout `Reconstruction.lean`.  Paper: Lemma 2.5 (the `hfgG` input to the
reconstruction argument). 

**[Classical — B10 (oriented form, B10′).]**  The tame quotient of `G_ℚ₂`, *oriented
against local reciprocity*: a closed normal pro-2 subgroup `W ≤ G_ℚ₂` (wild inertia) with
`G_ℚ₂/W ≅ T_tame = ⟨σ, τ ∣ τ^σ = τ²⟩_prof`, whose unramified coordinate `ν_t` matches B5's
reciprocity normalization — `ν_t(tameF(rec u)) = 1` for units `u` and
`ν_t(tameF(rec 2)) = ztwoOne⁻¹` (arithmetic Frobenius, geometric coordinate).

Citation, existence: **NSW [1], Ch. VII §7.5, Theorem (7.5.3) (Iwasawa)** — `G(k_tr|k)` is the
profinite group on `σ, τ` with the single relation `στσ⁻¹ = τ^q` (`q = 2`); with
**(7.5.2)** (split extension `1 → Ẑ^{(p′)}(1) → G(k_tr|k) → Γ → 1`) and `G(k̄|k_tr)`
pro-`p` (Serre, *Local Fields* [7], Ch. IV).  Citation, orientation clauses:
**Serre, *Local Fields*, Ch. XIII §4, Proposition 13 and its corollary** (local reciprocity
maps units onto inertia and a prime element to Frobenius).  Neukirch, *Algebraic Number Theory*,
Ch. V, Theorem (6.2) concerns the higher unit filtration (`n > 0`), not the `n = 0` assertion;
use **Chap. V, (1.2)** / NSW [1] (7.1.2)(i) for units being norms in unramified extensions.
(Verified against the cited PDFs; the audit copies are not vendored in this repository.  The
Frobenius-direction convention `σ = geometric` and the clause encoding are documented at
`OrientedTameQuotient` in `GQ2/TameQuotient.lean`.)

The orientation clauses are part of this interface because they cannot currently be derived from
B5 alone without local ramification theory for `Field.absoluteGaloisGroup` in Mathlib.  Paper:
Prop. 3.2 local side +
Prop. 3.14 / Cor. 3.12 (the "same natural unramified character").
`docs/literature-axioms.md` B10. 

**[Classical — B11a.]**  The dyadic Hilbert-symbol **norm criterion** over a finite base
`k/ℚ₂`, in Kummer-cup form: for `a, b ∈ kˣ`, `[a] ∪ [b] = 0` in `H²(G_k, 𝔽₂)` iff `b` is a norm
from `k(√a)` — iff `b = x² − a y²` has a solution in `k` (for `a` a square the norm form is
universal, so no non-square hypothesis is needed).

Citation: Serre, *Local Fields* [7], Ch. XIV §2, Proposition 4(iii) (symbol vanishes iff the
second entry is a norm), Proposition 5 (the symbol is the cup product), and Proposition 7(iii)
(the multiplicative-root-of-unity form); over `ℚ_p` also CiA Ch. III §1.1 Prop. 1.
Paper: §6.3 (norm-criterion input to the local square-class calculation). 

**[Classical — B7 (local Euler–Poincaré characteristic).]**  For every finite discrete
`G_ℚ₂`-module `M`, the continuous cohomology groups `Hⁱ(G_ℚ₂, M)` are finite for `i = 0, 1, 2`,
and

  `#H¹(G_ℚ₂, M) = #H⁰(G_ℚ₂, M) · #H²(G_ℚ₂, M) · 2 ^ v₂(#M)`.

Equivalently `χ := #H⁰ · #H² / #H¹ = ‖#M‖_{ℚ₂} = 2 ^ (−v₂(#M))`.

Citation: **NSW [1], Ch. VII §7.3, Theorem (7.3.1) (Tate)** (`χ(k, A) = ‖#A‖_k`); Serre,
*Galois Cohomology*, Ch. II §5.7 Theorem 5; Milne, *ADT* Thm I.2.8.  Paper: §9.2, eq. (145).
See `GQ2/EulerCharacteristic.lean` for conventions and for the (retained-for-faithfulness)
redundancy of the `H⁰`-finiteness clause. 

**The B3c axiom** (composite interface — Labute [2], Théorème 4, case (2): `q = 2`,
`n = 3` odd, `f = 2`).
There is a B4 isomorphism `ψ : G_{ℚ₂}(2) ≅ D₀` and a continuous descent `χ₂` of the cyclotomic
character through `G_{ℚ₂} ↠ G_{ℚ₂}(2)`, surjective (image invariant `{±1} × U₂⁽²⁾ = ℤ₂ˣ`),
with values `(χ(A), χ(S), χ(Y)) = (−1, 1, (−3)⁻¹)` — the paper's `χ_D`-row of eq. (13)
(Lemmas 3.4/3.5).

**Composite classification** (`docs/adversarial-axioms-review.md` §3): this is **not** a bare
Labute citation.  It bundles
(a) Labute's orientation/classification values, (b) the local-Galois fact that the Demushkin
dualizing character equals the cyclotomic character (through *this* quotient map — Labute Thm 4
does not by itself assert `chiCyc`-compatibility), and (c) the choice of a **normalized** B4
isomorphism realizing (a)+(b) on the marked generators.  Consequently **B3c subsumes a marked
version of B4**: a downstream declaration whose `#print axioms` shows `dyadicOrientation` need
not *also* list B4 in its **Ax** column unless B4 is consumed independently (the review-packet
classification table, `docs/orchestration/review-packet.md` §2, records this).

Deviation (route (ii), flagged in `GQ2/Orientation.lean`): the *abstract* dualizing
characterization of the canonical character (Labute Prop. 6) is not formalized; the bundle
asserts exactly the interface the paper consumes.

Citation: Labute [2], Théorème 4 case (2) and Théorème 8 (Canad. J. Math. 19 (1967), 106–132);
dualizing character = cyclotomic through this quotient: NSW [1], Ch. VII §7.5, (7.5.11)–(7.5.12);
Serre [3].  Paper: Lemma 3.4 → Prop. 1.1.  `docs/literature-axioms.md` B3/B3c. 

**The B9 axiom** (Kahn Théorème 2 at rank 1, expanded by Evens Theorem 1 / Kozlowski
Thm 1.1 for index 2; paper eq. (111), degrees ≤ 2, at the Lemma 6.16 diagonalizations), over an
arbitrary **finite dyadic base** `k`.

Setting: `k/ℚ₂` finite (an `IntermediateField` of the fixed `ℚ̄₂`, so all classes live over the
subtype group `G_k = k.fixingSubgroup ≤ G_ℚ₂`), `L = k(δ)` with `δ² = d ∈ kˣ`, `G_L = N =` the
stabilizer of `δ` within `G_k` (assumed of index 2 — i.e. `d` is a non-square in `k`), `s ∉ N`,
and `a = u + vδ ∈ Lˣ` with norm `n = u² − dv² ∈ kˣ` and a square root `β = √a ∈ k̄ˣ`.  With
`[x] = kummerClassK k x` the base-general Kummer classes (canonical roots, `GQ2/EvensKahn.lean`),
`∪ = trivialCupPairing`, `cor = corH1` and `N^{Ev} = evensNormH2` (the unbundled forms; the
Kummer 1-cocycle `α(g) = κ_β(g)` of `a` over `N` enters via its defining equation `hαdef`, with
its hom/continuity side-proofs quantified), the two components of (111) read:

* degree 1: `[2u] + [2dn/u] = [2] + [2d] + cor[a]`;
* degree 2: `[2u] ∪ [2dn/u] = [2] ∪ [2d] + ([2] + [2d]) ∪ cor[a] + N^{Ev}[a]`.

The cited theorems hold over any field of characteristic different from `2` (Kahn Th. 2 requires
no local hypothesis), while the paper invokes (111) over the finite dyadic base `k` of Lemma 6.16.
The interface is therefore base-general within the dyadic setting; `k = ℚ₂` is the bottom-field
instance.

Citation: Kahn, Invent. Math. 78 (1984), Théorème 2 (with Théorème 1); Kozlowski, Proc. AMS
91 (1984), Thm 1.1; Evens, Trans. AMS 108 (1963), Thm 1.  Paper: §6, eq. (111),
Lemmas 6.13/6.16.  `docs/literature-axioms.md` B9. 

**The B5 axiom.** Local class field theory for `ℚ₂` provides the reciprocity bundle.

Citation: NSW [1] (7.1.1)/(7.1.5); Serre *Local Fields* [7] Ch. XI–XIII.  Paper: Lemma 3.5,
eq. (13); Prop. 1.1. 

**[Composite — B8.]** Local cyclotomic action on the peripheral inertia generators of
`Δ = π₁^{pro-2}(ℙ¹ ∖ {0,1,∞})`: for every `u ∈ ℤ₂ˣ` there is a continuous automorphism `φ_u` of `Δ`
sending each peripheral generator to a cyclotomic conjugate, `φ_u(P) = c_P⁻¹ · P^u · c_P` (and
likewise `T`, `C`), the `u`-th power via ẑ-exponentiation.  This is Lemma 3.6's group-theoretic
conclusion; see `GQ2/PeripheralAction.lean` for the deviation from the literal `π₁` statement.

**This is a composite leaf, not Stix alone** (`docs/adversarial-axioms-review.md` §1).  Stix
supports that the decomposition group acts on
cuspidal inertia *through the cyclotomic character*; producing an automorphism for **every**
`u ∈ ℤ₂ˣ` — the `aut : ℤ_[2]ˣ → ContinuousMulEquiv Δ Δ` field, quantified over all units —
additionally needs a **cyclotomic-surjectivity** input (a decomposition-group element realizing
each `u`).  Locally, B5 supplies this through `χ_cyc(rec u) = u⁻¹` and dense reciprocity image.
B8 keeps the all-units form because that is the interface consumed by Lemma 3.6.

Citation: **Stix [8], §3.3 + Definition 37** (cuspidal inertia acts through the cyclotomic
character — the paper's exact citation) together with local cyclotomic surjectivity from B5;
classical origin Deligne, MSRI 16 (1989).  Paper: Lemma 3.6.  `docs/literature-axioms.md` B8. 

**The B6 axiom (base-generalized to all finite `k/ℚ₂`).** Local Tate duality at any local
Galois group `G` over `ℚ₂` (`G_ℚ₂` or an open finite-index subgroup `G_K`, `K/ℚ₂` finite — the
`IsLocalDualizingGroup` hypothesis): an invariant map `inv : H²(G, μₙ) ≃+ ℤ/n` making the
evaluation cup pairings `Hⁱ(G, Hom(M, μₙ)) × H^{2−i}(G, M) → H²(G, μₙ) ≅ ℤ/n` perfect for every
finite discrete `n`-torsion `G`-module `M`, in the three degree pairs `(0,2)`, `(1,1)`, `(2,0)`.

NSW (7.2.6) states Tate duality for arbitrary `p`-adic `k`, so the interface is parametrized by a
local dualizing group rather than restricted to `ℚ₂`.  The base member `k = ℚ₂` is the
in-repository definition `GQ2.tateDuality` below.

Citation: **NSW [1], Ch. VII §7.2, Theorem (7.2.6)** (local Tate duality, for any `p`-adic `k`);
Serre, *Galois Cohomology* II §5.2, Theorem 2; Milne, *ADT* I.2.3.  Induced mod-2 Hilbert-pairing
nondegeneracy over `G_K`: FV Ch. IV §5 Prop (5.1)(6)/Cor./Thm (5.2), O'Meara
ITQF 63:13.  Paper: §§5–8 (the `𝔽₂` dimension counts) and §6.3;
`docs/literature-axioms.md` B6, `docs/orchestration/p15f7-axiom-proposal.md`.