The local (140) residues for G_ℚ₂

For the local source Γ = G_ℚ₂ = AbsGalQ2, this file proves the per-source residues consumed by the source-generic phase140_from_residues in GQ2/Phase140Assembly.lean: hsep, hpartial, hZcard, and hμ (the T-cocycle count). hGaussZ is supplied separately (kept as a hypothesis here); htriv/hH2 are discharged locally (htriv_local' / card_H2_zmod2_eq_two).

#print axioms phase140_local is contained in the standard three axioms together with B6 (tateDualityAt) and B7 (absGalQ2_localEulerCharacteristic). The four residues are htriv_local', vFixedPts_eq_one, the two counting residues tcocycle_card_local (the hμ supplier) and hZcard_local; the deep separation residue hsep_local (7 stages: Additive T module → tDef ∈ Z² → dual/hpair → cup20-bridge with the χ↔n∈TCharC invariance transport → bijective_cup20 injectivity → B²-extraction → the direct M-lift f γ = ψγ·fLift γ); and — the last one — the nondegeneracy residue hpartial_local (contrapositive: ∀c, betaChi χ c = betaChi χ 0 ⟹ split χ∘mDef by gχ → the cup part iotaB- vanishes → the dual-connecting cochain ξ is a Z¹(Γ, ElemDual V) whose every cup value vanishes → [ξ]=0 by cup11 right-slot separation → ξ = ∂n → build the invariant M-character ψ(m) = χ(t-part m) + (gχ+n)(V-part m) (additive; Y-conjugation-invariant via bb=uσ(cc)·k, k∈M, M abelian, collapsing to hkey) → ψ = 0 by Half139Local.mchar_conj_invariant_eq_zero ((M∨)^C = 0, Lemma 7.1) → χ = 0, contradiction). The theorem hZcard_local requires hnt : ∃ g v, g • v ≠ v; the other module hypotheses alone do not imply this nontriviality condition, as explained in its declaration below.

The four residues follow two common patterns for the local source:

• the counting residues hμ and hZcard mirror hMcountM_local (GQ2/Half139Local.lean): build the additive 𝔽₂-module of the layer (T resp. V) with the ρ'-conjugation AbsGalQ2-action, bridge the crossed cocycles to Z¹_cont, apply card_Z1_eq (5.16 clause (ii), B7), and evaluate the fixedPts factor;
• the separation residues hsep and hpartial mirror hsep_hom_local (GQ2/RStageLocal.lean): the (T^∨)^C-perfectness of the T-obstruction pairing from prop_5_16 cup clauses (vi)/(iv)/(v) + a B²-extraction.

All four are ∀ ρ-parametric over the C-boundary lifts, in exactly the shape phase140_from_residues consumes; the assembly phase140_local wires them (plus the ledger hGaussZ) into the RecursionInputs.phase140-field display.

Axiom use: ⊆ {B6, B7} — B6/B7 via card_Z1_eq / card_H2_eq_fixedPts, exactly as in hMcountM_local/hZcount_local.

theorem GQ2.SectionEight.htriv_local' [DistribMulAction AbsGalQ2 (ZMod 2)] (γ : AbsGalQ2) (m : ZMod 2) : γ • m = m

The G_ℚ₂-action on 𝔽₂ is trivial (any group action on ZMod 2 fixes both elements). A self-contained copy of RStageLocal.htriv_local, inlined to keep this leaf's imports lean.

The shared T-module pack

Both T-layer residues below (tcocycle_card_local and hsep_local) run the same module setup: the polar radical T ≤ M of a RadicalCoverData is elementary abelian (M abelian and 2-torsion), additivized to an 𝔽₂-space carrying the conjugation action of the coset group Bg ⧸ M through Quotient.out representatives. The pack is extracted here once (the mbCommGroup/mbConjActC idiom of MStageCountGammaA); the residues install it by letI/have and diverge at their count/separation tails.

theorem GQ2.SectionEight.tcocycle_card_local {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} [IsTopologicalGroup AbsGalQ2] (b : AbsGalQ2 →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : BoundaryLifts b F RF.TC) : Nat.card (CentralObstruction.TCocycle (En.radData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)) = Nat.card (Additive ↥(En.radData l h).T) ^ 2 * Nat.card ↑(FoxH.fixedPts (RF.YB ⧸ (En.radData l h).M) (FoxH.ElemDual (Additive ↥(En.radData l h).T)))

The T-cocycle count for G_ℚ₂ (the hμ supplier, the Prop. 8.9 assembly): the crossed-T-cocycle count is the card_Z1_eq closed form #T² · #(T^∨)^{YB/M_B}, which is ρ-independent (the RHS sees only the frame-level datum En.radData l h, not ρ) — so the capstone reads off μ₀ and hμ := fun ρ => tcocycle_card_local … ρ. Mirrors hMcountM_local steps 1–3 at A := Additive (En.radData l h).T, but with a direct TCocycle ≃ Z¹_cont bridge (TCocycle stores continuity into Bg directly, and is always nonempty — no torsor/Nonempty detour).

theorem GQ2.SectionEight.vFixedPts_eq_one {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} (En : RF.Enrichment) (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) : Nat.card ↑(FoxH.fixedPts RF.YC (FoxH.ElemDual En.Vmod)) = 1

No YC-invariant functionals on V: #(V^∨)^{YC} = 1 — the fixedPts factor of the hZcard card_Z1_eq count. From DualityAssembly.card_fixedPts_elemDual_eq_one_of_nontrivial, packaging the ledger hsimple/hVne as IsSimpleModTwo RF.YC En.Vmod and the nontrivial action hnt. (Self-contained; no cocycle bridge needed — the crux of hZcard_local.)

theorem GQ2.SectionEight.hZcard_local {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 : AbsGalQ2 →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (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) (ρ : BoundaryLifts b F RF.TC) : Nat.card (AffineTLift.VCocycle (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)) = Nat.card En.Vmod * Nat.card En.Vmod

hZcard for G_ℚ₂ — #Z¹_{Γ,ρ'}(V) = #V². Mirrors hMcountM_local at A := En.Vmod (which already carries the RF.YC-action of the enrichment) with the descent lower map rho0 = ρ.1.1 (rho0_descData_rhoPrime, surjective since ρ is a ContSurj), building the VCocycle ≃ Z¹_cont(AbsGalQ2, En.Vmod) bridge and applying card_Z1_eq (5.16 clause (ii)) to get #V² · #fixedPts RF.YC (ElemDual En.Vmod); the fixedPts factor is 1 by vFixedPts_eq_one. The proof follows the bridge and module-instance setup from hMcountM_local at A := En.Vmod.

The hypothesis hnt (a nontrivial action) is necessary and is not derivable from hsimple/hfaith/hVne alone: in the corner #V = 2 ∧ YC = 1 the ledger is satisfiable (𝔽₂ is a faithful — vacuously — simple 𝔽₂[1]-module) yet #(V^∨)^{YC} = 2 ≠ 1, so hZcard is FALSE there. hnt (equivalently Nontrivial RF.YC, via hfaith) rules it out and is discharged at the capstone from the block's chief-factor structure (the ramified regular summand has a nontrivial YC-action).

theorem GQ2.SectionEight.hsep_local {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} [IsTopologicalGroup AbsGalQ2] [DistribMulAction AbsGalQ2 (ZMod 2)] [ContinuousSMul AbsGalQ2 (ZMod 2)] (b : AbsGalQ2 →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (Dsc : AffineTLift.Descent (En.radData l h)) (ρ : BoundaryLifts b F RF.TC) (c : AffineTLift.VCocycle (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)) (hc : ∀ (χ : ↥(AffineTLift.TCharC (En.radData l h))), AffineTLift.betaChi (descSections En l h Dsc) ⋯ χ c = 0) : AffineTLift.TLiftable ⋯ c

hsep for G_ℚ₂ — the (T^∨)^C-separation: a V-coordinate with all χ-obstructions betaChi χ c = 0 is T-liftable. The converse of the generic betaChi_of_tliftable (VLiftCount.lean); the hsep_hom_local pattern (prop_5_16 cup clause (vi) cup20-bijectivity

• B²-extraction) at the T-module through the M-lift obstruction.

Proof outline (mirroring RStageLocal.hsep_hom_local at the T-layer):

1. Module. A := Additive ↥(En.radData l h).T with the rhoPrime-conjugation AbsGalQ2-action, using tcocycle_card_local's setup (conj_eq_of_mk_eq_T, tCommGroup, actC/actG, hcomp, hsmul, ContinuousSMul, hA₂), same module as the T-count.
2. T-valued defect cocycle tDefZ2 : (fun p => Additive.ofMul (tDef S hσ c p)) ∈ Z2 AbsGalQ2 A — extract from chiDef_mem_Z2's hraw/hsub (VLiftCount.lean:234-252), BEFORE pushing through χ; the γ• in the Z2 identity is conjugation by fLift γ (a rep of ρ'γ, so = actG-action by conj_eq_of_mk_eq_T).
3. Dual module ElemDual A + hpair — copy hsep_hom_local:466-486 (compHom θ, ⊥ topology, hpair via htriv_local' + ElemDual.smul_apply + inv_smul_smul).
4. cup20-values vanish ∀ n : H0 AbsGalQ2 (ElemDual A), cup20 (dualEval A) hpair (H2mk … ⟨_,tDefZ2⟩) n = 0: cup20 [tDef] n = H2mk (fun gd => dualEval (tDef gd) ((gd.1*gd.2)•n)) (congrArg H2mk, as in hsep_hom_local:hred); n.2-invariance ⟹ = H2mk (fun gd => n(tDef gd)) = H2mk (chiDef χ_n c) where χ_n : ↥(TCharC D) := ⟨fun t => n.1 (Additive.ofMul t), ⟨additivity, conj-inv via θ-surj⟩⟩ (the hYinv transport, hsep_hom_local:493-512); then hc χ_n : betaChi χ_n c = 0 gives chiDef χ_n c ∈ B² (iotaB_eq_zero_iff), so H2mk (chiDef χ_n c) = 0 (H2mk_eq_zero_iff).
5. Class vanishes H2mk … ⟨_,tDefZ2⟩ = 0 via (bijective_cup20_dualEval hA₂ htriv_local' hpair).1 (injectivity) + map_zero + AddMonoidHom.ext over stage 4.
6. B²-extraction: (QuotientAddGroup.eq_zero_iff _).mp + mem_addSubgroupOf ⟹ ψ : AbsGalQ2 → A continuous with dOne ψ = tDef (hsep_hom_local:541-543).
7. Direct lift (the genuinely NEW part — no homLift_of_split for the abstract-D MLifts layer): f γ := (Additive.toMul (ψ γ) : Bg) * fLift S c γ; a continuous hom over ρ' (dOne ψ = tDef cancels the fLift-defect, exponent-2 kills the sign as in :554-563; ψ ∈ T ⊆ M so mk_M (f γ) = mk_M (fLift γ) = ρ'γ), and mk_T (f γ) = mk_T (fLift γ) = (qOfCocycle c) γ (since ψ ∈ T) ⟹ redTLift f = qOfCocycle c ⟹ TLiftable. Bespoke ~40 lines.

theorem GQ2.SectionEight.cup11_dualEval_right_separating [DistribMulAction AbsGalQ2 (ZMod 2)] {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [Finite A] [DistribMulAction AbsGalQ2 A] [ContinuousSMul AbsGalQ2 A] [TopologicalSpace (FoxH.ElemDual A)] [DiscreteTopology (FoxH.ElemDual A)] [DistribMulAction AbsGalQ2 (FoxH.ElemDual A)] [ContinuousSMul AbsGalQ2 (FoxH.ElemDual A)] (hA₂ : ∀ (a : A), a + a = 0) (htriv : ∀ (γ : AbsGalQ2) (m : ZMod 2), γ • m = m) (hpair : ∀ (γ : AbsGalQ2) (a : A) (lam : FoxH.ElemDual A), ((FoxH.dualEval A) (γ • a)) (γ • lam) = γ • ((FoxH.dualEval A) a) lam) (ξ : ContCoh.H1 AbsGalQ2 (FoxH.ElemDual A)) (hvan : ∀ (z : ContCoh.H1 AbsGalQ2 A), ((ContCoh.cup11 (FoxH.dualEval A) hpair) z) ξ = 0) : ξ = 0

cup11 right-slot separation (clause (iv), vanishing-detector form): a degree-1 ElemDual-class killed by the evaluation cup against every H¹(A)-class is zero. Mirrors bijective_cup11_dualEval's internals (cup11_comm slot swap + B6 perfect11 injectivity on the MuDual side); stated separately because the bijective form detects in the left slot while hpartial needs the right.

theorem GQ2.SectionEight.hpartial_local {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} [IsTopologicalGroup AbsGalQ2] [DistribMulAction AbsGalQ2 (ZMod 2)] [ContinuousSMul AbsGalQ2 (ZMod 2)] (b : AbsGalQ2 →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (Dsc : AffineTLift.Descent (En.radData l h)) (ρ : BoundaryLifts b F RF.TC) (χ : ↥(AffineTLift.TCharC (En.radData l h))) (hχ : χ ≠ 0) : ∃ (c : AffineTLift.VCocycle (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)), AffineTLift.betaChi (descSections En l h Dsc) ⋯ χ c ≠ AffineTLift.betaChi (descSections En l h Dsc) ⋯ χ 0

hpartial for G_ℚ₂ — nondegeneracy of the obstruction pairing in the character: every nonzero χ ∈ (T^∨)^C is detected by some V-coordinate. Cup-duality clauses (iv)/(v) of prop_5_16.

RECIPE: d(c) := betaChi χ c - betaChi χ 0 is ADDITIVE in c (betaChi_affine, KeystoneDelta.lean:1172), so the goal ∃ c, d(c) ≠ 0 is "the additive map d : VCocycle → 𝔽₂ is nonzero". d is the cup pairing of χ (as H⁰(ElemDual A), via the stage-4 χ ↔ n identification of hsep_local) against the class-of-c-defect in H¹/H²; by the perfect (1,1)/(0,2) pairings (bijective_cup11_dualEval / bijective_cup02_dualEval, clauses (iv)/(v), LocalLiftingDuality.lean:359/409) a NONZERO χ is detected by some class — i.e. d ≠ 0. Contrapositive form: if d = 0 (all c give betaChi χ c = betaChi χ 0) then χ = 0 by the injectivity half of the perfect pairing, contradicting hχ. The ∂-surjectivity (that the c ↦ defect-class map hits enough of H¹/H² to realize the pairing) is the substantive step, dual to hsep's bijective_cup20 injectivity. Couples to hsep_local's stage-1–4 infrastructure (same module A, dual, and χ ↔ n bridge).

The local (140) display

theorem GQ2.SectionEight.phase140_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} {RF : RecursionFrame T Blk} [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] [IsTopologicalGroup AbsGalQ2] [DistribMulAction AbsGalQ2 (ZMod 2)] [ContinuousSMul AbsGalQ2 (ZMod 2)] (b : AbsGalQ2 →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (Dsc : AffineTLift.Descent (En.radData l h)) (hfg : ∃ (s : Finset AbsGalQ2), (Subgroup.closure ↑s).topologicalClosure = ⊤) (μ₀ : ℕ) (G0 : ℤ) (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) (hμ : ∀ (ρ : BoundaryLifts b F RF.TC), Nat.card (CentralObstruction.TCocycle (En.radData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)) = μ₀) (hGaussZ : ∀ (ρ : BoundaryLifts b F RF.TC), ∑ᶠ (c : AffineTLift.VCocycle (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)), sign (AffineTLift.QZero (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ) c) = ↑(Nat.card En.Vmod) * G0) : 2 * ↑(Nat.card ↥(AffineTLift.TCharC (En.radData l h))) * ↑(RF.zBC b F l h) = ↑(Nat.card En.Vmod * μ₀) * (↑(Nat.card ↥RF.MB / Nat.card ↥RF.TBsub) * ↑(exactImageCount b F RF.TC) + G0 * ∑ᶠ (ζ : ↥(AffineTLift.TCharC (En.radData l h))), (2 * ↑(RF.nPhase b F (phaseChi En l h Dsc ζ)) - ↑(exactImageCount b F RF.TC)))

The RecursionInputs.phase140 field for G_ℚ₂: the source-generic phase140_from_residues with htriv/hH2 discharged locally and the four per-source residues supplied by the lemmas above. hGaussZ, μ₀, G0, and the module hypotheses hsimple/hVne/hnt are supplied by the prop_8_9 assembly in GQ2/Prop89Close.lean.

Paper-tag ledger (auto-generated by paperforge; do not edit)

• Lemma 7.1 = ⟦lem-simplehead⟧