Actionization of the Γ_A Gauss counts

Transport of the signed counts to the faithful quotient action.

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

A-4.5b: the actionization — counts at the faithful quotient

The SectionSix count pins (prop_6_9_*) take faithfulness and the ELEMENT-level tame dichotomy, neither of which the seam has (hfaith is not block-derivable — the e6/e7 amendment). The resolution: quotient the acting group by the action kernel. The induced action of C ⧸ K has the same orbit values (so hsimple/hinv transport verbatim), is faithful BY CONSTRUCTION (kerLift_injective-shaped), and converts the action-level dichotomy into the element-level one (c' τ = 1 ⟺ c τ acts trivially).

theorem GQ2.SectionEight.AffineTLift.zeroCount_unramified_of_action {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] (c : ↑Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (hsimple : ∀ (W : AddSubgroup V), (∀ (g : C), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hV : ∃ (v : V), v ≠ 0) (hunram : ∀ (v : V), c tameTau • v = v) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (hinv : QuadraticFp2.IsInvariant C q) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) : QuadraticFp2.zeroCount q = 2 ^ (2 * m - 1) - 2 ^ (m - 1)

The unramified zero count from action-level hypotheses (prop_6_9_unramified through the faithful quotient): no hfaith, and hunram in the action form the seam carries.

theorem GQ2.SectionEight.AffineTLift.finsum_sign_unramified_of_action {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] (c : ↑Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (hsimple : ∀ (W : AddSubgroup V), (∀ (g : C), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hV : ∃ (v : V), v ≠ 0) (hunram : ∀ (v : V), c tameTau • v = v) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (hinv : QuadraticFp2.IsInvariant C q) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) : ∑ᶠ (v : V), sign (q v) = -2 ^ m

The unramified V-sum: ∑ᶠ sign(q̄ v) = −2^m from action-level hypotheses — the value the unramified seam consumes after the x₀-supported section reindex.

theorem GQ2.SectionEight.AffineTLift.zeroCount_qDouble_ramified_of_faithful {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] (c : ↑Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (hfaith : ∀ (g : C), (∀ (v : V), g • v = v) → g = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (g : C), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : c tameTau ≠ 1) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (hinv : QuadraticFp2.IsInvariant C q) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) : QuadraticFp2.zeroCount (QuadraticFp2.qDouble q fun (x : V) => powOmega2 (c tameSigma) • x) = 2 ^ (2 * m - 1) + 2 ^ (m - 1)

THE RAMIFIED PACK, DISCHARGED (the Γ_A Gauss-sum package): prop_6_9_ramified's isotypic pack (s r a Wt e he hVU hrank) derived from the faithful simple ramified hypotheses via GQ2/RamifiedPack.lean — the single isotype P ∣ X^d − 1 (exists_single_isotype), the free D = AdjoinRoot P-structure V ≃+ D^{sV} (exists_isotypic_equiv), f = deg P even by the polar-adjoint involution (even_natDegree_of_aeval_inv_eq_zero), the ⟨cτ⟩-module Wt := D (rootAction/adjoinRoot_add_self/isSimpleModTwo_rootAction/equiv_zpowers_smul), the σ-semilinear descent count #V^U = 2^{r·sV} (card_fixed_powOmega2), and the rank parity from the first isomorphism theorem.

theorem GQ2.SectionEight.AffineTLift.zeroCount_qDouble_ramified_of_action {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] (c : ↑Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (hsimple : ∀ (W : AddSubgroup V), (∀ (g : C), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ (v : V), c tameTau • v ≠ v) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (hinv : QuadraticFp2.IsInvariant C q) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) : QuadraticFp2.zeroCount (QuadraticFp2.qDouble q fun (x : V) => powOmega2 (c tameSigma) • x) = 2 ^ (2 * m - 1) + 2 ^ (m - 1)

The ramified zero count from action-level hypotheses: the A-4.5b actionization pushed through qDouble — the faithful quotient has the same σ₂-action values (powOmega2_map along mk'), the action-level hram element-izes, and the proved faithful-level count applies verbatim.

theorem GQ2.SectionEight.AffineTLift.finsum_sign_ramified_of_action {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] (c : ↑Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (hsimple : ∀ (W : AddSubgroup V), (∀ (g : C), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ (v : V), c tameTau • v ≠ v) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (hinv : QuadraticFp2.IsInvariant C q) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card V = 2 ^ (2 * m)) : ∑ᶠ (v : V), sign (QuadraticFp2.qDouble q (fun (x : V) => powOmega2 (c tameSigma) • x) v) = 2 ^ m

The ramified V-sum: ∑ᶠ sign(qDouble) = +2^m — the plus finale on the ramified count.