The §6.2 orbit-sum decomposition on a multi-block regular module

The orbit decomposition of a (G/N)-invariant quadratic map Q on the block module 𝔽₂[G/N]^K = Fin K → RegRep N into the paper's three orbit-polynomial types ((75)/(76)/Lemma 6.2): the equivariant factor-set datum for Q is the sumDatum of

• square summands (squareOrbitDatum N).comap (blockProj j) — one per block j with Q(e_{j,1}) = 1;
• involution summands (invOrbitDatum N ū).comap (blockProj j) — one per block-involution position (j, ū) (ū² = 1 ≠ ū) with polar coordinate 1;
• free summands (freeOrbitDatum N ū).comap (blockProj₂ j k) — one per chosen orientation representative of the swap-orbit {(j,k,ū), (k,j,ū⁻¹)} with polar coordinate 1 (the same-block case j = k uses the non-injective pair projection).

Every summand is a definitional FactorSet.comap of a literal OrbitData datum, so the per-orbit graph pullbacks are syntactically the Lemma-6.15 inputs (SectionSix.lemma_6_15_square/free/involution) at the block coordinates of the cocycle — no per-orbit datum bridging is needed downstream (the Lemma 6.17 vanishing proof).

This is the orbit-decomposition clause of the Lemma 6.17 vanishing interface (docs/orchestration/p15f2b-foundation-notes.md); the banked normal form exists_datum_of_invariant_quadratic (the §9 induction) deliberately took the non-orbit-decomposed single-β route and cannot supply it. Layer plan:

• Carrier layer: the coordinate basis blockBas, its translation action, and the support decomposition (mirrors permBas/permBas_support_decomp on PermW).
• Coordinate layer: the diagonal/relative-position coordinates blockDiag/blockPolar of an invariant Q and their invariance reductions (mirrors the have-blocks of exists_datum_of_invariant_quadratic).
• Orientation layer: the swap posSwap on positions, the free/involution classification, and the orientation transversal freeReps (a noncomputable linear order picks one representative per free swap-orbit; the order never appears in any statement).
• Summand layer (§6.2): the three block datums, their equivariance, and their basis diagonal/polar evaluations.
• Assembly: the matching of basis coordinates and the capstone IsEquivariantFactorSet Q (sumDatum … orbitDatum) over an abstract pair (G, N).

Galois-free: everything is finite group theory over (G, N), [Finite (G ⧸ N)]. No axioms; Ax = ∅ (std-3 throughout).

The carrier 𝔽₂[G/N]^K and its coordinate basis

noncomputable def GQ2.regInd {G : Type u_1} [Group G] (N : Subgroup G) (y : G ⧸ N) : RegRep N

The single-coordinate indicator of the regular module 𝔽₂[G/N].

Equations

• GQ2.regInd N y h = if h = y then 1 else 0

theorem GQ2.regInd_smul {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (c y : G ⧸ N) : c • regInd N y = regInd N (c * y)

Left translation carries indicators to indicators: c • e_y = e_{c·y}.

noncomputable def GQ2.blockBas {G : Type u_1} [Group G] (N : Subgroup G) {K : ℕ} (j : Fin K) (y : G ⧸ N) : Fin K → RegRep N

The (j, y)-coordinate basis vector of the block module 𝔽₂[G/N]^K.

Equations

• GQ2.blockBas N j y i = if i = j then GQ2.regInd N y else 0

theorem GQ2.blockBas_smul {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} (c : G ⧸ N) (j : Fin K) (y : G ⧸ N) : c • blockBas N j y = blockBas N j (c * y)

Left translation on the block module carries basis vectors to basis vectors: c • e_{(j,y)} = e_{(j,cy)}.

theorem GQ2.regRep_sum_apply {G : Type u_1} [Group G] (N : Subgroup G) {ι : Type u_2} (s : Finset ι) (f : ι → RegRep N) (h : G ⧸ N) : (∑ o ∈ s, f o) h = ∑ o ∈ s, f o h

Pointwise evaluation of a finite sum in RegRep N.

theorem GQ2.block_sum_apply {G : Type u_1} [Group G] (N : Subgroup G) {K : ℕ} {ι : Type u_2} (s : Finset ι) (f : ι → Fin K → RegRep N) (i : Fin K) : (∑ o ∈ s, f o) i = ∑ o ∈ s, f o i

Blockwise evaluation of a finite sum in the block module.

theorem GQ2.blockBas_support_decomp {G : Type u_1} [Group G] (N : Subgroup G) {K : ℕ} [Fintype (G ⧸ N)] (F : Fin K → RegRep N) : F = ∑ p : Fin K × G ⧸ N with F p.1 p.2 = 1, blockBas N p.1 p.2

Every element of the block module is the sum of the basis vectors at its support (mirrors permBas_support_decomp).

Coordinates of an invariant quadratic map

noncomputable def GQ2.blockDiag {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} (Q : (Fin K → RegRep N) → ZMod 2) (j : Fin K) : ZMod 2

The diagonal coordinate of Q on block j (the basis diagonal is constant along each block by invariance).

Equations

• GQ2.blockDiag N Q j = Q (GQ2.blockBas N j 1)

noncomputable def GQ2.blockPolar {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} (Q : (Fin K → RegRep N) → ZMod 2) (j k : Fin K) (u : G ⧸ N) : ZMod 2

The relative-position polar coordinate of Q between blocks j, k at relative position u (all basis polar values reduce to these by invariance).

Equations

• GQ2.blockPolar N Q j k u = GQ2.QuadraticFp2.polar Q (GQ2.blockBas N j 1) (GQ2.blockBas N k u)

theorem GQ2.polar_smul_invariant {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} {Q : (Fin K → RegRep N) → ZMod 2} (hinv : QuadraticFp2.IsInvariant (G ⧸ N) Q) (c : G ⧸ N) (v w : Fin K → RegRep N) : QuadraticFp2.polar Q (c • v) (c • w) = QuadraticFp2.polar Q v w

Polar invariance under the simultaneous action, for any invariant map.

theorem GQ2.q_blockBas_eq {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} {Q : (Fin K → RegRep N) → ZMod 2} (hinv : QuadraticFp2.IsInvariant (G ⧸ N) Q) (j : Fin K) (x : G ⧸ N) : Q (blockBas N j x) = blockDiag N Q j

Diagonal orbit-constancy: Q(e_{j,x}) = Q(e_{j,1}).

theorem GQ2.polar_blockBas_eq {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} {Q : (Fin K → RegRep N) → ZMod 2} (hinv : QuadraticFp2.IsInvariant (G ⧸ N) Q) (j k : Fin K) (x y : G ⧸ N) : QuadraticFp2.polar Q (blockBas N j x) (blockBas N k y) = blockPolar N Q j k (x⁻¹ * y)

Polar coordinates in relative position: B_Q(e_{j,x}, e_{k,y}) = β_{j,k}(x⁻¹y).

theorem GQ2.blockPolar_symm {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} {Q : (Fin K → RegRep N) → ZMod 2} (hinv : QuadraticFp2.IsInvariant (G ⧸ N) Q) (j k : Fin K) (u : G ⧸ N) : blockPolar N Q j k u = blockPolar N Q k j u⁻¹

β-symmetry: β_{j,k}(u) = β_{k,j}(u⁻¹) (polar symmetry + invariance).

Position classification and the swap

def GQ2.posSwap {Γ : Type u_1} [Group Γ] {K : ℕ} (p : Fin K × Fin K × Γ) : Fin K × Fin K × Γ

The swap on relative positions: (j, k, u) ↦ (k, j, u⁻¹) (the two orders of an unordered coordinate-pair orbit).

Equations

• GQ2.posSwap p = (p.2.1, p.1, p.2.2⁻¹)

def GQ2.IsFreePos {Γ : Type u_1} [Group Γ] {K : ℕ} (p : Fin K × Fin K × Γ) : Prop

A free position: distinct blocks, or same-block relative position of order > 2. (The complements are the diagonal (j,j,1) and the involution positions (j,j,u), u² = 1 ≠ u.)

Equations

• GQ2.IsFreePos p = (p.1 ≠ p.2.1 ∨ p.2.2 * p.2.2 ≠ 1)

theorem GQ2.posSwap_ne_self {Γ : Type u_1} [Group Γ] {K : ℕ} {p : Fin K × Fin K × Γ} (h : IsFreePos p) : posSwap p ≠ p

The swap moves every free position (fixed points are exactly the involution positions and the diagonal).

@[reducible]

noncomputable def GQ2.posOrder {Γ : Type u_1} {K : ℕ} [Fintype Γ] : LinearOrder (Fin K × Fin K × Γ)

A noncomputable linear order on the position type, used only to orient the free swap-pairs (never appears in a statement).

Equations

• GQ2.posOrder = LinearOrder.lift' ⇑(Fintype.equivFin (Fin K × Fin K × Γ)) ⋯

The free-pair orientation transversal

noncomputable def GQ2.freeReps {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Fintype (G ⧸ N)] (Q : (Fin K → RegRep N) → ZMod 2) : Finset (Fin K × Fin K × G ⧸ N)

The orientation transversal: one representative per free swap-orbit with polar coordinate 1. The choice is made by the (hidden) linear order posOrder; consumers use only the three lemmas below, which never mention the order.

Equations

• GQ2.freeReps N Q = {p : Fin K × Fin K × G ⧸ N | GQ2.IsFreePos p ∧ GQ2.blockPolar N Q p.1 p.2.1 p.2.2 = 1 ∧ p < GQ2.posSwap p}

theorem GQ2.mem_freeReps_or_swap {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Fintype (G ⧸ N)] {Q : (Fin K → RegRep N) → ZMod 2} (hinv : QuadraticFp2.IsInvariant (G ⧸ N) Q) {p : Fin K × Fin K × G ⧸ N} (hfree : IsFreePos p) (hβ : blockPolar N Q p.1 p.2.1 p.2.2 = 1) : p ∈ freeReps N Q ∨ posSwap p ∈ freeReps N Q

Every free position with polar coordinate 1 is covered: itself or its swap is the chosen representative.

theorem GQ2.not_mem_freeReps_both {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Fintype (G ⧸ N)] {Q : (Fin K → RegRep N) → ZMod 2} {p : Fin K × Fin K × G ⧸ N} : ¬(p ∈ freeReps N Q ∧ posSwap p ∈ freeReps N Q)

The transversal is exclusive: never both a position and its swap.

The three §6.2 orbit summands on the block module

Each summand is a definitional FactorSet.comap of a literal OrbitData datum along a block projection, so downstream graph pullbacks are syntactically the Lemma-6.15 inputs at the block coordinates of the cocycle.

def GQ2.blockProj {G : Type u_1} [Group G] (N : Subgroup G) {K : ℕ} (j : Fin K) : (Fin K → RegRep N) →+ RegRep N

The block projection as an additive map.

Equations

• GQ2.blockProj N j = { toFun := fun (F : Fin K → GQ2.RegRep N) => F j, map_zero' := ⋯, map_add' := ⋯ }

def GQ2.blockProj₂ {G : Type u_1} [Group G] (N : Subgroup G) {K : ℕ} (j k : Fin K) : (Fin K → RegRep N) →+ RegRep N × RegRep N

The ordered-pair block projection (j = k allowed).

Equations

• GQ2.blockProj₂ N j k = { toFun := fun (F : Fin K → GQ2.RegRep N) => (F j, F k), map_zero' := ⋯, map_add' := ⋯ }

theorem GQ2.blockProj_smul {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} (j : Fin K) (c : G ⧸ N) (F : Fin K → RegRep N) : (blockProj N j) (c • F) = c • (blockProj N j) F

theorem GQ2.blockProj₂_smul {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} (j k : Fin K) (c : G ⧸ N) (F : Fin K → RegRep N) : (blockProj₂ N j k) (c • F) = c • (blockProj₂ N j k) F

noncomputable def GQ2.squareBlockDatum {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} (j : Fin K) : FactorSet (G ⧸ N) (Fin K → RegRep N)

Square summand (eq. (75)): the square-orbit datum on block j, extended by zero.

Equations

• GQ2.squareBlockDatum N j = (GQ2.squareOrbitDatum N).comap (GQ2.blockProj N j)

noncomputable def GQ2.freeBlockDatum {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} (j k : Fin K) (u : G ⧸ N) : FactorSet (G ⧸ N) (Fin K → RegRep N)

Free summand (eq. (76)): the free-orbit datum with shift u between blocks j, k (possibly equal — the same-block case comaps along the diagonal pair projection).

Equations

• GQ2.freeBlockDatum N j k u = (GQ2.freeOrbitDatum N u).comap (GQ2.blockProj₂ N j k)

noncomputable def GQ2.invBlockDatum {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} (j : Fin K) (u : G ⧸ N) : FactorSet (G ⧸ N) (Fin K → RegRep N)

Involution summand (Lemma 6.2): the involution-orbit datum at u on block j, extended by zero.

Equations

• GQ2.invBlockDatum N j u = (GQ2.invOrbitDatum N u).comap (GQ2.blockProj N j)

noncomputable def GQ2.squareBlockMap {G : Type u_1} [Group G] (N : Subgroup G) {K : ℕ} (j : Fin K) : (Fin K → RegRep N) → ZMod 2

The square map of the square summand.

Equations

• GQ2.squareBlockMap N j F = ∑ᶠ (h : G ⧸ N), F j h * F j h

noncomputable def GQ2.freeBlockMap {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} (j k : Fin K) (u : G ⧸ N) : (Fin K → RegRep N) → ZMod 2

The square map of the free summand.

Equations

• GQ2.freeBlockMap N j k u F = ∑ᶠ (h : G ⧸ N), F j h * F k (h * u)

noncomputable def GQ2.invBlockMap {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} (j : Fin K) (u : G ⧸ N) : (Fin K → RegRep N) → ZMod 2

The square map of the involution summand.

Equations

• GQ2.invBlockMap N j u F = ∑ᶠ (w : (G ⧸ N) ⧸ Subgroup.zpowers u), F j (Quotient.out w) * F j (Quotient.out w * u)

Equivariance of the three summands

theorem GQ2.isEquivariantFactorSet_squareBlockDatum {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Finite (G ⧸ N)] (j : Fin K) : IsEquivariantFactorSet (squareBlockMap N j) (squareBlockDatum N j)

The square summand is an equivariant factor set for its square map.

theorem GQ2.isEquivariantFactorSet_freeBlockDatum {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Finite (G ⧸ N)] (j k : Fin K) (u : G ⧸ N) : IsEquivariantFactorSet (freeBlockMap N j k u) (freeBlockDatum N j k u)

The free summand is an equivariant factor set for its square map.

theorem GQ2.isEquivariantFactorSet_invBlockDatum {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Finite (G ⧸ N)] (j : Fin K) {u : G ⧸ N} (hu2 : u * u = 1) : IsEquivariantFactorSet (invBlockMap N j u) (invBlockDatum N j u)

The involution summand is an equivariant factor set for its square map (banked isEquivariantFactorSet_invOrbitDatum + comap).

Quadraticity of the three square maps

Basis evaluations: factor sets, diagonals, polars

theorem GQ2.freeBlockDatum_f_blockBas {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} (j k : Fin K) (u : G ⧸ N) (m m' : Fin K) (x y : G ⧸ N) : (freeBlockDatum N j k u).f (blockBas N m x) (blockBas N m' y) = if j = m ∧ k = m' ∧ x * u = y then 1 else 0

The free summand's factor set at basis vectors: the single-position indicator.

theorem GQ2.squareBlockMap_blockBas {G : Type u_1} [Group G] (N : Subgroup G) {K : ℕ} (j m : Fin K) (y : G ⧸ N) : squareBlockMap N j (blockBas N m y) = if j = m then 1 else 0

The square summand's diagonal at basis vectors: 1 exactly on its own block.

theorem GQ2.freeBlockMap_blockBas {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Finite (G ⧸ N)] (j k : Fin K) (u : G ⧸ N) (m : Fin K) (y : G ⧸ N) : freeBlockMap N j k u (blockBas N m y) = if j = m ∧ k = m ∧ u = 1 then 1 else 0

The free summand's diagonal at basis vectors vanishes off u = 1 (in particular on every free position).

theorem GQ2.invBlockMap_blockBas {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} (j : Fin K) {u : G ⧸ N} (hu1 : u ≠ 1) (m : Fin K) (y : G ⧸ N) : invBlockMap N j u (blockBas N m y) = 0

The involution summand's diagonal at basis vectors vanishes (u ≠ 1).

theorem GQ2.polar_squareBlockMap {G : Type u_1} [Group G] (N : Subgroup G) {K : ℕ} [Finite (G ⧸ N)] (j : Fin K) (v w : Fin K → RegRep N) : QuadraticFp2.polar (squareBlockMap N j) v w = 0

The square summand's polar form vanishes identically (x ↦ Σ x_h² is additive over 𝔽₂).

theorem GQ2.polar_freeBlockMap_blockBas {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Finite (G ⧸ N)] (j k : Fin K) (u : G ⧸ N) (m m' : Fin K) (x y : G ⧸ N) : QuadraticFp2.polar (freeBlockMap N j k u) (blockBas N m x) (blockBas N m' y) = (if j = m ∧ k = m' ∧ x * u = y then 1 else 0) + if j = m' ∧ k = m ∧ y * u = x then 1 else 0

The free summand's polar at basis vectors: the two-order position indicator.

The involution summand's basis evaluation (the Quotient.out bookkeeping)

theorem GQ2.out_dichotomy {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {u : G ⧸ N} (hu2 : u * u = 1) (x : G ⧸ N) : Quotient.out ↑x = x ∨ Quotient.out ↑x = x * u

With u² = 1, the canonical ⟨u⟩-coset representative of x is x or x·u.

theorem GQ2.mk_mul_self_eq {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {u : G ⧸ N} : u * u = 1 → ∀ (x : G ⧸ N), ↑(x * u) = ↑x

With u² = 1, x and x·u lie in the same ⟨u⟩-coset.

theorem GQ2.invBlockDatum_f_blockBas {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} (j : Fin K) (u : G ⧸ N) (m m' : Fin K) (x y : G ⧸ N) : (invBlockDatum N j u).f (blockBas N m x) (blockBas N m' y) = if m = j ∧ m' = j ∧ Quotient.out ↑x = x ∧ x * u = y then 1 else 0

The involution summand's factor set at basis vectors: the out-guarded position indicator.

theorem GQ2.polar_invBlockMap_blockBas {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Finite (G ⧸ N)] (j : Fin K) {u : G ⧸ N} (hu2 : u * u = 1) (hu1 : u ≠ 1) (m m' : Fin K) (x y : G ⧸ N) : QuadraticFp2.polar (invBlockMap N j u) (blockBas N m x) (blockBas N m' y) = if m = j ∧ m' = j ∧ x * u = y then 1 else 0

The involution summand's polar at basis vectors: the u-pairing indicator on block j (the two out-guards sum to exactly one across the coset {x, xu}).

Sum-of-datums equivariance and the basis extensionality principle

theorem GQ2.isEquivariantFactorSet_sumDatum {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {ι : Type u_3} (s : Finset ι) (datf : ι → FactorSet C V) (qf : ι → V → ZMod 2) (hdatf : ∀ o ∈ s, IsEquivariantFactorSet (qf o) (datf o)) : IsEquivariantFactorSet (fun (v : V) => ∑ o ∈ s, qf o v) (OrbitVanish.sumDatum s datf)

A pointwise sum of equivariant factor sets is an equivariant factor set for the summed square map (generic; the datum-level shape of the §6.2 orbit assembly).

@[reducible]

noncomputable def GQ2.coordOrder {G : Type u_1} [Group G] (N : Subgroup G) {K : ℕ} [Fintype (G ⧸ N)] : LinearOrder (Fin K × G ⧸ N)

A noncomputable linear order on the coordinate positions, used only to split polar values into an ordered kernel (never appears in a statement).

Equations

• GQ2.coordOrder N = LinearOrder.lift' ⇑(Fintype.equivFin (Fin K × G ⧸ N)) ⋯

theorem GQ2.quadratic_ext {G : Type u_1} [Group G] (N : Subgroup G) {K : ℕ} [Fintype (G ⧸ N)] {Q₁ Q₂ : (Fin K → RegRep N) → ZMod 2} (hQ₁ : QuadraticFp2.IsQuadraticFp2 Q₁) (hQ₂ : QuadraticFp2.IsQuadraticFp2 Q₂) (hd : ∀ (p : Fin K × G ⧸ N), Q₁ (blockBas N p.1 p.2) = Q₂ (blockBas N p.1 p.2)) (hp : ∀ (p p' : Fin K × G ⧸ N), QuadraticFp2.polar Q₁ (blockBas N p.1 p.2) (blockBas N p'.1 p'.2) = QuadraticFp2.polar Q₂ (blockBas N p.1 p.2) (blockBas N p'.1 p'.2)) : Q₁ = Q₂

Basis extensionality for quadratic maps: two 𝔽₂-quadratic maps on the block module that agree on the basis diagonal and the basis polar are equal. (Both expand against a common ordered kernel through quadratic_expansion.)

The orbit index, datum, and the decomposition capstone

@[reducible, inline]

abbrev GQ2.OrbitIx (K : ℕ) (Γ : Type u_2) : Type u_2

The §6.2 orbit index: a square block j, an involution block-position (j, u), or a free block-pair-position (j, k, u).

Equations

• GQ2.OrbitIx K Γ = (Fin K ⊕ Fin K × Γ ⊕ Fin K × Fin K × Γ)

noncomputable def GQ2.orbitDatum {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} : OrbitIx K (G ⧸ N) → FactorSet (G ⧸ N) (Fin K → RegRep N)

The datum attached to each orbit index (a definitional block-comap of a literal OrbitData datum).

Equations

• GQ2.orbitDatum N (Sum.inl j) = GQ2.squareBlockDatum N j
• GQ2.orbitDatum N (Sum.inr (Sum.inl (j, u))) = GQ2.invBlockDatum N j u
• GQ2.orbitDatum N (Sum.inr (Sum.inr (j, k, u))) = GQ2.freeBlockDatum N j k u

noncomputable def GQ2.orbitSquareMap {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} : OrbitIx K (G ⧸ N) → (Fin K → RegRep N) → ZMod 2

The square map of each orbit index.

Equations

• GQ2.orbitSquareMap N (Sum.inl j) = GQ2.squareBlockMap N j
• GQ2.orbitSquareMap N (Sum.inr (Sum.inl (j, u))) = GQ2.invBlockMap N j u
• GQ2.orbitSquareMap N (Sum.inr (Sum.inr (j, k, u))) = GQ2.freeBlockMap N j k u

noncomputable def GQ2.sqIdx {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} (Q : (Fin K → RegRep N) → ZMod 2) : Finset (Fin K)

The square blocks present in Q: those with nonzero diagonal.

Equations

• GQ2.sqIdx N Q = {j : Fin K | GQ2.blockDiag N Q j = 1}

noncomputable def GQ2.invIdx {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Fintype (G ⧸ N)] (Q : (Fin K → RegRep N) → ZMod 2) : Finset (Fin K × G ⧸ N)

The involution block-positions present in Q.

Equations

• GQ2.invIdx N Q = {p : Fin K × G ⧸ N | p.2 * p.2 = 1 ∧ p.2 ≠ 1 ∧ GQ2.blockPolar N Q p.1 p.1 p.2 = 1}

noncomputable def GQ2.orbitIndexSet {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Fintype (G ⧸ N)] (Q : (Fin K → RegRep N) → ZMod 2) : Finset (OrbitIx K (G ⧸ N))

The orbit index set of Q: the disjoint union of the present square/involution/free positions.

Equations

• GQ2.orbitIndexSet N Q = (GQ2.sqIdx N Q).disjSum ((GQ2.invIdx N Q).disjSum (GQ2.freeReps N Q))

theorem GQ2.sum_orbitIndexSet {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Fintype (G ⧸ N)] {M : Type u_2} [AddCommMonoid M] (Q : (Fin K → RegRep N) → ZMod 2) (g : OrbitIx K (G ⧸ N) → M) : ∑ o ∈ orbitIndexSet N Q, g o = ∑ j ∈ sqIdx N Q, g (Sum.inl j) + (∑ p ∈ invIdx N Q, g (Sum.inr (Sum.inl p)) + ∑ r ∈ freeReps N Q, g (Sum.inr (Sum.inr r)))

The three-way split of a sum over the orbit index set.

theorem GQ2.mem_orbitIndexSet_inv {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Fintype (G ⧸ N)] {Q : (Fin K → RegRep N) → ZMod 2} {ju : Fin K × G ⧸ N} : Sum.inr (Sum.inl ju) ∈ orbitIndexSet N Q ↔ ju ∈ invIdx N Q

Involution-index membership.

theorem GQ2.isEqFS_orbitDatum {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Finite (G ⧸ N)] [Fintype (G ⧸ N)] (Q : (Fin K → RegRep N) → ZMod 2) (o : OrbitIx K (G ⧸ N)) : o ∈ orbitIndexSet N Q → IsEquivariantFactorSet (orbitSquareMap N o) (orbitDatum N o)

Each summand is an equivariant factor set for its square map (on the index set: involution positions are involutions).

theorem GQ2.isQuad_orbitSquareMap {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Finite (G ⧸ N)] [Fintype (G ⧸ N)] (Q : (Fin K → RegRep N) → ZMod 2) (o : OrbitIx K (G ⧸ N)) : o ∈ orbitIndexSet N Q → QuadraticFp2.IsQuadraticFp2 (orbitSquareMap N o)

Each summand's square map is quadratic.

noncomputable def GQ2.orbitSum {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Fintype (G ⧸ N)] (Q : (Fin K → RegRep N) → ZMod 2) : (Fin K → RegRep N) → ZMod 2

The summed square map of the orbit index set.

Equations

• GQ2.orbitSum N Q F = ∑ o ∈ GQ2.orbitIndexSet N Q, GQ2.orbitSquareMap N o F

theorem GQ2.orbitSum_blockBas {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Finite (G ⧸ N)] [Fintype (G ⧸ N)] {Q : (Fin K → RegRep N) → ZMod 2} (hinv : QuadraticFp2.IsInvariant (G ⧸ N) Q) (p : Fin K × G ⧸ N) : orbitSum N Q (blockBas N p.1 p.2) = Q (blockBas N p.1 p.2)

Diagonal matching: the orbit sum agrees with Q on basis vectors — only the square summand of the coordinate's own block contributes.

theorem GQ2.orbitSum_polar_blockBas {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Finite (G ⧸ N)] [Fintype (G ⧸ N)] {Q : (Fin K → RegRep N) → ZMod 2} (hinv : QuadraticFp2.IsInvariant (G ⧸ N) Q) (hQ : QuadraticFp2.IsQuadraticFp2 Q) (p p' : Fin K × G ⧸ N) : QuadraticFp2.polar (orbitSum N Q) (blockBas N p.1 p.2) (blockBas N p'.1 p'.2) = QuadraticFp2.polar Q (blockBas N p.1 p.2) (blockBas N p'.1 p'.2)

Polar matching: the orbit sum's polar agrees with Q's polar on basis vectors. The square summands contribute 0; the surviving contribution is the involution indicator (same-block involution positions) or the free indicator (an oriented representative of the swap-orbit), which in every case reconstructs blockPolar Q.

theorem GQ2.isEquivariantFactorSet_orbitSumDatum {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] {K : ℕ} [Finite (G ⧸ N)] [Fintype (G ⧸ N)] {Q : (Fin K → RegRep N) → ZMod 2} (hQ : QuadraticFp2.IsQuadraticFp2 Q) (hinv : QuadraticFp2.IsInvariant (G ⧸ N) Q) : IsEquivariantFactorSet Q (OrbitVanish.sumDatum (orbitIndexSet N Q) (orbitDatum N))

The §6.2 orbit decomposition (the Lemma 6.17 vanishing proof): a (G/N)-invariant 𝔽₂-quadratic map Q on the block module is the square map of the sumDatum of its orbit datums. Feeds OrbitVanish.Q0loc_vanish_of_datum_decomp with dat = sumDatum … orbitDatum.

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

• eq. (75) = ⟦eq-squareorbitfactor⟧
• eq. (76) = ⟦eq-freeorbitfactor⟧
• Lemma 6.2 = ⟦lem-halforbitcocycle⟧