The Γ_R GaussZResidue twins at the head-inflated enrichment

The Γ_R side of obligation ii.7 (the last supply seam): the two dichotomy twins gaussZResidueD_gammaR_{unramified,ramified} — GQ2/GaussZ/GammaAD.lean's gaussZResidueD_gammaA_* replayed over the Roe candidate Γ_R, in the exact SourceData.gaussZ_{unramified,ramified} field shapes (checked by the examples at the end of this file), so R32's sourceR binds them exactly as BoundaryMaps.sourceA binds the Γ_A twins (fun T Blk => … (tame := …) …).

The architecture is the Γ_A one stage-for-stage; what changes is word-shaped:

• the boundary interface is the abstract eq. (27) triple (tame, pro2, compat) with the four tame generator pinnings as hypotheses (at Γ_A these are the BoundaryMaps fields B.tameA_*; at Γ_R they will be sourceR's fields, backed by GQ2/Roe/Tame.lean's phiR_gamma* values), and the boundary map is sourceBoundaryMap tame pro2 compat;
• the gauge swap: x₁-supported sections (x1SecC/x1SecClass, slot 3) in place of x₀-supported ones (slot 2), through the Roe word bridge (ofZ1wR/h1CoordGammaR) at markC_R θ; the stage-6 slot facts read congrFun (hevalx v) 3 for the value and congrFun (hevalx v) 2 for the killed wild slot;
• the value side transports through the Sd-level reindexing exactly as for Γ_A (sdProjHom/kappa0Cocycle_reindexHom are imported generic; only the 8-line relZPairR_kappa0_reindexHom retype is new), and the wild peel is the unconditional Wall-shape evaluation liftMark_kappa0_wildValueR_fib_ramified (GQ2/GaussZ/KappaR.lean) — so both twins land stage 6 in the same FoxH.QZeroR (blockQbar …) (powOmega2 (cF tameSigma)) shape (⟦eq:QR⟧), and stage 7 is R27's banked QZeroR_finsum_sign_{unramified,ramified} (GQ2/Roe/Gauss.lean), which performs the split collapse Q_R⁰ = q̄ internally;
• stage-7 finiteness is finite_vcocycle_gammaR (σ-free from R31f's Phase140GammaR.hZcard_gammaR); the freeness hfix_of_simple_nt is imported generic.

The un/ramified dichotomy hypothesis is the same head-level F.alpha tameTau-action as on the Γ_A side — ρ-free and source-free, so the P4e/gaussZ_obtain_blockD_of_sources by_cases serves both sources at the shared external G0 = ∓2^m.

Axioms: std-3 throughout (no B-axioms, no sorries).

The Sd-level reindexing transport at the Roe relator pair

theorem GQ2.SectionNine.relZPairR_kappa0_reindexHom {C : Type u_1} {C' : Type u_2} [Group C] [Group C'] {V : Type u_3} [AddCommGroup V] [DistribMulAction C V] [DistribMulAction C' V] [Finite C] [Finite C'] [Finite V] {q q' : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (π : C' →* C) (hπ : ∀ (c' : C') (v : V), c' • v = π c' • v) (hdat' : IsEquivariantFactorSet q' (dat.reindexHom ⇑π)) (t : Marking (SectionEight.AffineTLift.Sd C' V)) : WordCoh2R.relZPairR t (SectionEight.AffineTLift.kappa0Cocycle (dat.reindexHom ⇑π) hdat') = WordCoh2R.relZPairR (Marking.map (sdProjHom π hπ) t) (SectionEight.AffineTLift.kappa0Cocycle dat hdat)

The Sd-level Roe relator transport (the ii.7 value-side seam): the Roe relator pair of the reindexed κ⁰ at a marking is the Roe relator pair of the base κ⁰ at the sdProjHom-mapped marking — relZPairR_comap + the generic cocycle identification kappa0Cocycle_reindexHom (imported from GQ2/GaussZ/GammaAD.lean).

The x₁-supported section classes (stages 4/5/6 of both twins)

The section cocycles secC v := ofZ1 ∘ ofZ1wR at the x₁-supported Roe word cocycles, their classes ψ v in the Gauss domain, the h1CoordGammaR-coordinate computation, the evalR roundtrip, and bijectivity given the section bijection. Generic in the enrichment and in the Z¹_R-membership pack (hmem), so the un/ramified twins differ only in how they discharge hmem/hsec (the split vs ramified shape lemmas). Instance context as in GQ2/GaussZ/CoordGammaR.lean (the callers' letI-packs supply it).

noncomputable def GQ2.SectionNine.x1SecC {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : SectionEight.RecursionFrame T Blk} (b : ↑GammaR.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : BoundaryLifts b F RF.TC) [TopologicalSpace (En.descData l h).Vmod] [DiscreteTopology (En.descData l h).Vmod] [DistribMulAction WordCohBridgeR.GR (En.descData l h).Vmod] [DistribMulAction RF.YC (En.descData l h).Vmod] [Finite (En.descData l h).Vmod] (hcomp : ∀ (γ : WordCohBridgeR.GR) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.rho0 (En.descData l h) (SectionEight.AffineTLift.rhoPrimeGR b F En l h ρ)) γ • v) (hcompat : ∀ (γ : WordCohBridgeR.GR) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.thetaGR b F ρ) γ • v) (hA₂ : ∀ (v : (En.descData l h).Vmod), v + v = 0) (hmem : ∀ (v : (En.descData l h).Vmod), FoxH.x1Supported v ∈ FoxH.Z1wR (markC_R (SectionEight.AffineTLift.thetaGR b F ρ))) (v : (En.descData l h).Vmod) : SectionEight.AffineTLift.VCocycle (En.descData l h) (SectionEight.AffineTLift.rhoPrimeGR b F En l h ρ)

The x₁-supported section cocycle at v (stage 4 of the twins).

Equations

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

noncomputable def GQ2.SectionNine.x1SecClass {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : SectionEight.RecursionFrame T Blk} (b : ↑GammaR.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : BoundaryLifts b F RF.TC) [TopologicalSpace (En.descData l h).Vmod] [DiscreteTopology (En.descData l h).Vmod] [DistribMulAction WordCohBridgeR.GR (En.descData l h).Vmod] [DistribMulAction RF.YC (En.descData l h).Vmod] [Finite (En.descData l h).Vmod] (hcomp : ∀ (γ : WordCohBridgeR.GR) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.rho0 (En.descData l h) (SectionEight.AffineTLift.rhoPrimeGR b F En l h ρ)) γ • v) (hcompat : ∀ (γ : WordCohBridgeR.GR) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.thetaGR b F ρ) γ • v) (hA₂ : ∀ (v : (En.descData l h).Vmod), v + v = 0) (hmem : ∀ (v : (En.descData l h).Vmod), FoxH.x1Supported v ∈ FoxH.Z1wR (markC_R (SectionEight.AffineTLift.thetaGR b F ρ))) (v : (En.descData l h).Vmod) : SectionEight.AffineTLift.VCocycle (En.descData l h) (SectionEight.AffineTLift.rhoPrimeGR b F En l h ρ) ⧸ SectionEight.AffineTLift.vCobRange (En.descData l h) (SectionEight.AffineTLift.rhoPrimeGR b F En l h ρ)

The class of x1SecC v in the Gauss domain Z¹⧸B¹ (the twins' ψ).

Equations

• GQ2.SectionNine.x1SecClass b F En l h ρ hcomp hcompat hA₂ hmem v = ↑(GQ2.SectionNine.x1SecC b F En l h ρ hcomp hcompat hA₂ hmem v)

theorem GQ2.SectionNine.evalR_ofZ1wR_x1Supported {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : SectionEight.RecursionFrame T Blk} (b : ↑GammaR.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : BoundaryLifts b F RF.TC) [TopologicalSpace (En.descData l h).Vmod] [DiscreteTopology (En.descData l h).Vmod] [DistribMulAction WordCohBridgeR.GR (En.descData l h).Vmod] [DistribMulAction RF.YC (En.descData l h).Vmod] [Finite (En.descData l h).Vmod] (hcompat : ∀ (γ : WordCohBridgeR.GR) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.thetaGR b F ρ) γ • v) (hA₂ : ∀ (v : (En.descData l h).Vmod), v + v = 0) (hmem : ∀ (v : (En.descData l h).Vmod), FoxH.x1Supported v ∈ FoxH.Z1wR (markC_R (SectionEight.AffineTLift.thetaGR b F ρ))) (v : (En.descData l h).Vmod) : WordCohBridgeR.evalR (WordCohBridgeR.ofZ1wR (SectionEight.AffineTLift.thetaGR b F ρ) hcompat ⋯ hA₂ ⟨FoxH.x1Supported v, ⋯⟩) = FoxH.x1Supported v

evalR recovers the x₁-supported tuple from the section's Roe word cocycle (stage 6's hevalx).

theorem GQ2.SectionNine.h1CoordGammaR_x1SecClass {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : SectionEight.RecursionFrame T Blk} (b : ↑GammaR.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : BoundaryLifts b F RF.TC) [TopologicalSpace (En.descData l h).Vmod] [DiscreteTopology (En.descData l h).Vmod] [DistribMulAction WordCohBridgeR.GR (En.descData l h).Vmod] [ContinuousSMul WordCohBridgeR.GR (En.descData l h).Vmod] [DistribMulAction RF.YC (En.descData l h).Vmod] [Finite (En.descData l h).Vmod] (hcomp : ∀ (γ : WordCohBridgeR.GR) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.rho0 (En.descData l h) (SectionEight.AffineTLift.rhoPrimeGR b F En l h ρ)) γ • v) (hcompat : ∀ (γ : WordCohBridgeR.GR) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.thetaGR b F ρ) γ • v) (hA₂ : ∀ (v : (En.descData l h).Vmod), v + v = 0) (hmem : ∀ (v : (En.descData l h).Vmod), FoxH.x1Supported v ∈ FoxH.Z1wR (markC_R (SectionEight.AffineTLift.thetaGR b F ρ))) (v : (En.descData l h).Vmod) : SectionEight.AffineTLift.h1CoordGammaR b F En l h ρ hcomp hcompat hA₂ (x1SecClass b F En l h ρ hcomp hcompat hA₂ hmem v) = FoxH.h1wMkR (markC_R (SectionEight.AffineTLift.thetaGR b F ρ)) ⟨FoxH.x1Supported v, ⋯⟩

The h1CoordGammaR-coordinate of x1SecClass v is the class of the x₁-supported Roe word cocycle (stage 5's hcoordψ).

theorem GQ2.SectionNine.x1SecClass_bijective {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : SectionEight.RecursionFrame T Blk} (b : ↑GammaR.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : BoundaryLifts b F RF.TC) [TopologicalSpace (En.descData l h).Vmod] [DiscreteTopology (En.descData l h).Vmod] [DistribMulAction WordCohBridgeR.GR (En.descData l h).Vmod] [ContinuousSMul WordCohBridgeR.GR (En.descData l h).Vmod] [DistribMulAction RF.YC (En.descData l h).Vmod] [Finite (En.descData l h).Vmod] (hcomp : ∀ (γ : WordCohBridgeR.GR) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.rho0 (En.descData l h) (SectionEight.AffineTLift.rhoPrimeGR b F En l h ρ)) γ • v) (hcompat : ∀ (γ : WordCohBridgeR.GR) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.thetaGR b F ρ) γ • v) (hA₂ : ∀ (v : (En.descData l h).Vmod), v + v = 0) (hmem : ∀ (v : (En.descData l h).Vmod), FoxH.x1Supported v ∈ FoxH.Z1wR (markC_R (SectionEight.AffineTLift.thetaGR b F ρ))) (hsec : Function.Bijective fun (v : (En.descData l h).Vmod) => FoxH.h1wMkR (markC_R (SectionEight.AffineTLift.thetaGR b F ρ)) ⟨FoxH.x1Supported v, ⋯⟩) : Function.Bijective (x1SecClass b F En l h ρ hcomp hcompat hA₂ hmem)

Bijectivity of v ↦ x1SecClass v, given the section bijection (stage 5's hψbij).

The twins

The head-slot projections (stage 2/6 of both twins)

blockProjF ∘ θ = cF ∘ tame (boundaryLift_head_gammaR through mk' (headActKer)), evaluated at the four Γ_R-generators: the tame slots project to the fixed headTameSurj-values (through the pinning hypotheses htσ/htτ — at sourceR these are the structure's tame_sigma/tame_tau fields), the wild slots to 1 (htx0/htx1). Both twins consume these at markC_R θ (via markC_R_map) and at the mapped Sd-marking's cc-slots (via the rho0-roundtrip).

theorem GQ2.SectionNine.boundaryLift_head_gammaR {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) (hE2 : ∀ (e : E), e ^ 2 = 1) (tame : ↑GammaR.toProfinite.toTop →ₜ* ↑Ttame.toProfinite.toTop) (pro2 : ↑GammaR.toProfinite.toTop →ₜ* ↑PiBd.toProfinite.toTop) (compat : ∀ (g : ↑GammaR.toProfinite.toTop), nuT (tame g) = nuTwo (pro2 g)) (F : BoundaryFrame H E) (ρ : BoundaryLifts (sourceBoundaryMap tame pro2 compat) F (blockFrame T Blk hE2).TC) (γ : ↑GammaR.toProfinite.toTop) : (blockFrame T Blk hE2).TC.piY (↑↑ρ γ) = F.alpha (tame γ)

Γ_R version of the boundary equation's head component: TC.piY ∘ ρ = α ∘ tame (rfl-deep — the first component of IsBoundaryLift at sourceBoundaryMap).

theorem GQ2.SectionNine.blockProjF_thetaGR {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) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (hE2 : ∀ (e : E), e ^ 2 = 1) (tame : ↑GammaR.toProfinite.toTop →ₜ* ↑Ttame.toProfinite.toTop) (pro2 : ↑GammaR.toProfinite.toTop →ₜ* ↑PiBd.toProfinite.toTop) (compat : ∀ (g : ↑GammaR.toProfinite.toTop), nuT (tame g) = nuTwo (pro2 g)) (F : BoundaryFrame H E) (ρ : BoundaryLifts (sourceBoundaryMap tame pro2 compat) F (blockFrame T Blk hE2).TC) (γ : WordCohBridgeR.GR) : (blockProjF T Blk) ((SectionEight.AffineTLift.thetaGR (sourceBoundaryMap tame pro2 compat) F ρ) γ) = (headTameSurj T Blk F) (tame γ)

The head factorization of the Γ_R boundary lift, through mk' (headActKer).

theorem GQ2.SectionNine.blockProjF_thetaGR_sigma {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) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (hE2 : ∀ (e : E), e ^ 2 = 1) (tame : ↑GammaR.toProfinite.toTop →ₜ* ↑Ttame.toProfinite.toTop) (pro2 : ↑GammaR.toProfinite.toTop →ₜ* ↑PiBd.toProfinite.toTop) (compat : ∀ (g : ↑GammaR.toProfinite.toTop), nuT (tame g) = nuTwo (pro2 g)) (F : BoundaryFrame H E) (ρ : BoundaryLifts (sourceBoundaryMap tame pro2 compat) F (blockFrame T Blk hE2).TC) (htσ : tame gammaSigmaR = tameSigma) : (blockProjF T Blk) ((SectionEight.AffineTLift.thetaGR (sourceBoundaryMap tame pro2 compat) F ρ) WordCohBridgeR.gammaGenR.σ) = (headTameSurj T Blk F) tameSigma

The σ-slot projects to the fixed tame σ-value.

theorem GQ2.SectionNine.blockProjF_thetaGR_tau {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) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (hE2 : ∀ (e : E), e ^ 2 = 1) (tame : ↑GammaR.toProfinite.toTop →ₜ* ↑Ttame.toProfinite.toTop) (pro2 : ↑GammaR.toProfinite.toTop →ₜ* ↑PiBd.toProfinite.toTop) (compat : ∀ (g : ↑GammaR.toProfinite.toTop), nuT (tame g) = nuTwo (pro2 g)) (F : BoundaryFrame H E) (ρ : BoundaryLifts (sourceBoundaryMap tame pro2 compat) F (blockFrame T Blk hE2).TC) (htτ : tame gammaTauR = tameTau) : (blockProjF T Blk) ((SectionEight.AffineTLift.thetaGR (sourceBoundaryMap tame pro2 compat) F ρ) WordCohBridgeR.gammaGenR.τ) = (headTameSurj T Blk F) tameTau

The τ-slot projects to the fixed tame τ-value.

theorem GQ2.SectionNine.blockProjF_thetaGR_x0 {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) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (hE2 : ∀ (e : E), e ^ 2 = 1) (tame : ↑GammaR.toProfinite.toTop →ₜ* ↑Ttame.toProfinite.toTop) (pro2 : ↑GammaR.toProfinite.toTop →ₜ* ↑PiBd.toProfinite.toTop) (compat : ∀ (g : ↑GammaR.toProfinite.toTop), nuT (tame g) = nuTwo (pro2 g)) (F : BoundaryFrame H E) (ρ : BoundaryLifts (sourceBoundaryMap tame pro2 compat) F (blockFrame T Blk hE2).TC) (htx0 : tame gammaX0R = 1) : (blockProjF T Blk) ((SectionEight.AffineTLift.thetaGR (sourceBoundaryMap tame pro2 compat) F ρ) WordCohBridgeR.gammaGenR.x₀) = 1

The x₀-slot projects to 1 (the wild generators die at the tame head).

theorem GQ2.SectionNine.blockProjF_thetaGR_x1 {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) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (hE2 : ∀ (e : E), e ^ 2 = 1) (tame : ↑GammaR.toProfinite.toTop →ₜ* ↑Ttame.toProfinite.toTop) (pro2 : ↑GammaR.toProfinite.toTop →ₜ* ↑PiBd.toProfinite.toTop) (compat : ∀ (g : ↑GammaR.toProfinite.toTop), nuT (tame g) = nuTwo (pro2 g)) (F : BoundaryFrame H E) (ρ : BoundaryLifts (sourceBoundaryMap tame pro2 compat) F (blockFrame T Blk hE2).TC) (htx1 : tame gammaX1R = 1) : (blockProjF T Blk) ((SectionEight.AffineTLift.thetaGR (sourceBoundaryMap tame pro2 compat) F ρ) WordCohBridgeR.gammaGenR.x₁) = 1

The x₁-slot projects to 1 (the wild generators die at the tame head).

theorem GQ2.SectionNine.blockProjF_markC_R_sigma {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) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (hE2 : ∀ (e : E), e ^ 2 = 1) (tame : ↑GammaR.toProfinite.toTop →ₜ* ↑Ttame.toProfinite.toTop) (pro2 : ↑GammaR.toProfinite.toTop →ₜ* ↑PiBd.toProfinite.toTop) (compat : ∀ (g : ↑GammaR.toProfinite.toTop), nuT (tame g) = nuTwo (pro2 g)) (F : BoundaryFrame H E) (ρ : BoundaryLifts (sourceBoundaryMap tame pro2 compat) F (blockFrame T Blk hE2).TC) (htσ : tame gammaSigmaR = tameSigma) : (blockProjF T Blk) (markC_R (SectionEight.AffineTLift.thetaGR (sourceBoundaryMap tame pro2 compat) F ρ)).σ = (headTameSurj T Blk F) tameSigma

The head projection of the markC_R θ σ-slot is the fixed tame σ-value (stage 2 of both twins, at markC_R θ via markC_R_map).

theorem GQ2.SectionNine.blockProjF_markC_R_tau {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) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (hE2 : ∀ (e : E), e ^ 2 = 1) (tame : ↑GammaR.toProfinite.toTop →ₜ* ↑Ttame.toProfinite.toTop) (pro2 : ↑GammaR.toProfinite.toTop →ₜ* ↑PiBd.toProfinite.toTop) (compat : ∀ (g : ↑GammaR.toProfinite.toTop), nuT (tame g) = nuTwo (pro2 g)) (F : BoundaryFrame H E) (ρ : BoundaryLifts (sourceBoundaryMap tame pro2 compat) F (blockFrame T Blk hE2).TC) (htτ : tame gammaTauR = tameTau) : (blockProjF T Blk) (markC_R (SectionEight.AffineTLift.thetaGR (sourceBoundaryMap tame pro2 compat) F ρ)).τ = (headTameSurj T Blk F) tameTau

The head projection of the markC_R θ τ-slot is the fixed tame τ-value (stage 2 of both twins, at markC_R θ via markC_R_map).

theorem GQ2.SectionNine.blockProjF_markC_R_x0 {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) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (hE2 : ∀ (e : E), e ^ 2 = 1) (tame : ↑GammaR.toProfinite.toTop →ₜ* ↑Ttame.toProfinite.toTop) (pro2 : ↑GammaR.toProfinite.toTop →ₜ* ↑PiBd.toProfinite.toTop) (compat : ∀ (g : ↑GammaR.toProfinite.toTop), nuT (tame g) = nuTwo (pro2 g)) (F : BoundaryFrame H E) (ρ : BoundaryLifts (sourceBoundaryMap tame pro2 compat) F (blockFrame T Blk hE2).TC) (htx0 : tame gammaX0R = 1) : (blockProjF T Blk) (markC_R (SectionEight.AffineTLift.thetaGR (sourceBoundaryMap tame pro2 compat) F ρ)).x₀ = 1

The head projection of the markC_R θ x₀-slot is 1 (the wild generators die at the tame head).

theorem GQ2.SectionNine.blockProjF_markC_R_x1 {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) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (hE2 : ∀ (e : E), e ^ 2 = 1) (tame : ↑GammaR.toProfinite.toTop →ₜ* ↑Ttame.toProfinite.toTop) (pro2 : ↑GammaR.toProfinite.toTop →ₜ* ↑PiBd.toProfinite.toTop) (compat : ∀ (g : ↑GammaR.toProfinite.toTop), nuT (tame g) = nuTwo (pro2 g)) (F : BoundaryFrame H E) (ρ : BoundaryLifts (sourceBoundaryMap tame pro2 compat) F (blockFrame T Blk hE2).TC) (htx1 : tame gammaX1R = 1) : (blockProjF T Blk) (markC_R (SectionEight.AffineTLift.thetaGR (sourceBoundaryMap tame pro2 compat) F ρ)).x₁ = 1

The head projection of the markC_R θ x₁-slot is 1 (the wild generators die at the tame head).

theorem GQ2.SectionNine.gaussZResidueD_gammaR_unramified {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) [Blk.frattiniK.Normal] [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (hE2 : ∀ (e : E), e ^ 2 = 1) (tame : ↑GammaR.toProfinite.toTop →ₜ* ↑Ttame.toProfinite.toTop) (pro2 : ↑GammaR.toProfinite.toTop →ₜ* ↑PiBd.toProfinite.toTop) (compat : ∀ (g : ↑GammaR.toProfinite.toTop), nuT (tame g) = nuTwo (pro2 g)) (htσ : tame gammaSigmaR = tameSigma) (htτ : tame gammaTauR = tameTau) (htx0 : tame gammaX0R = 1) (htx1 : tame gammaX1R = 1) (F : BoundaryFrame H E) (hsimple : ∀ (W : AddSubgroup (blockEnrichmentD T Blk hE2 F).Vmod), (∀ (g : (blockFrame T Blk hE2).YC), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hVne : ∃ (v : (blockEnrichmentD T Blk hE2 F).Vmod), v ≠ 0) (hnt : ∃ (g : (blockFrame T Blk hE2).YC) (v : (blockEnrichmentD T Blk hE2 F).Vmod), g • v ≠ v) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card (blockEnrichmentD T Blk hE2 F).Vmod = 2 ^ (2 * m)) (l : (blockFrame T Blk hE2).DR) (h : l ≠ (blockFrame T Blk hE2).zeroDR) (hunram : ∀ (v : Additive (↥Blk.P ⧸ Blk.S.subgroupOf Blk.P)), F.alpha tameTau • v = v) : SectionEight.GaussZResidue (sourceBoundaryMap tame pro2 compat) F (blockEnrichmentD T Blk hE2 F) l h (-2 ^ m)

hGaussZR at the head-inflated enrichment, unramified case (ii.7): for the block enrichment blockEnrichmentD, GaussZResidue (sourceBoundaryMap tame pro2 compat) F (blockEnrichmentD …) l h (−2^m) — the dichotomy hypothesis is the head-level F.alpha tameTau-triviality, uniform in ρ, exactly as for Γ_A.

theorem GQ2.SectionNine.gaussZResidueD_gammaR_ramified {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) [Blk.frattiniK.Normal] [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (hE2 : ∀ (e : E), e ^ 2 = 1) (tame : ↑GammaR.toProfinite.toTop →ₜ* ↑Ttame.toProfinite.toTop) (pro2 : ↑GammaR.toProfinite.toTop →ₜ* ↑PiBd.toProfinite.toTop) (compat : ∀ (g : ↑GammaR.toProfinite.toTop), nuT (tame g) = nuTwo (pro2 g)) (htσ : tame gammaSigmaR = tameSigma) (htτ : tame gammaTauR = tameTau) (htx0 : tame gammaX0R = 1) (htx1 : tame gammaX1R = 1) (F : BoundaryFrame H E) (hsimple : ∀ (W : AddSubgroup (blockEnrichmentD T Blk hE2 F).Vmod), (∀ (g : (blockFrame T Blk hE2).YC), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hVne : ∃ (v : (blockEnrichmentD T Blk hE2 F).Vmod), v ≠ 0) (hnt : ∃ (g : (blockFrame T Blk hE2).YC) (v : (blockEnrichmentD T Blk hE2 F).Vmod), g • v ≠ v) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card (blockEnrichmentD T Blk hE2 F).Vmod = 2 ^ (2 * m)) (l : (blockFrame T Blk hE2).DR) (h : l ≠ (blockFrame T Blk hE2).zeroDR) (hram : ∃ (v : Additive (↥Blk.P ⧸ Blk.S.subgroupOf Blk.P)), F.alpha tameTau • v ≠ v) : SectionEight.GaussZResidue (sourceBoundaryMap tame pro2 compat) F (blockEnrichmentD T Blk hE2 F) l h (2 ^ m)

hGaussZR at the head-inflated enrichment, ramified case (ii.7): inertia moves the module at the head — GaussZResidue (sourceBoundaryMap tame pro2 compat) F (blockEnrichmentD …) l h (+2^m).

Field-shape smoke tests

The two twins in the exact SourceData.gaussZ_{unramified,ramified} field types (GQ2/SourceData.lean), bound exactly as R32's sourceR will bind them — the named-arg partial application fun T Blk => … (tame := …) mirroring BoundaryMaps.sourceA's fun T Blk => … (B := B). The letI := smulZmod2 prefix instantiates at the global RStageGammaR scalar action (which is what sourceR's smulZmod2 field will be).

Paper-tag ledger (Roe note paper/roe-presentation-verification.tex; hand-maintained)

• Proposition 6.1/⟦prop:quadratic⟧, ⟦eq:QR⟧ — stage 6 lands both twins in the QZeroR two-term shape via liftMark_kappa0_wildValueR_fib_ramified.
• Corollary 6.2/⟦cor:gauss⟧ — stage 7 is QZeroR_finsum_sign_{unramified,ramified} (GQ2/Roe/Gauss.lean), giving the ∓2^m residues of gaussZResidueD_gammaR_{unramified,ramified}.
• Lemma 4.2/⟦lem:normalforms⟧ — the x₁-supported gauge of stages 3–5.