The κ⁰ normal form on permutation modules and the tame assembly

The analytic heart of the paper's Lemma 6.3 (κ⁰ base-class existence), in its own file for the kappa0_exists splice in GQ2/SectionNine.lean. This file carries copies of the small factor-set assembly lemmas in the GQ2.SectionNine namespace to avoid an import cycle; the scoping discussion is recorded in docs/orchestration/p17e-kappa0-scoping.md. The generic-in-V copies (datum_*, polar_*, isQuadraticFp2_*, quadratic_expansion, polar_sum_right) are public because the §6.2 orbit decomposition in GQ2/OrbitDecomp.lean consumes them.

Contents

• PermW H K — the permutation module 𝔽₂[H]^K (the codomain of lemma_6_11's split pair), a reducible synonym of Fin K → H → ZMod 2 carrying the blockwise left-translation DistribMulAction H instance. ⚠ Because the synonym is reducible, the instance is keyed on the raw function type Fin K → H → ZMod 2 (same H in both positions); no other instance can currently apply there (ZMod 2 carries no action of an abstract H), and the only importer is the §9 layer.
• quadratic_eq_double_sum — the expansion of a quadratic map in basis coordinates, in ordered-pair form: for any kernel f₀ with f₀ p p = Q(e_p) and f₀ p p' + f₀ p' p = polar Q (e_p) (e_{p'}), one has Q F = ∑_{p,p'} F_p F_{p'} f₀(p,p').
• invBlockSquare/isEquivariantFactorSet_invBlockDatum — the involution correction E_{n,u} (paper Lemma 6.2): the §9 induction's invOrbitDatum, instantiated at N = ⊥ and transported to block n of PermW H K by comapHom/comap (no new orientation bookkeeping).
• exists_datum_of_invariant_quadratic — the normal form (paper (75)/(76) + Lemma 6.2, assembly): every H-invariant quadratic map on PermW H K admits an equivariant factor-set datum. Deviation (documented): instead of decomposing into individual orbit polynomials S_j/C_{j,k,g} we build a single invariant biadditive refinement from the relative-position coordinates β n m u := polar Q (e_{n,1}) (e_{m,u}) — possible exactly off the involution locus, which is corrected by subtracting the E_{n,u} first. Equivalent to the paper's normal form with far less case machinery.
• kappa0_exists_tame — the full assembly over an abstract finite tame-generated group: 2-torsion derivation from nonsingularity, faithful-image reduction (via DistribMulAction.toAddAut, no quotient groups), the odd/unramified branch (t acts trivially ⟹ t = 1 ⟹ |Ĥ| odd by the O₂-linchpin ⟹ averaging), and the ramified branch (lemma_6_11_of_tame_pair ⟹ split pair ⟹ normal form ⟹ pullback). SectionNine.kappa0_exists becomes a two-reduction splice of this.

No axioms; Ax = ∅ (std-3 throughout).

The permutation module 𝔽₂[H]^K with the left-translation action

@[reducible, inline]

abbrev GQ2.PermW (H : Type) (K : ℕ) : Type

The permutation module 𝔽₂[H]^K — the codomain of lemma_6_11's split pair — as a reducible synonym; the DistribMulAction H instance below is the blockwise left-translation (h • F) n x = F n (h⁻¹x) (mirroring RegRep's convention).

Equations

• GQ2.PermW H K = (Fin K → H → ZMod 2)

@[implicit_reducible]

instance GQ2.instDistribMulActionPermW {H : Type} [Group H] {K : ℕ} : DistribMulAction H (PermW H K)

Blockwise left translation on 𝔽₂[H]^K. ⚠ Keyed on the raw function type (see the module docstring): do not introduce competing actions of H on Fin K → H → ZMod 2.

Equations

• GQ2.instDistribMulActionPermW = { smul := fun (h : H) (F : GQ2.PermW H K) (n : Fin K) (x : H) => F n (h⁻¹ * x), mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

theorem GQ2.PermW.smul_apply {H : Type} [Group H] {K : ℕ} (h : H) (F : PermW H K) (n : Fin K) (x : H) : (h • F) n x = F n (h⁻¹ * x)

noncomputable def GQ2.permBas {H : Type} {K : ℕ} (n : Fin K) (x : H) : PermW H K

The coordinate basis of PermW H K (the indicator of the coordinate (n, x)).

Equations

• GQ2.permBas n x m y = if m = n ∧ y = x then 1 else 0

theorem GQ2.permBas_smul {H : Type} [Group H] {K : ℕ} (h : H) (n : Fin K) (x : H) : h • permBas n x = permBas n (h * x)

Left translation carries basis vectors to basis vectors: h • e_{(n,x)} = e_{(n,hx)}.

theorem GQ2.permBas_support_decomp {H : Type} {K : ℕ} [Fintype H] (F : PermW H K) : F = ∑ p : Fin K × H with F p.1 p.2 = 1, permBas p.1 p.2

Every F : PermW H K is the sum of the basis vectors at its support.

The expansion of a quadratic map in coordinates (ordered-pair form)

theorem GQ2.polar_sum_right {V : Type u_1} [AddCommGroup V] {Q : V → ZMod 2} (hQ : QuadraticFp2.IsQuadraticFp2 Q) {ι : Type u_2} (v : ι → V) (x : V) (s : Finset ι) : QuadraticFp2.polar Q x (∑ i ∈ s, v i) = ∑ i ∈ s, QuadraticFp2.polar Q x (v i)

The polar form is additive in the second argument over finite sums (with polar Q x 0 = 0 from char 2).

theorem GQ2.quadratic_expansion {V : Type u_1} [AddCommGroup V] {Q : V → ZMod 2} (hQ : QuadraticFp2.IsQuadraticFp2 Q) {ι : Type u_2} (v : ι → V) (f₀ : ι → ι → ZMod 2) (hdiag : ∀ (i : ι), f₀ i i = Q (v i)) (hpolar : ∀ (i j : ι), i ≠ j → f₀ i j + f₀ j i = QuadraticFp2.polar Q (v i) (v j)) (s : Finset ι) : Q (∑ i ∈ s, v i) = ∑ i ∈ s, ∑ j ∈ s, f₀ i j

Expansion of a quadratic map over a family, ordered-pair form: if f₀ matches Q on the diagonal and symmetrizes to the polar form off it, then Q (∑_{i∈s} v i) = ∑_{i,j∈s} f₀ i j. (No Sym2: the two off-diagonal orders share the polar value between them.)

Private copies of the §9 factor-set assembly layer

These live in namespace GQ2.SectionNine, which will import this file for the splice — so we carry private copies (verbatim proofs). See the module docstring.

theorem GQ2.datum_of_invariant {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} {f : V → V → ZMod 2} (hcoc : ∀ (v w x : V), f (v + w) x + f v w = f v (w + x) + f w x) (hdiag : ∀ (v : V), f v v = q v) (hpolar : ∀ (v w : V), f v w + f w v = QuadraticFp2.polar q v w) (h0l : ∀ (v : V), f 0 v = 0) (h0r : ∀ (v : V), f v 0 = 0) (hinv : ∀ (c : C) (v w : V), f (c • v) (c • w) = f v w) : IsEquivariantFactorSet q { f := f, m := fun (x : C) (x_1 : V) => 0 }

Private copy of SectionNine.isEquivariantFactorSet_of_invariant.

theorem GQ2.datum_of_biadditive_invariant {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} {f : V → V → ZMod 2} (hl : ∀ (v v' w : V), f (v + v') w = f v w + f v' w) (hr : ∀ (v w w' : V), f v (w + w') = f v w + f v w') (hdiag : ∀ (v : V), f v v = q v) (hinv : ∀ (c : C) (v w : V), f (c • v) (c • w) = f v w) : IsEquivariantFactorSet q { f := f, m := fun (x : C) (x_1 : V) => 0 }

Private copy of SectionNine.isEquivariantFactorSet_of_biadditive_invariant.

theorem GQ2.datum_add {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q q' : V → ZMod 2} {dat dat' : FactorSet C V} (h : IsEquivariantFactorSet q dat) (h' : IsEquivariantFactorSet q' dat') : IsEquivariantFactorSet (fun (v : V) => q v + q' v) { f := fun (v w : V) => dat.f v w + dat'.f v w, m := fun (c : C) (v : V) => dat.m c v + dat'.m c v }

Private copy of SectionNine.IsEquivariantFactorSet.add.

theorem GQ2.datum_comap {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {W : Type u_3} [AddCommGroup W] [DistribMulAction C W] {q : W → ZMod 2} {dat : FactorSet C W} (hdat : IsEquivariantFactorSet q dat) (i : V →+ W) (hi : ∀ (c : C) (v : V), i (c • v) = c • i v) : IsEquivariantFactorSet (fun (v : V) => q (i v)) (dat.comap i)

Private copy of SectionNine.IsEquivariantFactorSet.comap.

theorem GQ2.datum_isInvariant {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} {dat : FactorSet C V} (hdat : IsEquivariantFactorSet q dat) (h2 : ∀ (v : V), v + v = 0) : QuadraticFp2.IsInvariant C q

A datum forces invariance of its square map (on a 2-torsion module): m_quad at (v, v) collapses to f(cv, cv) = f(v, v).

theorem GQ2.datum_isQuadratic {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} {dat : FactorSet C V} (hdat : IsEquivariantFactorSet q dat) (hfl : ∀ (v v' w : V), dat.f (v + v') w = dat.f v w + dat.f v' w) (hfr : ∀ (v w w' : V), dat.f v (w + w') = dat.f v w + dat.f v w') : QuadraticFp2.IsQuadraticFp2 q

A datum with a biadditive factor set forces its square map to be quadratic.

The involution-block correction E_{n,u} (paper Lemma 6.2, transported)

the §9 induction's invOrbitDatum lives over G ⧸ N acting on RegRep N. We instantiate it at G := H, N := ⊥ and transport along the canonical H ≃* H ⧸ ⊥ (comapHom) and the block projection PermW H K →+ RegRep ⊥ (comap) — no new orientation bookkeeping. The package records the two coordinate facts the normal form consumes: E vanishes on basis vectors, and its polar form is the indicator of the u-pairing on block n.

theorem GQ2.exists_invBlock_datum {H : Type} [Group H] {K : ℕ} [Fintype H] (n : Fin K) {u : H} (hu2 : u * u = 1) (hu1 : u ≠ 1) : ∃ (E : PermW H K → ZMod 2) (dat : FactorSet H (PermW H K)), IsEquivariantFactorSet E dat ∧ QuadraticFp2.IsQuadraticFp2 E ∧ (∀ (p : Fin K × H), E (permBas p.1 p.2) = 0) ∧ ∀ (p p' : Fin K × H), p ≠ p' → QuadraticFp2.polar E (permBas p.1 p.2) (permBas p'.1 p'.2) = if p.1 = n ∧ p'.1 = n ∧ p'.2 = p.2 * u then 1 else 0

The involution-block datum: for an involution u of H and a block n, there is a quadratic map E on 𝔽₂[H]^K with an equivariant factor-set datum whose basis diagonal is zero and whose basis polar form is the indicator of {x' = xu} on block n (the orbit polynomial E_{n,u} of the paper's normal form, Lemma 6.2).

The normal form: every invariant quadratic map on 𝔽₂[H]^K has a datum

The paper's step 2 of Lemma 6.3. Deviation (documented in the module docstring): a single invariant biadditive refinement f(F,G) = ∑ F_{n,x} G_{m,y} φ(n, m, x⁻¹y) replaces the square/free orbit-polynomial sums; the φ-kernel exists exactly off the involution locus, which is corrected by the E_{n,u} data first.

theorem GQ2.polar_finset_sum {V : Type u_1} [AddCommGroup V] {ι : Type u_2} (s : Finset ι) (qs : ι → V → ZMod 2) (v w : V) : QuadraticFp2.polar (fun (x : V) => ∑ i ∈ s, qs i x) v w = ∑ i ∈ s, QuadraticFp2.polar (qs i) v w

theorem GQ2.isQuadraticFp2_finset_sum {V : Type u_1} [AddCommGroup V] {ι : Type u_2} (s : Finset ι) (qs : ι → V → ZMod 2) (h : ∀ i ∈ s, QuadraticFp2.IsQuadraticFp2 (qs i)) : QuadraticFp2.IsQuadraticFp2 fun (v : V) => ∑ i ∈ s, qs i v

theorem GQ2.exists_datum_of_invariant_quadratic {H : Type} [Group H] {K : ℕ} [Finite H] (Q : PermW H K → ZMod 2) (hQ : QuadraticFp2.IsQuadraticFp2 Q) (hinv : QuadraticFp2.IsInvariant H Q) : ∃ (dat : FactorSet H (PermW H K)), IsEquivariantFactorSet Q dat

The κ⁰ normal form (Lemma 6.3, step 2): every H-invariant quadratic map on the permutation module 𝔽₂[H]^K admits an equivariant factor-set datum.

The tame assembly (Lemma 6.3, all pieces)

kappa0_exists_tame is the full statement over an abstract finite tame-generated group; the SectionNine.kappa0_exists splice unpacks ActsThroughTame/IsSimpleModTwo and pulls back along the surjection with comapHom.

theorem GQ2.kappa0_exists_tame {H : Type} [Group H] [Finite H] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction H V] {s t : H} (hgen : Subgroup.closure {s, t} = ⊤) (hrel : s⁻¹ * t * s = t ^ 2) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (hinv : QuadraticFp2.IsInvariant H q) (hnt : Nontrivial V) (hsimple : ∀ (W : AddSubgroup V), (∀ (g : H), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) : ∃ (dat : FactorSet H V), IsEquivariantFactorSet q dat

κ⁰ existence over a finite tame-generated group (paper Lemma 6.3): a nonsingular invariant quadratic map on a nontrivial simple module for a finite group generated by a tame pair (s, t) admits an equivariant factor-set datum.

Proof: 2-torsion follows from simplicity + nonsingularity (an odd-order module has zero polar pairings); the action factors through the faithful image Ĥ ≤ AddAut V (toAddAut), where either t̂ acts trivially — then t̂ = 1, |Ĥ| is odd (an involution would commute with t̂ and die by the O₂-linchpin two_torsion_of_centralizer_eq_one), and averaging gives the datum (datum_of_odd) — or the module is ramified and lemma_6_11_of_tame_pair split-embeds V into 𝔽₂[Ĥ]^N, where the normal form exists_datum_of_invariant_quadratic applies and pulls back (datum_of_split).

Paper-tag ledger (auto-generated by paperforge; do not edit)

• Lemma 6.2 = ⟦lem-halforbitcocycle⟧
• Lemma 6.3 = ⟦lem-basedetclass⟧