§8 R-stage obstruction module — Option-A construction

Builds the obstruction datum obs/hmB/hobs/hfib consumed by GQ2.SectionEight.stageR136_ofObstruction (GQ2/RStageObstruction.lean), from the Option-A compatibility structure RCoverData: the datum, absent from the bare RecursionFrame + Enrichment, that each scalar cover p_λ = (scalarCover l).p really is a quotient of the single radical extension Y ↠ B = Y/R — a hom family coverMap_λ : Y →* (scalarCover l).cover with p_λ ∘ coverMap_λ = π_B.

The compatibility datum remains a separate structure rather than a field of Enrichment, keeping the generic recursion frame independent of this particular cover realization. This file proves the obstruction bridge, fibre count, separation-based lift construction, and the resulting stageR136_ofRSepData interface consumed by the recursion splice.

noncomputable def GQ2.SectionEight.cardTwoLinEquiv {M : Type} [AddCommGroup M] [Module (ZMod 2) M] [Finite M] (hM : Nat.card M = 2) : M ≃ₗ[ZMod 2] ZMod 2

A finite 𝔽₂-module of cardinality 2 is ZMod 2 (linearly). Used to turn the scalar obstruction class homOb ∈ H²(Γ,𝔽₂) into an 𝔽₂ value once the source numeric #H²(Γ,𝔽₂) = 2 is available (prop_5_16/prop_5_15), so obs lands in D_Rᵛ.

Equations

• GQ2.SectionEight.cardTwoLinEquiv hM = (Module.finBasisOfFinrankEq (ZMod 2) M ⋯).equivFun.trans (LinearEquiv.funUnique (Fin 1) (ZMod 2) (ZMod 2))

def GQ2.SectionEight.trivialRCD {Bg : Type} [Group Bg] [Finite Bg] (C : CentralCover Bg) : RadicalCoverData Bg

The trivial (M = ⊥) radical-cover datum wrapping a bare central cover. All the GQ2.SectionEight.CentralObstruction engine (the kernel-sign calculus, the obstruction class, central_iff_ob_eq_zero) is stated over a RadicalCoverData, but its lifting content uses only the cover C; this reduces "a hom lifts through the central cover C" to the engine's MLifts.Central/ob at M = ⊥ (the square form is vacuous).

Equations

• GQ2.SectionEight.trivialRCD C = { C := C, M := ⊥, hM := ⋯, T := ⊥, hT := ⋯, hTM := ⋯, helem := ⋯, hcomm := ⋯, q := fun (x : ↥⊥) => 0, hq := ⋯, hrad := ⋯, hTzero := ⋯ }

Step 1 — the mB ⟺ ob bridge (via trivialRCD + central_iff_ob_eq_zero)

noncomputable def GQ2.SectionEight.trivialRho {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Bg : Type} [Group Bg] [TopologicalSpace Bg] (g : Γ →ₜ* Bg) : Γ →ₜ* Bg ⧸ ⊥

ρ = mk : Bg → Bg/⊥, precomposed with g; the lower map making g an M-lift of trivialRCD C (M = ⊥).

Equations

• GQ2.SectionEight.trivialRho g = { toMonoidHom := (QuotientGroup.mk' ⊥).comp g.toMonoidHom, continuous_toFun := ⋯ }

def GQ2.SectionEight.trivialMLift {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Bg : Type} [Group Bg] [TopologicalSpace Bg] [Finite Bg] (C : CentralCover Bg) (g : Γ →ₜ* Bg) : MLifts (trivialRCD C) (trivialRho g)

g itself as the M-lift of trivialRCD C over trivialRho g.

Equations

• GQ2.SectionEight.trivialMLift C g = ⟨g, ⋯⟩

noncomputable def GQ2.SectionEight.homOb {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [DistribMulAction Γ (ZMod 2)] {Bg : Type} [Group Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg] (C : CentralCover Bg) (g : Γ →ₜ* Bg) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) : ContCoh.H2 Γ (ZMod 2)

The scalar obstruction of a hom g through a bare central cover C — the CentralObstruction.ob of g viewed as an M = ⊥ lift.

Equations

• GQ2.SectionEight.homOb C g htriv = GQ2.SectionEight.CentralObstruction.ob (GQ2.SectionEight.trivialRCD C) (GQ2.SectionEight.trivialRho g) htriv (GQ2.SectionEight.trivialMLift C g)

theorem GQ2.SectionEight.liftsThroughCover_iff_homOb {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [DistribMulAction Γ (ZMod 2)] {Bg : Type} [Group Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg] (C : CentralCover Bg) (g : Γ →ₜ* Bg) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) : (∃ (h : Γ →ₜ* C.cover), ∀ (γ : Γ), C.p (h γ) = g γ) ↔ homOb C g htriv = 0

Step 1: g lifts through the central cover C iff its scalar obstruction vanishes.

structure GQ2.SectionEight.RCoverData {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) : Type

Option-A compatibility datum (the Prop. 8.9 assembly): the missing link between the frame's abstract scalar covers and the single radical extension Y ↠ B. For each nonzero scalar character λ, a homomorphism coverMap λ : Y →* (scalarCover λ).cover realizing scalarCover λ as a quotient of Y over B: p_λ ∘ coverMap λ = π_B. (This is the frame-level content of "p_λ is the pushout Y/ker λ ↠ Y/R", which the RecursionFrame/Enrichment document but do not carry.)

• coverMap (l : RF.DR) (h : l ≠ RF.zeroDR) : Y →* (RF.scalarCover l h).cover

  coverMap λ : Y →* B_λ, the realization of the scalar cover as a quotient of Y.

• coverMap_lifts (l : RF.DR) (h : l ≠ RF.zeroDR) : (RF.scalarCover l h).p.comp (self.coverMap l h) = RF.piB

  p_λ ∘ coverMap λ = π_B: the cover projects coverMap λ back to the B-stage map.

noncomputable def GQ2.SectionEight.RCoverData.coverMapC {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} (D : RCoverData RF) (l : RF.DR) (h : l ≠ RF.zeroDR) : Y →ₜ* (RF.scalarCover l h).cover

coverMap λ bundled as a ContinuousMonoidHom (free: Y is discrete).

Equations

• D.coverMapC l h = { toMonoidHom := D.coverMap l h, continuous_toFun := ⋯ }

theorem GQ2.SectionEight.RCoverData.lifts_scalarCover_of_liftB {Γ : Type} [Group Γ] [TopologicalSpace Γ] {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} (D : RCoverData RF) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (l : RF.DR) (h : l ≠ RF.zeroDR) (fY : BoundaryLifts b F T) : ∃ (g : Γ →ₜ* (RF.scalarCover l h).cover), ∀ (γ : Γ), (RF.scalarCover l h).p (g γ) = ↑↑(RF.liftB b F fY) γ

Easy hobs direction: if a B-stage boundary lift f lifts all the way to Y (is RF.liftB of some Y-lift F), then it lifts through every scalar cover p_λ — compose the Y-lift with coverMap λ. (The converse — "lifts through every p_λ ⟹ lifts to Y" — is the hard separation, using R-elementary-abelianness and the Frattini structure.)

Step 2 — the obstruction map obs, its linearity, and hmB

structure GQ2.SectionEight.RObstructionData {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) extends GQ2.SectionEight.RCoverData RF : Type 1

The R-stage obstruction datum (Option A, extended): the compat covers RCoverData together with the 𝔽₂-module realization of the scalar-character index D_R and the D_R ≃ (R^∨)^C pairing pair (a linear map D_Rmod → (R →+ 𝔽₂)), pinned to the covers by pair_coverMap (pair d = zsign ∘ coverMap_{λ} on R, for λ = toDR d ≠ 0). This is exactly what the concrete 𝒴-frame (the Prop. 8.9 assembly/d6) supplies; from it the obstruction map, its linearity, and hmB follow.

• coverMap (l : RF.DR) (h : l ≠ RF.zeroDR) : Y →* (RF.scalarCover l h).cover
• coverMap_lifts (l : RF.DR) (h : l ≠ RF.zeroDR) : (RF.scalarCover l h).p.comp (self.coverMap l h) = RF.piB
• DRmod : Type

  The 𝔽₂-module realization of the scalar-character index D_R.

• addCommGroup : AddCommGroup self.DRmod
• moduleZMod : Module (ZMod 2) self.DRmod
• finiteDRmod : Finite self.DRmod
• toDR : self.DRmod ≃ RF.DR

  D_Rmod ≃ D_R.

• h0 : self.toDR.symm RF.zeroDR = 0

  … sending 0 ↦ zeroDR.

• pair : self.DRmod →ₗ[ZMod 2] Additive ↥Blk.frattiniK →+ ZMod 2

  The D_R ≃ (R^∨)^C pairing: pair d is a 𝔽₂-functional on the radical R = Blk.frattiniK, linear in d.

• pair_coverMap (d : self.DRmod) (h : self.toDR d ≠ RF.zeroDR) (r : ↥Blk.frattiniK) : (self.pair d) (Additive.ofMul r) = CentralObstruction.zsign (trivialRCD (RF.scalarCover (self.toDR d) h)) ((self.coverMap (self.toDR d) h) ↑r)

  The pairing is zsign ∘ coverMap_λ on R (λ = toDR d ≠ 0): the scalar character d reads off the λ-cover's kernel sign of a radical element.

noncomputable def GQ2.SectionEight.slift {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (x : RF.YB) : Y

A set-theoretic section of π_B : Y ↠ B.

Equations

• GQ2.SectionEight.slift RF x = Function.surjInv ⋯ x

@[simp]

theorem GQ2.SectionEight.piB_slift {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (x : RF.YB) : RF.piB (slift RF x) = x

noncomputable def GQ2.SectionEight.rDefect {Γ : Type} [Group Γ] [TopologicalSpace Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (g : Γ →ₜ* RF.YB) (γ δ : Γ) : ↥Blk.frattiniK

The R-valued section defect of a B-stage map g : Γ → B for the single set-lift slift: Obs^s_g(γ,δ) = s(gγ)·s(gδ)·s(g(γδ))⁻¹ ∈ R = ker π_B.

Equations

• GQ2.SectionEight.rDefect RF g γ δ = ⟨GQ2.SectionEight.slift RF (g γ) * GQ2.SectionEight.slift RF (g δ) * (GQ2.SectionEight.slift RF (g (γ * δ)))⁻¹, ⋯⟩

@[implicit_reducible]

instance GQ2.SectionEight.instModuleH2 {Γ : Type} [Group Γ] [TopologicalSpace Γ] [DistribMulAction Γ (ZMod 2)] : Module (ZMod 2) (ContCoh.H2 Γ (ZMod 2))

H²(Γ,𝔽₂) is a ZMod 2-module (it has exponent 2, being a quotient of 𝔽₂-cochains).

Equations

• GQ2.SectionEight.instModuleH2 = AddCommGroup.zmodModule ⋯

noncomputable def GQ2.SectionEight.obsLiftFam {Γ : Type} [Group Γ] [TopologicalSpace Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (D : RObstructionData RF) (g : Γ →ₜ* RF.YB) (d : D.DRmod) (h : D.toDR d ≠ RF.zeroDR) : Γ → (RF.scalarCover (D.toDR d) h).cover

The lift family of g into the λ-cover built from the single set-section: x ↦ coverMap_λ (slift (g x)).

Equations

• GQ2.SectionEight.obsLiftFam RF D g d h x = (D.coverMap (D.toDR d) h) (GQ2.SectionEight.slift RF (g x))

theorem GQ2.SectionEight.obCocOf_obsLiftFam {Γ : Type} [Group Γ] [TopologicalSpace Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (D : RObstructionData RF) (g : Γ →ₜ* RF.YB) (d : D.DRmod) (h : D.toDR d ≠ RF.zeroDR) (γ δ : Γ) : CentralObstruction.obCocOf (trivialRCD (RF.scalarCover (D.toDR d) h)) (obsLiftFam RF D g d h) (γ, δ) = (D.pair d) (Additive.ofMul (rDefect RF g γ δ))

The pointwise obstruction identity: the obstruction cochain of the lift family equals pair d applied to the R-valued defect.

theorem GQ2.SectionEight.pairDefect_mem_Z2 {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) [DistribMulAction Γ (ZMod 2)] (D : RObstructionData RF) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (g : Γ →ₜ* RF.YB) (d : D.DRmod) (h : D.toDR d ≠ RF.zeroDR) : (fun (gd : Γ × Γ) => (D.pair d) (Additive.ofMul (rDefect RF g gd.1 gd.2))) ∈ ContCoh.Z2 Γ (ZMod 2)

theorem GQ2.SectionEight.homOb_eq_H2mk_pair {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) [DistribMulAction Γ (ZMod 2)] (D : RObstructionData RF) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (g : Γ →ₜ* RF.YB) (d : D.DRmod) (h : D.toDR d ≠ RF.zeroDR) : homOb (RF.scalarCover (D.toDR d) h) g htriv = (ContCoh.H2mk Γ (ZMod 2)) ⟨fun (gd : Γ × Γ) => (D.pair d) (Additive.ofMul (rDefect RF g gd.1 gd.2)), ⋯⟩

The connection (step 2 core): the scalar obstruction homOb of g through the λ-cover is the class of pair d ∘ rDefect — so it is H2mk of a cochain linear in d.

theorem GQ2.SectionEight.pairDefect_mem_Z2_all {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) [DistribMulAction Γ (ZMod 2)] (D : RObstructionData RF) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (g : Γ →ₜ* RF.YB) (d : D.DRmod) : (fun (gd : Γ × Γ) => (D.pair d) (Additive.ofMul (rDefect RF g gd.1 gd.2))) ∈ ContCoh.Z2 Γ (ZMod 2)

The obstruction cochain lies in Z² for every d (the toDR d = 0 case is the zero cochain, since pair 0 = 0).

noncomputable def GQ2.SectionEight.obsMapAdd {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) [DistribMulAction Γ (ZMod 2)] (D : RObstructionData RF) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (g : Γ →ₜ* RF.YB) : D.DRmod →+ ContCoh.H2 Γ (ZMod 2)

The obstruction map (additive) obsMapAdd g : D_Rmod →+ H²(Γ,𝔽₂), d ↦ [pair d ∘ rDefect] — additive in d (pair is linear), and equal to homOb(scalarCover λ) g at λ = toDR d ≠ 0 (homOb_eq_H2mk_pair).

Equations

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

noncomputable def GQ2.SectionEight.obs {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) [DistribMulAction Γ (ZMod 2)] (D : RObstructionData RF) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hcard : Nat.card (ContCoh.H2 Γ (ZMod 2)) = 2) (g : Γ →ₜ* RF.YB) : D.DRmod →ₗ[ZMod 2] ZMod 2

The obstruction functional obs g : D_Rmod →ₗ 𝔽₂ = D_Rᵛ: compose the additive obsMapAdd with the linear iso H²(Γ,𝔽₂) ≃ 𝔽₂ (from the source numeric #H² = 2). Linearity in the scalar c ∈ 𝔽₂ is the two-value case split.

Equations

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

theorem GQ2.SectionEight.obsMapAdd_eq_homOb {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) [DistribMulAction Γ (ZMod 2)] (D : RObstructionData RF) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (g : Γ →ₜ* RF.YB) (d : D.DRmod) (h : D.toDR d ≠ RF.zeroDR) : (obsMapAdd RF D htriv g) d = homOb (RF.scalarCover (D.toDR d) h) g htriv

obsMapAdd g d is the scalar obstruction of g through the λ-cover (λ = toDR d ≠ 0).

theorem GQ2.SectionEight.obs_zero_iff_lifts {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) [DistribMulAction Γ (ZMod 2)] (D : RObstructionData RF) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hcard : Nat.card (ContCoh.H2 Γ (ZMod 2)) = 2) (g : Γ →ₜ* RF.YB) (d : D.DRmod) (h : D.toDR d ≠ RF.zeroDR) : (obs RF D htriv hcard g) d = 0 ↔ ∃ (gc : Γ →ₜ* (RF.scalarCover (D.toDR d) h).cover), ∀ (γ : Γ), (RF.scalarCover (D.toDR d) h).p (gc γ) = g γ

**obs g d = 0 ⟺ g lifts through the λ-cover** (λ = toDR d ≠ 0): the hmB` pointwise identity.

theorem GQ2.SectionEight.obs_zero_iff_pairClass_zero {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) [DistribMulAction Γ (ZMod 2)] (D : RObstructionData RF) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hcard : Nat.card (ContCoh.H2 Γ (ZMod 2)) = 2) (g : Γ →ₜ* RF.YB) (d : D.DRmod) (h : D.toDR d ≠ RF.zeroDR) : (obs RF D htriv hcard g) d = 0 ↔ (ContCoh.H2mk Γ (ZMod 2)) ⟨fun (gd : Γ × Γ) => (D.pair d) (Additive.ofMul (rDefect RF g gd.1 gd.2)), ⋯⟩ = 0

obs at the 𝔽₂-cochain level (for the d6 separation discharge): obs g d = 0 iff the 𝔽₂-valued defect cochain pair d ∘ rDefect is a coboundary (H2mk = 0 in H²(Γ,𝔽₂)). This is the cochain-level face of obs_zero_iff_lifts; it pairs with homLift_of_split — from obs g = 0, d6 gets every pair d ∘ rDefect a coboundary, assembles the concrete R-splitting cochain (the (R^∨)^C-separation of H²(Γ,R)), and produces the hom lift.

theorem GQ2.SectionEight.hmB_holds {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) [DistribMulAction Γ (ZMod 2)] (D : RObstructionData RF) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hcard : Nat.card (ContCoh.H2 Γ (ZMod 2)) = 2) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (l : RF.DR) (h : l ≠ RF.zeroDR) : RF.mB b F l = Nat.card { f : BoundaryLifts b F RF.TB // (obs RF D htriv hcard ↑↑f) (D.toDR.symm l) = 0 }

hmB (step 2 payoff): m_{Γ,λ}(B) counts the B-lifts whose obstruction vanishes at the scalar character λ. Matches stageR136_ofObstruction's hmB hypothesis.

Step 5 — assemble: (136) modulo the two hard classical cores

theorem GQ2.SectionEight.stageR136_ofRObstructionData {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) [DistribMulAction Γ (ZMod 2)] (D : RObstructionData RF) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hcard : Nat.card (ContCoh.H2 Γ (ZMod 2)) = 2) (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (hsep : ∀ (g : BoundaryLifts b F RF.TB), obs RF D htriv hcard ↑↑g = 0 → ∃ (f : BoundaryLifts b F T), RF.liftB b F f = g) (hfib : ∀ (g : BoundaryLifts b F RF.TB), obs RF D htriv hcard ↑↑g = 0 → Nat.card { f : BoundaryLifts b F T // RF.liftB b F f = g } = RF.zR) : ↑(Nat.card RF.DR) * ↑(exactImageCount b F T) = ↑RF.zR * ∑ᶠ (l : RF.DR), (2 * ↑(RF.mB b F l) - ↑(exactImageCount b F RF.TB))

(136) from an RObstructionData, modulo the two hard classical cores. The obstruction map obs, its 𝔽₂-linearity, the counting identity hmB, and the easy direction of hobs (a lift to Y kills the obstruction) are all discharged here; the (136) display of Prop 8.9 then follows from stageR136_ofObstruction once the two remaining classical facts are supplied as hypotheses:

• hsep — the hard separation (the ⟹ of hobs): a B-stage boundary lift whose obstruction functional vanishes lifts all the way to Y. Classically this uses R-elementary-abelianness (lemma_7_2), the Frattini surjectivity eq_top_of_map_frattini_quotient_top, and the pushout link between the scalar covers and the single radical extension Y ↠ B.
• hfib — the z_R torsor count: every liftable fibre of RF.liftB has size z_R, the twisted-Z¹(Γ,R)-torsor count #Z¹(Γ,R) = z_R (the 5.15/5.16 numeric; B6/B7 enter here).

So the whole (136) numeric is reduced to exactly hsep + hfib, with the entire obstruction-theory machinery in between discharged.

Step 4 — hfib: the R-stage liftB-fibre is a Z¹(Γ, R)-torsor

The fibre of RF.liftB over a B-stage lift g is {f : Γ ↠ Y // π_B ∘ f = g} (framing is automatic, TB_head/TB_theta). Two such lifts f, f₀ differ by c γ := f γ · (f₀ γ)⁻¹ ∈ R (ker π_B = R), a crossed 1-cocycle for the f₀-conjugation action of Γ on R; conversely each cocycle twists f₀ to another fibre element (a homomorphism by the cocycle law, surjective by the Frattini argument eq_top_of_map_frattini_quotient_top, framed because R ≤ ker(π_Y, θ_Y)). So the fibre is a Z¹(Γ, R)-torsor; #Z¹(Γ, R) = z_R is the source numeric (5.15/5.16, d6).

theorem GQ2.SectionEight.R_le_ker_piY {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} : Blk.frattiniK ≤ T.piY.ker

R = Φ(K) ≤ K ≤ P ≤ L_Y = ker π_Y: R-twists preserve the head framing.

theorem GQ2.SectionEight.R_le_ker_thetaY {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (hE2 : ∀ (e : E), e ^ 2 = 1) : Blk.frattiniK ≤ T.thetaY.ker

R = Φ(K) ≤ ker θ_Y when E is elementary-2 (lemma_7_3): R-twists preserve the scalar framing. This is exactly the thm_4_2 decoration hypothesis (harmless downstream: §10 uses E = 0), and the one point flagged in docs/orchestration/p16d2-plan.md for the fibre count.

structure GQ2.SectionEight.RCocycle {Γ : Type} [Group Γ] [TopologicalSpace Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [TopologicalSpace Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (f₀ : Γ →ₜ* Y) : Type

The R-stage torsor group Z¹_{Γ,ρ}(R): continuous crossed 1-cocycles Γ → R = ker π_B for the f₀-conjugation action of Γ on R, f₀ a fixed reference Y-lift. (Multiplicative crossed-hom convention, as GQ2.SectionEight.TCocycle; the fibre of liftB over a liftable g is a torsor under this group with basepoint f₀.)

• u : Γ → Y

  The cocycle map.

• mem (γ : Γ) : self.u γ ∈ Blk.frattiniK

  Values lie in the radical R = ker π_B.

• cont : Continuous self.u

  Continuity.

• crossed (γ δ : Γ) : self.u (γ * δ) = self.u γ * (f₀ γ * self.u δ * (f₀ γ)⁻¹)

  The twisted (crossed) cocycle law u(γδ) = u γ · (f₀ γ · u δ · f₀ γ⁻¹).

theorem GQ2.SectionEight.RCocycle.ext {Γ : Type} [Group Γ] [TopologicalSpace Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [TopologicalSpace Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} {f₀ : Γ →ₜ* Y} {c c' : RCocycle RF f₀} (h : c.u = c'.u) : c = c'

Extensionality: only the underlying map matters.

theorem GQ2.SectionEight.RCocycle.u_one {Γ : Type} [Group Γ] [TopologicalSpace Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [TopologicalSpace Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} {f₀ : Γ →ₜ* Y} (c : RCocycle RF f₀) : c.u 1 = 1

Cocycles are normalized: u 1 = 1 (from crossed at (1,1), f₀ 1 = 1).

def GQ2.SectionEight.RCocycle.twistHom {Γ : Type} [Group Γ] [TopologicalSpace Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} {f₀ : Γ →ₜ* Y} (c : RCocycle RF f₀) : Γ →ₜ* Y

The reference lift f₀ twisted by a cocycle c: (c ⋆ f₀) γ = c.u γ · f₀ γ, a continuous homomorphism Γ → Y (homomorphism by crossed, continuous since Y is discrete).

Equations

• c.twistHom = { toFun := fun (γ : Γ) => c.u γ * f₀ γ, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

theorem GQ2.SectionEight.piB_eq_one_of_mem_R {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) {r : Y} (hr : r ∈ Blk.frattiniK) : RF.piB r = 1

π_B kills the radical: r ∈ R = ker π_B ⟹ π_B r = 1.

theorem GQ2.SectionEight.surj_of_piB_surj {Γ : Type} [Group Γ] [TopologicalSpace Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [TopologicalSpace Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) {φ : Γ →ₜ* Y} (hφ : Function.Surjective fun (γ : Γ) => RF.piB (φ γ)) : Function.Surjective ⇑φ

Frattini surjectivity (eq_top_of_map_frattini_quotient_top, R = Φ(K), K a 2-group): a continuous hom φ : Γ → Y whose π_B-composite is onto B is itself onto Y.

noncomputable def GQ2.SectionEight.fibreCocycleEquiv {Γ : Type} [Group Γ] [TopologicalSpace Γ] {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (hE2 : ∀ (e : E), e ^ 2 = 1) (g : BoundaryLifts b F RF.TB) (f₀ : BoundaryLifts b F T) (hf₀ : RF.liftB b F f₀ = g) : RCocycle RF ↑↑f₀ ≃ { f : BoundaryLifts b F T // RF.liftB b F f = g }

The R-stage fibre torsor (hfib core): fixing a lift f₀ of g, the fibre of RF.liftB over g is a torsor under RCocycle RF f₀.1.1 — every Y-lift of g is a unique cocycle-twist of f₀. The forward map lands in BoundaryLifts by Frattini surjectivity (surj_of_piB_surj) and R ≤ ker(π_Y, θ_Y) framing (needs hE2); the backward map reads off the R-valued difference f · f₀⁻¹.

Equations

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

theorem GQ2.SectionEight.hfib_holds {Γ : Type} [Group Γ] [TopologicalSpace Γ] {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (hE2 : ∀ (e : E), e ^ 2 = 1) (g : BoundaryLifts b F RF.TB) (f₀ : BoundaryLifts b F T) (hf₀ : RF.liftB b F f₀ = g) (hcount : Nat.card (RCocycle RF ↑↑f₀) = RF.zR) : Nat.card { f : BoundaryLifts b F T // RF.liftB b F f = g } = RF.zR

hfib (step 4 payoff): the liftB-fibre over a liftable g has size z_R, reduced to the source Z¹-count #RCocycle = z_R (the 5.15/5.16 numeric + card_DR, supplied by d6). The abstract torsor identification is fibreCocycleEquiv.

hsep wrapper: a bare homomorphism lift upgrades to a fibre element

theorem GQ2.SectionEight.liftB_fibre_nonempty_of_homLift {Γ : Type} [Group Γ] [TopologicalSpace Γ] {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (g : BoundaryLifts b F RF.TB) (φ : Γ →ₜ* Y) (hφ : ∀ (γ : Γ), RF.piB (φ γ) = ↑↑g γ) : ∃ (f : BoundaryLifts b F T), RF.liftB b F f = g

Frattini/framing wrapper for hsep: a bare homomorphism lift φ : Γ → Y of g (π_B ∘ φ = g) already lands in the liftB-fibre — it is surjective by surj_of_piB_surj (Frattini) and boundary-framed because the framing factors through π_B (TB_head/TB_theta). So hsep reduces to producing any homomorphism lift of g to Y; that existence is the separation core (obs g = 0 ⟹ the radical obstruction dies ⟹ glifts toY`).

theorem GQ2.SectionEight.homLift_of_split {Γ : Type} [Group Γ] [TopologicalSpace Γ] {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (g : Γ →ₜ* RF.YB) (c : Γ → ↥Blk.frattiniK) (hc : Continuous fun (γ : Γ) => ↑(c γ)) (hsplit : ∀ (γ δ : Γ), ↑(c (γ * δ)) = ↑(c γ) * (slift RF (g γ) * ↑(c δ) * (slift RF (g γ))⁻¹) * ↑(rDefect RF g γ δ)) : ∃ (φ : Γ →ₜ* Y), ∀ (γ : Γ), RF.piB (φ γ) = g γ

Constructive coboundary → hom lift (hsep interior): a continuous R-valued cochain c splitting the section defect rDefect (the twisted-coboundary equation) assembles the set-section slift ∘ g into a genuine continuous homomorphism φ γ = c γ · slift(g γ) lifting g. This is the abstractly-provable half of the separation: it turns "[rDefect] = 0 ∈ H²(Γ,R)" (a splitting cochain) into the hom lift that liftB_fibre_nonempty_of_homLift then upgrades to a fibre element. (slift is continuous because B = Y/R is discrete, so φ is genuinely continuous.)

theorem GQ2.SectionEight.stageR136_ofRSepData {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) [DistribMulAction Γ (ZMod 2)] (D : RObstructionData RF) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hcard : Nat.card (ContCoh.H2 Γ (ZMod 2)) = 2) (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hE2 : ∀ (e : E), e ^ 2 = 1) (hsep_hom : ∀ (g : BoundaryLifts b F RF.TB), obs RF D htriv hcard ↑↑g = 0 → ∃ (φ : Γ →ₜ* Y), ∀ (γ : Γ), RF.piB (φ γ) = ↑↑g γ) (hZcount : ∀ (f₀ : BoundaryLifts b F T), Nat.card (RCocycle RF ↑↑f₀) = RF.zR) : ↑(Nat.card RF.DR) * ↑(exactImageCount b F T) = ↑RF.zR * ∑ᶠ (l : RF.DR), (2 * ↑(RF.mB b F l) - ↑(exactImageCount b F RF.TB))

(136), fully discharged modulo the two irreducible concrete inputs (hsep_hom + hZcount). Every abstractly-provable ingredient is proven here — the obstruction map, hmB, the easy hobs, the hfib fibre-torsor, and hsep's Frattini/framing wrapper — so a caller (the concrete 𝒴-frame, the Prop. 8.9 assembly) supplies only:

• hsep_hom — the radical-obstruction separation: obs g = 0 ⟹ g has a homomorphism lift to Y. (Not provable in the bare abstract frame — it is the (R^∨)^C-detection of H²(Γ,R), a property of the concrete R + C-action. d6 discharges it, optionally via homLift_of_split.)
• hZcount — the source Z¹-count #RCocycle = z_R (5.15/5.16 numeric + card_DR).

and hE2 (E elementary-2, the thm_4_2 decoration hypothesis). This is the finish line of the abstract R-stage obstruction module: (136) reduced to exactly the source-arithmetic residues.

Paper-tag ledger (auto-generated by paperforge; do not edit)

• Prop 8.9 = ⟦thm-closedrecursion⟧ (= theorem 8.17 in current tex)