The mixed Heisenberg pairing as a Roe relator obstruction (mixedB_R = relZPairR)

The Γ_R twin of GQ2/MixedBObs.lean. The Heisenberg 2-cocycle kappaHeis, the structural isomorphism PhiHeis : CentExt kappaHeis →* HeisLift A C, and the base marking mBaseMarking are word-independent and reused verbatim from the Γ_A file; only the two statements that read a relator off a marking are re-derived at Marking.wildValueR:

• mixedB_eq_relZPairR — the traced Heisenberg central coordinate of the Roe wild relator, mixedB_R t x y (GQ2/Roe/FoxBasic.lean), is the traced fibre coordinate relZPairR of kappaHeis's lifted base marking. Same proof as the Γ_A original, with Marking.map_wildValue swapped for Marking.map_wildValueR.
• obs_inflation_R — the WordCoh2R obstruction of a continuous 2-cocycle on Γ_R that factors pointwise through a finite group L is the Roe relator-z pair of the pushforward marking gammaGenR.map H. Stated at F₄ ⧸ N_R (not at the Demushkin quotient DR, where GQ2/Roe/DRWordCoh.lean's obs_DR lives), exactly as Γ_A builds obs at F₄ ⧸ N_A.

Together these are the source-generic, edge-free half of the Γ_R ledger identity obs_R(varCoc u) = mixedB_R t_ρ x_w y_φ; the edge-specific half is assembled in GQ2/LedgerGammaR.lean.

theorem GQ2.MixedBObsR.mixedB_eq_relZPairR {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_R t x y = (WordCoh2R.relZPairR (MixedBObs.mBaseMarking t x y) MixedBObs.kappaHeis).1 + (WordCoh2R.relZPairR (MixedBObs.mBaseMarking t x y) MixedBObs.kappaHeis).2

mixedB_R is a Roe relator-z pair. The traced Heisenberg central coordinate of the Roe wild relator equals the traced fibre coordinate of kappaHeis's lifted base marking — i.e. mixedB_R is a WordCoh2R relator obstruction. Γ_R twin of MixedBObs.mixedB_eq_relZPair.

Obstruction of an inflated cocycle

The WordCoh2R obstruction obs_R of a continuous 2-cocycle on Γ_R that factors pointwise through a finite group L (φ(a,b) = κ(H a)(H b)) is the Roe relator-z pair of the pushforward marking gammaGenR.map H. This packages the entire LevelFactorR / relZPairR_comap computation once and generically, so the edge-specific ledger identity is a one-line application.

theorem GQ2.MixedBObsR.obs_inflation_R [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) {L : Type u_3} [Group L] [TopologicalSpace L] [DiscreteTopology L] [Finite L] (H : WordCohBridgeR.GR →ₜ* L) (κ : WordCoh2.TwoCocycle L) (φ : ↥(ContCoh.Z2 WordCohBridgeR.GR (ZMod 2))) (hφ : ∀ (a b : WordCohBridgeR.GR), ↑φ (a, b) = κ.κ (H a) (H b)) : (WordCoh2R.obs_R htriv) φ = (WordCoh2R.relZPairR (Marking.map H.toMonoidHom WordCohBridgeR.gammaGenR) κ).1 + (WordCoh2R.relZPairR (Marking.map H.toMonoidHom WordCohBridgeR.gammaGenR) κ).2

Obstruction of an inflated cocycle. If a continuous 2-cocycle φ on Γ_R factors pointwise through a finite group L as φ(a,b) = κ(H a)(H b) for a continuous hom H : Γ_R → L and a 2-cocycle κ on L, its Roe obstruction is the Roe relator-z pair of the pushforward marking gammaGenR.map H. Γ_R twin of MixedBObs.obs_inflation, at F₄ ⧸ N_R.