The mixed Heisenberg pairing as a relator obstruction (mixedB = relZPair)

A generic bridge (any finite A, C with DistribMulAction C A) recasting the traced Heisenberg central coordinate mixedB t x y (FoxHeisenberg) as the WordCoh2 relator-z pair relZPair (mBaseMarking t x y) kappaHeis of an explicit 2-cocycle kappaHeis on the base semidirect product WordLift (A × A^∨) C.

The structural heart is the isomorphism HeisLift A C ≅ CentExt kappaHeis: the map PhiHeis : CentExt kappaHeis →* HeisLift A C carries the liftMark of mBaseMarking onto heisMarking t x y and the fibre coordinate .fib onto the central coordinate .z. Under naturality of the relator values (Marking.map_{tame,wild}Value) this turns the traced-z sum defining mixedB into the traced-fib sum defining relZPair.

This is the source-generic, edge-free half of the Γ_A half-torsor proof ledger identity obs(varCoc u) = mixedB t_ρ x_w y_φ; the edge-specific half (identifying varCoc u with the inflation of kappaHeis) is assembled downstream over the RadicalCoverData context.

noncomputable def GQ2.MixedBObs.kappaHeis {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] : WordCoh2.TwoCocycle (FoxH.WordLift (A × FoxH.ElemDual A) C)

The Heisenberg 2-cocycle on the base semidirect product (A × A^∨) ⋊ C: κ((a,λ),g),((a',λ'),g')) = λ(g • a'). This is exactly the central defect of the HeisLift multiplication, now packaged as a TwoCocycle so it can drive the CentExt machinery of WordCoh2.

Equations

• GQ2.MixedBObs.kappaHeis = { κ := fun (p q : GQ2.FoxH.WordLift (A × GQ2.FoxH.ElemDual A) C) => p.u.2 (p.g • q.u.1), norm := ⋯, cocyc := ⋯ }

noncomputable def GQ2.MixedBObs.PhiHeis {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] : WordCoh2.CentExt kappaHeis →* FoxH.HeisLift A C

The structural isomorphism CentExt kappaHeis →* HeisLift A C, (⟨(a,λ),g⟩, z) ↦ ⟨a,λ,z,g⟩. It is a homomorphism precisely because kappaHeis's defect matches the HeisLift multiplication's central term λ(g • a').

Equations

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

noncomputable def GQ2.MixedBObs.mBaseMarking {C : Type u_1} {A : Type u_2} [AddCommGroup A] (t : Marking C) (x : Fin 4 → A) (y : Fin 4 → FoxH.ElemDual A) : Marking (FoxH.WordLift (A × FoxH.ElemDual A) C)

The base marking of (A × A^∨) ⋊ C whose generators carry the offsets (x i, y i) over t's generators — the base of the heisMarking.

Equations

• GQ2.MixedBObs.mBaseMarking t x y = { σ := { u := (x 0, y 0), g := t.σ }, τ := { u := (x 1, y 1), g := t.τ }, x₀ := { u := (x 2, y 2), g := t.x₀ }, x₁ := { u := (x 3, y 3), g := t.x₁ } }

theorem GQ2.MixedBObs.mBaseMarking_eq_liftMarking {C : Type u_1} {A : Type u_2} [AddCommGroup A] (t : Marking C) (x : Fin 4 → A) (y : Fin 4 → FoxH.ElemDual A) : mBaseMarking t x y = FoxH.liftMarking t fun (i : Fin 4) => (x i, y i)

mBaseMarking is the FoxHeisenberg liftMarking at the paired offsets — the form the WordCohBridge relator-death machinery (liftMarking_eval_univ) consumes.

theorem GQ2.MixedBObs.map_liftMark_mBase {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (t : Marking C) (x : Fin 4 → A) (y : Fin 4 → FoxH.ElemDual A) : Marking.map PhiHeis (WordCoh2.liftMark (mBaseMarking t x y) kappaHeis) = FoxH.heisMarking t x y

PhiHeis carries the lift of mBaseMarking onto heisMarking (generator by generator).

theorem GQ2.MixedBObs.mixedB_eq_relZPair {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) (x : Fin 4 → A) (y : Fin 4 → FoxH.ElemDual A) : FoxH.mixedB t x y = (WordCoh2.relZPair (mBaseMarking t x y) kappaHeis).1 + (WordCoh2.relZPair (mBaseMarking t x y) kappaHeis).2

mixedB is a relator-z pair. The traced Heisenberg central coordinate equals the traced fibre coordinate of kappaHeis's lifted base marking — i.e. mixedB is a WordCoh2 relator obstruction.

Obstruction of an inflated cocycle

The WordCoh2 obstruction obs of a continuous 2-cocycle on Γ_A that factors pointwise through a finite group L (φ(a,b) = κ(H a)(H b)) is the relator-z pair of the pushforward marking gammaGen.map H. This packages the entire LevelFactor / relZPair_comap computation once and generically, so the edge-specific ledger identity is a one-line application.

theorem GQ2.MixedBObs.obs_inflation [DistribMulAction (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)] (htriv : ∀ (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (m : ZMod 2), x • m = m) {L : Type u_3} [Group L] [TopologicalSpace L] [DiscreteTopology L] [Finite L] (H : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA →ₜ* L) (κ : WordCoh2.TwoCocycle L) (φ : ↥(ContCoh.Z2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2))) (hφ : ∀ (a b : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA), ↑φ (a, b) = κ.κ (H a) (H b)) : (WordCoh2.obs htriv) φ = (WordCoh2.relZPair (Marking.map H.toMonoidHom WordCohBridge.gammaGen) κ).1 + (WordCoh2.relZPair (Marking.map H.toMonoidHom WordCohBridge.gammaGen) κ).2

Obstruction of an inflated cocycle. If a continuous 2-cocycle φ on Γ_A factors pointwise through a finite group L as φ(a,b) = κ(H a)(H b) for a continuous hom H : Γ_A → L and a 2-cocycle κ on L, its obstruction is the relator-z pair of the pushforward marking gammaGen.map H.