The Hilbert ledger for Lemma 6.16 #
Proof layer for GQ2.SectionSix.lemma_6_16 (deep-unit Evens norm vanishing, paper eq. (110)),
following the paper's ledger (111)–(114) through axioms B9 (evensKahn_dyadic) and B11
(dyadicNormCriterion). Every theorem uses only the standard three axioms, except the Tier-4
assembly evensNorm_deepUnit_vanish, which additionally uses B9 and B11. Tier 5 supplies the
eq.-(94) deep-unit orthogonality instances: normForm_* is proved at the standard three axioms,
while cup_deep_* additionally uses B11a.
The ledger (paper, proof of Lemma 6.16) #
With L = k(δ), δ² = d, a = u + vδ a deep unit (a = 1 + 2b, ‖b‖ < 1), and
n = u² − dv²:
- (112)
u = 1 + (b + sb)is a unit (‖b + sb‖ < 1), andn = 1 + 2t + 4mwitht = b + sb,m = b·sb— pure algebra after applying the reflections(which sendsδ ↦ −δsinces ∉ Stab δ). - B9 degree 1 rearranged through
kummerClassK_mulgivescor α = [n]. - B9 degree 2 + bilinearity (
map_add) +(x,x) = (x,−1)(cup_self_eq_neg_one) collapse to (113):N^{Ev}[a] = (u,−d) + (2du, n)— equivalently, at the atom level used below,N^{Ev}[a] = (u,−1) + (u,d) + (2u,n) + (d,n). (u,d) = 0(cup_unramified_unit+cup_comm:uis a unit,k(δ)/kunramified) and(d,n) = 0(cup_of_normForm:n = u² − dv²is the norm form on the nose).- (114)
n/(2u−1) = 1 + 4m/(1+2t)has‖n/(2u−1) − 1‖ ≤ ‖4‖·‖b‖² < ‖4‖, sosq_of_near_one(Hensel) gives[n] = [2u−1]. - Steinberg (
cup_steinberg:1 − 2u = 1² − 2u·1²) gives(2u, 2u−1) = (2u, −1); and(2,−1) = 0(cup_two_neg_one:−1 = 1² − 2·1²), so(2u,−1) = (u,−1)and the two surviving terms cancel byh2_add_self.
Supporting lemmas #
h1_add_self/h2_add_self— 2-torsion of the coefficient quotients (pointwise char-2 atZ1/Z2level +H1mk/H2mkquotient induction).kummerClassK_mul,kummerClassK_one— via the twoℚ̄₂-level helperskcf_root_indep'andkcf_mul_of_fixed(off EvensKahn'stwo_values_of_fixed), transported throughH1mk.trivialCupPairing_comm— graded-commutativity in char 2: the two cup cocycles differ bydOne (g ↦ −(a g · b g))(identity holds over ℤ)∈ B2; theneq_zero_iff+h2_add_self.norm_galois— Galois invariance of the spectral norm, via MathlibNormedAlgebra.norm_eq_spectralNorm ℚ_[2]+spectralNorm_eq_of_equiv.sq_of_near_one— the Hensel depth‖z−1‖ < ‖4‖ ⟹ z ∈ (k^×)²: hand-rolled quadratic Newtonw ↦ w − (w²−z)/(2w)fromw₀ = 1inside↥k; invariants‖wₙ−1‖ ≤ ‖2‖,‖wₙ²−z‖ ≤ ‖2‖²·qⁿ⁺¹(q = ‖z−1‖/‖4‖ < 1) ⟹cauchySeq_of_le_geometric⟹ limit ⟹ root.NormedField ↥krestrictsℚ̄₂'s (rfl),CompleteSpace ↥k := FiniteDimensional.complete ℚ_[2] ↥k. Mathlib'sPadic.hensels_lemmaisℤ_p-specific;ℚ̄₂itself is NOT complete.evensNorm_deepUnit_vanish— the assembled ledger (5-step script above). Proof: step 1s'•δ = −δ(two_values_of_fixed+hs); step 2 applys'tohA⟹(u:ℚ̄₂) = 1+b+s'•b,(n:ℚ̄₂) = (1+2b)(1+2s'•b),‖u‖ = 1,‖n/(2u−1)−1‖ = ‖4‖‖b‖² < ‖4‖; step 3 degree-1 B9 +kummerClassK_mul/_inv/h1_add_self⟹cor = [n]; step 5-prep[n] = [2u−1](Henselsq_of_near_oneonn/(2u−1)+kummerClassK_mul_self); step 4 expand degree-2 (map_add), kill(2,u)+(u,2)(comm +h2_add_self),(u,d)(cup_unramified_unit),(d,n)(cup_of_normForm),(u,u)=(u,−1)(cup_self_eq_neg_one); step 5cup_steinberg+ Hensel ⟹(2,−1) = 0(cup_two_neg_one) closes it. (Usesset_option maxHeartbeats— large context.)
The lemma_6_16 splice additionally transports along the statement's hLδ, the Kummer
presentation of L/k; see docs/section67-extraction.md for the encoding decision.
Tier 0: coefficient 2-torsion #
H¹(G, 𝔽₂) is 2-torsion. The representative satisfies f + f = 0 pointwise (char 2), so
the sum is H1mk of the zero cocycle.
H²(G, 𝔽₂) is 2-torsion. Same shape as h1_add_self, at Z2.
Tier 1 helpers: base-general cocycle algebra over ℚ̄₂ #
Two square roots of the same ℚ̄₂-element give the same Kummer cocycle: α² = β² forces
α = ±β, and κ is sign-insensitive (kummerCocycleFun_neg). Base-general analogue of
Kummer.kummerCocycleFun_root_indep (no algebraMap-image hypothesis on the radicand).
Base-general cocycle multiplicativity at a group element g fixing both radicands A, B
(the two_values case analysis with abstract fixed squares, via two_values_of_fixed). Here
γ is any square root of A·B, so κ_γ = κ_{αβ} by kcf_root_indep'.
Tier 1: Kummer-class algebra over a finite dyadic base #
Multiplicativity of the base-general Kummer class. [O: sqrtCl (ab) and
sqrtCl a · sqrtCl b are square roots of the same nonzero element, so the cocycles agree by
Kummer.kummerCocycleFun_root_indep; then Kummer.kummerCocycleFun_mul
(GQ2/Kummer.lean:179) gives pointwise additivity, and H1mk is additive on Z1.]
The Kummer class of 1 vanishes. [O: 1 is its own square root; root-independence
makes the cocycle g ↦ if g • 1 = 1 then 0 else 1 ≡ 0.]
[a⁻¹] = [a] (derived).
[a²] = 0 (derived).
Tier 2: cup-symbol algebra #
Symmetry of the degree-(1,1) cup pairing in char 2. [O: at representatives,
cup11Fun a b + cup11Fun b a = δ¹(g ↦ a g · b g) — expand dOne; the pointwise product of
two 1-cocycles is a continuous 1-cochain, so the difference is in B2; conclude by
QuotientAddGroup.eq' through H2mk.]
The norm-form direction of the B11 criterion, applied: an explicit representation
b = x² − a y² kills the symbol. This consumes B11a directly rather than the bundled
dyadicNormCriterion, so the axiom trace is std-3 ∪ {B11a} without the unused B11b clause.
(a, −a) = 0 — the norm form represents −a as 0² − a·1².
Steinberg (a, 1−a) = 0 — the norm form represents 1 − a as 1² − a·1².
(2, −1) = 0 — −1 = 1² − 2·1² (the paper's 2 = N_{k(i)/k}(1+i) step, replaced by the
explicit dyadic representation; cf. the B11 docstring).
(a, a) = (a, −1) (derived: 0 = (a, −a) = (a, −1) + (a, a) + 2-torsion).
Unramified unit-norm vanishing: if k(δa)/k has equal norm value groups then every unit
symbol (a, u) dies — the B11 clause-2 consumer.
Tier 3: dyadic arithmetic #
Galois invariance of the spectral norm on ℚ̄₂. [O: ‖· ∘ g‖ is a field norm on ℚ̄₂
extending the ℚ₂-norm, and the extension norm on an algebraic extension of a complete field
is unique (Mathlib spectralNorm uniqueness layer); alternatively via the
|N_{k(x)/ℚ₂}(x)|^{1/deg} characterization, which is visibly g-invariant.]
Hensel depth over a finite dyadic base: anything within < ‖4‖ of 1 is a square —
the (114) step U_{2e+2}(k) ⊆ (k^×)². [O: Newton contraction w ↦ w − (w²−z)/(2w) starting
at w₀ = 1, run inside ↥k; needs NormedField ↥k (subfield of ℚ̄₂, SubfieldClass
instance) and CompleteSpace ↥k (FiniteDimensional.complete ℚ_[2] ↥k — finite-dimensional
over a complete field; NB ℚ̄₂ itself is NOT complete, completeness is intrinsic to k).
Estimates: ‖w_n − 1‖ ≤ ‖2‖ throughout, ‖w_{n+1}² − z‖ ≤ (‖w_n² − z‖/‖2‖)² — strictly
contracting below ‖4‖. Mathlib's Padic.hensels_lemma is ℤ_p-only; do not reach for it.]
Tier-4 helpers: reflection identities, the Hensel step, and 2-torsion bookkeeping #
Tier 4: the assembled ledger #
The Hilbert ledger (paper, proof of Lemma 6.16; eqs. (111)–(114)) in the B9-native
vocabulary: for a deep unit a = u + vδ = 1 + 2b (‖b‖ < 1) over the unramified quadratic
Kummer datum (d, δ), the index-two Evens norm of its Kummer cocycle vanishes.
Route (O-finish; every ingredient is in this file, B9, or B11):
s • δ = −δfromhs((s•δ)² = dforces±δ;+would putsin the stabilizer).- (112): from
hAand itss-image,(u:ℚ̄₂) = 1 + (b + s•b)and(n:ℚ̄₂) = (1+2b)(1+2(s•b))— so‖u − 1‖ < 1and, withnorm_galois,‖n/(2u−1) − 1‖ ≤ ‖4‖·‖b‖² < ‖4‖(‖1+2t‖ = 1by the ultrametric bound). - Apply
evensKahn_dyadic; rearrange degree 1 withkummerClassK_mul/h1_add_selftocorH1 … α … = kummerClassK k nU(nUthe unitn). - Substitute into degree 2; expand with
map_add/kummerClassK_mul; kill(u,d)bycup_unramified_unit+trivialCupPairing_comm,(d,n)bycup_of_normForm(witness⟨u, v, hn⟩), normalize(x,x)bycup_self_eq_neg_one— reaching (113) in the formN^{Ev} = (u,−1) + (2u, n). sq_of_near_oneonn/(2u−1)+kummerClassK_mul/kummerClassK_mul_selfgive[n] = [2u−1];cup_steinberg(ata := 2u,b := 1−2u, sign-flipped throughcup_neg_self) turns(2u, 2u−1)into(2u, −1);cup_two_neg_onereduces(2u,−1) = (u,−1);h2_add_selfcancels the two surviving terms.
Tier 5: the eq.-(94) deep-unit orthogonality #
Paper eq. (94) (§6.3, p. 29) is the Hilbert-symbol orthogonality Uᵢ^⊥ = U_{2e−i+1} of the
dyadic square-class filtration together with −1 ∈ U_e. Lemma 6.17 consumes only two "⊆"
instances: deep ⟂ deep (U_{e+1} ⟂ U_{e+1} — f1's isotropy and f2's free orbits) and
deep ⟂ −1 (f2's square orbits). Neither is a numbered theorem in the provided texts —
Fesenko–Vostokov, Local Fields and Their Extensions (2nd ed.), Ch. VII §4 records the
general statements only as Exercises 4c and 5b, and O'Meara, Introduction to Quadratic
Forms, §63 assembles them from the quadratic-defect propositions. They are proved here by
the classical norm-form
descent:
- values of the binary norm form
x² − a·y²are closed under multiplication (Brahmagupta–Fibonacci composition,normForm_mul) and inversion (normForm_inv); - for deep
b(‖b − 1‖ < ‖2‖), the exact solutionx₀ = (b+1)/2,y₀ = (b−1)/2ofx² − y² = brepresentsbup to the multiplicative erroru = (x₀² − a·y₀²)/bwith‖u − 1‖ = ‖a−1‖·(‖b−1‖/‖2‖)² ≤ ‖b−1‖·(‖a−1‖/‖2‖)— a strict contraction (adeep); - iterating (
normForm_of_deep_aux) drives the error below‖4‖, where the Local Square Theorem (sq_of_near_one; O'Meara 63:1) makes it a square, hence a norm-form value; b = x² − a·y²kills the symbol viacup_of_normForm(B11a = Serre LF Ch. XIV §2, Prop. 7 iii — the only axiom in the chain).
The normForm_* layer uses only the standard axioms; the cup_deep_* corollaries additionally
use B11a.
Brahmagupta–Fibonacci composition: values of x² − a·y² are closed under products.
Nonzero values of x² − a·y² are closed under inversion.
Deep units are norm-form values of each other — the "⊆" half of paper eq. (94) at
(U_{e+1}, U_{e+1}): for deep a, b ∈ k^× (‖· − 1‖ < ‖2‖, i.e. ∈ U_{e+1}(k)), b is
represented by the norm form x² − a·y² of k(√a)/k. [Provenance: paper §6.3 eq. (94);
Fesenko–Vostokov Ch. VII §4 Ex. 4c states the general i + j > 2e triviality (exercise —
hence proved, not leafed); O'Meara §63A is the quadratic-defect calculus behind it.
No axiom: Brahmagupta descent + Local Square Theorem.]
Deep units are norm-form values of every MID unit — the "⊆" half of eq. (94) at
(U_e, U_{e+1}): for a ∈ U_e(k) (‖a − 1‖ ≤ ‖2‖) and deep b ∈ U_{e+1}(k), b is
represented by x² − a·y². [Provenance: paper §6.3 eq. (94); Fesenko–Vostokov Ch. VII §4
Ex. 4c's i + j > 2e triviality at (e, e+1) (exercise — hence proved, not leafed);
O'Meara §63A. No axiom: Brahmagupta descent + Local Square Theorem.]
Eq. (94), deep ⟂ deep (the deep-part proof's isotropy hiso and the Lemma 6.17 vanishing proof's free-orbit leaf): the
symbol of two deep units vanishes. std-3 ∪ {B11a}.
Eq. (94), mid ⟂ deep — (U_e, U_{e+1}) = 1 (the deep-part proof's hsharp inclusion input): the
symbol of a MID unit against a deep unit vanishes. std-3 ∪ {B11a}.
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- eq. (110) = ⟦eq-evensvanish⟧
- eq. (111) = ⟦eq-SWconvention⟧
- eq. (114) = ⟦eq-n2u⟧
- eq. (94) = ⟦eq-unitorth⟧
- Lemma 6.16 = ⟦lem-evensvanish⟧
- Lemma 6.17 = ⟦lem-shapirodet⟧