Final assembly of lemma_6_17_vanish — wiring bricks

The capstone composing f2a (datum-independence) + Lemma 6.14 (RepIndependence.lemma_6_14) + f2b (the orbit decomposition regular_isometric_embedding_orbit) + f2c (hcoh/hvanish) through OrbitVanish.Q0loc_vanish_of_datum_decomp, then the SectionSix statement-move.

This file begins with the mechanical wiring bricks — independent of the open f2a/f2c1/f2c2 mathematics, buildable now. f2b's orbit datum lives over G ⧸ N while the ambient Q0loc / Lemma-6.14 transport is over C; the assembly reindexes the datum along e : C ≃* G ⧸ N (the FactorSet.reindexHom/Q0loc_reindexHom bridge proved in ShapiroDeepness). These two bricks say reindexHom distributes over sumDatum and preserves equivariance under the φ-pullback action — the two facts needed to feed the reindexed orbit sum into the reducer.

theorem GQ2.VanishClose.reindexHom_sumDatum {C : Type u_1} {C' : Type u_2} {V : Type u_3} {ι : Type u_4} (s : Finset ι) (datf : ι → FactorSet C V) (φ : C' → C) : (OrbitVanish.sumDatum s datf).reindexHom φ = OrbitVanish.sumDatum s fun (o : ι) => (datf o).reindexHom φ

reindexHom distributes over sumDatum (the Lemma 6.17 vanishing proof wiring): reindexing a datum sum's acting group along φ is the sum of the reindexed per-orbit data. Both sides have the same factor set (f is untouched by reindexHom) and the same corrections (m pre-composes φ inside each summand), so this is definitional.

theorem GQ2.VanishClose.isEquivariantFactorSet_reindexHom {C : Type u_1} {C' : Type u_2} {V : Type u_3} [Group C] [Group C'] [AddCommGroup V] [DistribMulAction C V] [DistribMulAction C' V] {q : V → ZMod 2} {dat : FactorSet C V} (h : IsEquivariantFactorSet q dat) (φ : C' →* C) (hφ : ∀ (c' : C') (v : V), c' • v = φ c' • v) : IsEquivariantFactorSet q (dat.reindexHom ⇑φ)

Equivariance is preserved under reindexHom (the Lemma 6.17 vanishing proof wiring): if dat is an equivariant factor set for q over C, φ : C' →* C is a group hom, and the C'-action on V is the φ-pullback of the C-action (hφ), then dat.reindexHom φ is an equivariant factor set for q over C'. The factor-set clauses are inherited verbatim (f unchanged); the correction clauses (59)/(60) transport by φ's multiplicativity and the hφ action identity.

The classifying equivalence e : C ≃* AbsGalQ2 ⧸ ker ρ

noncomputable def GQ2.VanishClose.eOfSurj {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (hρsurj : Function.Surjective ⇑ρ) : C ≃* AbsGalQ2 ⧸ ρ.ker

The classifying equivalence e : C ≃* AbsGalQ2 ⧸ ker ρ (the Lemma 6.17 vanishing proof): for a surjective ρ, the inverse of the first-isomorphism AbsGalQ2 ⧸ ker ρ ≃* C. It is what f2b's regular_isometric_embedding_orbit consumes to give the regular module W = Fin K → RegRep (ker ρ) its C-view (the e-pullback of the canonical G ⧸ N-action).

Equations

• GQ2.VanishClose.eOfSurj ρ hρsurj = (QuotientGroup.quotientKerEquivOfSurjective ρ.toMonoidHom hρsurj).symm

theorem GQ2.VanishClose.eOfSurj_rho {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (hρsurj : Function.Surjective ⇑ρ) (g : AbsGalQ2) : (eOfSurj ρ hρsurj) (ρ g) = ↑g

e ∘ ρ = mk' (the Lemma 6.17 vanishing proof): the classifying equivalence sends ρ g back to its coset, so e composed with ρ is the quotient map. This is the identity that turns the C-level reindexed pullback into the mk' N-level orbit map (where lemma_6_15_* are stated) and supplies the Q0loc/reducer compatibility hρW : g • w = ρ g • w on W.

The final assembly of lemma_6_17_vanish

Compose f2a (datum-independence) + Lemma 6.14 + f2b (regular embedding) + f2c1 (hcoh_*) + the deep-class vanishing (hvanish_cup square/free, InvolutionSplice.hvanish_involution_ker involution) through OrbitVanish.Q0loc_vanish_of_datum_decomp. The W = Fin K → RegRep (ker ρ) instances are letI-supplied on the base RegRep (ker ρ) (so f2c1's RegRep-instance arguments resolve and the block module's action is the Pi-lift); RegRep's opacity blocks the global trivial AbsGalQ2-action, so this is clean.

theorem GQ2.VanishClose.out_notMem_and_out_sq_mem (N : Subgroup AbsGalQ2) [N.Normal] {w : AbsGalQ2 ⧸ N} (hw2 : w * w = 1) (hwne : w ≠ 1) : Quotient.out w ∉ N ∧ Quotient.out w * Quotient.out w ∈ N

Out-lift of an order-2 nontrivial coset is a non-N involution mod N (the Lemma 6.17 vanishing proof wiring): for w : AbsGalQ2 ⧸ N with w * w = 1 and w ≠ 1, the section lift Quotient.out w lies outside N yet squares into N. The involution-position fact shared by the three Sum.inr (Sum.inl _) orbit branches of the final assembly.

theorem GQ2.VanishClose.evensNormFun_orbit_mem_Z2 (N : Subgroup AbsGalQ2) [N.Normal] (hNopen : IsOpen ↑N) (g : AbsGalQ2) (hgN : g ∉ N) (hg2 : g * g ∈ N) (β : AbsGalQ2 → RegRep N) (hZ1 : ShapiroRead.shapiroCoord N β ∈ ContCoh.Z1 (↥N) (ZMod 2)) : (evensNormFun (N.subgroupOf (N ⊔ Subgroup.zpowers g)) ⟨g, ⋯⟩ fun (w : ↥(N.subgroupOf (N ⊔ Subgroup.zpowers g))) => ShapiroRead.shapiroCoord N β ⟨↑↑w, ⋯⟩) ∈ ContCoh.Z2 (↥(N ⊔ Subgroup.zpowers g)) (ZMod 2)

The involution orbit's inner cochain is a 2-cocycle (the Lemma 6.17 vanishing proof wiring): the evensNormFun splice attached to an involution coset g ∉ N, g² ∈ N on the index-2 pair N ≤ N ⊔ ⟨g⟩, built from a block cocycle shapiroCoord N β, is a Z². Discharges the Sum.inr (Sum.inl _) branch of the hZ2 obligation.

theorem GQ2.VanishClose.hvanish_free_conj {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] (ρ : AbsGalQ2 →ₜ* C) (β γ : AbsGalQ2 → RegRep ρ.ker) (g : AbsGalQ2) (hZβ : ShapiroRead.shapiroCoord ρ.ker β ∈ ContCoh.Z1 (↥ρ.ker) (ZMod 2)) (hZγ : ShapiroRead.shapiroCoord ρ.ker γ ∈ ContCoh.Z1 (↥ρ.ker) (ZMod 2)) (hDβ : H1ofFun (↥ρ.ker) (ShapiroRead.shapiroCoord ρ.ker β) ∈ LocalKummer.deepClasses ρ.ker) (hDγ : H1ofFun (↥ρ.ker) (ShapiroRead.shapiroCoord ρ.ker γ) ∈ LocalKummer.deepClasses ρ.ker) : H2ofFun (↥ρ.ker) (ContCoh.cup11Fun AddMonoidHom.mul (ShapiroRead.shapiroCoord ρ.ker β) fun (n : ↥ρ.ker) => ShapiroRead.shapiroCoord ρ.ker γ (LocalKummer.conjMap ρ g n)) = 0

The free orbit's inner cochain vanishes in H² (the Lemma 6.17 vanishing proof wiring): the cup product of a deep ker ρ-block cocycle with the g-conjugate of another deep block cocycle is an H²-coboundary. Discharges the Sum.inr (Sum.inr _) branch of the hvanish obligation.

theorem GQ2.VanishClose.lemma_6_17_vanish_final {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction AbsGalQ2 V] [ContinuousSMul AbsGalQ2 V] [DistribMulAction C V] (D : TateDuality 2) (R : LocalReciprocity) (B : BoundaryMaps) (c : ↑Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : AbsGalQ2 →ₜ* C) (hfac : ∀ (g : AbsGalQ2), ρ g = c (B.tameF g)) (horient : TameUnitOrientation R B.tameF) (hρ : ∀ (g : AbsGalQ2) (v : V), g • v = ρ g • v) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ (v : V), c tameTau • v ≠ v) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hinv : QuadraticFp2.IsInvariant C q) (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (x : ContCoh.H1 AbsGalQ2 V) (hx : x ∈ SectionSix.deepPart ρ) : SectionSix.Q0loc D dat ρ x = 0

lemma_6_17_vanish, closed downstream (the Lemma 6.17 vanishing proof): the base connecting map Q⁰loc vanishes on the deep half, from lemma_6_17_vanish's own hypotheses plus the reciprocity datum (R, horient) threaded per the c2c4 consumer note (the architecture review flag).

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

• Lemma 6.14 = ⟦lem-regularrealization⟧