The Γ_R degree-2 presentation comparison — the obstruction layer

The Roe-candidate twin of GQ2/WordCoh2.lean's obstruction block: an injection H²(Γ_R, 𝔽₂) ↪ 𝔽₂ (obsH2_R/obsH2_R_injective), obtained by evaluating the two Γ_R relator words — the shared tame relator and the Roe wild relator r_R = (x₀^σ)⁻¹ · a · x₁² · c (Marking.wildValueR) — on a central extension of a finite admissible level. Together with a nonzero variation class this gives #H²(Γ_R, 𝔽₂) = 2 (GQ2/HalfTorsorGammaR.lean), the SourceData.cardH2 leaf for Γ_R.

What is new and what is inherited. GQ2/WordCoh2.lean develops its central-extension machinery for an arbitrary group L: TwoCocycle, CentExt (+ proj/incl), liftMark, shiftLiftMark, isPGroup_shiftLift_wildCore, the level-change pair TwoCocycle.comap/projExt, the Baer-sum comparison object FiberProd (+ pr1/pr2/prSum/liftMarkFP), the split and coboundary cocycles zeroCocycle/coboundaryCocycle (+ fibHom0/Psi), the shift comparison shiftCompare/wlBase, and the compactness lemma exists_openNormalSubgroup_factor_two. All of that is imported and reused verbatim — it never mentions a relator. What is re-derived here is exactly the part that reads the wild relator off a marking, plus the part typed at N_R:

• the relator-z pair relZPairR t c = (tame.fib, wild_R.fib) and its three structural laws (relZPairR_comap, relZPairR_add, relZPairR_zero/obs_coboundaryR_eq);
• the wild shift law shiftLiftMark_wildValueR_fib (from FoxH.liftMarking_wildValueR_u, whose row x₁ + (1 + S⁻¹)·x₂ replaces Γ_A's x₁ + (1 + S⁻¹)·x₃ — the same fibre shift a 1);
• the splitting section over N_R (NR_le_ker_shiftLiftR/sectionHomR), which runs the IsAdmissibleUR/isAdmissibleUR_iff_NR_le route in place of IsAdmissibleU/isAdmissibleU_iff_NA_le;
• the N_R-typed factoring/assembly chain and the obstruction homomorphism itself (LevelFactorR, obs_R, obs_ker_eq_B2_R, obsH2_R).

Statement shapes mirror the Γ_A originals binder-for-binder, so downstream ports read verbatim modulo the _R suffix.

The Roe relator-z pair

theorem GQ2.WordCoh2R.liftMark_wildValueR_base {L : Type u_1} [Group L] [Finite L] (t : Marking L) (c : WordCoh2.TwoCocycle L) : (WordCoh2.liftMark t c).wildValueR.base = t.wildValueR

The Roe wild relator value of the lifted marking projects to that of the base marking (needs L finite: Marking.map_wildValueR's ω₂-naturality is finite-only, and CentExt c is finite). Γ_R twin of WordCoh2.liftMark_wildValue_base.

noncomputable def GQ2.WordCoh2R.relZPairR {L : Type u_1} [Group L] [Finite L] (t : Marking L) (c : WordCoh2.TwoCocycle L) : ZMod 2 × ZMod 2

The Roe relator-z pair of c relative to a base marking t: the fibre coordinates of the tame and Roe wild relator values of the lifted marking — the degree-2 obstruction of c, pre-quotient by im d1_triv. Γ_R twin of WordCoh2.relZPair; only the second component differs (wildValueR for wildValue).

Equations

• GQ2.WordCoh2R.relZPairR t c = ((GQ2.WordCoh2.liftMark t c).tameValue.fib, (GQ2.WordCoh2.liftMark t c).wildValueR.fib)

theorem GQ2.WordCoh2R.relZPairR_fst {L : Type u_1} [Group L] [Finite L] (t : Marking L) (c : WordCoh2.TwoCocycle L) : (relZPairR t c).1 = (WordCoh2.relZPair t c).1

Sanity 1/2. The tame component of relZPairR is definitionally relZPair's — the tame relator is shared with Γ_A.

theorem GQ2.WordCoh2R.relZPairR_snd {L : Type u_1} [Group L] [Finite L] (t : Marking L) (c : WordCoh2.TwoCocycle L) : (relZPairR t c).2 = (WordCoh2.liftMark t c).wildValueR.fib

Sanity 2/2. The wild component of relZPairR is the Roe wild relator's fibre.

theorem GQ2.WordCoh2R.shiftLiftMark_wildValueR_base {L : Type u_1} [Group L] [Finite L] (t : Marking L) (a : Fin 4 → ZMod 2) (c : WordCoh2.TwoCocycle L) : (WordCoh2.shiftLiftMark t a c).wildValueR.base = t.wildValueR

The shifted lift's Roe wild relator value projects to the base's (needs L finite).

theorem GQ2.WordCoh2R.shiftLiftMark_wildValueR_eq_one {L : Type u_1} [Group L] [Finite L] (t : Marking L) (hw : t.WildRelR) (a : Fin 4 → ZMod 2) (c : WordCoh2.TwoCocycle L) (hz : (WordCoh2.shiftLiftMark t a c).wildValueR.fib = 0) : (WordCoh2.shiftLiftMark t a c).wildValueR = 1

Roe wild relator dies exactly. When the base marking satisfies the Roe wild relation and the shifted wild z-value is 0, the shifted lift's Roe wild relator value is the identity of the extension.

The Roe wild shift law

Shifting the lifted marking's fibre coordinates by a moves the Roe wild fibre obstruction by a 1 — the same shift as the tame one, and the same as Γ_A's wild shift, even though the underlying Fox row differs (x₁ + (1 + S⁻¹)·x₂ here versus x₁ + (1 + S⁻¹)·x₃ there): at the trivial action of CentExt c on 𝔽₂ both collapse to a 1 in characteristic 2.

theorem GQ2.WordCoh2R.liftMarking_wildValueR_g {L : Type u_1} [Group L] {c : WordCoh2.TwoCocycle L} [Finite L] (t : Marking L) (a : Fin 4 → ZMod 2) : (FoxH.liftMarking (WordCoh2.liftMark t c) a).wildValueR.g = (WordCoh2.liftMark t c).wildValueR

The Roe wild relator value's base coordinate of the lift recovers that of liftMark t c.

theorem GQ2.WordCoh2R.liftMarking_wildValueR_u_eq {L : Type u_1} [Group L] {c : WordCoh2.TwoCocycle L} [Finite L] (t : Marking L) (a : Fin 4 → ZMod 2) : (FoxH.liftMarking (WordCoh2.liftMark t c) a).wildValueR.u = a 1

The Roe wild fibre shift of the lift is a 1 (liftMarking_wildValueR_u at trivial action, char 2: the row a 1 + a 2 + S⁻¹·a 2 collapses to a 1).

theorem GQ2.WordCoh2R.shiftLiftMark_wildValueR_fib {L : Type u_1} [Group L] {c : WordCoh2.TwoCocycle L} [Finite L] (t : Marking L) (a : Fin 4 → ZMod 2) : (WordCoh2.shiftLiftMark t a c).wildValueR.fib = (WordCoh2.liftMark t c).wildValueR.fib + a 1

Roe wild shift law: shifting the lift by a changes the Roe wild fibre obstruction by a 1.

theorem GQ2.WordCoh2R.exists_shiftR_of_relZ_eq {L : Type u_1} [Group L] {c : WordCoh2.TwoCocycle L} [Finite L] (t : Marking L) (hrel : (WordCoh2.liftMark t c).tameValue.fib = (WordCoh2.liftMark t c).wildValueR.fib) : ∃ (a : Fin 4 → ZMod 2), (WordCoh2.shiftLiftMark t a c).tameValue.fib = 0 ∧ (WordCoh2.shiftLiftMark t a c).wildValueR.fib = 0

The d¹-adjustment. When the tame and Roe wild fibre obstructions of liftMark t c agree, the constant shift a ≡ (liftMark t c).tameValue.fib makes both shifted relator fibres vanish — the hypothesis feeding NR_le_ker_shiftLiftR.

Level change and additivity

relZPairR is natural in the base group (relZPairR_comap) and additive in the cocycle (relZPairR_add) — the two structural laws making the obstruction well defined and a homomorphism. Both comparison objects (projExt, FiberProd) are reused from WordCoh2.

theorem GQ2.WordCoh2R.relZPairR_comap {L : Type u_1} {L' : Type u_2} [Group L] [Group L'] [Finite L] [Finite L'] (t' : Marking L') (c : WordCoh2.TwoCocycle L) (φ : L' →* L) : relZPairR (Marking.map φ t') c = relZPairR t' (c.comap φ)

Level-independence of the Roe relator obstruction. Pulling c back along φ and pushing the base marking forward by φ give the same relZPairR.

theorem GQ2.WordCoh2R.relZPairR_add {L : Type u_1} [Group L] [Finite L] (t : Marking L) (c₁ c₂ : WordCoh2.TwoCocycle L) : relZPairR t (c₁ + c₂) = relZPairR t c₁ + relZPairR t c₂

Additivity of the Roe relator obstruction. Same fibre-product argument as WordCoh2.relZPair_add, now with Marking.map_wildValueR on the second component.

Vanishing on coboundaries

theorem GQ2.WordCoh2R.trivialMarking_wildValueR {L : Type u_1} [Group L] : { σ := 1, τ := 1, x₀ := 1, x₁ := 1 }.wildValueR = 1

The trivial marking (all four generators 1) satisfies the Roe wild relation. Both ω₂-subwords of r_R (inside aR and inside cR's sigma2) are powers of 1.

theorem GQ2.WordCoh2R.relZPairR_zero {L : Type u_1} [Group L] [Finite L] (t : Marking L) : relZPairR t WordCoh2.zeroCocycle = (0, 0)

The split extension has balanced (zero) Roe relator obstruction.

theorem GQ2.WordCoh2R.obs_coboundaryR_eq {L : Type u_1} [Group L] [Finite L] (t : Marking L) (lam : L → ZMod 2) (hlam1 : lam 1 = 0) : (relZPairR t (WordCoh2.coboundaryCocycle lam hlam1)).1 + (relZPairR t (WordCoh2.coboundaryCocycle lam hlam1)).2 = lam t.tameValue + lam t.wildValueR

The Roe obstruction of a finite-level coboundary is λ (tame relator) + λ (Roe wild relator). At an R-admissible level both relators die, so this is 0 — the vanishing of obs_R on B².

The splitting section: N_R ≤ ker (classify (shifted lift))

The injectivity crux, an exact mirror of WordCoh2.NA_le_ker_shiftLift with IsAdmissibleU/isAdmissibleU_iff_NA_le swapped for IsAdmissibleUR/isAdmissibleUR_iff_NR_le and Marking.map_wildRelator_eq_one_iff for Marking.map_wildRelatorR_eq_one_iff. The Pro2Core clause reuses the word-independent WordCoh2.isPGroup_shiftLift_wildCore.

theorem GQ2.WordCoh2R.NR_le_ker_shiftLiftR (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) [Finite (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)] (hU : NR ≤ ↑U.toOpenSubgroup) (c : WordCoh2.TwoCocycle (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)) (a : Fin 4 → ZMod 2) (htame0 : (WordCoh2.shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).tameValue.fib = 0) (hwild0 : (WordCoh2.shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).wildValueR.fib = 0) : NR ≤ (WordCoh2.shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).classify.ker

N_R ≤ ker for the shifted lift. ([Finite (F₄ ⧸ U)] is needed at statement level for CentExt c to be finite.)

noncomputable def GQ2.WordCoh2R.sectionHomR (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) [Finite (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)] (hU : NR ≤ ↑U.toOpenSubgroup) (c : WordCoh2.TwoCocycle (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)) (a : Fin 4 → ZMod 2) (htame0 : (WordCoh2.shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).tameValue.fib = 0) (hwild0 : (WordCoh2.shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).wildValueR.fib = 0) : WordCohBridgeR.GR →ₜ* WordCoh2.CentExt c

The splitting section Γ_R → CentExt c produced by NR_le_ker_shiftLiftR.

Equations

• GQ2.WordCoh2R.sectionHomR U hU c a htame0 hwild0 = GQ2.quotientLift GQ2.NR (GQ2.WordCoh2.shiftLiftMark (GQ2.Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) GQ2.univMarking) a c).classify ⋯

theorem GQ2.WordCoh2R.projC_comp_sectionHomR (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) [Finite (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)] (hU : NR ≤ ↑U.toOpenSubgroup) (c : WordCoh2.TwoCocycle (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)) (a : Fin 4 → ZMod 2) (htame0 : (WordCoh2.shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).tameValue.fib = 0) (hwild0 : (WordCoh2.shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).wildValueR.fib = 0) (g : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) : ((sectionHomR U hU c a htame0 hwild0) ((quotientMk NR) g)).base = (QuotientGroup.mk' ↑U.toOpenSubgroup) g

The section splits the base projection: proj ∘ s is the level projection Γ_R ↠ F₄ ⧸ U.

Coboundary extraction

theorem GQ2.WordCoh2R.cocycle_mem_B2_R [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) [Finite (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)] (hU : NR ≤ ↑U.toOpenSubgroup) (c : WordCoh2.TwoCocycle (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)) (a : Fin 4 → ZMod 2) (htame0 : (WordCoh2.shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).tameValue.fib = 0) (hwild0 : (WordCoh2.shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).wildValueR.fib = 0) (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) : (fun (p : WordCohBridgeR.GR × WordCohBridgeR.GR) => c.κ ((sectionHomR U hU c a htame0 hwild0) p.1).base ((sectionHomR U hU c a htame0 hwild0) p.2).base) ∈ ContCoh.B2 WordCohBridgeR.GR (ZMod 2)

Coboundary extraction. With 𝔽₂ a trivial Γ_R-module, the level cocycle pulled back through the splitting section is a continuous 2-coboundary dOne (fib ∘ s). Word-independent given the section, so this is the verbatim Γ_R retyping of WordCoh2.cocycle_mem_B2.

The level projection and the injectivity keystone

noncomputable def GQ2.WordCoh2R.levelProjR (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) (hU : NR ≤ ↑U.toOpenSubgroup) : WordCohBridgeR.GR →ₜ* ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup

The level projection Γ_R = F₄ ⧸ N_R ↠ F₄ ⧸ U for N_R ≤ U.

Equations

• GQ2.WordCoh2R.levelProjR U hU = GQ2.quotientLift GQ2.NR (GQ2.quotientMk ↑U.toOpenSubgroup) ⋯

@[simp]

theorem GQ2.WordCoh2R.levelProjR_quotientMk (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) (hU : NR ≤ ↑U.toOpenSubgroup) (g : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) : (levelProjR U hU) ((quotientMk NR) g) = (QuotientGroup.mk' ↑U.toOpenSubgroup) g

theorem GQ2.WordCoh2R.inflated_cocycle_mem_B2_R [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) [Finite (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)] (hU : NR ≤ ↑U.toOpenSubgroup) (c : WordCoh2.TwoCocycle (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)) (hrel : (WordCoh2.liftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) c).tameValue.fib = (WordCoh2.liftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) c).wildValueR.fib) (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) : (fun (p : WordCohBridgeR.GR × WordCohBridgeR.GR) => c.κ ((levelProjR U hU) p.1) ((levelProjR U hU) p.2)) ∈ ContCoh.B2 WordCohBridgeR.GR (ZMod 2)

Injectivity keystone. A finite-level cocycle with balanced Roe relator obstruction inflates to a continuous 2-coboundary on Γ_R.

Factoring a continuous cocycle through a finite level

The compactness core WordCoh2.exists_openNormalSubgroup_factor_two is stated for an arbitrary profinite group, so it is reused verbatim; only the transport to F₄ ⧸ U := comap N_R V is retyped.

theorem GQ2.WordCoh2R.exists_twoCocycle_factor_R (κ : WordCohBridgeR.GR × WordCohBridgeR.GR → ZMod 2) (hκc : Continuous κ) (hκ1 : κ (1, 1) = 0) (hκcoc : ∀ (a b c : WordCohBridgeR.GR), κ (a, b) + κ (a * b, c) = κ (a, b * c) + κ (b, c)) : ∃ (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) (hU : NR ≤ ↑U.toOpenSubgroup) (c : WordCoh2.TwoCocycle (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)), ∀ (x y : WordCohBridgeR.GR), κ (x, y) = c.κ ((levelProjR U hU) x) ((levelProjR U hU) y)

Factoring a normalized continuous 2-cocycle on Γ_R.

theorem GQ2.WordCoh2R.exists_oneCochain_factor_R (ψ : WordCohBridgeR.GR → ZMod 2) (hψc : Continuous ψ) : ∃ (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) (hU : NR ≤ ↑U.toOpenSubgroup) (lam : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup → ZMod 2), ∀ (x : WordCohBridgeR.GR), ψ x = lam ((levelProjR U hU) x)

Factoring a continuous 1-cochain on Γ_R.

Injectivity, assembled

theorem GQ2.WordCoh2R.mem_B2_of_factor_balanced_R [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (κ : WordCohBridgeR.GR × WordCohBridgeR.GR → ZMod 2) (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) [Finite (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)] (hU : NR ≤ ↑U.toOpenSubgroup) (c : WordCoh2.TwoCocycle (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)) (hfact : ∀ (x y : WordCohBridgeR.GR), κ (x, y) = c.κ ((levelProjR U hU) x) ((levelProjR U hU) y)) (hbal : (WordCoh2.liftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) c).tameValue.fib = (WordCoh2.liftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) c).wildValueR.fib) : κ ∈ ContCoh.B2 WordCohBridgeR.GR (ZMod 2)

Injectivity, consumable form. A continuous cochain factoring through a finite level whose Roe relator obstruction is balanced is a continuous 2-coboundary.

The obstruction map and #H²(Γ_R, 𝔽₂) ≤ 2

structure GQ2.WordCoh2R.LevelFactorR (κ : WordCohBridgeR.GR × WordCohBridgeR.GR → ZMod 2) : Type

A factorization of a Γ_R-cochain κ through a finite R-admissible level.

• U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop

  The finite R-admissible level F₄ ⧸ U.

• hU : NR ≤ ↑self.U.toOpenSubgroup

  N_R ≤ U, so Γ_R = F₄ ⧸ N_R ↠ F₄ ⧸ U.

• c : WordCoh2.TwoCocycle (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑self.U.toOpenSubgroup)

  The finite-level 2-cocycle whose inflation is κ.

• hfact (x y : WordCohBridgeR.GR) : κ (x, y) = self.c.κ ((levelProjR self.U ⋯) x) ((levelProjR self.U ⋯) y)

  κ is the inflation of c along levelProjR.

noncomputable def GQ2.WordCoh2R.LevelFactorR.obs {κ : WordCohBridgeR.GR × WordCohBridgeR.GR → ZMod 2} (F : LevelFactorR κ) : ZMod 2

The Roe relator obstruction of a factorization: the sum of the tame and Roe wild relator fibre-z values of the finite-level cocycle.

Equations

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

theorem GQ2.WordCoh2R.LevelFactorR.obs_eq_comap {κ : WordCohBridgeR.GR × WordCohBridgeR.GR → ZMod 2} (F : LevelFactorR κ) (W : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) (proj : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑W.toOpenSubgroup →* ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑F.U.toOpenSubgroup) (hproj : proj.comp (QuotientGroup.mk' ↑W.toOpenSubgroup) = QuotientGroup.mk' ↑F.U.toOpenSubgroup) : F.obs = (relZPairR (Marking.map (QuotientGroup.mk' ↑W.toOpenSubgroup) univMarking) (F.c.comap proj)).1 + (relZPairR (Marking.map (QuotientGroup.mk' ↑W.toOpenSubgroup) univMarking) (F.c.comap proj)).2

Level-independence. F.obs may be computed at any finer level W (relZPairR_comap).

theorem GQ2.WordCoh2R.LevelFactorR.obs_congr {κ : WordCohBridgeR.GR × WordCohBridgeR.GR → ZMod 2} (F₁ F₂ : LevelFactorR κ) : F₁.obs = F₂.obs

Well-definedness. F.obs depends only on κ, not on the chosen factorization.

theorem GQ2.WordCoh2R.levelProjR_comp (W U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) (hUW : NR ≤ ↑W.toOpenSubgroup) (hU : NR ≤ ↑U.toOpenSubgroup) (proj : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑W.toOpenSubgroup →* ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup) (hproj : proj.comp (QuotientGroup.mk' ↑W.toOpenSubgroup) = QuotientGroup.mk' ↑U.toOpenSubgroup) (x : WordCohBridgeR.GR) : proj ((levelProjR W hUW) x) = (levelProjR U hU) x

The two projections F₄ ⧸ W → F₄ ⧸ U (for N_R ≤ W ≤ U) and the level maps compose.

noncomputable def GQ2.WordCoh2R.normalizeCochainR (κ : WordCohBridgeR.GR × WordCohBridgeR.GR → ZMod 2) : WordCohBridgeR.GR × WordCohBridgeR.GR → ZMod 2

Normalize a 2-cochain at (1,1) by subtracting the (coboundary) constant κ (1,1).

Equations

• GQ2.WordCoh2R.normalizeCochainR κ = κ - fun (x : GQ2.WordCohBridgeR.GR × GQ2.WordCohBridgeR.GR) => κ (1, 1)

theorem GQ2.WordCoh2R.const2_mem_B2_R [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) (v : ZMod 2) : (fun (x : WordCohBridgeR.GR × WordCohBridgeR.GR) => v) ∈ ContCoh.B2 WordCohBridgeR.GR (ZMod 2)

Under the trivial action, a constant 2-cochain is a continuous coboundary.

theorem GQ2.WordCoh2R.nonempty_levelFactorR_normalize [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) (φ : ↥(ContCoh.Z2 WordCohBridgeR.GR (ZMod 2))) : Nonempty (LevelFactorR (normalizeCochainR ↑φ))

The normalization of a continuous 2-cocycle factors through a finite R-admissible level.

noncomputable def GQ2.WordCoh2R.obsFun_R [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) (φ : ↥(ContCoh.Z2 WordCohBridgeR.GR (ZMod 2))) : ZMod 2

The per-cocycle Roe obstruction: the relator obstruction of any factorization of the normalization.

Equations

• GQ2.WordCoh2R.obsFun_R htriv φ = ⋯.some.obs

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

obsFun_R may be computed at any factorization of the normalization.

theorem GQ2.WordCoh2R.obsFun_add_R [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) (φ ψ : ↥(ContCoh.Z2 WordCohBridgeR.GR (ZMod 2))) : obsFun_R htriv (φ + ψ) = obsFun_R htriv φ + obsFun_R htriv ψ

Additivity of the Roe obstruction. Both φ and ψ factor through a common refinement W = U_φ ⊓ U_ψ, where their finite-level cocycles pull back and add (relZPairR_add).

noncomputable def GQ2.WordCoh2R.obs_R [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) : ↥(ContCoh.Z2 WordCohBridgeR.GR (ZMod 2)) →+ ZMod 2

The Roe obstruction homomorphism Z²_cont(Γ_R, 𝔽₂) →+ 𝔽₂.

Equations

• GQ2.WordCoh2R.obs_R htriv = AddMonoidHom.mk' (GQ2.WordCoh2R.obsFun_R htriv) ⋯

theorem GQ2.WordCoh2R.obs_ker_le_R [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) : (obs_R htriv).ker ≤ (ContCoh.B2 WordCohBridgeR.GR (ZMod 2)).addSubgroupOf (ContCoh.Z2 WordCohBridgeR.GR (ZMod 2))

The kernel of the Roe obstruction lands in the 2-coboundaries.

theorem GQ2.WordCoh2R.obs_B2_eq_zero_R [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) : (ContCoh.B2 WordCohBridgeR.GR (ZMod 2)).addSubgroupOf (ContCoh.Z2 WordCohBridgeR.GR (ZMod 2)) ≤ (obs_R htriv).ker

obs_R kills B². A continuous coboundary normalizes to δ¹ψ' (ψ' 1 = 0), which factors through a finite R-admissible level as coboundaryCocycle λ; its obstruction is λ(tameValue) + λ(wildValueR) = λ 1 + λ 1 = 0 since both Γ_R relators die at that level (isAdmissibleUR_of_NR_le).

theorem GQ2.WordCoh2R.obs_ker_eq_B2_R [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) : (obs_R htriv).ker = (ContCoh.B2 WordCohBridgeR.GR (ZMod 2)).addSubgroupOf (ContCoh.Z2 WordCohBridgeR.GR (ZMod 2))

ker obs_R = B². The Roe obstruction is trivial on coboundaries and nowhere else, so it descends to an injection H²(Γ_R, 𝔽₂) ↪ 𝔽₂.

noncomputable def GQ2.WordCoh2R.obsH2_R [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) : ContCoh.H2 WordCohBridgeR.GR (ZMod 2) →+ ZMod 2

The descended Roe obstruction H²(Γ_R, 𝔽₂) →+ 𝔽₂.

Equations

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

theorem GQ2.WordCoh2R.obsH2_R_injective [DistribMulAction WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) : Function.Injective ⇑(obsH2_R htriv)

#H²(Γ_R, 𝔽₂) ≤ 2: a continuous 2-cocycle whose Roe obstruction is nonzero is not a coboundary. The degree-2 presentation comparison for Γ_R.

Paper-tag ledger (Roe note paper/roe-presentation-verification.tex; hand-maintained)

• eq. (1.2) = ⟦eq:relators⟧ — the Roe wild relator, read off the central extension by relZPairR; its death at every R-admissible level is what makes obs_R kill B².
• Definition 1.1 = ⟦def:GammaR⟧ — IsAdmissibleUR/N_R, via NR_le_ker_shiftLiftR.