The local GaussZResidue discharge (the e7 composition)

gaussZ_reduction (layer (I), GaussZReduction.lean) ∘ the H¹-transport (h1OfVQuot + QZeroBar_eq_Q0loc, GaussZLocal.lean) ∘ the pinned values (sum_sign_Q0loc_unramified/_ramified): for every boundary lift ρ of the local source,

∑ᶠ c : Z¹_{G_ℚ₂,ρ'}(V), sign(Q⁰ c) = #V · G0, G0 = −2^m (unram) / +2^m (ram)

— GaussZResidue B.bF F En l h G0 verbatim, i.e. prop_8_9's hGaussZF at the pinned value (design: docs/orchestration/p16d6e4a-evaluation-design.md §1 + §"Hypothesis supply").

• The tame factorization is packaged per boundary lift (hpack): each lower map ρ.1.1 : G_ℚ₂ → Y_C factors through B.tameF by a surjective c : Ttame → Y_C carrying the uniform un/ramified dichotomy on V. This is the single genuinely structural input beyond the En-form data — the §9 consumer derives it from the block's tame package (c3-G0 layer).
• Finiteness of Z¹ is σ-free via the e3 count hZcard_local (#Z¹ = #V² ≠ 0), so the discharge holds at every (l, h) — no descent datum needed (gaussZ_reduction was generalized to a [Finite Z¹] hypothesis accordingly).
• The AbsGalQ2-module structure on V is installed per-ρ by the letI-pullback along the lower map (the compHom idiom), making the bridge hypotheses (hcomp/hρ) rfl.
• The Γ_A twin (hGaussZA) has no prop_6_18-analog and stays on the prop_8_9 ledger — the sanctioned deferral (design §2), discharged by (83)-for-Γ_A or carried to the ThmFourTwo consumer.

The two theorems share their spine verbatim (the letI-instances are proof-local, so the pinned step cannot be abstracted into a common core without Π-over-instances noise).

theorem GQ2.SectionEight.AffineTLift.gaussZResidue_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] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} (B : BoundaryMaps) (F : BoundaryFrame H E) (En : RF.Enrichment) (D6 : TateDuality 2) (hsimple : ∀ (W : AddSubgroup En.Vmod), (∀ (g : RF.YC), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hVne : ∃ (v : En.Vmod), v ≠ 0) (hnt : ∃ (g : RF.YC) (v : En.Vmod), g • v ≠ v) (hfaith : ∀ (g : RF.YC), (∀ (v : En.Vmod), g • v = v) → g = 1) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card En.Vmod = 2 ^ (2 * m)) (l : RF.DR) (h : l ≠ RF.zeroDR) (hpack : ∀ (ρ : BoundaryLifts B.bF F RF.TC), ∃ (c : ↑Ttame.toProfinite.toTop →ₜ* RF.YC), Function.Surjective ⇑c ∧ (∀ (g : AbsGalQ2), ↑↑ρ g = c (B.tameF g)) ∧ ∀ (v : En.Vmod), c tameTau • v = v) : GaussZResidue B.bF F En l h (-2 ^ m)

hGaussZF, unramified case (the Prop. 8.9 assembly): with a per-lift tame package whose inertia acts trivially on V, GaussZResidue B.bF F En l h (−2^m) — the prop_8_9 ledger hypothesis at the pinned unramified value.

theorem GQ2.SectionEight.AffineTLift.gaussZResidue_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] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} (B : BoundaryMaps) (F : BoundaryFrame H E) (En : RF.Enrichment) (D6 : TateDuality 2) (R : LocalReciprocity) (horient : TameUnitOrientation R B.tameF) (hsimple : ∀ (W : AddSubgroup En.Vmod), (∀ (g : RF.YC), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hVne : ∃ (v : En.Vmod), v ≠ 0) (hnt : ∃ (g : RF.YC) (v : En.Vmod), g • v ≠ v) (hfaith : ∀ (g : RF.YC), (∀ (v : En.Vmod), g • v = v) → g = 1) (m : ℕ) (hm : 1 ≤ m) (hcard : Nat.card En.Vmod = 2 ^ (2 * m)) (l : RF.DR) (h : l ≠ RF.zeroDR) (hpack : ∀ (ρ : BoundaryLifts B.bF F RF.TC), ∃ (c : ↑Ttame.toProfinite.toTop →ₜ* RF.YC), Function.Surjective ⇑c ∧ (∀ (g : AbsGalQ2), ↑↑ρ g = c (B.tameF g)) ∧ ∃ (v : En.Vmod), c tameTau • v ≠ v) : GaussZResidue B.bF F En l h (2 ^ m)

hGaussZF, ramified case (the Prop. 8.9 assembly): with a per-lift tame package whose inertia moves V, GaussZResidue B.bF F En l h (+2^m) — the prop_8_9 ledger hypothesis at the pinned ramified value.