Lemma 8.6, local source: the B6 half-torsor count

Closes SectionEight.lemma_8_6_local through the central-obstruction framework engine (GQ2/CentralObstruction.lean): given NoDescent, the twist producing the flip involution is manufactured from B6's perfect (1,1) pairing (GQ2.tateDuality 2 |>.perfect11) applied to the T-conjugation module.

The bridge to the local half-torsor proof uses the shifted edge φ(γ)(s) := ε̄(ρ(γ))(γ⁻¹•s) is an exact Z¹(G_ℚ₂, (A_T)^{μ₂∨})-cocycle, and on the nose cup11Fun (muDualPairing) φ w = muNTwoEquiv.symm ∘ varCoc u_w for the crossed T-cocycle u_w corresponding to w ∈ Z¹(A_T). NoDescent forbids [φ] = 0 (a coboundary constant λ would trivialize the edge by ρ-surjectivity — not_noDescent_of_edge_trivial), so perfectness yields w with nonzero cup class, hence nonzero variation class, and the engine's half_count finishes with #H²(G_ℚ₂, 𝔽₂) = 2 (card_H2_zmod2_eq_two).

Hypotheses (per the lemma_8_2_local/lemma_8_3 amendment precedents): G_ℚ₂ compact + totally disconnected (instance binders) and topologically finitely generated (hfg, the B1-shaped input supplied upstream) — these finitize MLifts.

Axioms: B6 (tateDuality) and B7 (through card_H2_zmod2_eq_two's finiteness).

theorem GQ2.SectionEight.RadicalEdgeLocal.conj_eq_of_mk_eq {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) {b b' : Bg} (h : ↑b = ↑b') (t : ↥D.T) : b * ↑t * b⁻¹ = b' * ↑t * b'⁻¹

Conjugation of T-elements only depends on the M-coset of the conjugator (M centralizes T).

@[reducible]

def GQ2.SectionEight.RadicalEdgeLocal.tCommGroup {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) : CommGroup ↥D.T

The commutative group structure on ↥T (T ≤ M abelian).

Equations

• GQ2.SectionEight.RadicalEdgeLocal.tCommGroup D = { toGroup := inferInstance, mul_comm := ⋯ }

The B6 twist construction, staged

exists_good_twist below is assembled from private helpers, one per stage: the ρ-conjugation module (outConj/rhoConj/conjModule), the shifted-edge dual cocycle (shiftedEdge*), its class nonvanishing (shiftedEdge_class_ne_zero), the B6 pairing partner (exists_pairing_partner), and the crossed-cocycle packaging (twistCocycle) with its cup ↔ variation bridge (cup11Fun_shiftedEdge_eq_varCoc).

theorem GQ2.SectionEight.RadicalEdgeLocal.half_torsor_local {Bg : Type} [Group Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg] (D : RadicalCoverData Bg) [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hfg : ∃ (s : Finset AbsGalQ2), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hedge : D.NoDescent) (ρ : AbsGalQ2 →ₜ* Bg ⧸ D.M) (hρ : Function.Surjective ⇑ρ) : 2 * Nat.card { f : MLifts D ρ // MLifts.Central D f } = Nat.card (MLifts D ρ)

Lemma 8.6, local source, engine form — the half-torsor count for G_ℚ₂ from NoDescent, via B6. Consumed by SectionEight.lemma_8_6_local.

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

• Lemma 8.6 = ⟦lem-radicaledge⟧