Signed-count and even-cardinality bricks

The finite quadratic signed count and the even-dimension consequence of nonsingularity.

See GQ2.GaussZ.FinalGammaA for the paper-facing overview, source citations, and deviations.

A-4.5 bricks: the V-indexed signed count and the qDouble orientation bridge

En-free pieces of the seam assembly: the finsum_sign_eq extraction re-indexed by a plain finite type (the x₀-supported section makes the Gauss domain literally V), its two pinned-count finales (∓2^m), and the U⁻¹/U orientation identification that matches A-4.4b's Wall double to qDouble.

theorem GQ2.SectionEight.AffineTLift.finsum_sign_eq_count {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (zc : ℕ) (hzc : QuadraticFp2.zeroCount q = zc) {n : ℕ} (hn : Nat.card V = n) : ∑ᶠ (v : V), sign (q v) = 2 * ↑zc - ↑n

The signed-sum extraction over a plain finite type: with zeroCount q and #V known, ∑ᶠ sign(q v) = 2·zeroCount − #V (the GaussZLocal.finsum_sign_eq shape, En-free).

theorem GQ2.SectionEight.AffineTLift.finsum_sign_eq_neg_of_zeroCount {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (m : ℕ) (hm : 1 ≤ m) (hzc : QuadraticFp2.zeroCount q = 2 ^ (2 * m - 1) - 2 ^ (m - 1)) (hcard : Nat.card V = 2 ^ (2 * m)) : ∑ᶠ (v : V), sign (q v) = -2 ^ m

The minus finale: ∑ᶠ sign = −2^m from the unramified zero count 2^{2m−1} − 2^{m−1} (prop_6_9_unramified / zeroCount_of_arf_one's value).

theorem GQ2.SectionEight.AffineTLift.finsum_sign_eq_pos_of_zeroCount {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (m : ℕ) (hm : 1 ≤ m) (hzc : QuadraticFp2.zeroCount q = 2 ^ (2 * m - 1) + 2 ^ (m - 1)) (hcard : Nat.card V = 2 ^ (2 * m)) : ∑ᶠ (v : V), sign (q v) = 2 ^ m

The plus finale: ∑ᶠ sign = +2^m from the ramified zero count 2^{2m−1} + 2^{m−1} (prop_6_9_ramified / zeroCount_of_arf_zero's value).

theorem GQ2.SectionEight.AffineTLift.polar_smul_inv_eq {C : Type u_1} [Group C] {V : Type u_2} [AddCommGroup V] [DistribMulAction C V] (q : V → ZMod 2) (U : C) (hUq : ∀ (v : V), q (U • v) = q v) (x : V) : QuadraticFp2.polar q x (U⁻¹ • x) = QuadraticFp2.polar q x (U • x)

The qDouble orientation bridge: for q invariant under U, the Wall-double twist reads the same with U⁻¹ as with U — B(x, U⁻¹•x) = B(x, U•x) — so A-4.4b's value q(v) + B(v, σ₂⁻¹•v) IS qDouble q (σ₂ • ·) at v.

The even-dimension fact: nonsingular ⟹ #V = 2^{2m}

The c3-G0 package needs #V = 2^{2m} — the classical symplectic fact that a nonsingular alternating pairing forces even dimension, in counting form: split off a hyperbolic pair (v, w) through the surjective pairing hom u ↦ (B(u,v), B(u,w)) onto 𝔽₂²; the kernel is the perpendicular complement, of index exactly 4, and stays nonsingular.

theorem GQ2.SectionEight.AffineTLift.card_eq_two_pow_two_mul_of_nonsingular {V : Type u} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (hV₂ : ∀ (v : V), v + v = 0) : ∃ (m : ℕ), Nat.card V = 2 ^ (2 * m)

theorem GQ2.SectionEight.AffineTLift.exists_one_le_card_eq_two_pow_of_nonsingular {V : Type u_1} [AddCommGroup V] [Finite V] (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (hV₂ : ∀ (v : V), v + v = 0) (hVne : ∃ (v : V), v ≠ 0) : ∃ (m : ℕ), 1 ≤ m ∧ Nat.card V = 2 ^ (2 * m)

The consumer form: with a nonzero vector, #V = 2^{2m} with m ≥ 1 — the c3-G0 package's cardinality field, derived from the enrichment's nonsingular form.