The (136) R-stage for Γ = G_ℚ₂

Discharges the per-source residues of blockStageR136 (GQ2/BlockRStage.lean) at the local source Γ = AbsGalQ2, per the route of record (docs/orchestration/p16d6a-handoff.md §3): one prop_5_16-package invocation per twisted module, through its standalone pieces —

• hcard — #H²(G_ℚ₂, 𝔽₂) = 2 = card_H2_zmod2_eq_two (clause (iii));
• hZcount — #RCocycle = z_R = #R²·#D_R: the crossed-cocycle group is Z¹(G_ℚ₂, R_{f₀}) (multiplicative↔additive bridge, the Prop. 8.9 assembly TCocycle pattern), counted by card_Z1_eq (clause (ii)), with #fixedPts C (R^∨) = #D_R via the Y-invariance bridge (fixedPtsEquivRChar) + blockRChar_card;
• hsep_hom — the (R^∨)^C-separation: obs g = 0 forces every invariant character to kill the paired defect class (obs_zero_iff_pairClass_zero), the paired classes are the cup20-values of the R-valued defect class, bijective_cup20_dualEval (clause (vi)) forces [rDefect] = 0 in H²(G_ℚ₂, R_ρ), B²-extraction produces the continuous splitting cochain, and homLift_of_split assembles the lift.

The twisted action throughout is the C = Y/K-conjugation on R (well-defined by lemma_7_2's K-centrality, threaded as hRK), pulled back along the surjective lower map of the boundary lift (BoundaryLifts bundles surjectivity — this is why hsep_hom is supplied directly to blockStageR136 rather than through hsep_hom_of_splitCriterion, whose hsplit quantifies over arbitrary, possibly non-surjective g).

The lemma_7_2 outputs (hRK = R central in K, hR2 = R exponent 2) and hfg (t.f.g. of G_ℚ₂ — B1, reserved for the §9 induction) thread hypothesis-side to the assembly. Axioms here: std-3 + B6 + B7 (through card_Z1_eq/card_H2_zmod2_eq_two/ bijective_cup20_dualEval).

Main result: stageR136_local — the (136) identity for the block frame at the local source, the exact stageR136 field of the RecursionInputs bundle (the Prop. 8.9 assembly).

instance GQ2.RStageLocal.instNormalK {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} : Blk.K.Normal

K ◁ Y as an instance (the MinimalBlock field, made searchable).

The C = Y/K conjugation action on R (well-defined by K-centrality)

@[reducible]

def GQ2.RStageLocal.rCommGroup {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} (Blk : SectionSeven.MinimalBlock T.LY) (hRK : ∀ r ∈ Blk.frattiniK, ∀ k ∈ Blk.K, r * k = k * r) : CommGroup ↥Blk.frattiniK

R is abelian: it is central in K (hRK, from lemma_7_2) and contained in K.

Equations

• GQ2.RStageLocal.rCommGroup Blk hRK = { toGroup := inferInstance, mul_comm := ⋯ }

theorem GQ2.RStageLocal.conj_eq_of_mk_eq_K {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (hRK : ∀ r ∈ Blk.frattiniK, ∀ k ∈ Blk.K, r * k = k * r) {y w : Y} (h : (QuotientGroup.mk' Blk.K) y = (QuotientGroup.mk' Blk.K) w) (r : ↥Blk.frattiniK) : y * ↑r * y⁻¹ = w * ↑r * w⁻¹

Conjugation on R by an element of Y depends only on its K-coset (K-centrality).

theorem GQ2.RStageLocal.conj_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} (y : Y) (r : ↥Blk.frattiniK) : y * ↑r * y⁻¹ ∈ Blk.frattiniK

Conjugation by y lands back in R (R ◁ Y).

@[reducible]

noncomputable def GQ2.RStageLocal.conjC {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} (Blk : SectionSeven.MinimalBlock T.LY) (hRK : ∀ r ∈ Blk.frattiniK, ∀ k ∈ Blk.K, r * k = k * r) : DistribMulAction (Y ⧸ Blk.K) (Additive ↥Blk.frattiniK)

The C = Y/K conjugation action on Additive R (Quotient.out-conjugation; independent of the representative by conj_eq_of_mk_eq_K).

Equations

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

theorem GQ2.RStageLocal.conjC_smul_of_mk {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (hRK : ∀ r ∈ Blk.frattiniK, ∀ k ∈ Blk.K, r * k = k * r) (y : Y) (r : ↥Blk.frattiniK) : (QuotientGroup.mk' Blk.K) y • Additive.ofMul r = Additive.ofMul ⟨y * ↑r * y⁻¹, ⋯⟩

The action computed at any coset representative.

Shared C = Y/K-module helpers (used by hZcount and hsep_hom)

hZcount: the z_R torsor count at the local source

theorem GQ2.RStageLocal.hZcount_local {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} [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hE2 : ∀ (e : E), e ^ 2 = 1) (hRK : ∀ r ∈ Blk.frattiniK, ∀ k ∈ Blk.K, r * k = k * r) (hR2 : ∀ r ∈ Blk.frattiniK, r * r = 1) (b : AbsGalQ2 →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (f₀ : BoundaryLifts b F T) : Nat.card (SectionEight.RCocycle (blockFrameImpl T Blk hE2) ↑↑f₀) = (blockFrameImpl T Blk hE2).zR

The z_R torsor count, local source (the Prop. 8.9 assembly residue): for every boundary lift f₀, #RCocycle = z_R = #R² · #D_R. Route: RCocycle ≃ Z¹(G_ℚ₂, R_{f₀}) (multiplicative crossed ↔ additive, the conjugation action through C = Y/K pulled back along the surjective mk' K ∘ f₀), card_Z1_eq (5.16 clause (ii), B6+B7), and the invariant-character bridge fixedPts C (R^∨) ≃ D_Rmod + blockRChar_card.

hsep_hom: the (R^∨)^C separation at the local source

theorem GQ2.RStageLocal.htriv_local (γ : AbsGalQ2) (m : ZMod 2) : γ • m = m

The G_ℚ₂-action on 𝔽₂ is trivial (any group action on ZMod 2 fixes both elements).

theorem GQ2.RStageLocal.hsep_hom_local {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} [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hE2 : ∀ (e : E), e ^ 2 = 1) (hRK : ∀ r ∈ Blk.frattiniK, ∀ k ∈ Blk.K, r * k = k * r) (hR2 : ∀ r ∈ Blk.frattiniK, r * r = 1) (b : AbsGalQ2 →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (g : BoundaryLifts b F (blockFrameImpl T Blk hE2).TB) : SectionEight.obs (blockFrameImpl T Blk hE2) (blockRObstructionData T Blk hE2) htriv_local ⋯ ↑↑g = 0 → ∃ (φ : AbsGalQ2 →ₜ* Y), ∀ (γ : AbsGalQ2), (blockFrameImpl T Blk hE2).piB (φ γ) = ↑↑g γ

The (R^∨)^C-separation, local source (the Prop. 8.9 assembly residue): if the obstruction functional of a boundary lift g vanishes, g lifts to a continuous homomorphism into Y. Route: obs g = 0 kills every paired defect class (obs_zero_iff_pairClass_zero); the paired classes are the cup20-values of the R-valued defect class against the invariant characters, and H⁰(G_ℚ₂, R^∨) = (R^∨)^C = D_Rmod by surjectivity of the lower map; bijective_cup20_dualEval (5.16 clause (vi), B6) then forces [rDefect] = 0 in H²(G_ℚ₂, R_ρ); B²-extraction yields a continuous splitting cochain (exponent 2 kills the signs), and homLift_of_split assembles the lift.

The assembly, parametric over hsep_hom

theorem GQ2.RStageLocal.stageR136_local_of_hsep {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} [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hE2 : ∀ (e : E), e ^ 2 = 1) (hRK : ∀ r ∈ Blk.frattiniK, ∀ k ∈ Blk.K, r * k = k * r) (hR2 : ∀ r ∈ Blk.frattiniK, r * r = 1) (hfg : ∃ (s : Finset AbsGalQ2), (Subgroup.closure ↑s).topologicalClosure = ⊤) (b : AbsGalQ2 →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (hsep_hom : ∀ (g : BoundaryLifts b F (blockFrameImpl T Blk hE2).TB), SectionEight.obs (blockFrameImpl T Blk hE2) (blockRObstructionData T Blk hE2) htriv_local ⋯ ↑↑g = 0 → ∃ (φ : AbsGalQ2 →ₜ* Y), ∀ (γ : AbsGalQ2), (blockFrameImpl T Blk hE2).piB (φ γ) = ↑↑g γ) : ↑(Nat.card (blockFrameImpl T Blk hE2).DR) * ↑(exactImageCount b F T) = ↑(blockFrameImpl T Blk hE2).zR * ∑ᶠ (l : (blockFrameImpl T Blk hE2).DR), (2 * ↑((blockFrameImpl T Blk hE2).mB b F l) - ↑(exactImageCount b F (blockFrameImpl T Blk hE2).TB))

(136) for the block frame at the local source, parametric over hsep_hom (the Prop. 8.9 assembly residue assembly): htriv/hcard/hZcount are discharged (htriv_local/card_H2_zmod2_eq_two/hZcount_local); the remaining inputs are the lemma_7_2 structural facts (hRK/hR2), hfg (B1, reserved for the §9 induction), and hsep_hom — the (R^∨)^C-separation (next increment: prop_5_16 clause (vi) + B²-extraction + homLift_of_split; see the module docstring for the surjectivity scoping note).

theorem GQ2.RStageLocal.stageR136_local {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} [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hE2 : ∀ (e : E), e ^ 2 = 1) (hRK : ∀ r ∈ Blk.frattiniK, ∀ k ∈ Blk.K, r * k = k * r) (hR2 : ∀ r ∈ Blk.frattiniK, r * r = 1) (hfg : ∃ (s : Finset AbsGalQ2), (Subgroup.closure ↑s).topologicalClosure = ⊤) (b : AbsGalQ2 →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) : ↑(Nat.card (blockFrameImpl T Blk hE2).DR) * ↑(exactImageCount b F T) = ↑(blockFrameImpl T Blk hE2).zR * ∑ᶠ (l : (blockFrameImpl T Blk hE2).DR), (2 * ↑((blockFrameImpl T Blk hE2).mB b F l) - ↑(exactImageCount b F (blockFrameImpl T Blk hE2).TB))

(136) for the block frame at the local source — all residues discharged (the Prop. 8.9 assembly): htriv/hcard/hZcount/hsep_hom are all proved; the remaining hypotheses are the lemma_7_2 structural facts (hRK/hR2) and hfg (B1, reserved for the §9 induction). The conclusion is the stageR136 field of the local RecursionInputs bundle, verbatim.