Classical literature inputs for Theorem 1.2 #
Every axiom in the GQ2 library lives in this file, a rule enforced by
scripts/check_axioms.sh. Each axiom represents a published mathematical input used by the
paper; the paper-specific propositions and theorems are proved elsewhere in the library.
The current census contains nine axioms:
- B1
Foundations.absGalQ2_isTopologicallyFinitelyGenerated— topological finite generation ofG_ℚ₂. - B3c
dyadicOrientation— the canonical dyadic orientation in the marked cyclotomic interface used by Proposition 1.1. - B5
localReciprocity— local reciprocity forℚ₂with the paper normalization. - B6
tateDualityAt— local Tate duality over every finite extension ofℚ₂. - B7
Foundations.absGalQ2_localEulerCharacteristic— the local Euler characteristic. - B8
peripheralCyclotomicAction— the cyclotomic action on the peripheral generators ofΔ = maxPro2(F₂). - B9
evensKahn_dyadic— the degree-at-most-two Evens–Kahn identity over finite dyadic bases. - B10
tameQuotient— the oriented tame quotient ofG_ℚ₂. - B11a
hilbertSymbol_normCriterion_finiteDyadic— the Hilbert-symbol norm criterion over finite dyadic bases.
Four interfaces that were formerly axioms are now constructed in the repository under the same
names: HilbertSymbol.hilbertSymbol_dyadic, unramifiedQuadratic_units_are_norms,
kummerClassK_surjective, and dyadicUnitFiltration. Keeping their public names unchanged lets
consumers use the proved implementations without an API migration.
For review, the live leaves fall into three citation-faithfulness classes:
- direct classical theorems: B1, B6, and B7;
- classical theorems with encoding choices: B5, B9, and B10;
- composite project interfaces: B3c, B8, and B11a.
The declaration docstrings below give the precise statement, source citation, paper
cross-reference, and any encoding or convention that prevents the Lean statement from being a
verbatim transcription of one published theorem. The full dependency table is in
docs/literature-axioms.md, matching Appendix D of the paper.
References from the paper bibliography:
[1] Neukirch–Schmidt–Wingberg, Cohomology of Number Fields, 2nd ed., Springer 2015. (NSW) [2] Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132. [3] Serre, Structure de certains pro-p-groupes, Sém. Bourbaki 252 (1962–64). [4] Ribes–Zalesskiĭ, Profinite Groups, 2nd ed., Springer 2010. (RZ) [7] Serre, Local Fields, GTM 67, Springer 1979. [CiA] Serre, A Course in Arithmetic, GTM 7, Springer 1973.
B1 — topological finite generation #
[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).
B7 — the local Euler–Poincaré characteristic #
Statement conventions, citation discussion, and the derived stress tests
(finite_H1, card_H1, …) are in GQ2/EulerCharacteristic.lean, which imports this file.
[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.
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.
B3c — the canonical dyadic orientation (cyclotomic interface) #
The bundle DyadicOrientation — a B4 isomorphism together with the descended cyclotomic
character, normalized to Labute's Theorem 4(2) values on the marked generators — and the
route-(ii) decision with its flagged deviations are in GQ2/Orientation.lean; its stress
tests are bundle-parametrized and axiom-free.
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.
B5 — the local reciprocity bundle #
The bundle structure LocalReciprocity (with the convention table and the soundness note on
the profinite target of ν_ur) is defined in GQ2/Reciprocity.lean; its stress tests are
parametrized over an arbitrary bundle and are therefore axiom-free.
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.
B6 — local Tate duality (per-n bundle, at every finite k/ℚ₂) #
The dual module MuDual n M = Hom(M, μₙ) (conjugation action), the evaluation cup pairing,
the group-parametric bundle TateDualityG G n (with TateDuality n = the G_ℚ₂ member), and
the gate IsLocalDualizingGroup — with the encoding decisions and flagged deviations (per-n
form, ℤ/n-valued Pontryagin duals, single currying, unnormalized inv) — are defined in
GQ2/TateDuality.lean; its stress tests are parametrized over an arbitrary bundle and are
therefore axiom-free.
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.
B6 at the base field ℚ₂ — the G = G_ℚ₂ member of tateDualityAt, using
isLocalDualizingGroup_absGalQ2.
Equations
Instances For
B8 — the cyclotomic action on peripheral generators (Lemma 3.6) #
The concrete group Δ = maxPro2(FreeProfinite (Fin 2)), its peripheral generators P, T, C, and
the bundle PeripheralCyclotomicAction — with the flagged faithfulness deviation (the literal
statement is about the outer action on an étale/anabelian π₁, absent from Mathlib) and the pinning
of the exponent embedding ι — are defined in GQ2/PeripheralAction.lean.
[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.
B9 — the Evens/Kahn formula (paper eq. (111)), degrees ≤ 2 #
The ingredients — degree-1 corestriction corH1Z, the index-two Evens norm evensNormH2Z
(the paper's two-point graph cocycle (98), Lemma 6.13), and the subgroup Kummer cocycle
kummerZ1On — are all defined (with full well-formedness proofs) in GQ2/EvensKahn.lean;
Stiefel–Whitney classes of the rank-2 transfer forms enter through the paper's fixed
diagonalizations Tr_{L/k}⟨a⟩ ≃ ⟨2u, 2dn/u⟩, Tr_{L/k}⟨1⟩ ≃ ⟨2, 2d⟩ (Lemma 6.16), with
w₁⟨x,y⟩ = [x]+[y] and w₂⟨x,y⟩ = [x]∪[y] in Kummer classes. The axiom asserts the
degree-1 and degree-2 components of (111) for these representatives. Deviations (flagged;
see GQ2/EvensKahn.lean): truncation to degrees ≤ 2; concrete diagonal representatives
(Delzant well-definedness absorbed into the scoping); the degree-1 component is equivalent to
the classical cor[a] = [N_{L/k}a] compatibility.
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.
B10 — the tame quotient of G_ℚ₂ (Iwasawa) #
The bundle TameQuotientData (closed normal pro-2 W + G_ℚ₂/W ≅ T_tame), the NSW
convention notes (arithmetic-vs-geometric Frobenius, σ ↦ σ⁻¹), and the flagged deviation
(no ramification theory: W is characterized, not constructed; its maximality — paper
Lemma 3.3 — is deliberately not asserted here) are in GQ2/TameQuotient.lean.
[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.
B11 — the dyadic norm criterion over finite bases #
Section 6.3 uses the norm criterion and unit-norm surjectivity over arbitrary finite dyadic bases.
The interface separates the remaining classical axiom B11a from the spectral-norm convention and
the in-repository proof of unramified unit-norm surjectivity. The combined
dyadicNormCriterion theorem below preserves the paired interface for consumers:
hilbertSymbol_normCriterion_finiteDyadic— the symbol/norm criterion (classical).unramifiedQuadratic_units_are_norms— units of an unramified quadratic extension are norms (classical).IsUnramifiedQuadraticSpectral— not an axiom: the repo's spectral-norm working definition of "k(δa)/kis unramified" (equal norm value groups onℚ̄₂). Isolated here as the review's "riskiest piece": it is a project convention, not a Mathlib unramifiedness notion, and is deliberately adef(asserting nothing) rather than a bridge axiom.
Encoding conventions carried over from the pre-split axiom: the "b is a norm from k(√a)"
condition is the norm form b = x² − a y² (elementary, no relative field-extension
plumbing); unramifiedness by equal norm value groups through the spectral norm on ℚ̄₂ (the
GQ2/SectionSix.lean IsDeepUnit/lemma_6_16 convention).
Note for reviewers: the Steinberg relation [x]∪[1−x] = 0 and [2]∪[−1] = 0 used in
Lemma 6.16's proof are consequences of the criterion clause (norm representations
1 − x = 1² − x·1² and −1 = 1² − 2·1²), so they are deliberately not separate clauses.
Citation: Serre, Local Fields [7], Ch. XIV §2, Proposition 4(iii) (the symbol–norm criterion;
over ℚ_p also CiA [CiA] Ch. III §1.1 Prop. 1), and Ch. V §2 (norms of unramified extensions
are the units times the norms of uniformizers). Paper: §6.3, displays (93)/(94) and Lemma 6.16.
Project convention — isolated spectral-norm bridge. The repo's working
definition of "k(δa)/k is unramified", encoded via the spectral norm on ℚ̄₂: 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. 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.
Equations
- GQ2.IsUnramifiedQuadraticSpectral k δa = ∀ (z : AlgebraicClosure ℚ_[2]), z ≠ 0 → (∃ (x : ↥k) (y : ↥k), z = ↑x + ↑y * δa) → ∃ (w : ↥k), w ≠ 0 ∧ ‖z‖ = ‖↑w‖
Instances For
[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).
Unramified unit-norm surjectivity, formerly interface B11b. If
k(√a)/k is unramified (the IsUnramifiedQuadraticSpectral 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 spectral-unramifiedness convention remains isolated in
IsUnramifiedQuadraticSpectral, 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/𝔪)⁺.
Equations
Instances For
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- Cor 3.12 = ⟦cor-relativeDemushkin⟧
- eq. (111) = ⟦eq-SWconvention⟧
- eq. (13) = ⟦eq-localmarkingorientation⟧
- eq. (145) = ⟦eq-recursionR5a⟧
- eq. (93) = ⟦eq-squareclassgraded⟧
- Lemma 10.1 = ⟦lem-tameframeexhaustion⟧
- Lemma 3.3 = ⟦lem-o2tame⟧
- Lemma 3.4 = ⟦lem-standardorientation⟧
- Lemma 3.5 = ⟦lem-markedinitialform⟧
- Lemma 3.6 = ⟦lem-peripheralpower⟧ (= lemma 3.7 in current tex)
- Lemma 6.10 = ⟦lem-middlelayer⟧
- Lemma 6.11 = ⟦lem-faithfulprojective⟧
- Lemma 6.13 = ⟦lem-twopointevans⟧
- Lemma 6.16 = ⟦lem-evensvanish⟧
- Lemma 6.17 = ⟦lem-shapirodet⟧
- Prop 1.1 = ⟦prop-markedDem⟧
- Prop 3.14 = ⟦prop-compatiblemarking⟧
- Prop 3.2 = ⟦prop-tamequotient⟧
- Thm 1.1 = ⟦prop-markedDem⟧ [cited as theorem; paper says proposition]
- Theorem 1.2 = ⟦thm-main⟧
- Thm 2.5 = ⟦lem-reconstruction⟧ [cited as theorem; paper says lemma]
- Thm 4.2 = ⟦thm-fixedframe⟧