The Γ_A GaussZResidue twins at the head-inflated enrichment

The Γ_A side of the head-inflation reshape (docs/orchestration/p16d6e4aA-p4-tame-package.md §3, docs/orchestration/p16d6e4aA-p4d-handoff.md): the two gaussZResidue_gammaA_* twins of GQ2/GaussZFinalGammaA.lean replayed at En := blockEnrichmentD — without the refuted per-lift hpack. For an arbitrary boundary lift ρ the tame factorization is recovered at the faithful head quotient:

• the boundary equation's head component (boundaryLift_head_gammaA) identifies blockProjF ∘ θ = cF ∘ B.tameA with the fixed surjection cF := mk' ∘ F.alpha — tame-factored uniformly in ρ (θ := ρ.1.1 = thetaGA, rfl-deep);
• the space side (A-1/A-4.1: x0Supported/x0Section/h1CoordGammaA) runs at the RF.YC-marking markC θ verbatim; its action-level hypotheses discharge through blockProjF_compat + the head-slot projections + the banked …_of_gen lemmas at HVq;
• the value side transports through the NEW Sd-level reindexing: blockEnrichmentD's datum is definitionally (blockDatHV).reindexHom blockProjF, and relZPair_kappa0_reindexHom (below: κ⁰ of the reindexed datum = the sdProjHom-pullback of κ⁰ of the datum, then relZPair_comap) moves the A-3 keystone's relator pair onto the sdProjHom-mapped marking over Sd (HVq) V — whose wild slots are literally 1 and whose tame slots are the cF-values;
• the peels (A-4.2/4.3c/4.4b) and counts (finsum_sign_{unramified,ramified}_of_action) then run at C := HVq with dat := blockDatHV, hdat := blockDatHV_spec, form blockQbar, where the generation is gen_ttame_quotient cF and inertia-oddness is odd_orderOf_tameInertia cF.

The un/ramified dichotomy hypothesis is taken at the head (F.alpha tameTau-action, headAct) — ρ-free and source-free, matching the P4c local twins, so the P4e obtain can by_cases on it once for both sources.

Axioms: the unramified and ramified twins use only the standard axioms; the ramified zero count is provided by zeroCount_qDouble_ramified_of_faithful through finsum_sign_ramified_of_action.

The Sd-level reindexing transport (the one new ingredient)

noncomputable def GQ2.SectionNine.sdProjHom {C : Type u_1} {C' : Type u_2} [Group C] [Group C'] {V : Type u_3} [AddCommGroup V] [DistribMulAction C V] [DistribMulAction C' V] (π : C' →* C) (hπ : ∀ (c' : C') (v : V), c' • v = π c' • v) : SectionEight.AffineTLift.Sd C' V →* SectionEight.AffineTLift.Sd C V

The Sd-level projection V ⋊ C' →* V ⋊ C along π : C' →* C (identity on V) — a homomorphism exactly because the C'-action on V is the π-pullback of the C-action.

Equations

• GQ2.SectionNine.sdProjHom π hπ = { toFun := fun (p : GQ2.SectionEight.AffineTLift.Sd C' V) => GQ2.SectionEight.AffineTLift.Sd.mk p.v (π p.cc), map_one' := ⋯, map_mul' := ⋯ }

theorem GQ2.SectionNine.kappa0Cocycle_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] {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 ⇑π)) : SectionEight.AffineTLift.kappa0Cocycle (dat.reindexHom ⇑π) hdat' = (SectionEight.AffineTLift.kappa0Cocycle dat hdat).comap (sdProjHom π hπ)

κ⁰ of the reindexed datum is the sdProjHom-pullback of κ⁰ of the datum: f sees only V-arguments and m pre-composes with π — the graphPullback_reindexHom computation at the cocycle level.

theorem GQ2.SectionNine.relZPair_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)) : WordCoh2.relZPair t (SectionEight.AffineTLift.kappa0Cocycle (dat.reindexHom ⇑π) hdat') = WordCoh2.relZPair (Marking.map (sdProjHom π hπ) t) (SectionEight.AffineTLift.kappa0Cocycle dat hdat)

The Sd-level relator transport (the P4d value-side seam): the relator pair of the reindexed κ⁰ at a marking is the relator pair of the base κ⁰ at the sdProjHom-mapped marking (relZPair_comap + the cocycle identification above).

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

The section cocycles secC v := ofZ1 ∘ ofZ1w at the x₀-supported word cocycles, their classes ψ v in the Gauss domain, the h1CoordGammaA-coordinate computation, the eval roundtrip, and bijectivity given the A-4.1 section bijection. Generic in the enrichment and in the Z¹_w-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/CoordGammaA.lean (the callers' letI-packs supply it).

noncomputable def GQ2.SectionNine.x0SecC {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 : ↑GammaA.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 WordCohBridge.GA (En.descData l h).Vmod] [DistribMulAction RF.YC (En.descData l h).Vmod] [Finite (En.descData l h).Vmod] (hcomp : ∀ (γ : WordCohBridge.GA) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.rho0 (En.descData l h) (SectionEight.AffineTLift.rhoPrimeGA b F En l h ρ)) γ • v) (hcompat : ∀ (γ : WordCohBridge.GA) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.thetaGA b F ρ) γ • v) (hA₂ : ∀ (v : (En.descData l h).Vmod), v + v = 0) (hmem : ∀ (v : (En.descData l h).Vmod), FoxH.x0Supported v ∈ FoxH.Z1w (WordCohBridge.markC (SectionEight.AffineTLift.thetaGA b F ρ))) (v : (En.descData l h).Vmod) : SectionEight.AffineTLift.VCocycle (En.descData l h) (SectionEight.AffineTLift.rhoPrimeGA 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.x0SecClass {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 : ↑GammaA.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 WordCohBridge.GA (En.descData l h).Vmod] [DistribMulAction RF.YC (En.descData l h).Vmod] [Finite (En.descData l h).Vmod] (hcomp : ∀ (γ : WordCohBridge.GA) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.rho0 (En.descData l h) (SectionEight.AffineTLift.rhoPrimeGA b F En l h ρ)) γ • v) (hcompat : ∀ (γ : WordCohBridge.GA) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.thetaGA b F ρ) γ • v) (hA₂ : ∀ (v : (En.descData l h).Vmod), v + v = 0) (hmem : ∀ (v : (En.descData l h).Vmod), FoxH.x0Supported v ∈ FoxH.Z1w (WordCohBridge.markC (SectionEight.AffineTLift.thetaGA b F ρ))) (v : (En.descData l h).Vmod) : SectionEight.AffineTLift.VCocycle (En.descData l h) (SectionEight.AffineTLift.rhoPrimeGA b F En l h ρ) ⧸ SectionEight.AffineTLift.vCobRange (En.descData l h) (SectionEight.AffineTLift.rhoPrimeGA b F En l h ρ)

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

Equations

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

theorem GQ2.SectionNine.eval_ofZ1w_x0Supported {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 : ↑GammaA.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 WordCohBridge.GA (En.descData l h).Vmod] [DistribMulAction RF.YC (En.descData l h).Vmod] [Finite (En.descData l h).Vmod] (hcompat : ∀ (γ : WordCohBridge.GA) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.thetaGA b F ρ) γ • v) (hA₂ : ∀ (v : (En.descData l h).Vmod), v + v = 0) (hmem : ∀ (v : (En.descData l h).Vmod), FoxH.x0Supported v ∈ FoxH.Z1w (WordCohBridge.markC (SectionEight.AffineTLift.thetaGA b F ρ))) (v : (En.descData l h).Vmod) : WordCohBridge.eval (WordCohBridge.ofZ1w (SectionEight.AffineTLift.thetaGA b F ρ) hcompat ⋯ hA₂ ⟨FoxH.x0Supported v, ⋯⟩) = FoxH.x0Supported v

eval recovers the x₀-supported tuple from the section's word cocycle (stage 6's hevalx).

theorem GQ2.SectionNine.h1CoordGammaA_x0SecClass {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 : ↑GammaA.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 WordCohBridge.GA (En.descData l h).Vmod] [ContinuousSMul WordCohBridge.GA (En.descData l h).Vmod] [DistribMulAction RF.YC (En.descData l h).Vmod] [Finite (En.descData l h).Vmod] (hcomp : ∀ (γ : WordCohBridge.GA) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.rho0 (En.descData l h) (SectionEight.AffineTLift.rhoPrimeGA b F En l h ρ)) γ • v) (hcompat : ∀ (γ : WordCohBridge.GA) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.thetaGA b F ρ) γ • v) (hA₂ : ∀ (v : (En.descData l h).Vmod), v + v = 0) (hmem : ∀ (v : (En.descData l h).Vmod), FoxH.x0Supported v ∈ FoxH.Z1w (WordCohBridge.markC (SectionEight.AffineTLift.thetaGA b F ρ))) (v : (En.descData l h).Vmod) : SectionEight.AffineTLift.h1CoordGammaA b F En l h ρ hcomp hcompat hA₂ (x0SecClass b F En l h ρ hcomp hcompat hA₂ hmem v) = FoxH.h1wMk (WordCohBridge.markC (SectionEight.AffineTLift.thetaGA b F ρ)) ⟨FoxH.x0Supported v, ⋯⟩

The h1CoordGammaA-coordinate of x0SecClass v is the class of the x₀-supported word cocycle (stage 5's hcoordψ).

theorem GQ2.SectionNine.x0SecClass_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 : ↑GammaA.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 WordCohBridge.GA (En.descData l h).Vmod] [ContinuousSMul WordCohBridge.GA (En.descData l h).Vmod] [DistribMulAction RF.YC (En.descData l h).Vmod] [Finite (En.descData l h).Vmod] (hcomp : ∀ (γ : WordCohBridge.GA) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.rho0 (En.descData l h) (SectionEight.AffineTLift.rhoPrimeGA b F En l h ρ)) γ • v) (hcompat : ∀ (γ : WordCohBridge.GA) (v : (En.descData l h).Vmod), γ • v = (SectionEight.AffineTLift.thetaGA b F ρ) γ • v) (hA₂ : ∀ (v : (En.descData l h).Vmod), v + v = 0) (hmem : ∀ (v : (En.descData l h).Vmod), FoxH.x0Supported v ∈ FoxH.Z1w (WordCohBridge.markC (SectionEight.AffineTLift.thetaGA b F ρ))) (hsec : Function.Bijective fun (v : (En.descData l h).Vmod) => FoxH.h1wMk (WordCohBridge.markC (SectionEight.AffineTLift.thetaGA b F ρ)) ⟨FoxH.x0Supported v, ⋯⟩) : Function.Bijective (x0SecClass b F En l h ρ hcomp hcompat hA₂ hmem)

Bijectivity of v ↦ x0SecClass v, given the A-4.1 section bijection (stage 5's hψbij).

The twins

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

blockProjF ∘ θ = cF ∘ B.tameA (boundaryLift_head_gammaA through mk' (headActKer)), evaluated at the four Γ_A-generators: the tame slots project to the fixed headTameSurj-values, the wild slots to 1. Both twins consume these at markC θ (via markC_map) and at the mapped Sd-marking's cc-slots (via the rho0-roundtrip).

theorem GQ2.SectionNine.blockProjF_thetaGA {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) (B : BoundaryMaps) (F : BoundaryFrame H E) (ρ : BoundaryLifts B.bA F (blockFrame T Blk hE2).TC) (γ : WordCohBridge.GA) : (blockProjF T Blk) ((SectionEight.AffineTLift.thetaGA B.bA F ρ) γ) = (headTameSurj T Blk F) (B.tameA γ)

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

theorem GQ2.SectionNine.blockProjF_thetaGA_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) (B : BoundaryMaps) (F : BoundaryFrame H E) (ρ : BoundaryLifts B.bA F (blockFrame T Blk hE2).TC) : (blockProjF T Blk) ((SectionEight.AffineTLift.thetaGA B.bA F ρ) WordCohBridge.gammaGen.σ) = (headTameSurj T Blk F) tameSigma

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

theorem GQ2.SectionNine.blockProjF_thetaGA_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) (B : BoundaryMaps) (F : BoundaryFrame H E) (ρ : BoundaryLifts B.bA F (blockFrame T Blk hE2).TC) : (blockProjF T Blk) ((SectionEight.AffineTLift.thetaGA B.bA F ρ) WordCohBridge.gammaGen.τ) = (headTameSurj T Blk F) tameTau

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

theorem GQ2.SectionNine.blockProjF_thetaGA_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) (B : BoundaryMaps) (F : BoundaryFrame H E) (ρ : BoundaryLifts B.bA F (blockFrame T Blk hE2).TC) : (blockProjF T Blk) ((SectionEight.AffineTLift.thetaGA B.bA F ρ) WordCohBridge.gammaGen.x₀) = 1

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

theorem GQ2.SectionNine.blockProjF_thetaGA_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) (B : BoundaryMaps) (F : BoundaryFrame H E) (ρ : BoundaryLifts B.bA F (blockFrame T Blk hE2).TC) : (blockProjF T Blk) ((SectionEight.AffineTLift.thetaGA B.bA F ρ) WordCohBridge.gammaGen.x₁) = 1

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

theorem GQ2.SectionNine.blockProjF_markC_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) (B : BoundaryMaps) (F : BoundaryFrame H E) (ρ : BoundaryLifts B.bA F (blockFrame T Blk hE2).TC) : (blockProjF T Blk) (WordCohBridge.markC (SectionEight.AffineTLift.thetaGA B.bA F ρ)).σ = (headTameSurj T Blk F) tameSigma

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

theorem GQ2.SectionNine.blockProjF_markC_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) (B : BoundaryMaps) (F : BoundaryFrame H E) (ρ : BoundaryLifts B.bA F (blockFrame T Blk hE2).TC) : (blockProjF T Blk) (WordCohBridge.markC (SectionEight.AffineTLift.thetaGA B.bA F ρ)).τ = (headTameSurj T Blk F) tameTau

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

theorem GQ2.SectionNine.blockProjF_markC_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) (B : BoundaryMaps) (F : BoundaryFrame H E) (ρ : BoundaryLifts B.bA F (blockFrame T Blk hE2).TC) : (blockProjF T Blk) (WordCohBridge.markC (SectionEight.AffineTLift.thetaGA B.bA F ρ)).x₀ = 1

The head projection of the markC θ x₀-slot is 1 (the wild generators die at the tame head; the ramified twin's stage 2).

theorem GQ2.SectionNine.blockProjF_markC_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) (B : BoundaryMaps) (F : BoundaryFrame H E) (ρ : BoundaryLifts B.bA F (blockFrame T Blk hE2).TC) : (blockProjF T Blk) (WordCohBridge.markC (SectionEight.AffineTLift.thetaGA B.bA F ρ)).x₁ = 1

The head projection of the markC θ x₁-slot is 1 (the wild generators die at the tame head; the ramified twin's stage 2).

theorem GQ2.SectionNine.gaussZResidueD_gammaA_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) (B : BoundaryMaps) (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 B.bA F (blockEnrichmentD T Blk hE2 F) l h (-2 ^ m)

hGaussZA at the head-inflated enrichment, unramified case (P4d): for the block enrichment blockEnrichmentD, GaussZResidue B.bA F (blockEnrichmentD …) l h (−2^m) with no per-lift tame package — the dichotomy hypothesis is the head-level F.alpha tameTau-triviality, uniform in ρ.

theorem GQ2.SectionNine.gaussZResidueD_gammaA_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) (B : BoundaryMaps) (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 B.bA F (blockEnrichmentD T Blk hE2 F) l h (2 ^ m)

hGaussZA at the head-inflated enrichment, ramified case (P4d): inertia moves the module at the head — GaussZResidue B.bA F (blockEnrichmentD …) l h (+2^m), no per-lift package.

P4e: the hypothesis-free G0-obtain at the head-inflated enrichment

The ⟨G0, hGaussZA, hGaussZF⟩-obtain of the ThmFourTwo R-stage lane, at En := blockEnrichmentD: m comes free from the nonsingular form (A-4.6b), and the un/ramified dichotomy is a single by_cases on the head-level F.alpha tameTau-action — ρ- and source-uniform, so ONE case split serves all four twin applications. D6 is the global tateDuality 2; the tame-unit orientation (needed by the local ramified twin) is carried as a hypothesis — it is provable at the concrete boundaryMapsWitness (tameUnitOrientation_witness), the P5 consumer's discharge point.

theorem GQ2.SectionNine.gaussZ_obtain_blockD {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] [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] [IsTopologicalGroup AbsGalQ2] (hE2 : ∀ (e : E), e ^ 2 = 1) (B : BoundaryMaps) (F : BoundaryFrame H E) (R : LocalReciprocity) (horient : TameUnitOrientation R B.tameF) (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) : ∃ (G0 : ℤ), (∀ (l : (blockFrame T Blk hE2).DR) (h : l ≠ (blockFrame T Blk hE2).zeroDR), SectionEight.GaussZResidue B.bA F (blockEnrichmentD T Blk hE2 F) l h G0) ∧ ∀ (l : (blockFrame T Blk hE2).DR) (h : l ≠ (blockFrame T Blk hE2).zeroDR), SectionEight.GaussZResidue B.bF F (blockEnrichmentD T Blk hE2 F) l h G0

The G0-obtain at blockEnrichmentD (P4e): shared G0 = ∓2^m with the four gaussZResidueD_* twins dispatched by the head dichotomy.