DRWordCoh.lean

/-
Copyright (c) 2026 David Roe. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: David Roe, roed@mit.edu, using Claude Opus-4.8 and Fable-5
-/
module

public import GQ2.Roe.DRAbelianization
public import GQ2.Cohomology

@[expose] public section

/-!
# The `D_R` degree-2 presentation comparison — single-relator obstruction (ticket R13b)

The `D_R = ⟨s, x, y | r₂⟩_{pro-2}` analogue of the (non-`module`) Γ_A degree-2 bridge
`GQ2/WordCoh2.lean`.  Because `D_R` has a **single** relator, the relator obstruction is a *single*
`𝔽₂` value (not the tame/wild pair of Γ_A), so there is no "balance" (`im d¹`) condition: the
obstruction map lands in `𝔽₂` directly and injectivity is exactly the `#H² ≤ 2` statement.

`GQ2/WordCoh2.lean` is not a `module`, so its generic central-extension algebra cannot be imported
here; the `## Generic central-extension algebra` section below re-derives the pieces we need
(`TwoCocycle`, `CentExt`, `FiberProd`, `zeroCocycle`, `coboundaryCocycle`, `Psi`,
`TwoCocycle.comap`/`projExt`, `exists_openNormalSubgroup_factor_two`) verbatim in the `GQ2.DRCoh`
namespace.  On top of that:

* `drRelZ m c` — the fibre of `drWord` evaluated at the zero-fibre lift of a triple `m : Fin 3 → L`;
  naturality (`drRelZ_comap`), additivity (`drRelZ_add`), coboundary law (`drRelZ_coboundary`);
* the profinite factoring `exists_twoCocycle_factor_DR` (the generic compactness core applied to the
  pro-2 group `D_R` *directly* — the relation is inherited by every finite quotient `D_R ⧸ V`);
* `DRLevelFactor`/`obs`/`obs_congr` — the level-independent single-`𝔽₂` obstruction;
* the injectivity keystone: when `obs = 0` the relator dies exactly, so `drLiftHom` directly builds a
  splitting section `D_R → CentExt c` and the pulled-back cocycle is a continuous coboundary;
* `obsH2_DR : H²(D_R, 𝔽₂) →+ 𝔽₂`, its injectivity, and the bridge `obsFun_DR_eq_of_factor` computing
  the obstruction at *any* finite quotient — consumed by `GQ2/Roe/DRH2.lean` and `DRDemushkin.lean`.
-/

namespace GQ2

/-! ## Generic central-extension algebra (re-derived from `GQ2/WordCoh2.lean`)

Verbatim ports of the generic-in-`L` declarations of the non-`module` `GQ2/WordCoh2.lean`, placed in
the fresh `GQ2.DRCoh` namespace to avoid any clash with `GQ2.WordCoh2.*` (both are visible in the
top-level `GQ2.lean` aggregate). -/

namespace DRCoh

variable {L : Type*} [Group L]

/-- A `ZMod 2`-valued 2-cocycle on `L`, normalized at `(1,1)` (`WordCoh2.TwoCocycle`). -/
structure TwoCocycle (L : Type*) [Group L] where
  /-- The underlying 2-cochain. -/
  κ : L → L → ZMod 2
  /-- Normalization at the identity. -/
  norm : κ 1 1 = 0
  /-- The 2-cocycle identity (trivial coefficients). -/
  cocyc : ∀ a b c : L, κ a b + κ (a * b) c = κ a (b * c) + κ b c

namespace TwoCocycle

variable (c : TwoCocycle L)

theorem κ_one_left (l : L) : c.κ 1 l = 0 := by simpa [c.norm] using c.cocyc 1 1 l

theorem κ_one_right (l : L) : c.κ l 1 = 0 := by simpa [c.norm] using c.cocyc l 1 1

theorem κ_inv (l : L) : c.κ l l⁻¹ = c.κ l⁻¹ l := by
  simpa [c.κ_one_left, c.κ_one_right] using c.cocyc l l⁻¹ l

end TwoCocycle

/-- The central extension `L ×_κ ZMod 2` (`WordCoh2.CentExt`). -/
def CentExt (_c : TwoCocycle L) : Type _ := L × ZMod 2

namespace CentExt

variable {c : TwoCocycle L}

/-- Base coordinate. -/
def base (p : CentExt c) : L := p.1
/-- Fibre coordinate. -/
def fib (p : CentExt c) : ZMod 2 := p.2

@[ext] theorem ext {p q : CentExt c} (h1 : p.base = q.base) (h2 : p.fib = q.fib) : p = q :=
  Prod.ext h1 h2

instance : Group (CentExt c) where
  mul p q := (p.1 * q.1, p.2 + q.2 + c.κ p.1 q.1)
  one := (1, 0)
  inv p := (p.1⁻¹, p.2 + c.κ p.1 p.1⁻¹)
  mul_assoc p q r := by
    apply Prod.ext
    · exact mul_assoc p.1 q.1 r.1
    · show p.2 + q.2 + c.κ p.1 q.1 + r.2 + c.κ (p.1 * q.1) r.1
        = p.2 + (q.2 + r.2 + c.κ q.1 r.1) + c.κ p.1 (q.1 * r.1)
      linear_combination c.cocyc p.1 q.1 r.1
  one_mul p := by
    apply Prod.ext
    · exact one_mul p.1
    · show (0 : ZMod 2) + p.2 + c.κ 1 p.1 = p.2
      rw [c.κ_one_left, add_zero, zero_add]
  mul_one p := by
    apply Prod.ext
    · exact mul_one p.1
    · show p.2 + 0 + c.κ p.1 1 = p.2
      rw [c.κ_one_right, add_zero, add_zero]
  inv_mul_cancel p := by
    apply Prod.ext
    · exact inv_mul_cancel p.1
    · show p.2 + c.κ p.1 p.1⁻¹ + p.2 + c.κ p.1⁻¹ p.1 = 0
      rw [c.κ_inv]
      exact (by decide : ∀ x y : ZMod 2, x + y + x + y = 0) _ _

@[simp] theorem mul_base (p q : CentExt c) : (p * q).base = p.base * q.base := rfl
@[simp] theorem mul_fib (p q : CentExt c) : (p * q).fib = p.fib + q.fib + c.κ p.base q.base := rfl
@[simp] private theorem one_base : (1 : CentExt c).base = 1 := rfl
@[simp] private theorem one_fib : (1 : CentExt c).fib = 0 := rfl

/-- The base projection `CentExt c →* L`. -/
def proj (c : TwoCocycle L) : CentExt c →* L where
  toFun := CentExt.base
  map_one' := rfl
  map_mul' := mul_base

/-- The central inclusion `ZMod 2 → CentExt c`. -/
def incl (c : TwoCocycle L) : ZMod 2 → CentExt c := fun z => (1, z)

@[simp] private theorem incl_base (z : ZMod 2) : (incl c z).base = 1 := rfl
@[simp] private theorem incl_fib (z : ZMod 2) : (incl c z).fib = z := rfl

theorem base_eq_one_iff (p : CentExt c) : p.base = 1 ↔ p = incl c p.fib :=
  ⟨fun h => CentExt.ext h rfl, fun h => by rw [h]; rfl⟩

@[simp] theorem incl_zero : incl c (0 : ZMod 2) = 1 := rfl

@[simp] theorem incl_mul_fib (z : ZMod 2) (p : CentExt c) : (incl c z * p).fib = z + p.fib := by
  show z + p.fib + c.κ 1 p.base = z + p.fib
  rw [c.κ_one_left, add_zero]

instance : TopologicalSpace (CentExt c) := ⊥
instance : DiscreteTopology (CentExt c) := ⟨rfl⟩
instance [Finite L] : Finite (CentExt c) := inferInstanceAs (Finite (L × ZMod 2))

end CentExt

/-! ### Level change: pulling a cocycle back along a group hom -/

section LevelChange

variable {L L' : Type*} [Group L] [Group L']

/-- Pull back a 2-cocycle along `φ : L' →* L`. -/
def TwoCocycle.comap (c : TwoCocycle L) (φ : L' →* L) : TwoCocycle L' where
  κ a b := c.κ (φ a) (φ b)
  norm := by simp only [map_one]; exact c.norm
  cocyc a b d := by simp only [map_mul]; exact c.cocyc (φ a) (φ b) (φ d)

@[simp] theorem TwoCocycle.comap_κ (c : TwoCocycle L) (φ : L' →* L) (a b : L') :
    (c.comap φ).κ a b = c.κ (φ a) (φ b) := rfl

/-- The base hom `φ` lifts to `CentExt (c.comap φ) →* CentExt c`. -/
def projExt (c : TwoCocycle L) (φ : L' →* L) : CentExt (c.comap φ) →* CentExt c where
  toFun p := ((φ p.base, p.fib) : CentExt c)
  map_one' := CentExt.ext (map_one φ) rfl
  map_mul' p q := CentExt.ext (map_mul φ p.base q.base) rfl

@[simp] theorem projExt_fib (c : TwoCocycle L) (φ : L' →* L) (p : CentExt (c.comap φ)) :
    (projExt c φ p).fib = p.fib := rfl

end LevelChange

/-! ### Additivity infrastructure: sum cocycle and fiber product -/

section Additivity

variable {L : Type*} [Group L]

/-- Pointwise sum of 2-cocycles. -/
instance : Add (TwoCocycle L) where
  add c₁ c₂ :=
    { κ := fun a b => c₁.κ a b + c₂.κ a b
      norm := by rw [c₁.norm, c₂.norm, add_zero]
      cocyc := fun a b d => by
        have h1 := c₁.cocyc a b d; have h2 := c₂.cocyc a b d; linear_combination h1 + h2 }

@[simp] theorem TwoCocycle.add_κ (c₁ c₂ : TwoCocycle L) (a b : L) :
    (c₁ + c₂).κ a b = c₁.κ a b + c₂.κ a b := rfl

/-- The fiber product `CentExt c₁ ×_L CentExt c₂`. -/
def FiberProd (_c₁ _c₂ : TwoCocycle L) : Type _ := L × ZMod 2 × ZMod 2

namespace FiberProd

variable {c₁ c₂ : TwoCocycle L}

/-- Base coordinate. -/
def base (p : FiberProd c₁ c₂) : L := p.1
/-- First fibre coordinate. -/
def fibA (p : FiberProd c₁ c₂) : ZMod 2 := p.2.1
/-- Second fibre coordinate. -/
def fibB (p : FiberProd c₁ c₂) : ZMod 2 := p.2.2

@[ext] private theorem ext {p q : FiberProd c₁ c₂} (h1 : p.base = q.base) (h2 : p.fibA = q.fibA)
    (h3 : p.fibB = q.fibB) : p = q :=
  Prod.ext h1 (Prod.ext h2 h3)

instance : Group (FiberProd c₁ c₂) where
  mul p q := (p.1 * q.1, p.2.1 + q.2.1 + c₁.κ p.1 q.1, p.2.2 + q.2.2 + c₂.κ p.1 q.1)
  one := (1, 0, 0)
  inv p := (p.1⁻¹, p.2.1 + c₁.κ p.1 p.1⁻¹, p.2.2 + c₂.κ p.1 p.1⁻¹)
  mul_assoc p q r := by
    apply FiberProd.ext
    · exact mul_assoc p.1 q.1 r.1
    · show p.2.1 + q.2.1 + c₁.κ p.1 q.1 + r.2.1 + c₁.κ (p.1 * q.1) r.1
        = p.2.1 + (q.2.1 + r.2.1 + c₁.κ q.1 r.1) + c₁.κ p.1 (q.1 * r.1)
      linear_combination c₁.cocyc p.1 q.1 r.1
    · show p.2.2 + q.2.2 + c₂.κ p.1 q.1 + r.2.2 + c₂.κ (p.1 * q.1) r.1
        = p.2.2 + (q.2.2 + r.2.2 + c₂.κ q.1 r.1) + c₂.κ p.1 (q.1 * r.1)
      linear_combination c₂.cocyc p.1 q.1 r.1
  one_mul p := by
    apply FiberProd.ext
    · exact one_mul p.1
    · show (0 : ZMod 2) + p.2.1 + c₁.κ 1 p.1 = p.2.1; rw [c₁.κ_one_left, add_zero, zero_add]
    · show (0 : ZMod 2) + p.2.2 + c₂.κ 1 p.1 = p.2.2; rw [c₂.κ_one_left, add_zero, zero_add]
  mul_one p := by
    apply FiberProd.ext
    · exact mul_one p.1
    · show p.2.1 + 0 + c₁.κ p.1 1 = p.2.1; rw [c₁.κ_one_right, add_zero, add_zero]
    · show p.2.2 + 0 + c₂.κ p.1 1 = p.2.2; rw [c₂.κ_one_right, add_zero, add_zero]
  inv_mul_cancel p := by
    apply FiberProd.ext
    · exact inv_mul_cancel p.1
    · show p.2.1 + c₁.κ p.1 p.1⁻¹ + p.2.1 + c₁.κ p.1⁻¹ p.1 = 0
      rw [c₁.κ_inv]; exact (by decide : ∀ x y : ZMod 2, x + y + x + y = 0) _ _
    · show p.2.2 + c₂.κ p.1 p.1⁻¹ + p.2.2 + c₂.κ p.1⁻¹ p.1 = 0
      rw [c₂.κ_inv]; exact (by decide : ∀ x y : ZMod 2, x + y + x + y = 0) _ _

@[simp] private theorem mul_base (p q : FiberProd c₁ c₂) : (p * q).base = p.base * q.base := rfl

/-- Projection to the first central extension. -/
def pr1 : FiberProd c₁ c₂ →* CentExt c₁ where
  toFun p := ((p.base, p.fibA) : CentExt c₁)
  map_one' := rfl
  map_mul' _ _ := rfl

/-- Projection to the second central extension. -/
def pr2 : FiberProd c₁ c₂ →* CentExt c₂ where
  toFun p := ((p.base, p.fibB) : CentExt c₂)
  map_one' := rfl
  map_mul' _ _ := rfl

/-- The fibre-sum hom to the sum extension. -/
def prSum : FiberProd c₁ c₂ →* CentExt (c₁ + c₂) where
  toFun p := ((p.base, p.fibA + p.fibB) : CentExt (c₁ + c₂))
  map_one' := CentExt.ext rfl (add_zero (0 : ZMod 2))
  map_mul' p q := CentExt.ext rfl <| by
    show (p.fibA + q.fibA + c₁.κ p.base q.base) + (p.fibB + q.fibB + c₂.κ p.base q.base)
        = (p.fibA + p.fibB) + (q.fibA + q.fibB) + (c₁.κ p.base q.base + c₂.κ p.base q.base)
    ring

@[simp] theorem pr1_fib (p : FiberProd c₁ c₂) : (pr1 p).fib = p.fibA := rfl
@[simp] theorem pr2_fib (p : FiberProd c₁ c₂) : (pr2 p).fib = p.fibB := rfl
@[simp] theorem prSum_fib (p : FiberProd c₁ c₂) : (prSum p).fib = p.fibA + p.fibB := rfl

instance [Finite L] : Finite (FiberProd c₁ c₂) := inferInstanceAs (Finite (L × ZMod 2 × ZMod 2))

end FiberProd

end Additivity

/-! ### The split and coboundary cocycles -/

section SplitCoboundary

variable {L : Type*} [Group L]

/-- The trivial (split) 2-cocycle `κ ≡ 0`. -/
def zeroCocycle : TwoCocycle L where
  κ _ _ := 0
  norm := rfl
  cocyc _ _ _ := rfl

/-- The fibre projection `CentExt zeroCocycle →* Multiplicative 𝔽₂`. -/
def fibHom0 : CentExt (zeroCocycle : TwoCocycle L) →* Multiplicative (ZMod 2) where
  toFun p := Multiplicative.ofAdd p.fib
  map_one' := rfl
  map_mul' p q := by
    show Multiplicative.ofAdd (p * q).fib = Multiplicative.ofAdd p.fib * Multiplicative.ofAdd q.fib
    rw [CentExt.mul_fib, show (zeroCocycle : TwoCocycle L).κ p.base q.base = (0 : ZMod 2) from rfl,
      add_zero, ofAdd_add]

/-- The coboundary 2-cocycle `δ¹λ`. -/
def coboundaryCocycle (lam : L → ZMod 2) (hlam1 : lam 1 = 0) : TwoCocycle L where
  κ a b := lam a + lam b + lam (a * b)
  norm := by simp [hlam1]
  cocyc a b c := by
    show lam a + lam b + lam (a * b) + (lam (a * b) + lam c + lam (a * b * c))
      = lam a + lam (b * c) + lam (a * (b * c)) + (lam b + lam c + lam (b * c))
    rw [mul_assoc a b c]
    abel_nf
    simp [CharTwo.two_eq_zero]

/-- The trivialization hom `Ψ_λ : (l, z) ↦ (l, z + λ l)`. -/
def Psi (lam : L → ZMod 2) (hlam1 : lam 1 = 0) :
    CentExt (coboundaryCocycle lam hlam1) →* CentExt (zeroCocycle : TwoCocycle L) where
  toFun p := ((p.base, p.fib + lam p.base) : CentExt (zeroCocycle : TwoCocycle L))
  map_one' := CentExt.ext rfl (by show (0 : ZMod 2) + lam 1 = 0; simp [hlam1])
  map_mul' p q := by
    refine CentExt.ext rfl ?_
    · show (p * q).fib + lam (p * q).base
          = (p.fib + lam p.base) + (q.fib + lam q.base)
            + (zeroCocycle : TwoCocycle L).κ p.base q.base
      rw [CentExt.mul_fib, CentExt.mul_base,
        show (zeroCocycle : TwoCocycle L).κ p.base q.base = (0 : ZMod 2) from rfl,
        show (coboundaryCocycle lam hlam1).κ p.base q.base
          = lam p.base + lam q.base + lam (p.base * q.base) from rfl]
      abel_nf
      simp [CharTwo.two_eq_zero]

@[simp] theorem Psi_fib (lam : L → ZMod 2) (hlam1 : lam 1 = 0)
    (p : CentExt (coboundaryCocycle lam hlam1)) : (Psi lam hlam1 p).fib = p.fib + lam p.base := rfl

end SplitCoboundary

/-- Two `TwoCocycle`s with equal cochain are equal. -/
theorem TwoCocycle.ext {L : Type*} [Group L] {c d : TwoCocycle L} (h : c.κ = d.κ) : c = d := by
  cases c; cases d; subst h; rfl

/-! ### Factoring a continuous 2-variable map through a finite quotient -/

/-- **Uniform local constancy** (2-variable form) — `WordCoh2.exists_openNormalSubgroup_factor_two`,
generic in the profinite group `G`. -/
theorem exists_openNormalSubgroup_factor_two
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    {M : Type*} [TopologicalSpace M] [DiscreteTopology M]
    (f : G × G → M) (hf : Continuous f) :
    ∃ V : OpenNormalSubgroup G, ∀ x y : G, ∀ u ∈ V, ∀ v ∈ V, f (x * u, y * v) = f (x, y) := by
  have hbox : ∀ p : G × G, ∃ W : OpenNormalSubgroup G,
      ∀ u ∈ W, ∀ v ∈ W, f (p.1 * u, p.2 * v) = f p := by
    intro p
    have hop : IsOpen (f ⁻¹' {f p}) := (isOpen_discrete _).preimage hf
    obtain ⟨A, B, hA, hB, hpA, hpB, hAB⟩ := isOpen_prod_iff.mp hop p.1 p.2 rfl
    have hOA : IsOpen ((fun w => p.1 * w) ⁻¹' A) := hA.preimage (continuous_const.mul continuous_id)
    have hOB : IsOpen ((fun w => p.2 * w) ⁻¹' B) := hB.preimage (continuous_const.mul continuous_id)
    have h1A : (1 : G) ∈ (fun w => p.1 * w) ⁻¹' A := by simpa using hpA
    have h1B : (1 : G) ∈ (fun w => p.2 * w) ⁻¹' B := by simpa using hpB
    obtain ⟨WA, hWA⟩ := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one hOA h1A
    obtain ⟨WB, hWB⟩ := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one hOB h1B
    refine ⟨WA ⊓ WB, fun u hu v hv => ?_⟩
    have huA : p.1 * u ∈ A := hWA (SetLike.le_def.mp inf_le_left hu)
    have hvB : p.2 * v ∈ B := hWB (SetLike.le_def.mp inf_le_right hv)
    have hmem : (p.1 * u, p.2 * v) ∈ f ⁻¹' {f p} := hAB (Set.mk_mem_prod huA hvB)
    simpa using hmem
  choose W hW using hbox
  obtain ⟨t, ht⟩ := isCompact_univ.elim_finite_subcover
    (fun p : G × G => (fun q : G × G => (p.1⁻¹ * q.1, p.2⁻¹ * q.2)) ⁻¹' (↑(W p) ×ˢ ↑(W p)))
    (fun p => (((W p).toOpenSubgroup.isOpen.prod (W p).toOpenSubgroup.isOpen)).preimage
      (by fun_prop))
    (fun q _ => Set.mem_iUnion.mpr ⟨q, by
      rw [Set.mem_preimage, Set.mem_prod, inv_mul_cancel, inv_mul_cancel]
      exact ⟨one_mem _, one_mem _⟩⟩)
  have hne : t.Nonempty := by
    obtain ⟨i, hi, _⟩ := Set.mem_iUnion₂.mp (ht (Set.mem_univ ((1, 1) : G × G)))
    exact ⟨i, hi⟩
  refine ⟨t.inf' hne W, fun x y u hu v hv => ?_⟩
  have hxy : (x, y) ∈ ⋃ p ∈ t,
      (fun q : G × G => (p.1⁻¹ * q.1, p.2⁻¹ * q.2)) ⁻¹' (↑(W p) ×ˢ ↑(W p)) := ht (Set.mem_univ _)
  rw [Set.mem_iUnion₂] at hxy
  obtain ⟨p, hpt, hp⟩ := hxy
  rw [Set.mem_preimage, Set.mem_prod] at hp
  obtain ⟨hx, hy⟩ := hp
  have hVle : t.inf' hne W ≤ W p := Finset.inf'_le _ hpt
  have huWp : u ∈ W p := SetLike.le_def.mp hVle hu
  have hvWp : v ∈ W p := SetLike.le_def.mp hVle hv
  have hfxy : f (x, y) = f p := by
    have h := hW p (p.1⁻¹ * x) hx (p.2⁻¹ * y) hy
    rwa [mul_inv_cancel_left, mul_inv_cancel_left] at h
  have hfxuyv : f (x * u, y * v) = f p := by
    have hxu : p.1⁻¹ * (x * u) ∈ W p := by rw [← mul_assoc]; exact mul_mem hx huWp
    have hyv : p.2⁻¹ * (y * v) ∈ W p := by rw [← mul_assoc]; exact mul_mem hy hvWp
    have h := hW p (p.1⁻¹ * (x * u)) hxu (p.2⁻¹ * (y * v)) hyv
    rwa [mul_inv_cancel_left, mul_inv_cancel_left] at h
  rw [hfxuyv, hfxy]

end DRCoh

open GQ2.DRCoh ContCoh

/-- The carrier of `D_R` as a plain `Type`.  Coercing the `ProfiniteGrp` object `DR` once (rather
than inside an explicit product `DRT × DRT`, where the second ascription fails to
fire) avoids a universe-inference quirk. -/
abbrev DRT : Type := DR

/-! ## The single-relator obstruction `drRelZ` -/

section RelZ

variable {L : Type*} [Group L]

/-- The three `D_R` generators `m 0, m 1, m 2` placed in `CentExt c` with zero fibre. -/
def drLift (m : Fin 3 → L) (c : TwoCocycle L) (k : Fin 3) : CentExt c := ((m k, 0) : CentExt c)

@[simp] theorem drLift_base (m : Fin 3 → L) (c : TwoCocycle L) (k : Fin 3) :
    (drLift m c k).base = m k := rfl

@[simp] theorem drLift_fib (m : Fin 3 → L) (c : TwoCocycle L) (k : Fin 3) :
    (drLift m c k).fib = 0 := rfl

/-- The **single-relator obstruction** of a 2-cocycle `c` relative to the marking `m : Fin 3 → L`:
the fibre coordinate of `drWord` evaluated at the zero-fibre lift.  The `D_R` analogue of
`WordCoh2.relZPair`, but a *single* `𝔽₂` value (one relator). -/
def drRelZ (m : Fin 3 → L) (c : TwoCocycle L) : ZMod 2 :=
  (drWord (drLift m c 0) (drLift m c 1) (drLift m c 2)).fib

/-- The base of the lifted relator value is the base relator value. -/
theorem drRelZ_base (m : Fin 3 → L) (c : TwoCocycle L) :
    (drWord (drLift m c 0) (drLift m c 1) (drLift m c 2)).base = drWord (m 0) (m 1) (m 2) := by
  have h := map_drWord (CentExt.proj c) (drLift m c 0) (drLift m c 1) (drLift m c 2)
  simpa only [CentExt.proj, MonoidHom.coe_mk, OneHom.coe_mk, drLift_base] using h

end RelZ

section RelZComap

variable {L L' : Type*} [Group L] [Group L']

/-- **Level-independence.**  Pulling `c` back along `φ` and pushing the marking forward by `φ` give
the same obstruction (`WordCoh2.relZPair_comap`, single relator). -/
theorem drRelZ_comap (m : Fin 3 → L') (c : TwoCocycle L) (φ : L' →* L) :
    drRelZ (fun k => φ (m k)) c = drRelZ m (c.comap φ) := by
  have h := map_drWord (projExt c φ) (drLift m (c.comap φ) 0) (drLift m (c.comap φ) 1)
    (drLift m (c.comap φ) 2)
  have hlift : ∀ k, projExt c φ (drLift m (c.comap φ) k) = drLift (fun k => φ (m k)) c k :=
    fun _ => rfl
  rw [hlift, hlift, hlift] at h
  show (drWord (drLift (fun k => φ (m k)) c 0) _ _).fib = (drWord (drLift m (c.comap φ) 0) _ _).fib
  rw [← h, projExt_fib]

end RelZComap

section RelZAdd

variable {L : Type*} [Group L]

/-- The fiber-product lift of a marking (both fibres zero). -/
def drLiftFP (m : Fin 3 → L) (c₁ c₂ : TwoCocycle L) (k : Fin 3) : FiberProd c₁ c₂ :=
  ((m k, 0, 0) : FiberProd c₁ c₂)

private theorem map_pr1_drLiftFP (m : Fin 3 → L) (c₁ c₂ : TwoCocycle L) (k : Fin 3) :
    FiberProd.pr1 (drLiftFP m c₁ c₂ k) = drLift m c₁ k := rfl

private theorem map_pr2_drLiftFP (m : Fin 3 → L) (c₁ c₂ : TwoCocycle L) (k : Fin 3) :
    FiberProd.pr2 (drLiftFP m c₁ c₂ k) = drLift m c₂ k := rfl

private theorem map_prSum_drLiftFP (m : Fin 3 → L) (c₁ c₂ : TwoCocycle L) (k : Fin 3) :
    FiberProd.prSum (drLiftFP m c₁ c₂ k) = drLift m (c₁ + c₂) k :=
  CentExt.ext rfl (add_zero (0 : ZMod 2))

/-- **Additivity of the relator obstruction** (`WordCoh2.relZPair_add`, single relator). -/
theorem drRelZ_add (m : Fin 3 → L) (c₁ c₂ : TwoCocycle L) :
    drRelZ m (c₁ + c₂) = drRelZ m c₁ + drRelZ m c₂ := by
  have h1 := map_drWord FiberProd.pr1 (drLiftFP m c₁ c₂ 0) (drLiftFP m c₁ c₂ 1) (drLiftFP m c₁ c₂ 2)
  have h2 := map_drWord FiberProd.pr2 (drLiftFP m c₁ c₂ 0) (drLiftFP m c₁ c₂ 1) (drLiftFP m c₁ c₂ 2)
  have hs := map_drWord FiberProd.prSum (drLiftFP m c₁ c₂ 0) (drLiftFP m c₁ c₂ 1)
    (drLiftFP m c₁ c₂ 2)
  simp only [map_pr1_drLiftFP] at h1
  simp only [map_pr2_drLiftFP] at h2
  simp only [map_prSum_drLiftFP] at hs
  show (drWord (drLift m (c₁ + c₂) 0) _ _).fib = (drWord (drLift m c₁ 0) _ _).fib
    + (drWord (drLift m c₂ 0) _ _).fib
  rw [← hs, ← h1, ← h2, FiberProd.prSum_fib, FiberProd.pr1_fib, FiberProd.pr2_fib]

end RelZAdd

section RelZCoboundary

variable {L : Type*} [Group L]

/-- Every relator value dies in `Multiplicative (ZMod 2)` (the abelian collapse `−4x + 2y ≡ 0`). -/
private theorem drWord_multZMod2_eq_one (u v w : Multiplicative (ZMod 2)) : drWord u v w = 1 := by
  revert u v w; decide

/-- **The obstruction of the split cocycle vanishes** (`WordCoh2.relZPair_zero`). -/
theorem drRelZ_zero (m : Fin 3 → L) : drRelZ m (zeroCocycle : TwoCocycle L) = 0 := by
  have h := map_drWord (fibHom0 (L := L)) (drLift m zeroCocycle 0) (drLift m zeroCocycle 1)
    (drLift m zeroCocycle 2)
  have hgen : ∀ k, fibHom0 (drLift m (zeroCocycle : TwoCocycle L) k) = 1 := fun _ => rfl
  rw [hgen, hgen, hgen, drWord_multZMod2_eq_one] at h
  have hval : Multiplicative.ofAdd (drRelZ m (zeroCocycle : TwoCocycle L))
      = (1 : Multiplicative (ZMod 2)) := h
  simpa using Multiplicative.ofAdd.injective hval

/-- **The obstruction of a coboundary** is `lam` of the base relator value
(`WordCoh2.obs_coboundary_eq`, single relator).  It vanishes when the marking satisfies the
relation. -/
theorem drRelZ_coboundary (m : Fin 3 → L) (lam : L → ZMod 2) (hlam1 : lam 1 = 0) :
    drRelZ m (coboundaryCocycle lam hlam1) = lam (drWord (m 0) (m 1) (m 2)) := by
  set θ : CentExt (coboundaryCocycle lam hlam1) →* Multiplicative (ZMod 2) :=
    (fibHom0 (L := L)).comp (Psi lam hlam1) with hθ
  have h := map_drWord θ (drLift m (coboundaryCocycle lam hlam1) 0)
    (drLift m (coboundaryCocycle lam hlam1) 1) (drLift m (coboundaryCocycle lam hlam1) 2)
  have hgen : ∀ k,
      θ (drLift m (coboundaryCocycle lam hlam1) k) = Multiplicative.ofAdd (lam (m k)) := by
    intro k
    show Multiplicative.ofAdd ((Psi lam hlam1 (drLift m (coboundaryCocycle lam hlam1) k)).fib) = _
    rw [Psi_fib, drLift_fib, drLift_base, zero_add]
  rw [hgen, hgen, hgen, drWord_multZMod2_eq_one] at h
  have hval : Multiplicative.ofAdd
      ((drWord (drLift m (coboundaryCocycle lam hlam1) 0) (drLift m (coboundaryCocycle lam hlam1) 1)
        (drLift m (coboundaryCocycle lam hlam1) 2)).fib
      + lam (drWord (m 0) (m 1) (m 2))) = (1 : Multiplicative (ZMod 2)) := by
    rw [← h]
    show _ = Multiplicative.ofAdd
      ((Psi lam hlam1 (drWord (drLift m (coboundaryCocycle lam hlam1) 0) _ _)).fib)
    rw [Psi_fib, drRelZ_base]
  have hsum : drRelZ m (coboundaryCocycle lam hlam1) + lam (drWord (m 0) (m 1) (m 2)) = 0 :=
    Multiplicative.ofAdd.injective (hval.trans ofAdd_zero.symm)
  rw [eq_neg_of_add_eq_zero_left hsum, CharTwo.neg_eq]

end RelZCoboundary

/-! ## The named generator triple and its image obstruction -/

/-- The marked generators `s, x, y` of `D_R`, packaged as a triple. -/
noncomputable def drGens : Fin 3 → DRT := ![drS, drX, drY]

@[simp] theorem drGens_zero : drGens 0 = drS := rfl
@[simp] theorem drGens_one : drGens 1 = drX := rfl
@[simp] theorem drGens_two : drGens 2 = drY := rfl

/-- The obstruction of `c` read through the marking `φ ∘ (s, x, y)` for a hom `φ : D_R →* L`. -/
theorem drRelZ_drGens_comap {L : Type*} [Group L] (φ : DRT →* L) (c : TwoCocycle L) :
    drRelZ (fun k => φ (drGens k)) c = drRelZ drGens (c.comap φ) :=
  drRelZ_comap drGens c φ

/-! ## Factoring a continuous cocycle through a finite quotient of `D_R`

`D_R` is profinite and already the presented pro-2 group, so the generic compactness core applies
*directly*: a continuous 2-cocycle on `D_R` factors through a finite quotient `D_R ⧸ V`, and the
relation `drWord (s,x,y) = 1` is inherited by that quotient (no `N_A`/admissibility machinery). -/

section Factoring

/-- **Factoring a normalized continuous 2-cocycle on `D_R`** (`WordCoh2.exists_twoCocycle_factor`,
directly on `D_R`). -/
theorem exists_twoCocycle_factor_DR
    (κ : DRT × DRT → ZMod 2)
    (hκc : Continuous κ) (hκ1 : κ (1, 1) = 0)
    (hκcoc : ∀ a b c : DRT, κ (a, b) + κ (a * b, c) = κ (a, b * c) + κ (b, c)) :
    ∃ (V : OpenNormalSubgroup DRT) (c : TwoCocycle (DRT ⧸ V.toSubgroup)),
      ∀ x y : DRT,
        κ (x, y) = c.κ (QuotientGroup.mk' V.toSubgroup x) (QuotientGroup.mk' V.toSubgroup y) := by
  obtain ⟨V, hV⟩ := DRCoh.exists_openNormalSubgroup_factor_two κ hκc
  refine ⟨V, ?_, ?_⟩
  · refine { κ := fun p q => Quotient.liftOn₂ p q (fun x y => κ (x, y)) ?_, norm := ?_, cocyc := ?_ }
    · intro x₁ y₁ x₂ y₂ hx hy
      have hxv : x₁⁻¹ * x₂ ∈ V.toSubgroup := QuotientGroup.leftRel_apply.mp hx
      have hyv : y₁⁻¹ * y₂ ∈ V.toSubgroup := QuotientGroup.leftRel_apply.mp hy
      have h := hV x₁ y₁ _ hxv _ hyv
      rw [mul_inv_cancel_left, mul_inv_cancel_left] at h
      exact h.symm
    · show κ (1, 1) = 0; exact hκ1
    · intro a b c
      induction a using QuotientGroup.induction_on with | H x =>
      induction b using QuotientGroup.induction_on with | H y =>
      induction c using QuotientGroup.induction_on with | H z =>
      show κ (x, y) + κ (x * y, z) = κ (x, y * z) + κ (y, z)
      exact hκcoc x y z
  · intro x y; rfl

/-- **Factoring a continuous 1-cochain on `D_R`**. -/
theorem exists_oneCochain_factor_DR
    (ψ : DRT → ZMod 2) (hψc : Continuous ψ) :
    ∃ (V : OpenNormalSubgroup DRT) (lam : DRT ⧸ V.toSubgroup → ZMod 2),
      ∀ x : DRT, ψ x = lam (QuotientGroup.mk' V.toSubgroup x) := by
  obtain ⟨V, hV⟩ := DRCoh.exists_openNormalSubgroup_factor_two (fun p => ψ p.1)
    (hψc.comp continuous_fst)
  refine ⟨V, fun p => Quotient.liftOn p (fun x => ψ x) ?_, ?_⟩
  · intro x₁ x₂ hx
    have hxv : x₁⁻¹ * x₂ ∈ V.toSubgroup := QuotientGroup.leftRel_apply.mp hx
    have h := hV x₁ x₁ _ hxv 1 (one_mem _)
    rw [mul_inv_cancel_left, mul_one] at h
    exact h.symm
  · intro x; rfl

end Factoring

/-! ## The level-independent obstruction `DRLevelFactor.obs` -/

section LevelFactor

/-- Every open normal subgroup of `D_R` has finite quotient. -/
instance quotient_finite_openNormal_DR (V : OpenNormalSubgroup DRT) :
    Finite (DRT ⧸ V.toSubgroup) :=
  Subgroup.quotient_finite_of_isOpen V.toSubgroup V.isOpen'

/-- A factorization of a `D_R`-cochain `κ` through a finite quotient `D_R ⧸ V`. -/
structure DRLevelFactor (κ : DRT × DRT → ZMod 2) where
  /-- The finite level `D_R ⧸ V`. -/
  V : OpenNormalSubgroup DRT
  /-- The finite-level 2-cocycle whose inflation is `κ`. -/
  c : TwoCocycle (DRT ⧸ V.toSubgroup)
  /-- `κ` is the inflation of `c`. -/
  hfact : ∀ x y : DRT,
    κ (x, y) = c.κ (QuotientGroup.mk' V.toSubgroup x) (QuotientGroup.mk' V.toSubgroup y)

/-- The relator obstruction of a factorization: the single-relator obstruction of the finite-level
cocycle at the projected generators. -/
noncomputable def DRLevelFactor.obs {κ : DRT × DRT → ZMod 2}
    (F : DRLevelFactor κ) : ZMod 2 :=
  drRelZ (fun k => QuotientGroup.mk' F.V.toSubgroup (drGens k)) F.c

/-- **Level-independence.**  `F.obs` may be computed at any finer level `W` through the pulled-back
cocycle `F.c.comap proj`. -/
theorem DRLevelFactor.obs_eq_comap {κ : DRT × DRT → ZMod 2}
    (F : DRLevelFactor κ) (W : OpenNormalSubgroup DRT)
    (proj : (DRT ⧸ W.toSubgroup) →* (DRT ⧸ F.V.toSubgroup))
    (hproj : proj.comp (QuotientGroup.mk' W.toSubgroup) = QuotientGroup.mk' F.V.toSubgroup) :
    F.obs = drRelZ (fun k => QuotientGroup.mk' W.toSubgroup (drGens k)) (F.c.comap proj) := by
  rw [← drRelZ_comap (fun k => QuotientGroup.mk' W.toSubgroup (drGens k)) F.c proj]
  show drRelZ (fun k => QuotientGroup.mk' F.V.toSubgroup (drGens k)) F.c
    = drRelZ (fun k => proj (QuotientGroup.mk' W.toSubgroup (drGens k))) F.c
  congr 1
  funext k
  rw [← MonoidHom.comp_apply, hproj]

/-- **Well-definedness.**  `F.obs` depends only on `κ`, not on the chosen factorization. -/
theorem DRLevelFactor.obs_congr {κ : DRT × DRT → ZMod 2}
    (F₁ F₂ : DRLevelFactor κ) : F₁.obs = F₂.obs := by
  set W : OpenNormalSubgroup DRT := F₁.V ⊓ F₂.V with hWdef
  have hW1 : W.toSubgroup ≤ F₁.V.toSubgroup := fun x hx => SetLike.le_def.mp inf_le_left hx
  have hW2 : W.toSubgroup ≤ F₂.V.toSubgroup := fun x hx => SetLike.le_def.mp inf_le_right hx
  set p1 : (DRT ⧸ W.toSubgroup) →* (DRT ⧸ F₁.V.toSubgroup) :=
    QuotientGroup.map W.toSubgroup F₁.V.toSubgroup (MonoidHom.id _)
      (by rw [Subgroup.comap_id]; exact hW1) with hp1def
  set p2 : (DRT ⧸ W.toSubgroup) →* (DRT ⧸ F₂.V.toSubgroup) :=
    QuotientGroup.map W.toSubgroup F₂.V.toSubgroup (MonoidHom.id _)
      (by rw [Subgroup.comap_id]; exact hW2) with hp2def
  have hp1 : p1.comp (QuotientGroup.mk' W.toSubgroup) = QuotientGroup.mk' F₁.V.toSubgroup := by
    ext g; rw [hp1def, MonoidHom.comp_apply, QuotientGroup.map_mk']; rfl
  have hp2 : p2.comp (QuotientGroup.mk' W.toSubgroup) = QuotientGroup.mk' F₂.V.toSubgroup := by
    ext g; rw [hp2def, MonoidHom.comp_apply, QuotientGroup.map_mk']; rfl
  rw [F₁.obs_eq_comap W p1 hp1, F₂.obs_eq_comap W p2 hp2]
  have hcc : F₁.c.comap p1 = F₂.c.comap p2 := by
    apply TwoCocycle.ext
    funext a b
    obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective W.toSubgroup a
    obtain ⟨h, rfl⟩ := QuotientGroup.mk'_surjective W.toSubgroup b
    have e1g : p1 (QuotientGroup.mk' W.toSubgroup g) = QuotientGroup.mk' F₁.V.toSubgroup g := by
      rw [← MonoidHom.comp_apply, hp1]
    have e1h : p1 (QuotientGroup.mk' W.toSubgroup h) = QuotientGroup.mk' F₁.V.toSubgroup h := by
      rw [← MonoidHom.comp_apply, hp1]
    have e2g : p2 (QuotientGroup.mk' W.toSubgroup g) = QuotientGroup.mk' F₂.V.toSubgroup g := by
      rw [← MonoidHom.comp_apply, hp2]
    have e2h : p2 (QuotientGroup.mk' W.toSubgroup h) = QuotientGroup.mk' F₂.V.toSubgroup h := by
      rw [← MonoidHom.comp_apply, hp2]
    rw [TwoCocycle.comap_κ, TwoCocycle.comap_κ, e1g, e1h, e2g, e2h,
      ← F₁.hfact g h, ← F₂.hfact g h]
  rw [hcc]

end LevelFactor

/-! ## `CentExt` over a finite quotient of `D_R` is pro-2 -/

/-- `CentExt c` over a finite quotient of the pro-2 group `D_R` is a finite `2`-group, hence
pro-2 — the target hypothesis of `drLiftHom`. -/
theorem isProP_CentExt {V : OpenNormalSubgroup DRT} (c : TwoCocycle (DRT ⧸ V.toSubgroup)) :
    IsProP 2 (CentExt c) := by
  haveI : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
  obtain ⟨k, hk⟩ := (IsPGroup.iff_card (p := 2)).mp (isProP_DR V)
  refine isProP_of_isPGroup ((IsPGroup.iff_card (p := 2)).mpr ⟨k + 1, ?_⟩)
  have hcard : Nat.card (CentExt c) = Nat.card (DRT ⧸ V.toSubgroup) * Nat.card (ZMod 2) :=
    Nat.card_prod _ _
  rw [hcard, hk, Nat.card_zmod, pow_succ]

/-! ## The relation holds at every finite level -/

/-- The Roe relation `drWord (s, x, y) = 1` is inherited by every finite quotient `D_R ⧸ V`. -/
theorem drWord_mk_eq_one (V : OpenNormalSubgroup DRT) :
    drWord (QuotientGroup.mk' V.toSubgroup (drGens 0)) (QuotientGroup.mk' V.toSubgroup (drGens 1))
      (QuotientGroup.mk' V.toSubgroup (drGens 2)) = 1 := by
  have h := map_drWord (QuotientGroup.mk' V.toSubgroup) (drGens 0) (drGens 1) (drGens 2)
  simp only [drGens_zero, drGens_one, drGens_two] at h ⊢
  rw [← h, dr_relation, map_one]

/-! ## The obstruction homomorphism and its injectivity -/

/-- Normalize a 2-cochain at `(1,1)` by subtracting the constant `κ (1,1)`. -/
noncomputable def normalizeCochain (κ : DRT × DRT → ZMod 2) : DRT × DRT → ZMod 2 :=
  κ - fun _ => κ (1, 1)

private theorem normalizeCochain_add (κ κ' : DRT × DRT → ZMod 2) :
    normalizeCochain (κ + κ') = normalizeCochain κ + normalizeCochain κ' := by
  funext p; simp only [normalizeCochain, Pi.add_apply, Pi.sub_apply]; abel

section Obstruction

variable [DistribMulAction DRT (ZMod 2)] [ContinuousSMul DRT (ZMod 2)]

variable (htriv : ∀ (x : DRT) (m : ZMod 2), x • m = m)
include htriv

omit [ContinuousSMul DRT (ZMod 2)] in
/-- A constant 2-cochain is a continuous coboundary. -/
theorem const2_mem_B2 (v : ZMod 2) :
    (fun _ : DRT × DRT => v) ∈ B2 DRT (ZMod 2) := by
  rw [B2, AddSubgroup.mem_map]
  refine ⟨fun _ => v, continuous_const, ?_⟩
  funext p
  simp only [dOne, AddMonoidHom.coe_mk, ZeroHom.coe_mk, htriv]
  abel

omit [ContinuousSMul DRT (ZMod 2)] in
/-- The normalization of a continuous 2-cocycle factors through a finite quotient. -/
theorem nonempty_levelFactor_normalize (φ : Z2 DRT (ZMod 2)) :
    Nonempty (DRLevelFactor (normalizeCochain φ.1)) := by
  have hφcont : Continuous φ.1 := (mem_Z2_iff.mp φ.2).1
  have hφcoc := (mem_Z2_iff.mp φ.2).2
  have hcont : Continuous (normalizeCochain φ.1) := hφcont.sub continuous_const
  have hnorm : normalizeCochain φ.1 (1, 1) = 0 := by
    simp only [normalizeCochain, Pi.sub_apply, sub_self]
  have hcoc : ∀ a b c, normalizeCochain φ.1 (a, b) + normalizeCochain φ.1 (a * b, c)
      = normalizeCochain φ.1 (a, b * c) + normalizeCochain φ.1 (b, c) := by
    intro a b c
    have hz := hφcoc a b c
    rw [htriv] at hz
    simp only [normalizeCochain, Pi.sub_apply]
    linear_combination -hz
  obtain ⟨V, c, hfact⟩ := exists_twoCocycle_factor_DR (normalizeCochain φ.1) hcont hnorm hcoc
  exact ⟨V, c, hfact⟩

/-- The per-cocycle obstruction. -/
noncomputable def obsFun_DR (φ : Z2 DRT (ZMod 2)) : ZMod 2 :=
  (nonempty_levelFactor_normalize htriv φ).some.obs

omit [ContinuousSMul DRT (ZMod 2)] in
/-- `obsFun_DR` may be computed at *any* factorization of the normalization. -/
theorem obsFun_DR_eq (φ : Z2 DRT (ZMod 2)) (F : DRLevelFactor (normalizeCochain φ.1)) :
    obsFun_DR htriv φ = F.obs :=
  DRLevelFactor.obs_congr _ F

omit [ContinuousSMul DRT (ZMod 2)] in
/-- **Additivity of the obstruction.** -/
theorem obsFun_DR_add (φ ψ : Z2 DRT (ZMod 2)) :
    obsFun_DR htriv (φ + ψ) = obsFun_DR htriv φ + obsFun_DR htriv ψ := by
  set Fφ := (nonempty_levelFactor_normalize htriv φ).some with hFφ
  set Fψ := (nonempty_levelFactor_normalize htriv ψ).some with hFψ
  set W : OpenNormalSubgroup DRT := Fφ.V ⊓ Fψ.V with hWdef
  have hW1 : W.toSubgroup ≤ Fφ.V.toSubgroup := fun x hx => SetLike.le_def.mp inf_le_left hx
  have hW2 : W.toSubgroup ≤ Fψ.V.toSubgroup := fun x hx => SetLike.le_def.mp inf_le_right hx
  set pφ : (DRT ⧸ W.toSubgroup) →* (DRT ⧸ Fφ.V.toSubgroup) :=
    QuotientGroup.map W.toSubgroup Fφ.V.toSubgroup (MonoidHom.id _)
      (by rw [Subgroup.comap_id]; exact hW1) with hpφdef
  set pψ : (DRT ⧸ W.toSubgroup) →* (DRT ⧸ Fψ.V.toSubgroup) :=
    QuotientGroup.map W.toSubgroup Fψ.V.toSubgroup (MonoidHom.id _)
      (by rw [Subgroup.comap_id]; exact hW2) with hpψdef
  have hpφ : pφ.comp (QuotientGroup.mk' W.toSubgroup) = QuotientGroup.mk' Fφ.V.toSubgroup := by
    ext g; rw [hpφdef, MonoidHom.comp_apply, QuotientGroup.map_mk']; rfl
  have hpψ : pψ.comp (QuotientGroup.mk' W.toSubgroup) = QuotientGroup.mk' Fψ.V.toSubgroup := by
    ext g; rw [hpψdef, MonoidHom.comp_apply, QuotientGroup.map_mk']; rfl
  have hFsum : obsFun_DR htriv (φ + ψ)
      = drRelZ (fun k => QuotientGroup.mk' W.toSubgroup (drGens k))
          (Fφ.c.comap pφ + Fψ.c.comap pψ) := by
    refine obsFun_DR_eq htriv (φ + ψ) ⟨W, Fφ.c.comap pφ + Fψ.c.comap pψ, ?_⟩
    intro x y
    rw [TwoCocycle.add_κ, TwoCocycle.comap_κ, TwoCocycle.comap_κ]
    have hex : ∀ (z : DRT), pφ (QuotientGroup.mk' W.toSubgroup z) = QuotientGroup.mk' Fφ.V.toSubgroup z :=
      fun z => by rw [← MonoidHom.comp_apply, hpφ]
    have hey : ∀ (z : DRT), pψ (QuotientGroup.mk' W.toSubgroup z) = QuotientGroup.mk' Fψ.V.toSubgroup z :=
      fun z => by rw [← MonoidHom.comp_apply, hpψ]
    rw [hex, hex, hey, hey, ← Fφ.hfact x y, ← Fψ.hfact x y]
    show normalizeCochain (φ.1 + ψ.1) (x, y) = normalizeCochain φ.1 (x, y) + normalizeCochain ψ.1 (x, y)
    rw [normalizeCochain_add, Pi.add_apply]
  rw [obsFun_DR_eq htriv φ Fφ, obsFun_DR_eq htriv ψ Fψ, hFsum,
    Fφ.obs_eq_comap W pφ hpφ, Fψ.obs_eq_comap W pψ hpψ, drRelZ_add]

/-- The **obstruction homomorphism** `Z²_cont(D_R, 𝔽₂) →+ 𝔽₂`. -/
noncomputable def obs_DR : Z2 DRT (ZMod 2) →+ ZMod 2 :=
  AddMonoidHom.mk' (obsFun_DR htriv) (obsFun_DR_add htriv)

/-! ### The obstruction kills coboundaries -/

omit [ContinuousSMul DRT (ZMod 2)] in
/-- **`obs` kills `B²`.**  A continuous coboundary normalizes to `δ¹ψ'` (`ψ' 1 = 0`), which factors
as `coboundaryCocycle λ`; its obstruction is `λ (drWord (s,x,y)) = λ 1 = 0` (the relation dies at the
level). -/
theorem obs_DR_B2_eq_zero :
    (B2 DRT (ZMod 2)).addSubgroupOf (Z2 DRT (ZMod 2)) ≤ (obs_DR htriv).ker := by
  intro x hx
  rw [AddMonoidHom.mem_ker]
  rw [AddSubgroup.mem_addSubgroupOf, B2, AddSubgroup.mem_map] at hx
  obtain ⟨ψ, hψc, hψeq⟩ := hx
  have hψcont : Continuous ψ := mem_C1_iff.mp hψc
  have hx1 : x.1 = dOne DRT (ZMod 2) ψ := hψeq.symm
  set ψ' : DRT → ZMod 2 := ψ - fun _ => ψ 1 with hψ'def
  obtain ⟨V, lam, hlamfact⟩ := exists_oneCochain_factor_DR ψ' (hψcont.sub continuous_const)
  have hlam1 : lam 1 = 0 := by
    have h := hlamfact 1
    rw [show QuotientGroup.mk' V.toSubgroup (1 : DRT) = 1 from map_one _] at h
    rw [← h]; simp [hψ'def]
  have hfact : ∀ p q : DRT, normalizeCochain x.1 (p, q)
      = (coboundaryCocycle lam hlam1).κ (QuotientGroup.mk' V.toSubgroup p)
          (QuotientGroup.mk' V.toSubgroup q) := by
    intro p q
    show normalizeCochain x.1 (p, q)
      = lam (QuotientGroup.mk' V.toSubgroup p) + lam (QuotientGroup.mk' V.toSubgroup q)
        + lam (QuotientGroup.mk' V.toSubgroup p * QuotientGroup.mk' V.toSubgroup q)
    rw [← map_mul (QuotientGroup.mk' V.toSubgroup) p q, ← hlamfact p, ← hlamfact q,
      ← hlamfact (p * q), hx1]
    simp only [normalizeCochain, Pi.sub_apply, hψ'def, dOne, AddMonoidHom.coe_mk,
      ZeroHom.coe_mk, htriv, mul_one, CharTwo.sub_eq_add]
    abel
  have hobs : obsFun_DR htriv x = 0 := by
    rw [obsFun_DR_eq htriv x ⟨V, coboundaryCocycle lam hlam1, hfact⟩]
    show drRelZ (fun k => QuotientGroup.mk' V.toSubgroup (drGens k)) (coboundaryCocycle lam hlam1) = 0
    rw [drRelZ_coboundary]
    have : drWord (QuotientGroup.mk' V.toSubgroup (drGens 0)) (QuotientGroup.mk' V.toSubgroup (drGens 1))
        (QuotientGroup.mk' V.toSubgroup (drGens 2)) = 1 := drWord_mk_eq_one V
    rw [this, hlam1]
  exact hobs

/-! ### The injectivity keystone: `obs = 0` ⟹ coboundary (via a `drLiftHom` section) -/

omit [ContinuousSMul DRT (ZMod 2)] in
/-- **Coboundary extraction.**  A continuous hom `sect : D_R → CentExt c` splitting the level
projection (`(sect g).base = mk_V g`) makes the level cocycle a continuous coboundary `δ¹ (fib ∘
sect)`. -/
theorem cocycle_mem_B2_DR {V : OpenNormalSubgroup DRT} {c : TwoCocycle (DRT ⧸ V.toSubgroup)}
    (sect : ContinuousMonoidHom DR (CentExt c)) :
    (fun p : DRT × DRT => c.κ (sect p.1).base (sect p.2).base) ∈ B2 DRT (ZMod 2) := by
  have key : ∀ x y z : ZMod 2, y - (x + y + z) + x = z := by decide
  refine ⟨fun g => (sect g).fib, ?_, ?_⟩
  · rw [SetLike.mem_coe, mem_C1_iff]
    exact (continuous_of_discreteTopology (f := CentExt.fib)).comp sect.continuous_toFun
  · funext p
    obtain ⟨g, h⟩ := p
    show g • (sect h).fib - (sect (g * h)).fib + (sect g).fib = c.κ (sect g).base (sect h).base
    rw [htriv, map_mul sect, CentExt.mul_fib]
    exact key (sect g).fib (sect h).fib (c.κ (sect g).base (sect h).base)

omit [ContinuousSMul DRT (ZMod 2)] in
/-- **Injectivity keystone.**  A continuous 2-cocycle with `obs = 0` is a continuous coboundary: the
relator dies exactly at the factoring level, so `drLiftHom` builds a splitting section and the level
cocycle is `δ¹ (fib ∘ section)`. -/
theorem obs_DR_ker_le :
    (obs_DR htriv).ker ≤ (B2 DRT (ZMod 2)).addSubgroupOf (Z2 DRT (ZMod 2)) := by
  intro φ hφ
  rw [AddMonoidHom.mem_ker] at hφ
  rw [AddSubgroup.mem_addSubgroupOf]
  set F := (nonempty_levelFactor_normalize htriv φ).some with hF
  have hobs0 : F.obs = 0 := by rw [← obsFun_DR_eq htriv φ F]; exact hφ
  -- build the splitting section from `drLiftHom`
  set V := F.V with hV
  set c := F.c with hc
  set m : Fin 3 → CentExt c := fun k => drLift (fun j => QuotientGroup.mk' V.toSubgroup (drGens j)) c k
    with hm
  have hrel : drWord (m 0) (m 1) (m 2) = 1 := by
    apply CentExt.ext
    · show (drWord (m 0) (m 1) (m 2)).base = (1 : CentExt c).base
      rw [drRelZ_base]; exact drWord_mk_eq_one V
    · show (drWord (m 0) (m 1) (m 2)).fib = (1 : CentExt c).fib
      exact hobs0
  set sect : ContinuousMonoidHom DR (CentExt c) := drLiftHom (isProP_CentExt c) m hrel with hsect
  -- `sect` splits the level projection
  haveI : DiscreteTopology (DRT ⧸ V.toSubgroup) :=
    Subgroup.instDiscreteTopologyQuotientOfSeparatelyContinuousMul V.toOpenSubgroup
  have hbase : ∀ g : DRT, (sect g).base = QuotientGroup.mk' V.toSubgroup g := by
    have hcomp : (⟨CentExt.proj c, continuous_of_discreteTopology⟩ :
        ContinuousMonoidHom (CentExt c) (DRT ⧸ V.toSubgroup)).comp sect = quotientMk V.toSubgroup := by
      refine dr_hom_ext _ _ ?_ ?_ ?_
      · show CentExt.proj c (sect drS) = quotientMk V.toSubgroup drS
        rw [hsect, drLiftHom_S]; rfl
      · show CentExt.proj c (sect drX) = quotientMk V.toSubgroup drX
        rw [hsect, drLiftHom_X]; rfl
      · show CentExt.proj c (sect drY) = quotientMk V.toSubgroup drY
        rw [hsect, drLiftHom_Y]; rfl
    intro g
    exact DFunLike.congr_fun hcomp g
  -- the normalization is the level cocycle pulled back through the section
  have hnB2 : normalizeCochain φ.1 ∈ B2 DRT (ZMod 2) := by
    have heq : normalizeCochain φ.1 = fun p : DRT × DRT => c.κ (sect p.1).base (sect p.2).base := by
      funext p
      rw [hbase, hbase]
      exact F.hfact p.1 p.2
    rw [heq]
    exact cocycle_mem_B2_DR htriv sect
  have hconst : φ.1 = normalizeCochain φ.1 + fun _ => φ.1 (1, 1) := by
    funext p; simp only [normalizeCochain, Pi.sub_apply, Pi.add_apply]; abel
  rw [hconst]
  exact AddSubgroup.add_mem _ hnB2 (const2_mem_B2 htriv (φ.1 (1, 1)))

/-! ### Assembly: the descended obstruction and its injectivity -/

/-- The **descended obstruction** `H²(D_R, 𝔽₂) →+ 𝔽₂`. -/
noncomputable def obsH2_DR : H2 DRT (ZMod 2) →+ ZMod 2 :=
  QuotientAddGroup.lift _ (obs_DR htriv) (fun _ h => obs_DR_B2_eq_zero htriv h)

omit [ContinuousSMul DRT (ZMod 2)] in
/-- **`obsH2_DR` is injective** — the `#H² ≤ 2` half. -/
theorem obsH2_DR_injective : Function.Injective (obsH2_DR htriv) := by
  rw [injective_iff_map_eq_zero]
  intro a
  induction a using QuotientAddGroup.induction_on with | H φ =>
  intro ha
  exact (QuotientAddGroup.eq_zero_iff φ).mpr (obs_DR_ker_le htriv (AddMonoidHom.mem_ker.mpr ha))

/-! ### The factoring bridge: computing `obsH2_DR` at any finite quotient -/

omit [ContinuousSMul DRT (ZMod 2)] in
/-- **The obstruction at an explicit factoring.**  For a continuous 2-cocycle `φ` factoring through
a finite quotient `L` as `φ (g, h) = c.κ (ρ g) (ρ h)`, the obstruction is the single-relator
obstruction `drRelZ (ρ ∘ (s, x, y)) c` — the hook the Gram matrix of `GQ2/Roe/DRH2.lean` consumes. -/
theorem obsH2_DR_eq_of_factor {L : Type} [Group L] [Finite L]
    (φ : Z2 DRT (ZMod 2)) (ρ : DRT →* L) (c : TwoCocycle L)
    (hfact : ∀ g h : DRT, φ.1 (g, h) = c.κ (ρ g) (ρ h)) :
    obsH2_DR htriv (H2mk DRT (ZMod 2) φ) = drRelZ (fun k => ρ (drGens k)) c := by
  -- `φ` is already normalized: `φ (1,1) = c.κ 1 1 = 0`.
  have hone : φ.1 (1, 1) = 0 := by rw [hfact, map_one, c.norm]
  have hnorm : normalizeCochain φ.1 = φ.1 := by
    funext p; simp only [normalizeCochain, Pi.sub_apply, hone, sub_zero]
  set F := (nonempty_levelFactor_normalize htriv φ).some with hF
  have h1 : obsH2_DR htriv (H2mk DRT (ZMod 2) φ) = F.obs := rfl
  -- Both markings pull `c` (resp. `F.c`) back to the *same* cocycle on `D_R` itself, so no
  -- continuity of `ρ` is needed: the two factorizations agree pointwise through `hfact`.
  have hcc : F.c.comap (QuotientGroup.mk' F.V.toSubgroup) = c.comap ρ := by
    refine TwoCocycle.ext ?_
    funext g h
    rw [TwoCocycle.comap_κ, TwoCocycle.comap_κ, ← F.hfact g h, hnorm, hfact]
  rw [h1]
  show drRelZ (fun k => QuotientGroup.mk' F.V.toSubgroup (drGens k)) F.c = _
  rw [drRelZ_comap drGens F.c (QuotientGroup.mk' F.V.toSubgroup), drRelZ_comap drGens c ρ, hcc]

end Obstruction

end GQ2