The affine T-lifting obstruction over the V-cocycle layer (Lemma 8.7, (131))

For a V-coordinate c ∈ Z¹_{Γ,ρ}(V) (c1a's VCocycle), when is g_c = qOfCocycle c the T-reduction of an actual — and central — M-lift? Following the paper's Lemma 8.7 (p. 41) at cocycle level:

• tDef — the T-valued defect of the pointwise lift γ ↦ mV(c γ)·uσ(ρ'γ) of g_c (the paper's "∂c + ρ^*e" in one piece; CountSections fixes the normalized set-sections).
• TCharC — the C-invariant 𝔽₂-character group D = (T^∨)^C (the paper's phase index).
• chiDef — the χ-pushforward χ_*(tDef c) ∈ Z²(Γ,𝔽₂) (chiDef_mem_Z2: C-invariance of χ kills the crossed twist), and betaChi χ c := ι_Γ(χ_* tDef c) — the χ-component of the T-lifting obstruction.
• TLiftable (131): c is the V-coordinate of an M-lift; tliftable_iff characterizes it — the easy direction (betaChi ≡ 0) is generic (betaChi_of_tliftable), the converse is the source-specific separation hsep (the (T^∨)^C ≅ H²_{Γ,ρ}(T)^∨ perfectness of cor. 5.17/5.16, threaded to the d6e residue list — the d6a hsep_hom idiom).
• betaXi — the scalar obstruction ι_Γ(g_c^*ξ) through the descended cover Q̃ = B̃/N (xi of the Prop. 8.9 assembly), with central_iff_betaXi: an M-lift over g_c is central iff betaXi c = 0 (the bridge from CentralObstruction.ob through mk_N).
• mem_centralImage_iff: c is the V-coordinate of a central M-lift iff TLiftable c ∧ betaXi c = 0 — the complete (131)-characterization the master count consumes.

Everything is source-generic std-3; the Γ-specific inputs (hsep, and the counting facts) are threaded as hypotheses.

The C-invariant character group D = (T^∨)^C

def GQ2.SectionEight.AffineTLift.TCharC {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) : AddSubgroup (↥D.T → ZMod 2)

The C-invariant 𝔽₂-characters of T (the paper's D = (T^∨)^C, p. 42): additive characters T → 𝔽₂ invariant under the full B-conjugation (which factors through C since M centralizes T). An additive subgroup of the function space.

Equations

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

instance GQ2.SectionEight.AffineTLift.instFiniteSubtypeForallMemSubgroupTZModOfNatNatAddSubgroupTCharC {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} : Finite ↥(TCharC D)

theorem GQ2.SectionEight.AffineTLift.TCharC.map_mul {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} (χ : ↥(TCharC D)) (t t' : ↥D.T) : ↑χ (t * t') = ↑χ t + ↑χ t'

theorem GQ2.SectionEight.AffineTLift.TCharC.map_one {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} (χ : ↥(TCharC D)) : ↑χ 1 = 0

theorem GQ2.SectionEight.AffineTLift.TCharC.map_inv {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} (χ : ↥(TCharC D)) (t : ↥D.T) : ↑χ t⁻¹ = ↑χ t

theorem GQ2.SectionEight.AffineTLift.TCharC.conj_invariant {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} (χ : ↥(TCharC D)) (bb : Bg) (t : ↥D.T) (h : bb * ↑t * bb⁻¹ ∈ D.T) : ↑χ ⟨bb * ↑t * bb⁻¹, h⟩ = ↑χ t

The section data and the pointwise B-lift

structure GQ2.SectionEight.AffineTLift.CountSections {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} (DD : DescData D) (σ : DD.C0 →* Bg ⧸ D.T) : Type

The section pair for the master count: normalized set-sections mV of descend and uσ of piT over the splitting σ.

• mV : DD.Vmod → ↥D.M

  A set-section of descend : M ↠ V.

• descend_mV (v : DD.Vmod) : DD.descend (self.mV v) = Multiplicative.ofAdd v
• mV_zero : self.mV 0 = 1
• uσ : DD.C0 → Bg

  A set-lift of σ : C₀ → Q through piT : B ↠ Q.

• piT_uσ (cc : DD.C0) : piT (self.uσ cc) = σ cc
• uσ_one : self.uσ 1 = 1

theorem GQ2.SectionEight.AffineTLift.countSections_exist {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} (DD : DescData D) (σ : DD.C0 →* Bg ⧸ D.T) : Nonempty (CountSections DD σ)

Section pairs exist (finite surjections; normalize at the identity).

noncomputable def GQ2.SectionEight.AffineTLift.fLift {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {ρ : Γ →ₜ* Bg ⧸ D.M} (c : VCocycle DD ρ) : Γ → Bg

The pointwise B-lift γ ↦ mV(c γ) · uσ(ρ'γ) of g_c = qOfCocycle c.

Equations

• GQ2.SectionEight.AffineTLift.fLift S c γ = ↑(S.mV (c.c γ)) * S.uσ ((GQ2.SectionEight.AffineTLift.rho0 DD ρ) γ)

theorem GQ2.SectionEight.AffineTLift.piT_mV {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) (v : DD.Vmod) : piT ↑(S.mV v) = (iV DD) (Multiplicative.ofAdd v)

mV covers iV through piT.

theorem GQ2.SectionEight.AffineTLift.fLift_mk {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (c : VCocycle DD ρ) (γ : Γ) : piT (fLift S c γ) = ↑(qOfCocycle DD ρ σ hσ c) γ

The pointwise lift lies over g_c through piT.

theorem GQ2.SectionEight.AffineTLift.fLift_defect_mem {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (c : VCocycle DD ρ) (γ δ : Γ) : fLift S c γ * fLift S c δ * (fLift S c (γ * δ))⁻¹ ∈ D.T

The defect of the pointwise lift lies in T.

noncomputable def GQ2.SectionEight.AffineTLift.tDef {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (c : VCocycle DD ρ) (p : Γ × Γ) : ↥D.T

The T-valued defect of the pointwise lift — the paper's ∂c + ρ^*e in one piece (Lemma 8.7's normalized-cocycle representative, pulled back along the graph of c).

Equations

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

noncomputable def GQ2.SectionEight.AffineTLift.chiDef {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (χ : ↥(TCharC D)) (c : VCocycle DD ρ) : Γ × Γ → ZMod 2

The χ-pushforward of the defect.

Equations

• GQ2.SectionEight.AffineTLift.chiDef S hσ χ c p = ↑χ (GQ2.SectionEight.AffineTLift.tDef S hσ c p)

theorem GQ2.SectionEight.AffineTLift.fLift_continuous {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {ρ : Γ →ₜ* Bg ⧸ D.M} (c : VCocycle DD ρ) : Continuous (fLift S c)

The pointwise lift is continuous (through the discrete Q × B/M, since V carries no topology — the iV-embedded continuity of c is inverted by injectivity).

theorem GQ2.SectionEight.AffineTLift.tDef_continuous {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) [IsTopologicalGroup Γ] (c : VCocycle DD ρ) : Continuous (tDef S hσ c)

The T-defect is continuous.

theorem GQ2.SectionEight.AffineTLift.chiDef_mem_Z2 {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) [IsTopologicalGroup Γ] [DistribMulAction Γ (ZMod 2)] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (χ : ↥(TCharC D)) (c : VCocycle DD ρ) : chiDef S hσ χ c ∈ ContCoh.Z2 Γ (ZMod 2)

The χ-pushforward of the defect is a continuous 2-cocycle: the nonabelian defect identity conjugates by fLift, and C-invariance of χ kills the conjugation.

noncomputable def GQ2.SectionEight.AffineTLift.betaChi {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) [DistribMulAction Γ (ZMod 2)] (χ : ↥(TCharC D)) (c : VCocycle DD ρ) : ZMod 2

The χ-component of the T-lifting obstruction: β_χ(c) := ι_Γ(χ_* tDef c).

Equations

• GQ2.SectionEight.AffineTLift.betaChi S hσ χ c = GQ2.SectionEight.iotaB (GQ2.SectionEight.AffineTLift.chiDef S hσ χ c)

(131): the T-liftability characterization

def GQ2.SectionEight.AffineTLift.TLiftable {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) (c : VCocycle DD ρ) : Prop

T-liftability of a V-coordinate: c is the T-reduction of an actual M-lift.

Equations

• GQ2.SectionEight.AffineTLift.TLiftable hσ c = ∃ (f : GQ2.SectionEight.MLifts D ρ), GQ2.SectionEight.AffineTLift.redTLift DD f = GQ2.SectionEight.AffineTLift.qOfCocycle DD ρ σ hσ c

theorem GQ2.SectionEight.AffineTLift.betaChi_of_tliftable {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) [DistribMulAction Γ (ZMod 2)] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) {c : VCocycle DD ρ} (hc : TLiftable hσ c) (χ : ↥(TCharC D)) : betaChi S hσ χ c = 0

The generic direction of (131): a liftable V-coordinate has vanishing χ-obstruction for every χ — the defect of the pointwise lift is a crossed coboundary, and χ (being C-invariant) sends it to a plain continuous coboundary.

The scalar obstruction through the descended cover

noncomputable def GQ2.SectionEight.AffineTLift.betaXi {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) [DistribMulAction Γ (ZMod 2)] (Dsc : Descent D) (c : VCocycle DD ρ) : ZMod 2

The scalar obstruction of a V-coordinate: ι_Γ(g_c^* ξ), the lifting obstruction of g_c through the descended central double cover Q̃ = B̃/N ↠ Q (defect cocycle ξ).

Equations

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

theorem GQ2.SectionEight.AffineTLift.ccZsign_inv {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} (Dsc : Descent D) {x : covQ Dsc} (hx : x ∈ (descP Dsc).ker) : ccZsign Dsc x⁻¹ = ccZsign Dsc x

ccZsign of an inverse kernel element.

theorem GQ2.SectionEight.AffineTLift.discreteTopology_covQ {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} (Dsc : Descent D) : DiscreteTopology (covQ Dsc)

The descended cover is discrete (quotient of the discrete cover).

theorem GQ2.SectionEight.AffineTLift.descP_lift_sign_mem_B2_iff {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] [DistribMulAction Γ (ZMod 2)] (Dsc : Descent D) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) {L1 L2 : Γ → covQ Dsc} (hL1 : Continuous L1) (hL2 : Continuous L2) (hover : ∀ (γ : Γ), (descP Dsc) (L1 γ) = (descP Dsc) (L2 γ)) (hmul : ∀ (γ δ : Γ), (descP Dsc) (L2 (γ * δ)) = (descP Dsc) (L2 γ) * (descP Dsc) (L2 δ)) : (fun (p : Γ × Γ) => ccZsign Dsc (L1 p.1 * L1 p.2 * (L1 (p.1 * p.2))⁻¹)) ∈ ContCoh.B2 Γ (ZMod 2) ↔ (fun (p : Γ × Γ) => ccZsign Dsc (L2 p.1 * L2 p.2 * (L2 (p.1 * p.2))⁻¹)) ∈ ContCoh.B2 Γ (ZMod 2)

Sign-defect well-definedness: two continuous pointwise lifts of the same continuous homomorphic map through descP have z̄-sign defect cochains differing by a continuous coboundary — hence the same B²-membership.

theorem GQ2.SectionEight.AffineTLift.ccZsign_mk_of_ker {Bg : Type} [Group Bg] [Finite Bg] {D : RadicalCoverData Bg} (Dsc : Descent D) {x : D.C.cover} (hx : x ∈ D.C.p.ker) : ccZsign Dsc ((QuotientGroup.mk' Dsc.N) x) = CentralObstruction.zsign D x

zsign on the cover kernel matches ccZsign after mk_N.

theorem GQ2.SectionEight.AffineTLift.central_iff_betaXi {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) [IsTopologicalGroup Γ] [DistribMulAction Γ (ZMod 2)] (Dsc : Descent D) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) {c : VCocycle DD ρ} {f : MLifts D ρ} (hf : redTLift DD f = qOfCocycle DD ρ σ hσ c) : MLifts.Central D f ↔ betaXi hσ Dsc c = 0

The scalar-obstruction bridge: an M-lift with T-reduction g_c is central iff the ξ-obstruction of g_c vanishes — CentralObstruction.ob computed through mk_N and transported to the s₀-section by sign-defect well-definedness.

theorem GQ2.SectionEight.AffineTLift.mem_centralImage_iff {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) [IsTopologicalGroup Γ] [DistribMulAction Γ (ZMod 2)] (Dsc : Descent D) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (c : VCocycle DD ρ) : (∃ (f : { f : MLifts D ρ // MLifts.Central D f }), cocycleOfQ DD ρ σ hσ (redTLift DD ↑f) = c) ↔ TLiftable hσ c ∧ betaXi hσ Dsc c = 0

The complete (131)-characterization (the Prop. 8.9 assembly): c is the V-coordinate of a central M-lift iff it is T-liftable and its scalar ξ-obstruction vanishes.

Group structure and finiteness of Z¹_{Γ,ρ}(V)

The χ-additivity of the T-obstruction and the base form Q⁰

@[implicit_reducible]

noncomputable instance GQ2.SectionEight.AffineTLift.instNegVCocycle {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {ρ : Γ →ₜ* Bg ⧸ D.M} : Neg (VCocycle DD ρ)

Negation on Z¹_{Γ,ρ}(V) is the identity (V has exponent 2).

Equations

• GQ2.SectionEight.AffineTLift.instNegVCocycle = { neg := fun (a : GQ2.SectionEight.AffineTLift.VCocycle DD ρ) => a }

@[implicit_reducible]

noncomputable instance GQ2.SectionEight.AffineTLift.instAddCommGroupVCocycle {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {ρ : Γ →ₜ* Bg ⧸ D.M} : AddCommGroup (VCocycle DD ρ)

Z¹_{Γ,ρ}(V) is an elementary abelian 2-group.

Equations

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

theorem GQ2.SectionEight.AffineTLift.finite_vcocycle {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {ρ : Γ →ₜ* Bg ⧸ D.M} (σ : DD.C0 →* Bg ⧸ D.T) (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) : Finite (VCocycle DD ρ)

theorem GQ2.SectionEight.AffineTLift.betaChi_zero_char {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) [DistribMulAction Γ (ZMod 2)] (c : VCocycle DD ρ) : betaChi S hσ 0 c = 0

β_χ vanishes at the zero character.

theorem GQ2.SectionEight.AffineTLift.betaChi_add_char {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) [IsTopologicalGroup Γ] [DistribMulAction Γ (ZMod 2)] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hH2 : Nat.card (ContCoh.H2 Γ (ZMod 2)) = 2) (χ ψ : ↥(TCharC D)) (c : VCocycle DD ρ) : betaChi S hσ (χ + ψ) c = betaChi S hσ χ c + betaChi S hσ ψ c

β_χ is additive in the character (ι_Γ-additivity, #H²(Γ,𝔽₂) = 2).

noncomputable def GQ2.SectionEight.AffineTLift.QZero {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] (DD : DescData D) (ρ : Γ →ₜ* Bg ⧸ D.M) [DistribMulAction Γ (ZMod 2)] (c : VCocycle DD ρ) : ZMod 2

The base determinant form Q⁰_{Γ,ρ} on Z¹_{Γ,ρ}(V): ι_Γ of the graph pullback of the fixed equivariant base class κ⁰ (eq. (62)/(133)-side).

Equations

• GQ2.SectionEight.AffineTLift.QZero DD ρ c = GQ2.SectionEight.iotaB (GQ2.graphPullback DD.dat (fun (γ : Γ) => (GQ2.SectionEight.AffineTLift.rho0 DD ρ) γ) c.c)

The master count

theorem GQ2.SectionEight.AffineTLift.card_range_redT_eq {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) : Nat.card ↑(Set.range fun (f : { f : MLifts D ρ // MLifts.Central D f }) => redT ρ ↑f) = Nat.card { c : VCocycle DD ρ // ∃ (f : { f : MLifts D ρ // MLifts.Central D f }), cocycleOfQ DD ρ σ hσ (redTLift DD ↑f) = c }

Transporting the central red_T-image count to the V-cocycle layer.

theorem GQ2.SectionEight.AffineTLift.two_mul_card_centralImage {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {DD : DescData D} {σ : DD.C0 →* Bg ⧸ D.T} (S : CountSections DD σ) {ρ : Γ →ₜ* Bg ⧸ D.M} (hσ : ∀ (cc : DD.C0), (piQbar DD) (σ cc) = cc) [IsTopologicalGroup Γ] [DistribMulAction Γ (ZMod 2)] (Dsc : Descent D) [CompactSpace Γ] [TotallyDisconnectedSpace Γ] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hH2 : Nat.card (ContCoh.H2 Γ (ZMod 2)) = 2) (hsep : ∀ (c : VCocycle DD ρ), (∀ (χ : ↥(TCharC D)), betaChi S hσ χ c = 0) → TLiftable hσ c) (haff : ∀ (χ : ↥(TCharC D)) (c c' : VCocycle DD ρ), betaChi S hσ χ (c + c') = betaChi S hσ χ c + betaChi S hσ χ c' + betaChi S hσ χ 0) (hpartial : ∀ (χ : ↥(TCharC D)), χ ≠ 0 → ∃ (c : VCocycle DD ρ), betaChi S hσ χ c ≠ betaChi S hσ χ 0) (Δ : ↥(TCharC D) → DD.C0 × DD.C0 → ZMod 2) (sh : ↥(TCharC D) → VCocycle DD ρ) (hkey : ∀ (χ : ↥(TCharC D)) (c : VCocycle DD ρ), betaChi S hσ χ c + betaXi hσ Dsc c = QZero DD ρ (c + sh χ) + iotaB (pullCoc (fun (γ : Γ) => (rho0 DD ρ) γ) (Δ χ))) (G0 : ℤ) (hZcard : Nat.card (VCocycle DD ρ) = Nat.card DD.Vmod * Nat.card DD.Vmod) (hGaussZ : ∑ᶠ (c : VCocycle DD ρ), sign (QZero DD ρ c) = ↑(Nat.card DD.Vmod) * G0) : 2 * ↑(Nat.card ↥(TCharC D)) * ↑(Nat.card ↑(Set.range fun (f : { f : MLifts D ρ // MLifts.Central D f }) => redT ρ ↑f)) = ↑(Nat.card DD.Vmod) * (↑(Nat.card DD.Vmod) + G0 * ∑ᶠ (χ : ↥(TCharC D)), sign (iotaB (pullCoc (fun (γ : Γ) => (rho0 DD ρ) γ) (Δ χ))))

The master count (the Prop. 8.9 assembly/c1c interface): the per-ρ phase-obstruction identity of the paper's Prop 8.9 proof, derived from the (131)-characterization by double Fourier expansion. The source-specific inputs are threaded: hH2 (#H²(Γ,𝔽₂) = 2), hsep (the (T^∨)^C-separation of the T-obstruction), haff/hpartial (affineness and nontriviality of the χ-components — ∂-surjectivity), hkey (the (135) completed square, from the keystone file), hZcard (#Z¹(V) = #V²) and hGaussZ (G(Q⁰) = #V·G0 — the source-Gauss transport).

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

• cor 5.17 = ⟦cor-adjointboundary⟧
• eq. (62) = ⟦eq-baseconnectingcochain⟧
• Lemma 8.7 = ⟦lem-affinelifting⟧
• Prop 8.9 = ⟦thm-closedrecursion⟧ (= theorem 8.17 in current tex)