The 𝔽₂-cover obstruction calculus and the

paper-faithful (140) reducer

Central 𝔽₂-covers enter the (140) analysis through one scalar invariant: whether a continuous hom f : Γ → C₀ lifts through the cover. This file builds that calculus and the (140) reducer consuming it:

• iotaB — the coboundary indicator ι_Γ on 2-cochains (0 iff the cochain is a continuous coboundary); additive on cocycles when #H²(Γ,𝔽₂) = 2 (iotaB_add — the only place the source's H²-size enters, threaded as hH2).

• pullCoc — pullback of a finite-group 2-cochain along f × f, with Z2/B2 membership lemmas (pullCoc_mem_Z2, pullCoc_coboundary_mem_B2).

• centralCover_lift_iff — for a central double cover equipped with a section of defect δ (s c · s d = z^{δ(c,d)} · s(cd) — centralCoverOfCocycle_exists_section supplies it for the phase covers): f lifts iff f^*δ ∈ B²(Γ,𝔽₂). This is the (141)-side liftability criterion and the s_Γ(ζ)-to-n_{Γ,0}(ζ) conversion.

• phaseSign/sum_phaseSign — the signed liftability count (141): Σ_ρ (±1) = 2·n_{Γ,0}(ζ) − e_Γ(C).

• phase140_of_phaseObstruction — the paper-faithful (140) reducer: unlike phase140_of_nonsingular (which routes through the Lin/κ_ρ/ε_ρ/N(κ,ε)-interpolation of lemma_8_5), this reducer consumes the per-ρ phase-obstruction identity

  2·|D_T| · #(central red_T image)(ρ) = |V| · (|V| + G0 · Σ_ζ phaseSign(ζ, ρ))

  — exactly the shape the paper's proof of Prop 8.9 produces from (126)+(135) before summing over ρ (pp. 42–43), with the phase family and μ-slot as in the c1s-repaired engine (μ_total = |V|·μ₀). The master-count file (GQ2/VLiftCount.lean) supplies hMobst.

Everything is source-generic; all std-3.

The coboundary indicator ι_Γ

noncomputable def GQ2.SectionEight.iotaB {Γ : Type} [Group Γ] [TopologicalSpace Γ] [DistribMulAction Γ (ZMod 2)] (φ : Γ × Γ → ZMod 2) : ZMod 2

The coboundary indicator ι_Γ on 𝔽₂-valued 2-cochains: 0 iff the cochain is a continuous coboundary. On cocycles, with #H²(Γ,𝔽₂) = 2, this is the composite of the class map with the unique isomorphism H²(Γ,𝔽₂) ≅ 𝔽₂ (iotaB_add).

Equations

• GQ2.SectionEight.iotaB φ = if φ ∈ GQ2.ContCoh.B2 Γ (ZMod 2) then 0 else 1

theorem GQ2.SectionEight.iotaB_eq_zero_iff {Γ : Type} [Group Γ] [TopologicalSpace Γ] [DistribMulAction Γ (ZMod 2)] {φ : Γ × Γ → ZMod 2} : iotaB φ = 0 ↔ φ ∈ ContCoh.B2 Γ (ZMod 2)

theorem GQ2.SectionEight.iotaB_of_mem_B2 {Γ : Type} [Group Γ] [TopologicalSpace Γ] [DistribMulAction Γ (ZMod 2)] {φ : Γ × Γ → ZMod 2} (h : φ ∈ ContCoh.B2 Γ (ZMod 2)) : iotaB φ = 0

theorem GQ2.SectionEight.H2mk_eq_zero_iff {Γ : Type} [Group Γ] [TopologicalSpace Γ] [DistribMulAction Γ (ZMod 2)] (φ : ↥(ContCoh.Z2 Γ (ZMod 2))) : (ContCoh.H2mk Γ (ZMod 2)) φ = 0 ↔ ↑φ ∈ ContCoh.B2 Γ (ZMod 2)

The H²-class of a cocycle vanishes iff its underlying cochain is a coboundary.

theorem GQ2.SectionEight.iotaB_add {Γ : Type} [Group Γ] [TopologicalSpace Γ] [DistribMulAction Γ (ZMod 2)] (hH2 : Nat.card (ContCoh.H2 Γ (ZMod 2)) = 2) {φ ψ : Γ × Γ → ZMod 2} (hφ : φ ∈ ContCoh.Z2 Γ (ZMod 2)) (hψ : ψ ∈ ContCoh.Z2 Γ (ZMod 2)) : iotaB (φ + ψ) = iotaB φ + iotaB ψ

Additivity of ι_Γ on cocycles (#H²(Γ,𝔽₂) = 2): the indicator is the unique isomorphism H² ≅ 𝔽₂ composed with the class map, hence additive. The hH2 hypothesis is the per-source #H²(Γ,𝔽₂) = 2 count (lemma_8_2-adjacent; threaded to the d6e residue list).

Pullback of finite-group 2-cochains

def GQ2.SectionEight.pullCoc {Γ C0 : Type} (f : Γ → C0) (δ : C0 × C0 → ZMod 2) : Γ × Γ → ZMod 2

Pullback of a finite-group 2-cochain along (the square of) a map.

Equations

• GQ2.SectionEight.pullCoc f δ p = δ (f p.1, f p.2)

theorem GQ2.SectionEight.pullCoc_mem_Z2 {Γ : Type} [Group Γ] [TopologicalSpace Γ] [DistribMulAction Γ (ZMod 2)] {C0 : Type} [Group C0] [TopologicalSpace C0] [DiscreteTopology C0] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (f : Γ →ₜ* C0) {δ : C0 × C0 → ZMod 2} (hcoc : ∀ (g h k : C0), δ (h, k) + δ (g, h * k) = δ (g * h, k) + δ (g, h)) : pullCoc (⇑f) δ ∈ ContCoh.Z2 Γ (ZMod 2)

The pullback of a raw 2-cocycle along a continuous hom is a continuous 2-cocycle.

Central-cover z-power calculus and the lifting criterion

theorem GQ2.SectionEight.CentralCover.p_z_eq_one {Y0 : Type} [Group Y0] [Finite Y0] (CC : CentralCover Y0) : CC.p CC.z = 1

p z = 1 for any central double cover.

theorem GQ2.SectionEight.CentralCover.ker_dichotomy {Y0 : Type} [Group Y0] [Finite Y0] (CC : CentralCover Y0) {x : CC.cover} (hx : x ∈ CC.p.ker) : x = 1 ∨ x = CC.z

Kernel dichotomy for a central double cover: ker p = {1, z}.

theorem GQ2.SectionEight.CentralCover.z_pow_comm {Y0 : Type} [Group Y0] [Finite Y0] (CC : CentralCover Y0) (n : ℕ) (x : CC.cover) : CC.z ^ n * x = x * CC.z ^ n

z-powers are central.

theorem GQ2.SectionEight.CentralCover.z_pow_val_inj {Y0 : Type} [Group Y0] [Finite Y0] (CC : CentralCover Y0) {a b : ZMod 2} (h : CC.z ^ a.val = CC.z ^ b.val) : a = b

𝔽₂-exponents of z are determined: z^{a} = z^{b} → a = b.

theorem GQ2.SectionEight.centralCover_lift_iff {Γ : Type} [Group Γ] [TopologicalSpace Γ] [DistribMulAction Γ (ZMod 2)] {Y0 : Type} [Group Y0] [TopologicalSpace Y0] [DiscreteTopology Y0] [Finite Y0] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (CC : CentralCover Y0) (s : Y0 → CC.cover) (hs : ∀ (c : Y0), CC.p (s c) = c) (δ : Y0 × Y0 → ZMod 2) (hdef : ∀ (c d : Y0), s c * s d = CC.z ^ (δ (c, d)).val * s (c * d)) (f : Γ →ₜ* Y0) : (∃ (g : Γ →ₜ* CC.cover), ∀ (γ : Γ), CC.p (g γ) = f γ) ↔ pullCoc (⇑f) δ ∈ ContCoh.B2 Γ (ZMod 2)

The central-cover lifting criterion: for a central double cover of Y₀ equipped with a set-section of multiplication defect δ (s c · s d = z^{δ(c,d)} · s(cd)), a continuous hom f : Γ → Y₀ lifts through the cover iff the pulled-back defect f^*δ is a continuous coboundary. (centralCoverOfCocycle_exists_section supplies such a section, with defect the defining cocycle, for the twisted-product phase covers.)

theorem GQ2.SectionEight.sign_iotaB_pullCoc_eq_lift_sign {Γ : Type} [Group Γ] [TopologicalSpace Γ] [DistribMulAction Γ (ZMod 2)] {Y0 : Type} [Group Y0] [TopologicalSpace Y0] [DiscreteTopology Y0] [Finite Y0] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (δ : Y0 × Y0 → ZMod 2) (hcoc : ∀ (g h k : Y0), δ (h, k) + δ (g, h * k) = δ (g * h, k) + δ (g, h)) (hl : ∀ (c : Y0), δ (1, c) = 0) (hr : ∀ (c : Y0), δ (c, 1) = 0) (f : Γ →ₜ* Y0) : sign (iotaB (pullCoc (⇑f) δ)) = if ∃ (g : Γ →ₜ* (AffineTLift.centralCoverOfCocycle δ hcoc hl hr).cover), ∀ (γ : Γ), (AffineTLift.centralCoverOfCocycle δ hcoc hl hr).p (g γ) = f γ then 1 else -1

The sign bridge (the Prop. 8.9 assembly supply): for the twisted-product phase cover of a normalized raw 2-cocycle δ, the master count's ±1 (sign ι_Γ(f^*δ)) IS the signed liftability through the cover — phaseSign's if-form at f. Composes centralCover_lift_iff with the canonical section of centralCoverOfCocycle and ι_Γ's defining dichotomy.

The signed phase-liftability count (141)

noncomputable def GQ2.SectionEight.phaseSign {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (Cζ : CentralCover RF.YC) (ρ : BoundaryLifts b F RF.TC) : ℤ

The signed liftability of a lower exact-image map through a phase cover: +1 when a lift exists, −1 otherwise — (141)'s summand (−1)^{ι_Γ(ρ^*ζ)} in predicate form.

Equations

• GQ2.SectionEight.phaseSign RF b F Cζ ρ = if ∃ (g : Γ →ₜ* Cζ.cover), ∀ (γ : Γ), Cζ.p (g γ) = ↑↑ρ γ then 1 else -1

theorem GQ2.SectionEight.sum_phaseSign {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) [Fintype (BoundaryLifts b F RF.TC)] (Cζ : CentralCover RF.YC) : ∑ᶠ (ρ : BoundaryLifts b F RF.TC), phaseSign RF b F Cζ ρ = 2 * ↑(RF.nPhase b F Cζ) - ↑(exactImageCount b F RF.TC)

(141): the signed liftability sum over the lower exact-image maps is 2·n_{Γ,0}(ζ) − e_Γ(C).

The paper-faithful (140) reducer

theorem GQ2.SectionEight.phase140_of_phaseObstruction {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] [DistribMulAction Γ (ZMod 2)] [ContinuousSMul Γ (ZMod 2)] {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) (μ₀ : ℕ) (G0 : ℤ) (DT : Type) [Fintype DT] (phase : DT → CentralCover RF.YC) (l : RF.DR) (h : l ≠ RF.zeroDR) (D : RadicalCoverData RF.YB) (hD : D.M = RF.MB) (hC : D.C = RF.scalarCover l h) (Dsc : AffineTLift.Descent D) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) [Fintype (BoundaryLifts b F RF.TC)] (cardV : ℕ) (hWV : cardV = Nat.card ↥RF.MB / Nat.card ↥RF.TBsub) (hμ : ∀ (ρ : BoundaryLifts b F RF.TC), Nat.card (CentralObstruction.TCocycle D (RF.rhoPrime b F D hD ρ)) = μ₀) (hMobst : ∀ (ρ : BoundaryLifts b F RF.TC), 2 * ↑(Nat.card DT) * ↑(Nat.card ↑(Set.range fun (f : { f : MLifts D (RF.rhoPrime b F D hD ρ) // MLifts.Central D f }) => AffineTLift.redT (RF.rhoPrime b F D hD ρ) ↑f)) = ↑cardV * (↑cardV + G0 * ∑ᶠ (ζ : DT), phaseSign RF b F (phase ζ) ρ)) : 2 * ↑(Nat.card DT) * ↑(RF.zBC b F l h) = ↑(cardV * μ₀) * (↑(Nat.card ↥RF.MB / Nat.card ↥RF.TBsub) * ↑(exactImageCount b F RF.TC) + G0 * ∑ᶠ (ζ : DT), (2 * ↑(RF.nPhase b F (phase ζ)) - ↑(exactImageCount b F RF.TC)))

The (140) display from per-ρ phase-obstruction data (the Prop. 8.9 assembly, paper-faithful form). Unlike phase140_of_nonsingular (which interpolates through lemma_8_5's Lin/κ_ρ/ε_ρ/N(κ,ε) data), this reducer consumes the identity the paper's Prop 8.9 proof actually produces per lower map (pp. 42–43, (126)+(135) before the ρ-sum):

2·|D_T| · #(central red_T image)(ρ) = |V| · (|V| + G0 · Σ_ζ (±1)_{ζ,ρ}),

with (±1)_{ζ,ρ} = phaseSign (phase ζ) ρ the signed liftability through the phase cover. Combined with the T-torsor factoring (zBC_eq_mu_mul_reductionCount, needing μ-independence hμ) and the (141) count (sum_phaseSign), the boxed (140) follows with the c1s multiplicity slot μ_total = |V|·μ₀. The master-count file supplies hMobst.

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

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