The involution kernel for Lemma 6.11

The fixed-point bound for the involution in a cyclic Sylow 2-subgroup and the resulting ramified tame-pair freeness package. See GQ2.RegularSummand for the paper-facing overview and references.

The weight-orbit kernel: the involution counting bound

involution_fixedPoints_sq_le was the last sorry of the lemma_6_11 chain (the paper's pp. 29–30 weight-orbit content). It is proved here by an explicit 𝔽₂-rational trace element — a recorded deviation from the paper's 𝔽̄₂ weight-orbit argument: no base change, no idempotent decomposition, no semilinear algebra.

Set t := c τ, of odd order m with ⟨t⟩ ⊴ C, and let ω = g₀^{2^{s-1}} be the involution of the cyclic Sylow-2 subgroup (s ≥ 1; the trivial-Sylow case is handled by the consumer). Conjugation gives ω t ω⁻¹ = t^q with q² ≡ 1 (mod m).

• ω centralizes ⟨t⟩ (q ≡ 1) — impossible (two_torsion_of_centralizer_eq_one, the O₂-linchpin of Remark 6.12): the centralizer D := C_C(⟨t⟩) is abelian (⟨t⟩ is central in it and D/⟨t⟩ embeds in the cyclic C/⟨t⟩), hence its 2-torsion S is a normal 2-subgroup of C containing ω; a 2-group acting on the even-cardinality module V has a second fixed point beyond 0 (orbit counting), the S-fixed subgroup is C-stable by normality, so simplicity forces S to act trivially — against faithfulness and ω ≠ 1.

• Otherwise, an explicit trace element. g := gcd(q−1, m) is a unitary divisor: gcd(q−1, m/g) = 1 (coprime_sub_one_div_gcd, from m ∣ (q−1)(q+1) and m odd). So on u := t^g, of order r := m/g, multiplication by q is a fixed-point-free involution of (ZMod r) ∖ {0}. Every nontrivial power of t has zero fixed space (fixedPoints_zpowers_tame_eq_zero: its fixed subgroup is C-stable since ⟨t⟩ ⊴ C, and faithfulness kills ⊤), so the geometric sum ∑_{j<r} u^j • v vanishes (sum_range_orderOf_smul_eq_zero). For ω-fixed v, summing over the val-smaller half Λ of each pair {k, qk} gives w := ∑_{k∈Λ} u^{k.val} • v with w + ω•w = ∑_{k≠0} u^{k.val} • v = v — an explicit additive-Hilbert-90 trace. Hence ker(1+ω) ⊆ range(1+ω), and #V^ω ^ 2 ≤ #ker·#range = #V by first-isomorphism counting.

theorem GQ2.fixedPoints_zpowers_tame_eq_zero {C : Type} [Group C] [Finite C] {V : Type} [AddCommGroup V] [DistribMulAction C V] {sg t : C} (hgen : Subgroup.closure {sg, t} = ⊤) (hrel : sg⁻¹ * t * sg = t ^ 2) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) {n : C} (hn : n ∈ Subgroup.zpowers t) (hn1 : n ≠ 1) (v : V) : n • v = v → v = 0

Every nontrivial element of the inertia ⟨t⟩ has zero fixed space on a faithful simple module — the "all isotypic factors are faithful" content of the weight-orbit plan, in operator form. The fixed space of n = t^k is C-stable (a conjugate h⁻¹ n h = (h⁻¹th)^k is again a power of n since h⁻¹th ∈ ⟨t⟩ by normality); simplicity leaves ⊥ or ⊤, and ⊤ makes n act trivially, so n = 1 by faithfulness.

theorem GQ2.sum_range_orderOf_smul_eq_zero {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] {u : C} (hfree : ∀ (v : V), u • v = v → v = 0) (v : V) : ∑ j ∈ Finset.range (orderOf u), u ^ j • v = 0

The geometric sum of a fixed-point-free finite-order action vanishes: the sum ∑_{j < orderOf u} u^j • v is u-invariant, so it lies in the zero fixed space.

theorem GQ2.two_torsion_of_centralizer_eq_one {C : Type} [Group C] [Finite C] {V : Type} [AddCommGroup V] [DistribMulAction C V] [Finite V] {sg t : C} (hgen : Subgroup.closure {sg, t} = ⊤) (hrel : sg⁻¹ * t * sg = t ^ 2) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hV0 : ∃ (v₀ : V), v₀ ≠ 0) {x : C} (hx2 : x ^ 2 = 1) (hxt : x * t = t * x) : x = 1

The O₂-linchpin (Remark 6.12): on a nonzero faithful simple 2-torsion module, an element of order dividing 2 commuting with the inertia generator t is trivial. The centralizer D := C_C(⟨t⟩) is abelian (⟨t⟩ ≤ Z(D) and D/⟨t⟩ embeds in the cyclic C/⟨t⟩, so commutative_of_cyclic_center_quotient applies); its 2-torsion S is therefore a subgroup, normal in C, and IsPGroup 2. A 2-group acting on a module of even cardinality with one fixed point has another (IsPGroup.exists_fixed_point_of_prime_dvd_card_of_fixed_point), so the S-fixed subgroup is nonzero and C-stable, hence ⊤ by simplicity: S acts trivially and faithfulness collapses it.

theorem GQ2.involution_fixedPoints_sq_le_of_tame_pair {C : Type} [Group C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] {sg t : C} (hgen : Subgroup.closure {sg, t} = ⊤) (hrel : sg⁻¹ * t * sg = t ^ 2) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ (v : V), t • v ≠ v) (P : Sylow 2 C) (g₀ : ↥↑P) (hg : ∀ (x : ↥↑P), x ∈ Subgroup.zpowers g₀) (s : ℕ) (hs1 : 1 ≤ s) (hs : Nat.card ↥↑P = 2 ^ s) : Nat.card { v : V // g₀ ^ (2 ^ s / 2) • v = v } ^ 2 ≤ Nat.card V

The involution counting bound (the key finite-group input to Lemma 6.11): the involution ω = g₀^{2^{s-1}} of the cyclic Sylow-2 subgroup acts freely enough on the ramified simple faithful module, #V^ω ^ 2 ≤ #V. This is the p = 2 elementary-abelian case of the paper's pp. 29–30 weight-orbit argument.

The hypothesis hs1 : 1 ≤ s is necessary. The bound is false for a trivial Sylow-2 subgroup (s = 0 gives ω = 1, e.g. the Frobenius group C₇ ⋊ C₃ of order 21 acting on 𝔽₈ is ramified simple faithful with #V^ω = #V); the sole consumer card_fixedPoints_pow_le_of_ramified needs no leaf there (#V^P ^ 1 ≤ #V is subtype counting).

Proof: t := c τ has odd order m and ⟨t⟩ ⊴ C; conjugation gives ω t ω⁻¹ = t^q, q² ≡ 1 (mod m). If t^q = t, then ω lies in the 2-torsion of the abelian centralizer C_C(⟨t⟩) — a normal 2-subgroup acting trivially by simplicity, against faithfulness (two_torsion_of_centralizer_eq_one), impossible since ω ≠ 1. Otherwise the trace element w := ∑_{k ∈ Λ} (t^g)^{k.val} • v over a transversal Λ of the fixed-point-free involution k ↦ qk of (ZMod (m/g)) ∖ {0} (g := gcd(q−1, m), unitary by coprime_sub_one_div_gcd) satisfies w + ω•w = v for every ω-fixed v (geometric-sum vanishing sum_range_orderOf_smul_eq_zero + fixedPoints_zpowers_tame_eq_zero), so ker(1+ω) ⊆ range(1+ω) and first-isomorphism counting gives the bound.

theorem GQ2.card_fixedPoints_pow_le_of_ramified_of_tame_pair {C : Type} [Group C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] {sg t : C} (hgen : Subgroup.closure {sg, t} = ⊤) (hrel : sg⁻¹ * t * sg = t ^ 2) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ (v : V), t • v ≠ v) (P : Sylow 2 C) : Nat.card { v : V // ∀ (p : ↥↑P), p • v = v } ^ Nat.card ↥↑P ≤ Nat.card V

The Sylow-2 fixed-space bound on a ramified simple faithful module. The full bound #V^P ^ |P| ≤ #V follows (via card_fixedPoints_pow_le_of_half, the elementary-abelian reduction) from the involution counting bound #V^ω ^ 2 ≤ #V for the involution ω = g₀^{2^{s-1}} in the cyclic Sylow-2 subgroup (involution_fixedPoints_sq_le above, which needs 1 ≤ s); a trivial Sylow-2 subgroup gives the bound by subtype counting.

Faithfulness is genuinely needed (Remark 6.12: C₃ ⋊ C₄ acting through S₃ on 𝔽₄ is ramified simple but its central C₂ fixes everything, so #V^ω = #V > #V^{1/2}).

theorem GQ2.sylow_free_of_ramified_of_tame_pair {C : Type} [Group C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] {sg t : C} (hgen : Subgroup.closure {sg, t} = ⊤) (hrel : sg⁻¹ * t * sg = t ^ 2) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ (v : V), t • v ≠ v) (P : Sylow 2 C) : ∃ (r : ℕ) (φ : V ≃+ (Fin r → ↥↑P → ZMod 2)), ∀ (p : ↥↑P) (v : V) (n : Fin r) (x : ↥↑P), φ (↑p • v) n x = φ v n (p⁻¹ * x)

𝔽₂[P]-freeness of the restriction to the Sylow 2-subgroup (Lemma 6.11, steps 1–2): a ramified simple faithful module is equivariantly additively isomorphic to a regular module 𝔽₂[P]^r. Proved from the counting criterion free_of_card_fixedPoints_pow_le at the cyclic Sylow 2-subgroup (isCyclic_of_isPGroup_two_of_tame, with the tame relation transported from tame_relation along c) and the counting bound card_fixedPoints_pow_le_of_ramified above. This argument uses only the standard axioms.

theorem GQ2.sylow_split_pair_of_ramified_of_tame_pair {C : Type} [Group C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] {sg t : C} (hgen : Subgroup.closure {sg, t} = ⊤) (hrel : sg⁻¹ * t * sg = t ^ 2) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ (v : V), t • v ≠ v) (P : Sylow 2 C) : ∃ (r : ℕ) (j : V →+ Fin r → ↥↑P → ZMod 2) (q : (Fin r → ↥↑P → ZMod 2) →+ V), (∀ (p : ↥↑P) (v : V) (n : Fin r) (x : ↥↑P), j (↑p • v) n x = j v n (p⁻¹ * x)) ∧ (∀ (p : ↥↑P) (F : Fin r → ↥↑P → ZMod 2), (q fun (n : Fin r) (x : ↥↑P) => F n (p⁻¹ * x)) = ↑p • q F) ∧ ∀ (v : V), q (j v) = v

The weight-orbit kernel in split-pair form (what lemma_6_11 consumes): the equivariant 𝔽₂[P]-freeness sylow_free_of_ramified yields an equivariant split pair — take j := φ, q := φ⁻¹. Retraction equivariance is φ's equivariance transported across the iso (φ⁻¹-inject, then φ's equivariance at φ⁻¹ F), and q ∘ j = id is φ⁻¹ ∘ φ = id.

theorem GQ2.lemma_6_11_of_tame_pair {C : Type} [Group C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] {sg t : C} (hgen : Subgroup.closure {sg, t} = ⊤) (hrel : sg⁻¹ * t * sg = t ^ 2) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ (v : V), t • v ≠ v) : ∃ (N : ℕ) (ι : V →+ Fin N → C → ZMod 2) (r : (Fin N → C → ZMod 2) →+ V), (∀ (h : C) (v : V) (n : Fin N) (x : C), ι (h • v) n x = ι v n (h⁻¹ * x)) ∧ (∀ (h : C) (F : Fin N → C → ZMod 2), (r fun (n : Fin N) (x : C) => F n (h⁻¹ * x)) = h • r F) ∧ ∀ (v : V), r (ι v) = v

Lemma 6.11, abstract tame-pair form: the split-summand package from a generating pair (sg, t) with the tame relation, rather than a Ttame-marking. This is the form the κ⁰ assembly consumes (ActsThroughTame supplies exactly such a pair); the Ttame form below is a wrapper.

theorem GQ2.lemma_6_11 {C : Type} [Group C] [TopologicalSpace C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] (c : ↑Ttame.toProfinite.toTop →ₜ* C) (hgen : Subgroup.closure {c tameSigma, c tameTau} = ⊤) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ (v : V), c tameTau • v ≠ v) : ∃ (N : ℕ) (ι : V →+ Fin N → C → ZMod 2) (r : (Fin N → C → ZMod 2) →+ V), (∀ (h : C) (v : V) (n : Fin N) (x : C), ι (h • v) n x = ι v n (h⁻¹ * x)) ∧ (∀ (h : C) (F : Fin N → C → ZMod 2), (r fun (n : Fin N) (x : C) => F n (h⁻¹ * x)) = h • r F) ∧ ∀ (v : V), r (ι v) = v

Lemma 6.11 (paper node, §6.3): a ramified simple faithful 2-torsion module over the tame image is an equivariant split summand of a regular module. The regular module 𝔽₂[C]^N is Fin N → C → ZMod 2 with the left-translation action written inline; ι is the equivariant embedding, r the equivariant retraction.

The proof composes the odd-index relative trace regular_summand_of_subgroup_summand at a Sylow 2-subgroup (Sylow.not_dvd_index gives the odd index) composed with the weight-orbit kernel sylow_split_pair_of_ramified above.

From this the deep-count multiplicativity (Hom(V^∨, −)-exactness) follows — equivariant_lift_of_regular_summand below — which is the sole remaining input to lemma_6_17_dim's lower bound #X₊ ≥ 2^m. Applied at V := V^∨ (also ramified simple faithful) by the consumer.