The local GaussZResidue twins at the head-inflated enrichment

The local side of the head-inflation reshape (docs/orchestration/p16d6e4aA-p4-tame-package.md §3): the two gaussZResidue_local_* twins of GQ2/GaussZFinal.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:

• blockEnrichmentD's datum is definitionally (blockDatHV).reindexHom blockProjF, so Q0loc transports down Q0loc_reindexHom_hom (the MonoidHom-level variant of the banked Q0loc_reindexHom) from (dat, ρ.1.1) to (blockDatHV, blockProjF ∘ ρ.1.1);
• the boundary equation's head component (boundaryLift_head_local) identifies blockProjF ∘ ρ.1.1 = cF ∘ B.tameF with the fixed surjection cF := mk' ∘ F.alpha — tame-factored uniformly in ρ;
• the workers sum_sign_Q0loc_{unramified,ramified} then run at C := HVq T Blk, where hfaith is hvAct_faithful (true by construction) and the invariance/simplicity inputs are the hv_inv/hv_simple transports;
• the V^{C₀} = 0 freeness runs on hfix_of_simple_nt (no hfaith at Y⧸K — it is false there whenever K < L_Y).

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

The MonoidHom-level Q0loc reindexing transport

theorem GQ2.SectionNine.Q0loc_reindexHom_hom {C C' : Type} [Group C] [TopologicalSpace C] [Group C'] [TopologicalSpace C'] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [DistribMulAction AbsGalQ2 V] [DistribMulAction C V] [DistribMulAction C' V] (D : TateDuality 2) (dat : FactorSet C V) (φ : C' →* C) (hφ : ∀ (c' : C') (v : V), c' • v = φ c' • v) (ρ' : AbsGalQ2 →ₜ* C') (ρc : AbsGalQ2 →ₜ* C) (hρc : ∀ (g : AbsGalQ2), ρc g = φ (ρ' g)) (x : ContCoh.H1 AbsGalQ2 V) : SectionSix.Q0loc D (dat.reindexHom ⇑φ) ρ' x = SectionSix.Q0loc D dat ρc x

Q0loc reindexing along a MonoidHom-composite (the P4c transport): Q⁰_loc of the φ-reindexed datum along ρ' equals Q⁰_loc of the datum along any continuous hom ρc whose values are φ ∘ ρ'. The MonoidHom-level variant of the banked ShapiroDeepness.Q0loc_reindexHom (which requires φ bundled continuous); here φ is a plain →* and the composite is supplied as ρc, matching the blockProjF-composite construction.

The twins

noncomputable def GQ2.SectionNine.headTameSurj {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) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (F : BoundaryFrame H E) : ↑Ttame.toProfinite.toTop →ₜ* HVq T Blk

The fixed tame surjection into the faithful head quotient (cF := mk'(headActKer) ∘ F.alpha), shared by the four gaussZResidueD_* twins (this file and GQ2/GaussZ/GammaAD.lean); the target carries the ⊥-topology of the twins' letI-pack.

Equations

• GQ2.SectionNine.headTameSurj T Blk F = { toMonoidHom := (QuotientGroup.mk' (GQ2.SectionNine.headActKer T Blk)).comp F.alpha.toMonoidHom, continuous_toFun := ⋯ }

theorem GQ2.SectionNine.headTameSurj_surjective {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) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (F : BoundaryFrame H E) : Function.Surjective ⇑(headTameSurj T Blk F)

headTameSurj is surjective (mk' after the surjective F.alpha).

theorem GQ2.SectionNine.gaussZResidueD_local_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) (D6 : TateDuality 2) (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.bF F (blockEnrichmentD T Blk hE2 F) l h (-2 ^ m)

hGaussZF at the head-inflated enrichment, unramified case (P4c): for the block enrichment blockEnrichmentD, GaussZResidue B.bF 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_local_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) (D6 : TateDuality 2) (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) (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.bF F (blockEnrichmentD T Blk hE2 F) l h (2 ^ m)

hGaussZF at the head-inflated enrichment, ramified case (P4c): inertia moves the module at the head — GaussZResidue B.bF F (blockEnrichmentD …) l h (+2^m), no per-lift package; the local side carries the tame-unit orientation as before.