The central-obstruction engine for Lemma 8.6

The Γ-generic machinery behind the §8 half-torsor count, faithful to the paper's proof of Lemma 8.6:

• kernel-sign calculus zsign on the central double cover (ker p = {1, z} ≅ 𝔽₂);
• the commutator/square ledger of the cover over M (x̃ỹ = ỹx̃·z^{B_q}, from hq);
• the linear complement s(T) to ⟨z⟩ in p⁻¹(T) (TComplement, exists since p⁻¹(T) is elementary abelian — q|_T = 0 and T ⊆ rad B_q);
• the edge cocycle edge b t of (128) — the conjugation defect of the complement — with its crossed-cocycle law, additivity, M-invariance, and the descent construction (not_noDescent_of_edge_trivial: a crossed trivialization of the edge produces the normal complement, refuting NoDescent);
• the twist involution on MLifts by continuous crossed T-cocycles (TCocycle, twist);
• the scalar obstruction class ob f ∈ H²(Γ, 𝔽₂) (Central f ↔ ob f = 0) and the exact variation formula (129): ob (twist u f) = ob f + [varCoc u], with the variation class independent of f;
• the assembled abstract half-count half_count: a twist with nonzero variation class swaps Central and its complement, so exactly half the M-lifts are central.

The per-source content — producing the nonzero-variation twist from NoDescent (B6 for the local source, 5.15/5.16 for the candidate source) — lives in the downstream local and Γ_A half-torsor proofs. No axioms enter here; everything is std-3.

The kernel-sign calculus: ker p = {1, z} ≅ 𝔽₂

noncomputable def GQ2.SectionEight.CentralObstruction.zsign {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (x : D.C.cover) : ZMod 2

The z-logarithm on the cover: 0 at 1, 1 elsewhere — meaningful on ker p = {1,z}.

Equations

• GQ2.SectionEight.CentralObstruction.zsign D x = if x = 1 then 0 else 1

@[simp]

theorem GQ2.SectionEight.CentralObstruction.zsign_one {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) : zsign D 1 = 0

theorem GQ2.SectionEight.CentralObstruction.zsign_z {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) : zsign D D.C.z = 1

theorem GQ2.SectionEight.CentralObstruction.z_mem_ker {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) : D.C.z ∈ D.C.p.ker

z is in the kernel.

theorem GQ2.SectionEight.CentralObstruction.p_z_eq_one {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) : D.C.p D.C.z = 1

p z = 1.

theorem GQ2.SectionEight.CentralObstruction.ker_cases {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) {x : D.C.cover} (hx : x ∈ D.C.p.ker) : x = 1 ∨ x = D.C.z

The kernel of the cover has exactly the two elements 1 and z.

theorem GQ2.SectionEight.CentralObstruction.z_pow_zsign {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) {x : D.C.cover} (hx : x ∈ D.C.p.ker) : D.C.z ^ (zsign D x).val = x

Reconstruction: a kernel element is z to its sign.

theorem GQ2.SectionEight.CentralObstruction.zsign_mul {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) {x y : D.C.cover} (hx : x ∈ D.C.p.ker) (hy : y ∈ D.C.p.ker) : zsign D (x * y) = zsign D x + zsign D y

zsign is additive on the kernel.

theorem GQ2.SectionEight.CentralObstruction.ker_inv_eq {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) {x : D.C.cover} (hx : x ∈ D.C.p.ker) : x⁻¹ = x

Kernel elements are their own inverses.

theorem GQ2.SectionEight.CentralObstruction.ker_comm {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) {d : D.C.cover} (hd : d ∈ D.C.p.ker) (w : D.C.cover) : d * w = w * d

Kernel elements are central.

theorem GQ2.SectionEight.CentralObstruction.zsign_z_pow {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (a : ZMod 2) : zsign D (D.C.z ^ a.val) = a

zsign of a z-power: zsign (z^(a.val)) = a.

The cover ledger over M: squares and commutators

theorem GQ2.SectionEight.CentralObstruction.comm_mem_ker {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) {x y : D.C.cover} (hx : D.C.p x ∈ D.M) (hy : D.C.p y ∈ D.M) : y⁻¹ * x⁻¹ * y * x ∈ D.C.p.ker

Commutator membership: the commutator of two lifts of M-elements is in the kernel.

theorem GQ2.SectionEight.CentralObstruction.mul_comm_z {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) {x y : D.C.cover} (hx : D.C.p x ∈ D.M) (hy : D.C.p y ∈ D.M) : y * x = x * y * D.C.z ^ (polarMul D.q (fun (a b : ↥D.M) => ⟨↑a * ↑b, ⋯⟩) ⟨D.C.p x, hx⟩ ⟨D.C.p y, hy⟩).val

The commutator/polar ledger (extraspecial-style): for lifts x, y of M-elements, y·x = x·y·z^{B_q(px, py)}. Derived from hq (the square form) alone.

The preimage of T and the linear complement s(T)

theorem GQ2.SectionEight.CentralObstruction.sq_eq_one_of_p_mem_T {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) {x : D.C.cover} (hx : D.C.p x ∈ D.T) : x * x = 1

Lifts of T-elements square to 1 (q|_T = 0).

theorem GQ2.SectionEight.CentralObstruction.comm_of_p_mem_T {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) {x y : D.C.cover} (hx : D.C.p x ∈ D.T) (hy : D.C.p y ∈ D.M) : y * x = x * y

Lifts of T-elements commute with all lifts of M-elements (T ⊆ rad B_q).

structure GQ2.SectionEight.CentralObstruction.TComplement {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) : Type

The linear complement datum: a homomorphic section s : T → B̃ of p over T. (The paper's complement s(T) to ⟨z⟩ in the elementary abelian p⁻¹(T); z ∉ range s is automatic since s 1 = 1 ≠ z and p (s t) = t ≠ 1 = p z otherwise.)

• s : ↥D.T →* D.C.cover

  The section homomorphism.

• sect (t : ↥D.T) : D.C.p (self.s t) = ↑t

  It sections p over T.

theorem GQ2.SectionEight.CentralObstruction.tComplement_nonempty {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) : Nonempty (TComplement D)

A linear complement exists: split off z by an 𝔽₂-functional on the elementary abelian p⁻¹(T).

The edge cocycle of (128)

theorem GQ2.SectionEight.CentralObstruction.conj_mem_T {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (b : Bg) (t : ↥D.T) : b * ↑t * b⁻¹ ∈ D.T

Conjugates of T-elements stay in T (T normal).

noncomputable def GQ2.SectionEight.CentralObstruction.edge {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (S : TComplement D) (b : Bg) (t : ↥D.T) : ZMod 2

The edge cocycle ε(b)(t) of (128): the z-defect of conjugating the complement, x·s(t)·x⁻¹ = s(btb⁻¹)·z^{ε(b)(t)} for any lift x of b. (Defined with the pinned surjInv lift; lift-independence is edge_spec.)

Equations

• GQ2.SectionEight.CentralObstruction.edge D S b t = GQ2.SectionEight.CentralObstruction.zsign D (Function.surjInv ⋯ b * S.s t * (Function.surjInv ⋯ b)⁻¹ * (S.s ⟨b * ↑t * b⁻¹, ⋯⟩)⁻¹)

theorem GQ2.SectionEight.CentralObstruction.edge_defect_mem_ker {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (S : TComplement D) {x : D.C.cover} {b : Bg} (hx : D.C.p x = b) (t : ↥D.T) : x * S.s t * x⁻¹ * (S.s ⟨b * ↑t * b⁻¹, ⋯⟩)⁻¹ ∈ D.C.p.ker

The conjugation defect is a kernel element.

theorem GQ2.SectionEight.CentralObstruction.edge_spec {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (S : TComplement D) {x : D.C.cover} {b : Bg} (hx : D.C.p x = b) (t : ↥D.T) : x * S.s t * x⁻¹ = S.s ⟨b * ↑t * b⁻¹, ⋯⟩ * D.C.z ^ (edge D S b t).val

The edge specification: for ANY lift x of b, x·s(t)·x⁻¹ = s(btb⁻¹)·z^{ε(b)(t)}. (Two lifts differ by the central z, which cancels in conjugation, so the defect is lift-independent.)

theorem GQ2.SectionEight.CentralObstruction.edge_eq_of_spec {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (S : TComplement D) {x : D.C.cover} {b : Bg} (hx : D.C.p x = b) (t : ↥D.T) (a : ZMod 2) (h : x * S.s t * x⁻¹ = S.s ⟨b * ↑t * b⁻¹, ⋯⟩ * D.C.z ^ a.val) : edge D S b t = a

Read the edge off from any lift-conjugation identity.

theorem GQ2.SectionEight.CentralObstruction.edge_mul {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (S : TComplement D) (b₁ b₂ : Bg) (t : ↥D.T) : edge D S (b₁ * b₂) t = edge D S b₁ ⟨b₂ * ↑t * b₂⁻¹, ⋯⟩ + edge D S b₂ t

Edge crossed-cocycle law: ε(b₁b₂)(t) = ε(b₁)(b₂tb₂⁻¹) + ε(b₂)(t).

theorem GQ2.SectionEight.CentralObstruction.edge_add {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (S : TComplement D) (b : Bg) (t t' : ↥D.T) : edge D S b (t * t') = edge D S b t + edge D S b t'

Edge additivity in t (the complement is linear).

theorem GQ2.SectionEight.CentralObstruction.conj_M_fix {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (m : Bg) (hm : m ∈ D.M) (t : ↥D.T) : ⟨m * ↑t * m⁻¹, ⋯⟩ = t

The value of s on a conjugate-by-M argument is unchanged (M centralizes T).

theorem GQ2.SectionEight.CentralObstruction.edge_M_zero {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (S : TComplement D) (m : Bg) (hm : m ∈ D.M) (t : ↥D.T) : edge D S m t = 0

M has zero edge: conjugation by (lifts of) M-elements fixes the complement pointwise (T ⊆ rad B_q).

theorem GQ2.SectionEight.CentralObstruction.edge_coset {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (S : TComplement D) (b m : Bg) (hm : m ∈ D.M) (t : ↥D.T) : edge D S (b * m) t = edge D S b t

Edge M-coset invariance: ε(bm) = ε(b) for m ∈ M.

theorem GQ2.SectionEight.CentralObstruction.not_noDescent_of_edge_trivial {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (S : TComplement D) (ℓ : ↥D.T → ZMod 2) (hadd : ∀ (t t' : ↥D.T), ℓ (t * t') = ℓ t + ℓ t') (h : ∀ (b : Bg) (t : ↥D.T), edge D S b t = ℓ ⟨b * ↑t * b⁻¹, ⋯⟩ + ℓ t) : ¬D.NoDescent

The descent construction: a crossed trivialization ε(b)(t) = ℓ(btb⁻¹) + ℓ(t) of the edge by an additive ℓ yields a normal complement to p⁻¹(T) missing z — refuting NoDescent. (Alter the complement by z^ℓ; the new complement is conjugation-stable.)

The quotient edge (M-coset descent of the edge cocycle)

noncomputable def GQ2.SectionEight.CentralObstruction.edgeQ {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (S : TComplement D) (c : Bg ⧸ D.M) (t : ↥D.T) : ZMod 2

The edge evaluated at the canonical representative of an Bg⧸M-class (well-defined by edge_coset).

Equations

• GQ2.SectionEight.CentralObstruction.edgeQ D S c t = GQ2.SectionEight.CentralObstruction.edge D S (Quotient.out c) t

theorem GQ2.SectionEight.CentralObstruction.edgeQ_eq {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) (S : TComplement D) (c : Bg ⧸ D.M) {b : Bg} (hb : ↑b = c) (t : ↥D.T) : edgeQ D S c t = edge D S b t

edgeQ computes at any representative.

The Γ-layer: twisting, obstruction, and the variation formula (129)

structure GQ2.SectionEight.CentralObstruction.TCocycle {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) : Type

A continuous crossed T-valued 1-cocycle over ρ (the paper's u ∈ Z¹_{Γ,ρ}(T)): u(γδ) = u(γ)·(b·u(δ)·b⁻¹) for any representative b of ρ(γ) (well-defined since M — hence its subgroup image in the conjugation — acts trivially on the abelian T).

• u : Γ → Bg

  The underlying function, valued in T.

• mem (γ : Γ) : self.u γ ∈ D.T
• cont : Continuous self.u
• crossed (γ δ : Γ) (b : Bg) : ↑b = ρ γ → self.u (γ * δ) = self.u γ * (b * self.u δ * b⁻¹)

theorem GQ2.SectionEight.CentralObstruction.TCocycle.u_one {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) (u : TCocycle D ρ) : u.u 1 = 1

noncomputable def GQ2.SectionEight.CentralObstruction.twist {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] [DiscreteTopology Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) (u : TCocycle D ρ) (f : MLifts D ρ) : MLifts D ρ

The twist of an M-lift by a crossed T-cocycle: (u·f)(γ) = u(γ)·f(γ).

Equations

• GQ2.SectionEight.CentralObstruction.twist D ρ u f = ⟨{ toMonoidHom := MonoidHom.mk' (fun (γ : Γ) => u.u γ * ↑f γ) ⋯, continuous_toFun := ⋯ }, ⋯⟩

theorem GQ2.SectionEight.CentralObstruction.twist_twist {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] [DiscreteTopology Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) (u : TCocycle D ρ) (f : MLifts D ρ) : twist D ρ u (twist D ρ u f) = f

Twisting is an involution (T has exponent 2).

The scalar obstruction class

noncomputable def GQ2.SectionEight.CentralObstruction.obCocOf {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) {Γ : Type} [Group Γ] (F : Γ → D.C.cover) : Γ × Γ → ZMod 2

The obstruction 2-cochain of a lift family F : Γ → B̃.

Equations

• GQ2.SectionEight.CentralObstruction.obCocOf D F gd = GQ2.SectionEight.CentralObstruction.zsign D (F gd.1 * F gd.2 * (F (gd.1 * gd.2))⁻¹)

noncomputable def GQ2.SectionEight.CentralObstruction.liftFam {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) (f : MLifts D ρ) : Γ → D.C.cover

The canonical lift family of an M-lift (pinned via surjInv).

Equations

• GQ2.SectionEight.CentralObstruction.liftFam D ρ f γ = Function.surjInv ⋯ (↑f γ)

theorem GQ2.SectionEight.CentralObstruction.liftFam_p {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) (f : MLifts D ρ) (γ : Γ) : D.C.p (liftFam D ρ f γ) = ↑f γ

theorem GQ2.SectionEight.CentralObstruction.liftFam_cont {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] [DiscreteTopology Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) (f : MLifts D ρ) : Continuous (liftFam D ρ f)

theorem GQ2.SectionEight.CentralObstruction.obDefect_mem_ker {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) {F : Γ → D.C.cover} {f : MLifts D ρ} (hF : ∀ (γ : Γ), D.C.p (F γ) = ↑f γ) (γ δ : Γ) : F γ * F δ * (F (γ * δ))⁻¹ ∈ D.C.p.ker

Section defects of a lift family lie in the kernel.

theorem GQ2.SectionEight.CentralObstruction.obCocOf_mem_Z2 {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) [DistribMulAction Γ (ZMod 2)] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) {F : Γ → D.C.cover} (hFc : Continuous F) {f : MLifts D ρ} (hF : ∀ (γ : Γ), D.C.p (F γ) = ↑f γ) : obCocOf D F ∈ ContCoh.Z2 Γ (ZMod 2)

The obstruction cochain of a (continuous) lift family is a continuous 2-cocycle.

noncomputable def GQ2.SectionEight.CentralObstruction.ob {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] [DiscreteTopology Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) [DistribMulAction Γ (ZMod 2)] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (f : MLifts D ρ) : ContCoh.H2 Γ (ZMod 2)

The obstruction class ob(f) ∈ H²(Γ, 𝔽₂) of an M-lift: the class of the section defect of (any) continuous lift family through the cover.

Equations

• GQ2.SectionEight.CentralObstruction.ob D ρ htriv f = (GQ2.ContCoh.H2mk Γ (ZMod 2)) ⟨GQ2.SectionEight.CentralObstruction.obCocOf D (GQ2.SectionEight.CentralObstruction.liftFam D ρ f), ⋯⟩

theorem GQ2.SectionEight.CentralObstruction.obCocOf_diff {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) {f : MLifts D ρ} {F F' : Γ → D.C.cover} (hF : ∀ (γ : Γ), D.C.p (F γ) = ↑f γ) (hF' : ∀ (γ : Γ), D.C.p (F' γ) = ↑f γ) (γ δ : Γ) : obCocOf D F (γ, δ) = obCocOf D F' (γ, δ) + (zsign D (F γ * (F' γ)⁻¹) + zsign D (F δ * (F' δ)⁻¹) + zsign D (F (γ * δ) * (F' (γ * δ))⁻¹))

Lift-family difference formula: two lift families of the same M-lift have obstruction cochains differing by the explicit coboundary data of c(γ) = zsign(F γ·F'γ⁻¹).

theorem GQ2.SectionEight.CentralObstruction.ob_eq_of_liftFam {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] [DiscreteTopology Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) [DistribMulAction Γ (ZMod 2)] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (f : MLifts D ρ) {F : Γ → D.C.cover} (hFc : Continuous F) (hFp : ∀ (γ : Γ), D.C.p (F γ) = ↑f γ) : ob D ρ htriv f = (ContCoh.H2mk Γ (ZMod 2)) ⟨obCocOf D F, ⋯⟩

The obstruction class is lift-family independent.

theorem GQ2.SectionEight.CentralObstruction.discreteTopology_quotient {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] [DiscreteTopology Bg] : DiscreteTopology (Bg ⧸ D.M)

The quotient of a discrete group is discrete.

theorem GQ2.SectionEight.CentralObstruction.central_iff_ob_eq_zero {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] [DiscreteTopology Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) [DistribMulAction Γ (ZMod 2)] (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (f : MLifts D ρ) : MLifts.Central D f ↔ ob D ρ htriv f = 0

The central relation is the vanishing of the obstruction class: f lifts through the cover iff ob f = 0.

The variation class of a twist (the (129) cup term)

noncomputable def GQ2.SectionEight.CentralObstruction.varCoc {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) (S : TComplement D) (u : TCocycle D ρ) : Γ × Γ → ZMod 2

The variation 2-cochain of a crossed T-cocycle: the (129) cup term (γ, δ) ↦ ε̄(ρ(γ))(u(δ)) — independent of any M-lift.

Equations

• GQ2.SectionEight.CentralObstruction.varCoc D ρ S u gd = GQ2.SectionEight.CentralObstruction.edgeQ D S (ρ gd.1) ⟨u.u gd.2, ⋯⟩

theorem GQ2.SectionEight.CentralObstruction.varCoc_mem_Z2 {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] [DiscreteTopology Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) [DistribMulAction Γ (ZMod 2)] (S : TComplement D) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (u : TCocycle D ρ) : varCoc D ρ S u ∈ ContCoh.Z2 Γ (ZMod 2)

The variation cochain is a continuous 2-cocycle.

theorem GQ2.SectionEight.CentralObstruction.ob_twist {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] [DiscreteTopology Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) [DistribMulAction Γ (ZMod 2)] (S : TComplement D) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (u : TCocycle D ρ) (f : MLifts D ρ) : ob D ρ htriv (twist D ρ u f) = ob D ρ htriv f + (ContCoh.H2mk Γ (ZMod 2)) ⟨varCoc D ρ S u, ⋯⟩

The variation formula (129), class level: twisting shifts the obstruction class by the (f-independent) variation class of u.

The abstract half-count

theorem GQ2.SectionEight.CentralObstruction.two_mul_card_of_swap {X : Type} [Finite X] (σ : X → X) (hσ : Function.Involutive σ) (P : X → Prop) (hswap : ∀ (x : X), P (σ x) ↔ ¬P x) : 2 * Nat.card { x : X // P x } = Nat.card X

Flip counting: an involution swapping a predicate with its complement forces the predicate to hold on exactly half of a finite type.

theorem GQ2.SectionEight.CentralObstruction.half_count {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) [TopologicalSpace Bg] [DiscreteTopology Bg] {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] (ρ : Γ →ₜ* Bg ⧸ D.M) [DistribMulAction Γ (ZMod 2)] [Finite (MLifts D ρ)] (S : TComplement D) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (u : TCocycle D ρ) (hvar : (ContCoh.H2mk Γ (ZMod 2)) ⟨varCoc D ρ S u, ⋯⟩ ≠ 0) (hcard : Nat.card (ContCoh.H2 Γ (ZMod 2)) = 2) : 2 * Nat.card { f : MLifts D ρ // MLifts.Central D f } = Nat.card (MLifts D ρ)

The engine's half-count (Lemma 8.6, count clause, source-generic): given a crossed T-cocycle whose variation class is nonzero, and #H²(Γ,𝔽₂) = 2, exactly half of the M-lifts satisfy the central relation.

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

• Lemma 8.6 = ⟦lem-radicaledge⟧