The Hermitian-line count (paper Prop 6.18, unramified computation)

The final computation of the paper's Prop 6.18 (unramified case): on D = 𝔽_{2^{2m}} the Hermitian trace form x ↦ Tr(c·x^{2^m+1}) (c outside the fixed field D₀ = 𝔽_{2^m}, so the D₀-level form Tr_{D₀/𝔽₂}(a·N(x)) in absolute-trace clothing) has exactly 1 + (2^m+1)(2^{m−1}−1) = 2^{2m−1} − 2^{m−1} zeros — the minus-type count. Everything is finite-field counting: norm fibres are ker-cosets of size 2^m+1 (cyclic gcd count), and the nonzero trace-kernel of the fixed field contributes 2^{m−1}−1.

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

theorem GQ2.DeepPart.ringChar_eq_two_of_card {D : Type u_1} [Field D] [Fintype D] {m : ℕ} : 1 ≤ m → ∀ (hcard : Fintype.card D = 2 ^ (2 * m)), ringChar D = 2

A field of order 2^{2m} (m ≥ 1) has characteristic 2.

theorem GQ2.DeepPart.algebraMap_trace_eq {D : Type u_1} [Field D] [Fintype D] {m : ℕ} (hm : 1 ≤ m) (hcard : Fintype.card D = 2 ^ (2 * m)) [Algebra (ZMod (ringChar D)) D] (z : D) : (algebraMap (ZMod (ringChar D)) D) ((Algebra.trace (ZMod (ringChar D)) D) z) = ∑ i ∈ Finset.range (2 * m), z ^ 2 ^ i

The absolute trace of D = 𝔽_{2^{2m}}, written as the Frobenius-power sum.

theorem GQ2.DeepPart.trace_eq_zero_iff {D : Type u_1} [Field D] [Fintype D] {m : ℕ} (hm : 1 ≤ m) (hcard : Fintype.card D = 2 ^ (2 * m)) [Algebra (ZMod (ringChar D)) D] (z : D) : (Algebra.trace (ZMod (ringChar D)) D) z = 0 ↔ ∑ i ∈ Finset.range (2 * m), z ^ 2 ^ i = 0

Detecting trace-vanishing through the Frobenius-power sum.

theorem GQ2.DeepPart.trace_pow_two {D : Type u_1} [Field D] [Fintype D] {m : ℕ} (hm : 1 ≤ m) (hcard : Fintype.card D = 2 ^ (2 * m)) [Algebra (ZMod (ringChar D)) D] (z : D) : (Algebra.trace (ZMod (ringChar D)) D) (z ^ 2) = (Algebra.trace (ZMod (ringChar D)) D) z

Frobenius-invariance of the trace: Tr(z²) = Tr(z) (shift the Frobenius sum).

theorem GQ2.DeepPart.trace_pow_pow {D : Type u_1} [Field D] [Fintype D] {m : ℕ} (hm : 1 ≤ m) (hcard : Fintype.card D = 2 ^ (2 * m)) [Algebra (ZMod (ringChar D)) D] (k : ℕ) (z : D) : (Algebra.trace (ZMod (ringChar D)) D) (z ^ 2 ^ k) = (Algebra.trace (ZMod (ringChar D)) D) z

Iterated Frobenius-invariance: Tr(z^{2^k}) = Tr(z).

theorem GQ2.DeepPart.trace_eq_zero_of_frobenius_fixed {D : Type u_1} [Field D] [Fintype D] {m : ℕ} (hm : 1 ≤ m) (hcard : Fintype.card D = 2 ^ (2 * m)) [Algebra (ZMod (ringChar D)) D] {y : D} (hy : y ^ 2 ^ m = y) : (Algebra.trace (ZMod (ringChar D)) D) y = 0

The trace vanishes on the fixed field: Tr(y) = 0 whenever y^{2^m} = y (the Frobenius-sum doubles up in characteristic 2).

theorem GQ2.DeepPart.card_pow_fixed {D : Type u_1} [Field D] [Fintype D] (n : ℕ) (hn : 2 ≤ n) : Nat.card { y : D // y ^ n = y } = 1 + Nat.card { u : Dˣ // u ^ (n - 1) = 1 }

Solution count of y^n = y via the unit split: 1 + #{u : Dˣ | u^{n−1} = 1}.

def GQ2.DeepPart.frobFixed (D : Type u_2) [Field D] [CharP D 2] (m : ℕ) : AddSubgroup D

The Frobenius^m-fixed subfield 𝔽_{2^m} ⊆ D, as an additive subgroup.

Equations

• GQ2.DeepPart.frobFixed D m = { carrier := {y : D | y ^ 2 ^ m = y}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem GQ2.DeepPart.card_frobFixed {D : Type u_1} [Field D] [Fintype D] {m : ℕ} (hm : 1 ≤ m) (hcard : Fintype.card D = 2 ^ (2 * m)) [CharP D 2] : Nat.card ↥(frobFixed D m) = 2 ^ m

#𝔽_{2^m} = 2^m inside D = 𝔽_{2^{2m}} (cyclic gcd count on the units).

theorem GQ2.DeepPart.exists_trace_rep {D : Type u_1} [Field D] [Fintype D] {m : ℕ} (hm : 1 ≤ m) (hcard : Fintype.card D = 2 ^ (2 * m)) [Algebra (ZMod (ringChar D)) D] (e2 : ZMod (ringChar D) ≃+ ZMod 2) (f : D →+ ZMod 2) : ∃ (w : D), ∀ (x : D), f x = e2 ((Algebra.trace (ZMod (ringChar D)) D) (w * x))

Trace representation of 𝔽₂-functionals: every additive functional D →+ ZMod 2 is x ↦ Tr(w·x) for some w (the trace pairing is perfect, by nondegeneracy + counting).

theorem GQ2.DeepPart.exists_add_pow_eq {D : Type u_1} [Field D] [Fintype D] {m : ℕ} (hm : 1 ≤ m) (hcard : Fintype.card D = 2 ^ (2 * m)) {y : D} (hy : y ^ 2 ^ m = y) : ∃ (c : D), c + c ^ 2 ^ m = y

Artin–Schreier surjectivity onto the fixed field: every y with y^{2^m} = y is c + c^{2^m} for some c (the map c ↦ c + c^{2^m} has kernel and image the fixed field).

theorem GQ2.DeepPart.dvd_of_two_pow_sub_one_dvd {s t : ℕ} (hs : 1 ≤ s) (h : 2 ^ s - 1 ∣ 2 ^ t - 1) : s ∣ t

2^s − 1 ∣ 2^t − 1 forces s ∣ t (Euclidean division on the exponents).

theorem GQ2.DeepPart.subring_eq_top_of_normOne_le {D : Type u_1} [Field D] [Fintype D] {m : ℕ} (hm : 1 ≤ m) (hcard : Fintype.card D = 2 ^ (2 * m)) (S : Subring D) (hU : ∀ (u : Dˣ), u ^ (2 ^ m + 1) = 1 → ↑u ∈ S) : S = ⊤

A subring containing the norm-one circle is everything: a subring of D = 𝔽_{2^{2m}} containing all 2^m+1 norm-one units has 2-power order > 2^m whose predecessor divides 2^{2m}−1 (Lagrange on its unit group), forcing order 2^{2m}.

theorem GQ2.DeepPart.card_filter_eq_of_mem_range {G : Type u_2} {H : Type u_3} [Group G] [Fintype G] [DecidableEq G] [Group H] [DecidableEq H] (f : G →* H) {y : H} (hy : y ∈ f.range) : {u : G | f u = y}.card = {u : G | u ∈ f.ker}.card

Fibres of a group hom over range points have the size of the kernel.

theorem GQ2.DeepPart.hermitian_form_eq_trace_form {D : Type u_1} [Field D] [Fintype D] {m : ℕ} (hm : 1 ≤ m) (hcard : Fintype.card D = 2 ^ (2 * m)) [Algebra (ZMod (ringChar D)) D] (e2 : ZMod (ringChar D) ≃+ ZMod 2) (Q : D → ZMod 2) (hQ : QuadraticFp2.IsQuadraticFp2 Q) (hns : QuadraticFp2.Nonsingular Q) (hU : ∀ (u : Dˣ), u ^ (2 ^ m + 1) = 1 → ∀ (x : D), Q (↑u * x) = Q x) : ∃ (c : D), c ^ 2 ^ m ≠ c ∧ ∀ (x : D), Q x = e2 ((Algebra.trace (ZMod (ringChar D)) D) (c * x ^ (2 ^ m + 1)))

Lemma 6.7 (invariant quadratic forms on a Hermitian line), existence form: every nonsingular quadratic form on D = 𝔽_{2^{2m}} invariant under the norm-one circle U = {u : u^{2^m+1} = 1} is the Hermitian trace form of some c outside the fixed field. (The adjoint identity holds on a subring containing U, hence everywhere; the polar form is then trace-represented with Frobenius-fixed coefficient, an Artin–Schreier preimage matches the polars, and the additive U-invariant difference vanishes.)