Lemma 8.6, Γ_A source: the duality half via prop_5_15

The Γ_A-side analogue of RadicalEdgeLocal.exists_good_twist: from NoDescent, the Fox–Heisenberg self-duality prop_5_15 produces a nonzero traced mixed pairing mixedB t_ρ x_w y_φ ≠ 0, where y_φ is the shifted-edge dual class and x_w its prop_5_15-pairing partner. This is the c3 result; the Θ–mixedB comparison (mixedB ≠ 0 ⟹ [varCoc u_w] ≠ 0, using c2's θ) is the Γ_A half-torsor proof.

Structural pivot (docs/orchestration/p16c3-recon.md): MuDual's DistribMulAction is hardcoded to AbsGalQ2 (GQ2/TateDuality.lean), so the local proof's φf : Γ → MuDual 2 (Additive ↥T) does not port to Γ = GA. The shifted-edge cocycle is built directly in ElemDual (Additive ↥T) (generic DistribMulAction C (ElemDual A), FoxHeisenberg; (g•λ)a = λ(g⁻¹•a)), which also removes dualAddEquiv from the bridge.

Source group is the raw GA = F₄ ⧸ N_A (matching WordCohBridge; the GammaA transport is the Γ_A half-torsor proof). The C = Bg ⧸ D.M-conjugation action on T is the primary module structure (what mixedB/Z1w/markC consume); the GA-action is its pullback DistribMulAction.compHom ρ (so hcompat for h1Equiv is rfl).

Axioms (target): std-3 only — the pairing comes from prop_5_15 (the Prop. 5.15 proof), not B6.

The C = Bg ⧸ D.M-conjugation module on T

M centralizes T (D.hcomm + D.hTM), so c • t := b t b⁻¹ (any b over c) is a well-defined action of the finite discrete group C = Bg ⧸ D.M on the abelian 2-group T.

@[implicit_reducible]

noncomputable instance GQ2.SectionEight.RadicalEdgeGammaA.instACGaddT {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) : AddCommGroup (Additive ↥D.T)

↥D.T is commutative (T ≤ M abelian) — additive form for the word complex. Built on top of the existing AddGroup (Additive ↥D.T) (from the subgroup Group), so no diamond.

Equations

• GQ2.SectionEight.RadicalEdgeGammaA.instACGaddT D = { toAddGroup := inferInstance, add_comm := ⋯ }

noncomputable def GQ2.SectionEight.RadicalEdgeGammaA.cactFun {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (c : Bg ⧸ D.M) (t : ↥D.T) : ↥D.T

The conjugation action of C = Bg ⧸ D.M on T, at the canonical representative.

Equations

• GQ2.SectionEight.RadicalEdgeGammaA.cactFun D c t = ⟨Quotient.out c * ↑t * (Quotient.out c)⁻¹, ⋯⟩

theorem GQ2.SectionEight.RadicalEdgeGammaA.cactFun_eq {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (c : Bg ⧸ D.M) {b : Bg} (hb : ↑b = c) (t : ↥D.T) : ↑(cactFun D c t) = b * ↑t * b⁻¹

theorem GQ2.SectionEight.RadicalEdgeGammaA.cactFun_mul {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (c c' : Bg ⧸ D.M) (t : ↥D.T) : cactFun D (c * c') t = cactFun D c (cactFun D c' t)

@[implicit_reducible]

noncomputable instance GQ2.SectionEight.RadicalEdgeGammaA.cActT {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) : DistribMulAction (Bg ⧸ D.M) (Additive ↥D.T)

The C = Bg ⧸ D.M-conjugation action on Additive ↥D.T.

Equations

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

theorem GQ2.SectionEight.RadicalEdgeGammaA.cActT_toMul {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (c : Bg ⧸ D.M) (t : Additive ↥D.T) : Additive.toMul (c • t) = cactFun D c (Additive.toMul t)

@[implicit_reducible]

instance GQ2.SectionEight.RadicalEdgeGammaA.instTopElemDualT {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) : TopologicalSpace (FoxH.ElemDual (Additive ↥D.T))

The discrete topology on the 𝔽₂-dual (a valid coefficient module).

Equations

• GQ2.SectionEight.RadicalEdgeGammaA.instTopElemDualT D = ⊥

instance GQ2.SectionEight.RadicalEdgeGammaA.instDiscElemDualT {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) : DiscreteTopology (FoxH.ElemDual (Additive ↥D.T))

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

• Lemma 8.6 = ⟦lem-radicaledge⟧