Discharged and derived interfaces over the literature axioms #
Companion to GQ2/Foundations/Axioms.lean — the census file, which since 2026-07-27 contains
the nine axiom declarations and nothing else. This file hosts the derived layer that
shares the axioms' public interface:
- the formerly-axiom interfaces discharged by in-repository proofs, under their original
names —
HilbertSymbol.hilbertSymbol_dyadic(B7′),unramifiedQuadratic_units_are_norms(B11b),kummerClassK_surjective(B12),dyadicUnitFiltration(B13); evensKahn_dyadic— the pre-2026-07-24 B9 axiom, re-derived byte-identically from the current B9 leafrelativeStiefelWhitney_dyadictogether with B11a;tateDuality— thek = ℚ₂member of the B6 axiomtateDualityAt;- the
HasEqualNormValueGroupsconventiondef, its negative stress test, and the combineddyadicNormCriterion.
Every name is unchanged from when these declarations lived in Axioms.lean, so consumers
needed no migration; importers of the old combined file now import this one (a strict API
superset, since GQ2.Foundations.Axioms is a public import above). The split exists for
auditability: the proofs collected here are what pulled the proof layer into the axiom
file's transitive imports, and after the split the axiom file's import closure is its
statement vocabulary only. Census history and citations remain with the axioms and in
docs/literature-axioms.md.
B7′ — the dyadic Hilbert-symbol formula #
hilbertSymbol, ε, ω, unit2, unitCoe, signOf and their unconditional theory live in
GQ2/HilbertSymbol.lean.
The dyadic Hilbert symbol formula, formerly interface B7′.
Writing a = 2^α u, b = 2^β v with u, v ∈ ℤ₂ˣ, the Hilbert symbol over ℚ₂ is
(a, b)₂ = (-1)^{ε(u) ε(v) + α ω(v) + β ω(u)}.
Citation: Serre, A Course in Arithmetic [CiA], Ch. III §1.2, Theorem 1 (the p = 2
case), with ε, ω the residue characters of Ch. II §3.3. This is exactly the paper's
Lemma 3.5 formula for the cup product on H¹(ℚ₂, μ₂). Convention: signOf sends the
𝔽₂-valued exponent to {±1} = ℤˣ; every element of ℚ₂ˣ has the form 2^α u (α ∈ ℤ,
u ∈ ℤ₂ˣ), so this determines the symbol on all of ℚ₂ˣ × ℚ₂ˣ.
The theorem delegates to hilbertSymbol_dyadic' in GQ2/HilbertSymbolDyadicClose.lean, whose
proof uses 2-adic Hensel lifting, the norm-form identity (a,b) = (a,−ab), and finite mod-8
computations.
B6 at the base field — the G = G_ℚ₂ member of the axiom tateDualityAt #
B6 at the base field ℚ₂ — the G = G_ℚ₂ member of tateDualityAt, using
isLocalDualizingGroup_absGalQ2.
Equations
Instances For
The B11 convention layer and the discharged B11b #
The full B11 conventions and citations are with the B11a axiom in
GQ2/Foundations/Axioms.lean; this section holds the pieces that are not axioms.
Equal norm value groups for k(δa)/k — the project's unramifiedness criterion. Every
nonzero z = x + y·δa (x, y ∈ k) has the same norm as some nonzero element of the base k,
i.e. k(δa) and k have equal norm value groups. For a quadratic extension of complete
discretely valued fields this says e(k(δa)/k) = 1, the standard unramifiedness criterion
(Serre, Local Fields, Ch. I §4); the definition is named by what it literally asserts because
the equivalence with a bona-fide ramification-theoretic notion is not proved here (no Mathlib
ramification theory applies at these types yet — IsNonarchimedeanLocalField has no
extension/ramification layer as of 2026-07-24). This is not a Mathlib unramifiedness notion
and is asserted by nothing (it is a def, not an axiom); it is the convention the §6 ledger
consumes, named and isolated per adversarial review rec 2 so a human reviewer can see exactly
where the project departs from a directly citable statement. Named
IsUnramifiedQuadraticSpectral before 2026-07-24 (deprecated alias below).
Equations
- GQ2.HasEqualNormValueGroups k δa = ∀ (z : AlgebraicClosure ℚ_[2]), z ≠ 0 → (∃ (x : ↥k) (y : ↥k), z = ↑x + ↑y * δa) → ∃ (w : ↥k), w ≠ 0 ∧ ‖z‖ = ‖↑w‖
Instances For
Alias of GQ2.HasEqualNormValueGroups.
Equal norm value groups for k(δa)/k — the project's unramifiedness criterion. Every
nonzero z = x + y·δa (x, y ∈ k) has the same norm as some nonzero element of the base k,
i.e. k(δa) and k have equal norm value groups. For a quadratic extension of complete
discretely valued fields this says e(k(δa)/k) = 1, the standard unramifiedness criterion
(Serre, Local Fields, Ch. I §4); the definition is named by what it literally asserts because
the equivalence with a bona-fide ramification-theoretic notion is not proved here (no Mathlib
ramification theory applies at these types yet — IsNonarchimedeanLocalField has no
extension/ramification layer as of 2026-07-24). This is not a Mathlib unramifiedness notion
and is asserted by nothing (it is a def, not an axiom); it is the convention the §6 ledger
consumes, named and isolated per adversarial review rec 2 so a human reviewer can see exactly
where the project departs from a directly citable statement. Named
IsUnramifiedQuadraticSpectral before 2026-07-24 (deprecated alias below).
Instances For
Negative stress test for HasEqualNormValueGroups (adversarial-review plan U1): the
ramified quadratic extension ℚ₂(√2)/ℚ₂ fails the criterion, so the predicate is not
vacuously satisfied — it genuinely detects e = 1. Take the base k = ⊥ (every element is the
image of a 2-adic scalar) and δa any square root of 2 in ℚ̄₂. The witness z = δa
(= ↑0 + ↑1·δa) has ‖δa‖² = ‖δa²‖ = ‖(2 : ℚ̄₂)‖ = ‖(2 : ℚ₂)‖, while every nonzero w ∈ ⊥ is
algebraMap c for some c ∈ ℚ₂ with ‖w‖ = ‖c‖ in the discrete value group {2ⁿ : n ∈ ℤ}.
A match ‖δa‖ = ‖w‖ would give ‖(2 : ℚ₂)‖ = ‖c²‖, i.e. v₂(2) = v₂(c²), i.e. 1 = 2·v₂(c)
in ℤ — impossible. Contrast unramifiedQuadratic_units_are_norms, whose conclusion the
criterion supplies precisely in the unramified case it does hold.
B9, derived form (the pre-flip axiom, now a theorem over B9 + B11a) #
Formerly the B9 axiom — since 2026-07-24 a derived theorem (the B9-A flip; the statement
is byte-identical to the pre-flip axiom, zero consumer churn — the B7′/B11b/B12/B13 pattern).
Eq. (111) at the paper's Lemma 6.16 diagonalizations Tr_{L/k}⟨a⟩ ≃ ⟨2u, 2dn/u⟩,
Tr_{L/k}⟨1⟩ ≃ ⟨2, 2d⟩, with w₁⟨x,y⟩ = [x]+[y] and w₂⟨x,y⟩ = [x] ⌣ [y]:
- degree 1:
[2u] + [2dn/u] = [2] + [2d] + cor[a]; - degree 2:
[2u] ⌣ [2dn/u] = [2] ⌣ [2d] + ([2] + [2d]) ⌣ cor[a] + N^{Ev}[a].
Proof: evensKahn_dyadic_of_rsw (GQ2/EvensKahnDerived.lean) applied to the B9 axiom
relativeStiefelWhitney_dyadic and to B11a (the hnorm input of the Delzant well-definedness
layer); the T2 trace-form diagonalizations and the proved swOne/swTwo invariance do the
rewriting. #print axioms: relativeStiefelWhitney_dyadic and
hilbertSymbol_normCriterion_finiteDyadic (+ the standard three). Full setting and citations:
the B9 axiom's docstring in GQ2/Foundations/Axioms.lean and docs/literature-axioms.md §B9.
Unramified unit-norm surjectivity, formerly interface B11b. If
k(√a)/k is unramified (the HasEqualNormValueGroups convention on a chosen root δa,
δa² = a), then every unit of k (‖u‖ = 1) is a norm from k(√a) — i.e. u = x² − a y² is
solvable in k.
Citation: Serre, Local Fields [7], Ch. V §2 (norms of unramified extensions are the units times the norms of uniformizers). Paper: §6.3 (unramified-norm input to the local calculation).
The proof in GQ2/UnramifiedQuadraticNorms.lean completes the square using the involution
σδ = −δ, then constructs a depth-by-depth norm-form approximation
wₙ₊₁ = wₙ(1 + πⁿ⁺¹z₀) against the dyadic unit filtration. Exact trace coverage
z ↦ z + σz supplies each increment.
The combined dyadic norm criterion. This theorem pairs the classical B11a leaf with the
proved unramified-unit theorem. The equal-norm-value-groups convention remains isolated in
HasEqualNormValueGroups (named IsUnramifiedQuadraticSpectral before 2026-07-24), which is a
definition rather than an axiom.
In-repository Kummer and unit-filtration interfaces #
Lemma 6.17 uses local Kummer surjectivity and the graded structure of the dyadic unit filtration.
Both interfaces are constructed below from in-repository proofs. The surrounding
DeepKummerData assembly is developed in GQ2/LocalKummer.lean; its remaining inputs include
coprime averaging, the Hensel square criterion, graded duality, Lemma 6.10, and Lemma 6.11.
Local Kummer theory, surjective half, formerly interface B12.
For a finite extension k/ℚ₂, the Kummer class map descends to an isomorphism
k^×/(k^×)² ≅ H¹(G_k, ℤ/2) (continuous cochain cohomology; μ₂ ≅ ℤ/2, canonical in
char 0). This theorem exposes only surjectivity; injectivity is proved separately by
Kummer.kummerClass_eq_zero_iff ([a] = 0 ↔ IsSquare a) via Mathlib's infinite Galois
correspondence.
Citation: NSW [1], Ch. VI §2 — Theorem (6.2.1) (Hilbert's Satz 90)
and the Kummer-sequence isomorphism H¹(G_K, μ_n) ≅ K^×/K^{×n} displayed immediately after it
(electronic ed. p. 344), dual form Theorem (6.2.2); at n = 2. Secondary: Serre, Local
Fields [7], Ch. XIV §2 (p. 206). Both verified verbatim against the cited PDFs; the audit
copies are not vendored in this repository.
The proof in GQ2/KummerSurjectivity.lean combines completing the square with the
Krull–Galois correspondence from GQ2/KummerKrullBridge.lean, where an open index-two subgroup
produces the required quadratic subextension.
Paper: §6.3 (Lemma 6.17, "By Hochschild–Serre and Kummer theory").
docs/literature-axioms.md B12.
The dyadic unit filtration interface, formerly B13.
Every finite extension k/ℚ₂ carries a DyadicUnitFiltration (GQ2/UnitFiltration.lean):
a uniformizer π (an element of maximal spectral norm < 1 — discreteness of the value
group), the normalization ‖2‖ = ‖π‖^e (e = v_k(2) ≥ 1), a residue degree f ≥ 1, and
the graded counts of the unit filtration U^{(i)} = 1 + 𝔭_k^i:
#(U^{(0)}/U^{(1)}) = 2^f − 1 and #(U^{(i)}/U^{(i+1)}) = 2^f for i ≥ 1.
Citation: Serre, Local Fields [7], Ch. IV §2, Proposition 6 (verified verbatim against
the cited source, pp. 66–67; the audit copy is not vendored): "(a) U_L/U_L^{(1)} = L̄^*;
(b) for i ≥ 1, the group
U^{(i)}/U^{(i+1)} is canonically isomorphic to 𝔭_L^i/𝔭_L^{i+1}, which is itself
isomorphic (non-canonically) to the additive group of the residue field L̄" — read through
#L̄ = 2^f, #L̄^× = 2^f − 1. Uniformizer existence: Serre LF Ch. I–II (discrete
valuations, complete fields; standard).
Deviations (flagged, review-packet §3): stated in spectral-norm vocabulary (no valuation
ring/residue field is constructed — the graded pieces enter through their cardinalities, the
form the multiplicity count consumes); the proposal's (F2) inertia-twist clause
(θ_g = (g•π)/π acting on gr_j by θ_g^j) is derivable from the exact ℚ̄₂-algebra action
and the he normalization, so it is deliberately not stored as a field.
Paper: §6.3, eq. (93) (the display's own bracket "[7, Ch. XIV §§2–3]" is coarse — the
filtration is Ch. IV §2). docs/literature-axioms.md B13.
The definition delegates to dyadicUnitFiltration' in GQ2/UnitFiltrationCounts.lean, built on
GQ2/UnitFiltrationTop.lean; Classical.choice selects witnesses from the proved existence
lemmas. The uniformizer comes from compactness of the
unit ball + an O/2O pigeonhole (no spectral-norm value formula); the residue field O/𝔪 is the
finite quotient of the valuation subring; and the graded counts are the explicit isomorphisms
U^{(0)}/U^{(1)} ≅ (O/𝔪)ˣ and U^{(i)}/U^{(i+1)} ≅ (O/𝔪)⁺.