Gauss sum over a Lagrangian (the ramified Prop 6.18 combinatorial core)

The zero-count of a nonsingular 𝔽₂ quadratic form q on #V = 2^{2m} is 2^{2m−1} ± 2^{m−1} by its Arf invariant (GQ2/GaussCount.lean, zeroCount_of_arf_{zero,one}). Lemma 6.17 supplies Q⁰_loc with a half-dimensional totally singular subspace X₊ (deep units, #X₊² = #H¹, Q⁰_loc|X₊ = 0). The keystone below turns that into arf = 0 (positive Gauss sign): a totally singular, self-perpendicular X forces g(q) = #X > 0. This is pure 𝔽₂ combinatorics — no cohomology — proved by the two-way evaluation of ∑_v ∑_{x∈X} (−1)^{q(v+x)}.

This file is part of the GQ2.DeepPart split (the deep-part proof); see GQ2/DeepPart.lean for the overview.

theorem GQ2.QuadraticFp2.gaussSum_eq_card_of_lagrangian {V : Type u_1} [AddCommGroup V] [Fintype V] (q : V → ZMod 2) (hq : IsQuadraticFp2 q) (X : AddSubgroup V) (hsing : ∀ x ∈ X, q x = 0) (hperp : ∀ (v : V), (∀ (x : ↥X), polar q v ↑x = 0) → v ∈ X) : gaussSum q = ↑(Nat.card ↥X)

Gauss sum over a Lagrangian: if X ≤ V is totally singular (q|X = 0) and self-perpendicular (every v pairing trivially with all of X already lies in X), then the Gauss sum is g(q) = #X. The combinatorial heart of the ramified Prop 6.18: a half-dimensional totally singular subspace forces the positive Gauss sign.

theorem GQ2.QuadraticFp2.arf_zero_of_lagrangian {V : Type u_1} [AddCommGroup V] [Fintype V] (q : V → ZMod 2) (hq : IsQuadraticFp2 q) (X : AddSubgroup V) (hsing : ∀ x ∈ X, q x = 0) (hperp : ∀ (v : V), (∀ (x : ↥X), polar q v ↑x = 0) → v ∈ X) : arf q = 0

A Lagrangian forces Arf 0 (positive Gauss sign). Given a totally singular, self-perpendicular X ≤ V (a "Lagrangian" for the nonsingular q), arf q = 0. This is the combinatorial step behind the ramified case of Prop 6.18 (eq. (115)).

theorem GQ2.QuadraticFp2.selfperp_of_card_sq {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (hq : IsQuadraticFp2 q) (h2 : ∀ (v : V), v + v = 0) (hns : Nonsingular q) (X : AddSubgroup V) (hsing : ∀ x ∈ X, q x = 0) (hcard : Nat.card ↥X ^ 2 = Nat.card V) (v : V) : (∀ (x : ↥X), polar q v ↑x = 0) → v ∈ X

Self-perpendicularity of a half-dimensional totally singular subspace (𝔽₂ duality). For a nonsingular q on an exponent-2 group with q|X = 0 and #X² = #V, the perp X⊥ equals X: anything pairing trivially with all of X already lies in X. Proof: the descended polar functional injects X⊥ ↪ (V/X)^∨ (injective by nonsingularity), so #X⊥ ≤ #(V/X) = #V/#X = #X; with X ⊆ X⊥ (total singularity) this forces X⊥ = X. (No character-extension needed.)

theorem GQ2.QuadraticFp2.arf_zero_of_card_sq {V : Type u_1} [AddCommGroup V] [Fintype V] (q : V → ZMod 2) (hq : IsQuadraticFp2 q) (h2 : ∀ (v : V), v + v = 0) (hns : Nonsingular q) (X : AddSubgroup V) (hsing : ∀ x ∈ X, q x = 0) (hcard : Nat.card ↥X ^ 2 = Nat.card V) : arf q = 0

A half-dimensional totally singular subspace forces Arf 0 (the ramified Prop 6.18 input). Combines selfperp_of_card_sq (self-⊥ from #X² = #V) with arf_zero_of_lagrangian.

def GQ2.QuadraticFp2.polarBihom {V : Type u_1} [AddCommGroup V] (q : V → ZMod 2) (hq : IsQuadraticFp2 q) : V →+ V →+ ZMod 2

The polar form, bundled biadditively (first slot outer).

Equations

• GQ2.QuadraticFp2.polarBihom q hq = AddMonoidHom.mk' (fun (v : V) => AddMonoidHom.mk' (fun (w : V) => GQ2.QuadraticFp2.polar q v w) ⋯) ⋯

@[simp]

theorem GQ2.QuadraticFp2.polarBihom_apply {V : Type u_1} [AddCommGroup V] (q : V → ZMod 2) (hq : IsQuadraticFp2 q) (v w : V) : ((polarBihom q hq) v) w = polar q v w

theorem GQ2.QuadraticFp2.addHom_restrict_surjective {A : Type u_2} [AddCommGroup A] [Finite A] (h2 : ∀ (a : A), a + a = 0) (X : AddSubgroup A) : Function.Surjective fun (f : A →+ ZMod 2) => f.comp X.subtype

Restriction of 𝔽₂-functionals to a subgroup is surjective (pure counting: the kernel of restriction is Hom(A/X, 𝔽₂), so the image has the size of Hom(X, 𝔽₂)).

theorem GQ2.QuadraticFp2.mem_of_pairing_eq_zero {A : Type u_2} [AddCommGroup A] [Finite A] (h2 : ∀ (a : A), a + a = 0) (P : A →+ A →+ ZMod 2) (hnd : ∀ (z : A), z ≠ 0 → ∃ (w : A), (P z) w ≠ 0) (X : AddSubgroup A) (hX : ∀ x ∈ X, ∀ x' ∈ X, (P x) x' = 0) (hcard : Nat.card ↥X * Nat.card ↥X = Nat.card A) {c : A} (hall : ∀ y ∈ X, (P c) y = 0) : c ∈ X

Perp membership from a Lagrangian count: for a biadditive nondegenerate 𝔽₂-pairing and a subgroup X with #X² = #A on which the pairing vanishes, anything pairing trivially with all of X lies in X (the perp has the size of X by counting, and contains it).

theorem GQ2.IsEquivariantFactorSet.m_zero {V : Type u_1} [AddCommGroup V] {C : Type u_2} [Group C] [DistribMulAction C V] {q : V → ZMod 2} {dat : FactorSet C V} (hdat : IsEquivariantFactorSet q dat) (c : C) : dat.m c 0 = 0

The equivariant-lift correction kills 0: m_c(0) = 0 (from (59) at v = w = 0).