Orbit-data def-layer for §6 (extracted from GQ2/SectionSix.lean)

The factor-set / regular-representation / orbit-datum definitions of Lemmas 6.1–6.2 (eqs. (59)–(76)), lifted out of GQ2/SectionSix.lean into this lower shared file.

Why. The §6 proof own-files (GQ2/ShapiroLedger.lean, and future ones) need these defs to state and prove their _aux lemmas, but must not import SectionSix — otherwise splicing an own-file's proved lemma back into SectionSix (lemma_6_15_free := ShapiroLedger.lemma_6_15_free_aux …) is a circular import. Placing the def-layer here, in the top-level namespace GQ2 (not GQ2.SectionSix), lets both SectionSix and the own-files reach the names unqualified with no per-file edits (they are all in namespace GQ2). See docs/orchestration/orbit-data-refactor.md.

Moved verbatim from SectionSix. No axioms; Ax = ∅.

Factor-set data (Lemma 6.1, eqs. (59)–(62))

structure GQ2.FactorSet (C : Type u_1) (V : Type u_2) : Type (max u_1 u_2)

Factor-set datum for a C-module V (Lemma 6.1): a normalized factor set f together with the central corrections m_c of a chosen equivariant lift. The defining identities (59)/(60) and the compatibility with a quadratic form q are the Prop bundle IsEquivariantFactorSet below.

• f : V → V → ZMod 2

  The normalized factor set f : V × V → 𝔽₂.

• m : C → V → ZMod 2

  The equivariant-lift corrections m_c : V → 𝔽₂ (eq. (59)/(60)).

structure GQ2.IsEquivariantFactorSet {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] (q : V → ZMod 2) (dat : FactorSet C V) : Prop

The identities making (f, m) an equivariant factor-set datum for q (Lemma 6.1): f has square map q and polar form B_q, is normalized, and m satisfies (59)/(60) with m_1 = 0.

• f_cocycle (v w x : V) : dat.f (v + w) x + dat.f v w = dat.f v (w + x) + dat.f w x

  f is a genuine factor set: the (trivial-action, additive) 2-cocycle identity on V — the associativity of the central extension E_f (Lemma 6.1's "normalized factor set"). This field is required for graphPullback_mem_Z2; all of the paper's concrete factor sets ((75)/(76)/(73)/(95)) are bilinear in the coordinates, hence satisfy it.

• f_diag (v : V) : dat.f v v = q v
• f_polar (v w : V) : dat.f v w + dat.f w v = QuadraticFp2.polar q v w
• f_zero_left (v : V) : dat.f 0 v = 0
• f_zero_right (v : V) : dat.f v 0 = 0
• m_quad (c : C) (v w : V) : dat.m c (v + w) + dat.m c v + dat.m c w = dat.f (c • v) (c • w) + dat.f v w

  Eq. (59): m_c(v+w) + m_c(v) + m_c(w) = f(cv, cw) + f(v, w).

• m_mul (c d : C) (v : V) : dat.m (c * d) v = dat.m c (d • v) + dat.m d v

  Eq. (60): m_{cd}(v) = m_c(dv) + m_d(v).

• m_one (v : V) : dat.m 1 v = 0

  Eq. (60): m_1 = 0.

def GQ2.kappa0 {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] (dat : FactorSet C V) : V × C → V × C → ZMod 2

The base central cocycle κ⁰_q on V ⋊ C (eq. (61)): κ⁰((v,c),(w,d)) = f(v, c·w) + m_c(w), as a raw function on pairs.

Equations

• GQ2.kappa0 dat p q = dat.f p.1 (p.2 • q.1) + dat.m p.2 q.1

def GQ2.graphPullback {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {Γ : Type u_3} (dat : FactorSet C V) (ρ : Γ → C) (b : Γ → V) : Γ × Γ → ZMod 2

The graph pullback (b, ρ)^* κ⁰_q (eq. (62)) along a lower map ρ : Γ → C and a 1-cochain b : Γ → V: (g, h) ↦ f(b(g), ρ(g)·b(h)) + m_{ρ(g)}(b(h)). This is the only form in which the base class enters the §6 statements.

Equations

• GQ2.graphPullback dat ρ b p = dat.f (b p.1) (ρ p.1 • b p.2) + dat.m (ρ p.1) (b p.2)

def GQ2.FactorSet.comap {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] {W : Type u_3} [AddCommGroup W] [DistribMulAction C W] (dat : FactorSet C W) (i : V →+ W) : FactorSet C V

Pullback of a factor-set datum along an equivariant additive map i : V →+ W (the (i ⋊ 1)^* of eq. (77), datum level).

Equations

• dat.comap i = { f := fun (v w : V) => dat.f (i v) (i w), m := fun (c : C) (v : V) => dat.m c (i v) }

The regular representation and orbit data (Lemma 6.2, eqs. (67)–(76))

RegRep/*OrbitDatum need only [Group G] [N.Normal] (the topological/DistribMulAction G 𝔽₂ context that surrounds them in SectionSix is not used by the defs themselves).

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

The regular permutation module 𝔽₂[G/N] (coordinates X_h, h ∈ G/N), as a type synonym carrying the left-regular action (c·x)_h = x_{c⁻¹h} (Lemma 6.2's convention).

Equations

• GQ2.RegRep N = (G ⧸ N → ZMod 2)

@[implicit_reducible]

instance GQ2.instAddCommGroupRegRep {G : Type u_1} [Group G] (N : Subgroup G) : AddCommGroup (RegRep N)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance GQ2.instDistribMulActionQuotientSubgroupRegRep {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] : DistribMulAction (G ⧸ N) (RegRep N)

The left-regular action on 𝔽₂[G/N].

Equations

• GQ2.instDistribMulActionQuotientSubgroupRegRep N = { smul := fun (c : G ⧸ N) (x : GQ2.RegRep N) (h : G ⧸ N) => x (c⁻¹ * h), mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

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

The square-orbit datum S (eq. (75)): f(x,y) = Σ_h x_h y_h, m = 0.

Equations

• GQ2.squareOrbitDatum N = { f := fun (x y : GQ2.RegRep N) => ∑ᶠ (h : G ⧸ N), x h * y h, m := fun (x : G ⧸ N) (x_1 : GQ2.RegRep N) => 0 }

noncomputable def GQ2.freeOrbitDatum {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar : G ⧸ N) : FactorSet (G ⧸ N) (RegRep N × RegRep N)

The free-orbit datum C_{j,k,ḡ} (eq. (76)) on two regular summands with shift ḡ: f((x,x'),(y,y')) = Σ_h x_h y'_{hḡ}, m = 0.

Equations

• GQ2.freeOrbitDatum N gbar = { f := fun (x y : GQ2.RegRep N × GQ2.RegRep N) => ∑ᶠ (h : G ⧸ N), x.1 h * y.2 (h * gbar), m := fun (x : G ⧸ N) (x_1 : GQ2.RegRep N × GQ2.RegRep N) => 0 }

noncomputable def GQ2.invOrbitDatum {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (gbar : G ⧸ N) : FactorSet (G ⧸ N) (RegRep N)

The involution-orbit datum E_ḡ (Lemma 6.2, eqs. (67)–(70)) for an involution ḡ ∈ G/N: with R the canonical transversal of the ⟨ḡ⟩-cosets, f_g(x,y) = Σ_{u∈R} x_u y_{uḡ} and m^g_c(x) = Σ_{u∈R} ε_c(u)·x_{π_c(u)} x_{π_c(u)ḡ} (orientation bookkeeping (67) via the canonical representatives).

Equations

• One or more equations did not get rendered due to their size.

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

• eq. (59) = ⟦eq-mquadratic⟧
• eq. (61) = ⟦eq-basekappacochain⟧
• eq. (62) = ⟦eq-baseconnectingcochain⟧
• eq. (67) = ⟦eq-piepsilon⟧
• eq. (70) = ⟦eq-mhalforbit⟧
• eq. (75) = ⟦eq-squareorbitfactor⟧
• eq. (76) = ⟦eq-freeorbitfactor⟧
• eq. (77) = ⟦eq-basepullback⟧
• Lemma 6.1 = ⟦lem-extraspecialconnecting⟧
• Lemma 6.2 = ⟦lem-halforbitcocycle⟧