Stiefel–Whitney classes of binary quadratic forms over finite dyadic bases (B9-A, node N1)

The B9-A plan (docs/orchestration/b9a-proof-plan.md) restates axiom B9 at the quadratic-form level: the relative Stiefel–Whitney identity needs invariants w₁ q ∈ H¹(G_k, 𝔽₂) and w₂ q ∈ H²(G_k, 𝔽₂) defined on isometry classes of nondegenerate binary quadratic forms over a finite dyadic base k, rather than on the fixed diagonal representatives of Lemma 6.16. This file provides that layer.

Design (N1 decision, recorded in docs/orchestration/b9a-t1-design.md)

Forms are Mathlib QuadraticForm ↥k V with QuadraticMap.Equivalent as the isometry-class relation; the diagonal representatives are QuadraticMap.weightedSumSquares with unit weights on the model Fin 2 → ↥k (diagForm). This matches QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate', whose only friction — Invertible (2 : ↥k) — vanishes in characteristic zero (the global invertibleTwo instance). No bespoke light structure is needed.

• diagForm k x y — the diagonal binary form ⟨x, y⟩ with unit weights x, y ∈ (↥k)ˣ.
• IsDiagonalization k Q x y — Q is isometric to ⟨x, y⟩.
• swOne k Q, swTwo k htriv Q — the degree-1 and degree-2 Stiefel–Whitney classes, defined by Classical.choice of a diagonalization, with values [x] + [y] and [x] ⌣[htriv] [y] in the base-general Kummer classes kummerClassK of GQ2/EvensKahn.lean; junk value 0 when no unit diagonalization exists (the repository's junk-value convention, cf. IsDemushkin).

The invariance layer (node N2 of the plan; proved by ticket T3, 2026-07-24)

• exists_isDiagonalization — a nondegenerate binary form has a unit diagonalization (proved).
• swOne_well_defined — degree-1 (discriminant) invariance across diagonalizations (proved via an exact Brahmagupta identity x'y' = xy·(ad−bc)² extracted from the isometry).
• swTwo_well_defined — degree-2 (Delzant/Hasse) invariance (proved: representation lemma + a single Steinberg instance). Its cup-relation input is the B11a norm criterion; since this file is strictly upstream of GQ2/Foundations/Axioms.lean (the B9 axiom lives there and imports this file), the criterion enters as the explicit hypothesis hnorm, instantiated by hilbertSymbol_normCriterion_finiteDyadic at the flip site (plan node N2; owner decision Q2). All three are sorry-free with #print axioms = the standard three.

The evaluation lemmas swOne_diag/swTwo_diag and the isometry-class congruences swOne_congr/swTwo_congr are proved here from the two invariance statements.

Citations

Delzant, C. R. Acad. Sci. Paris 255 (1962) (Stiefel–Whitney classes of quadratic forms in Galois cohomology); Serre, A Course in Arithmetic, Ch. IV; Kahn, Invent. Math. 78 (1984). Paper: §6, eq. (111), Lemma 6.16. Plan: docs/orchestration/b9a-proof-plan.md nodes N1/N2.

noncomputable def GQ2.diagForm (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (x y : (↥k)ˣ) : QuadraticForm (↥k) (Fin 2 → ↥k)

The diagonal binary quadratic form ⟨x, y⟩ over ↥k with unit weights, on the model Fin 2 → ↥k: the value at v is x·v₀² + y·v₁². Unit weights make nondegeneracy automatic and are exactly what QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate' produces.

Equations

• GQ2.diagForm k x y = QuadraticMap.weightedSumSquares ↥k ![x, y]

@[simp]

theorem GQ2.diagForm_apply (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (x y : (↥k)ˣ) (v : Fin 2 → ↥k) : (diagForm k x y) v = ↑x * (v 0 * v 0) + ↑y * (v 1 * v 1)

def GQ2.IsDiagonalization (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) {V : Type u_1} [AddCommGroup V] [Module (↥k) V] (Q : QuadraticForm (↥k) V) (x y : (↥k)ˣ) : Prop

Q is diagonalized by the unit pair (x, y): an isometry Q ≃ ⟨x, y⟩ onto the diagonal model. The Stiefel–Whitney classes below are defined by choice of such a pair; node N2 (ticket T3) shows the resulting classes do not depend on the choice.

Equations

• GQ2.IsDiagonalization k Q x y = QuadraticMap.Equivalent Q (GQ2.diagForm k x y)

theorem GQ2.isDiagonalization_of_equivalent (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module (↥k) V] [AddCommGroup W] [Module (↥k) W] {Q : QuadraticForm (↥k) V} {Q' : QuadraticForm (↥k) W} {x y : (↥k)ˣ} (h : QuadraticMap.Equivalent Q Q') (hd : IsDiagonalization k Q' x y) : IsDiagonalization k Q x y

Diagonalizations transport along isometries of forms.

Private helpers: two-torsion, cup symmetry, and Kummer-class algebra

The invariance proofs below need the 2-torsion of the 𝔽₂-cohomology groups, symmetry of the trivial cup pairing, and multiplicativity of kummerClassK. The public forms of these lemmas live in GQ2/HilbertLedger.lean, which is strictly downstream of this file (it imports GQ2/Foundations/Axioms.lean, which will import this file at the B9-A flip, plan node N5), so they are re-proved here as private lemmas — the approved default of docs/orchestration/b9a-t1-design.md, owner question Q3. Cup symmetry alone is derived rather than re-proved: GQ2/CupSymmetry.lean is upstream, and its cup11_comm specializes to the multiplication pairing on ZMod 2, which is its own transpose.

theorem GQ2.exists_isDiagonalization (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) {V : Type u_1} [AddCommGroup V] [Module (↥k) V] (Q : QuadraticForm (↥k) V) (hdim : Module.finrank (↥k) V = 2) (hQ : LinearMap.SeparatingLeft (QuadraticMap.associated Q)) : ∃ (x : (↥k)ˣ) (y : (↥k)ˣ), IsDiagonalization k Q x y

Existence of a unit diagonalization for a nondegenerate binary form (char 0, so no Invertible (2 : ↥k) friction). Nondegeneracy is Mathlib's SeparatingLeft for the associated bilinear form, the exact hypothesis of QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate'.

theorem GQ2.swOne_well_defined (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) {x y x' y' : (↥k)ˣ} (h : QuadraticMap.Equivalent (diagForm k x y) (diagForm k x' y')) : kummerClassK k x + kummerClassK k y = kummerClassK k x' + kummerClassK k y'

Degree-1 invariance (discriminant). Isometric diagonal binary forms have the same degree-1 Stiefel–Whitney class [x] + [y]: the discriminants differ by the square of the change-of-basis determinant (QuadraticForm.discr_comp), and Kummer classes kill squares.

theorem GQ2.swTwo_well_defined (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (htriv : ∀ (g : ↥k.fixingSubgroup) (m : ZMod 2), g • m = m) (hnorm : ∀ (a b : (↥k)ˣ), ((trivialCupPairing 2 (↥k.fixingSubgroup) htriv) (kummerClassK k a)) (kummerClassK k b) = 0 ↔ ∃ (z : ↥k) (w : ↥k), ↑b = z ^ 2 - ↑a * w ^ 2) {x y x' y' : (↥k)ˣ} (h : QuadraticMap.Equivalent (diagForm k x y) (diagForm k x' y')) : ((trivialCupPairing 2 (↥k.fixingSubgroup) htriv) (kummerClassK k x)) (kummerClassK k y) = ((trivialCupPairing 2 (↥k.fixingSubgroup) htriv) (kummerClassK k x')) (kummerClassK k y')

Degree-2 invariance (Delzant). Isometric diagonal binary forms have the same cup class [x] ⌣ [y]. This is the classical binary Hasse-invariant well-definedness: a representation lemma extracts x' = x·a² + y·b² from the isometry, then a chain equivalence and the cup identities close the computation. The cup-relation inputs (Steinberg-type identities) are consequences of the B11a norm criterion, which enters as the hypothesis hnorm so that this file stays strictly upstream of GQ2/Foundations/Axioms.lean; the flip (ticket T5) instantiates hnorm := hilbertSymbol_normCriterion_finiteDyadic k htriv.

The Stiefel–Whitney classes

noncomputable def GQ2.swOne (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) {V : Type u_1} [AddCommGroup V] [Module (↥k) V] (Q : QuadraticForm (↥k) V) : ContCoh.H1 (↥k.fixingSubgroup) (ZMod 2)

The degree-1 Stiefel–Whitney class w₁ Q ∈ H¹(G_k, 𝔽₂) of a quadratic form over ↥k: the sum [x] + [y] of the base-general Kummer classes of a chosen unit diagonalization Q ≃ ⟨x, y⟩; junk value 0 when no unit diagonalization exists. Independence of the choice is swOne_well_defined (node N2); the evaluation at a given diagonalization is swOne_diag.

Equations

• GQ2.swOne k Q = if h : ∃ (x : (↥k)ˣ) (y : (↥k)ˣ), GQ2.IsDiagonalization k Q x y then GQ2.kummerClassK k h.choose + GQ2.kummerClassK k ⋯.choose else 0

noncomputable def GQ2.swTwo (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (htriv : ∀ (g : ↥k.fixingSubgroup) (m : ZMod 2), g • m = m) {V : Type u_1} [AddCommGroup V] [Module (↥k) V] (Q : QuadraticForm (↥k) V) : ContCoh.H2 (↥k.fixingSubgroup) (ZMod 2)

The degree-2 Stiefel–Whitney class w₂ Q ∈ H²(G_k, 𝔽₂): the cup product [x] ⌣[htriv] [y] of the Kummer classes of a chosen unit diagonalization Q ≃ ⟨x, y⟩; junk value 0 when no unit diagonalization exists. Independence of the choice is swTwo_well_defined (node N2); evaluation is swTwo_diag.

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.swOne_diag (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) {V : Type u_1} [AddCommGroup V] [Module (↥k) V] {Q : QuadraticForm (↥k) V} {x y : (↥k)ˣ} (hd : IsDiagonalization k Q x y) : swOne k Q = kummerClassK k x + kummerClassK k y

Evaluation of swOne at a diagonalization: if Q ≃ ⟨x, y⟩ then w₁ Q = [x] + [y].

theorem GQ2.swTwo_diag (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (htriv : ∀ (g : ↥k.fixingSubgroup) (m : ZMod 2), g • m = m) (hnorm : ∀ (a b : (↥k)ˣ), ((trivialCupPairing 2 (↥k.fixingSubgroup) htriv) (kummerClassK k a)) (kummerClassK k b) = 0 ↔ ∃ (z : ↥k) (w : ↥k), ↑b = z ^ 2 - ↑a * w ^ 2) {V : Type u_1} [AddCommGroup V] [Module (↥k) V] {Q : QuadraticForm (↥k) V} {x y : (↥k)ˣ} (hd : IsDiagonalization k Q x y) : swTwo k htriv Q = ((trivialCupPairing 2 (↥k.fixingSubgroup) htriv) (kummerClassK k x)) (kummerClassK k y)

Evaluation of swTwo at a diagonalization: if Q ≃ ⟨x, y⟩ then w₂ Q = [x] ⌣[htriv] [y]. Carries the same hnorm hypothesis as swTwo_well_defined.

theorem GQ2.swOne_congr (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module (↥k) V] [AddCommGroup W] [Module (↥k) W] {Q : QuadraticForm (↥k) V} {Q' : QuadraticForm (↥k) W} (h : QuadraticMap.Equivalent Q Q') : swOne k Q = swOne k Q'

swOne is an isometry-class invariant (node N2 consequence).

theorem GQ2.swTwo_congr (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (htriv : ∀ (g : ↥k.fixingSubgroup) (m : ZMod 2), g • m = m) (hnorm : ∀ (a b : (↥k)ˣ), ((trivialCupPairing 2 (↥k.fixingSubgroup) htriv) (kummerClassK k a)) (kummerClassK k b) = 0 ↔ ∃ (z : ↥k) (w : ↥k), ↑b = z ^ 2 - ↑a * w ^ 2) {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module (↥k) V] [AddCommGroup W] [Module (↥k) W] {Q : QuadraticForm (↥k) V} {Q' : QuadraticForm (↥k) W} (h : QuadraticMap.Equivalent Q Q') : swTwo k htriv Q = swTwo k htriv Q'

swTwo is an isometry-class invariant (node N2 consequence). Carries the hnorm hypothesis of swTwo_well_defined.