The ι_{Γ_R}-computation rule

The Γ_R twin of GQ2/IotaGammaA.lean: the coboundary indicator ι_Γ (Phase140.iotaB, the Q⁰-valuation) is computed, over the raw candidate carrier GR = F₄ ⧸ N_R, by the Roe word-relator obstruction of the WordCoh2R degree-2 presentation comparison:

• iotaB_eq_obsR — ι_{Γ_R} φ = obs_R φ for every continuous 2-cocycle φ: both are 𝔽₂-valued with the same vanishing locus (iotaB_eq_zero_iff vs WordCoh2R.obs_ker_eq_B2_R), hence equal.
• iotaB_eq_levelFactor_obsR — the evaluation form: ι_{Γ_R} φ is the (tame + Roe wild) relator obstruction F.obs of any finite R-admissible-level factorization F of the (1,1)-normalization of φ (obsFun_eq_R well-definedness).
• QZero_eq_obsR / QZero_eq_levelFactor_obsR — the same, specialized to the base determinant form: Q⁰_{Γ_R,ρ'}(c) is the Roe relator obstruction of any level factorization of the (normalized) graph pullback.

Everything is glue over proved technology: iotaB/iotaB_eq_zero_iff and graphPullback_mem_Z2_of_cocycle/QZero are generic in Γ and reused verbatim; the only Γ_R-specific inputs are WordCoh2R.obs_ker_eq_B2_R and WordCoh2R.obsFun_eq_R.

theorem GQ2.IotaGammaR.iotaB_eq_obsR [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) (φ : ↥(ContCoh.Z2 WordCohBridgeR.GR (ZMod 2))) : SectionEight.iotaB ↑φ = (WordCoh2R.obs_R htriv) φ

The ι_{Γ_R}-computation rule: the coboundary indicator agrees with the Roe word-relator obstruction on every continuous 2-cocycle — both are 𝔽₂-valued with kernel exactly B²(Γ_R, 𝔽₂).

theorem GQ2.IotaGammaR.iotaB_eq_levelFactor_obsR [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) (φ : ↥(ContCoh.Z2 WordCohBridgeR.GR (ZMod 2))) (F : WordCoh2R.LevelFactorR (WordCoh2R.normalizeCochainR ↑φ)) : SectionEight.iotaB ↑φ = F.obs

The evaluation form: ι_{Γ_R} φ is the (tame + Roe wild) relator obstruction of any finite R-admissible-level factorization of the (1,1)-normalization of φ.

theorem GQ2.IotaGammaR.QZero_eq_obsR [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : SectionEight.RadicalCoverData Bg} {DD : SectionEight.AffineTLift.DescData D} {ρM : WordCohBridgeR.GR →ₜ* Bg ⧸ D.M} (c : SectionEight.AffineTLift.VCocycle DD ρM) : SectionEight.AffineTLift.QZero DD ρM c = (WordCoh2R.obs_R htriv) ⟨graphPullback DD.dat (fun (γ : WordCohBridgeR.GR) => (SectionEight.AffineTLift.rho0 DD ρM) γ) c.c, ⋯⟩

Q⁰ over Γ_R is the Roe word-relator obstruction: the base determinant form evaluates through obs_R at the graph pullback.

theorem GQ2.IotaGammaR.QZero_eq_levelFactor_obsR [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : SectionEight.RadicalCoverData Bg} {DD : SectionEight.AffineTLift.DescData D} {ρM : WordCohBridgeR.GR →ₜ* Bg ⧸ D.M} (c : SectionEight.AffineTLift.VCocycle DD ρM) (F : WordCoh2R.LevelFactorR (WordCoh2R.normalizeCochainR (graphPullback DD.dat (fun (γ : WordCohBridgeR.GR) => (SectionEight.AffineTLift.rho0 DD ρM) γ) c.c))) : SectionEight.AffineTLift.QZero DD ρM c = F.obs

The consumable form: Q⁰_{Γ_R,ρ'}(c) is the (tame + Roe wild) relator obstruction of any finite R-admissible-level factorization of the normalized graph pullback.