Twisted trace forms of dyadic quadratic extensions (B9-A, node N3) #
Second layer of the B9-A plan (docs/orchestration/b9a-proof-plan.md): the quadratic extension
k(δ)/k and the a-twisted trace forms Tr_{k(δ)/k}⟨a⟩ consumed by the B9 axiom
relativeStiefelWhitney_dyadic (in GQ2/Foundations/Axioms.lean since the 2026-07-24 flip;
its draft lived at the bottom of this file during development).
The field construction (L-encoding decision, docs/orchestration/b9a-t1-design.md) #
L is quadExt k δ := IntermediateField.adjoin ↥k {δ}, the adjoin over ↥k inside ℚ̄₂.
No ambient L : IntermediateField ℚ_[2] ℚ̄₂ is carried: the subgroup side of the axiom (the
hidx/hUo stabilizer encoding, reused verbatim from B9) and the field side are parametrized
by the same δ, so their compatibility is provable rather than hypothesized
(GQ2/KummerKrullBridge.lean machinery; see finrank_quadExt_eq_two). All trace/finrank API
applies because quadExt k δ is an intermediate field of ℚ̄₂/↥k: Algebra ↥k ↥(quadExt k δ)
and Algebra.trace ↥k ↥(quadExt k δ) are found by instance search, and finite-dimensionality
over ↥k follows from integrality of δ (finiteDimensional_quadExt).
Contents #
quadExt k δ— the extensionk(δ)of↥k;isIntegral_of_sq_eq,finiteDimensional_quadExt(proved).finrank_quadExt_eq_two—[k(δ) : k] = 2from the B9 index-2 stabilizer hypothesis (proved, T2, viaKummerSurjectivity.exists_quadratic_of_open_index_two+ Krull).traceFormOne k δ—Tr⟨1⟩ : z ↦ Tr_{k(δ)/k}(z·z);traceFormTwisted k δ a—Tr⟨a⟩ : z ↦ Tr_{k(δ)/k}(a·z·z). Both are genuineQuadraticForm ↥k ↥(quadExt k δ)definitions (no sorries), built fromAlgebra.traceFormviaLinearMap.BilinMap.toQuadraticMap.traceFormOne_isDiagonalization,traceFormTwisted_isDiagonalization— Lemma 6.16's diagonalizationsTr⟨1⟩ ≃ ⟨2, 2d⟩andTr⟨a⟩ ≃ ⟨2u, 2dn/u⟩fora = u + vδ(proved, T2: basis{1, δ}and completing the square withu ∈ kˣ).
Citations #
Kahn, Invent. Math. 78 (1984), Théorème 2; Evens, Trans. AMS 108 (1963), Thm 1; Kozlowski, Proc. AMS 91 (1984), Thm 1.1. Paper: §6, eq. (111), Lemmas 6.13/6.16.
The extension k(δ) of the finite dyadic base k, as an intermediate field of ℚ̄₂/↥k.
For the B9-A setting δ² = d ∈ kˣ with d a nonsquare, this is the quadratic extension L
of the Evens–Kahn identity; the degree-2 fact is finrank_quadExt_eq_two.
Equations
- GQ2.quadExt k δ = (↥k)⟮δ⟯
Instances For
A square root of an element of k is integral over ↥k (monic witness X² − d).
k(δ) is a finite extension of ↥k when δ² ∈ k — the instance input for the trace
form's nondegeneracy (Algebra.traceForm_nondegenerate, char 0 so separability is free).
[k(δ) : k] = 2 from the B9 subgroup encoding: if the stabilizer of δ meets
G_k = k.fixingSubgroup in an open subgroup of index 2, then quadExt k δ is quadratic
over ↥k. This is the bridge that lets the draft axiom's field-level hypothesis hdeg be
discharged from the verbatim B9 hypotheses hUo/hidx at the flip (plan node N3, risk R2).
The untwisted trace form Tr⟨1⟩ of k(δ)/k: the quadratic form
z ↦ Tr_{k(δ)/k}(z·z) over ↥k, i.e. Algebra.traceForm read as a quadratic map.
Equations
- GQ2.traceFormOne k δ = LinearMap.BilinMap.toQuadraticMap (Algebra.traceForm ↥k ↥(GQ2.quadExt k δ))
Instances For
The a-twisted trace form Tr⟨a⟩ of k(δ)/k: the quadratic form
z ↦ Tr_{k(δ)/k}(a·z·z) over ↥k, from the twisted bilinear form
(z, w) ↦ Tr(a·z·w). For a ∈ k(δ)ˣ this is Kahn's transfer Tr_{L/k}⟨a⟩ of the rank-1
form ⟨a⟩.
Equations
- GQ2.traceFormTwisted k δ a = LinearMap.BilinMap.toQuadraticMap (LinearMap.compl₁₂ (Algebra.traceForm ↥k ↥(GQ2.quadExt k δ)) (LinearMap.mulLeft (↥k) a) LinearMap.id)
Instances For
Lemma 6.16, first diagonalization: Tr⟨1⟩ ≃ ⟨2, 2d⟩ over the basis {1, δ}
(Gram matrix diag(Tr 1, Tr δ²) = diag(2, 2d)).
Lemma 6.16, second diagonalization: for a = u + vδ with norm n = u² − dv²
(u, n, d units of k), Tr⟨a⟩ ≃ ⟨2u, 2dn/u⟩ — Gram (2u, 2vd; 2vd, 2ud) on {1, δ},
completed to squares using u ∈ kˣ.