The involution hvanish in ker ρ-vocabulary (the U₀-splice)

The last §6.3 input of the lemma_6_17_vanish assembly: for a deep block coordinate α : ↥(ker ρ) → 𝔽₂ and an involution lift ĝ (ĝ ∉ ker ρ, ĝ² ∈ ker ρ, U₀ = ker ρ ⊔ ⟨ĝ⟩), the Evens-norm inner cochain of the reducer's involution orbit vanishes: H²ofFun ↥U₀ (evensNormFun ((ker ρ).subgroupOf U₀) ⟨ĝ,_⟩ (α-restriction)) = 0.

The c2 lane delivers this over the splitting-field tower — hvanish_involution (ShapiroDeepness, via lemma_6_16), the c2a Kummer package (kummer_presentation_of_index_two), and the analytic hunram_involution (UnramifiedBridge, c2c) — all in (k, L) IntermediateField-vocabulary. This file is the splice:

• No Evens-norm cohomology-invariance is needed (the flagged f2d risk dissolves): with trivial coefficients B¹ = 0, so cohomologous scalar cocycles are equal — eq_of_H1ofFun_eq extracts, from the deep-class witness of [α], a square root β with kummerCocycleFun β = α on the nose on ker ρ. The two candidate inner cochains coincide.
• The tower: L := ResidueLift.splitField ρ, k := fixedField (toGal U₀) (the kerGal-idiom carrier copy), with the infinite Galois correspondence recovering k.fixingSubgroup = toGal U₀; [k : ℚ₂] < ∞ from U₀ ⊇ ker ρ open.
• The index-2 bricks: (N.subgroupOf U₀).index = 2 in both views, from the coset decomposition of N ⊔ ⟨ĝ⟩ (N normal, ĝ² ∈ N: every element lands in N ∪ Nĝ⁻¹).
• The carrier splice: evensAux/bS/evensNormFun are Quotient.out-free (membership tests and s-translates only), so the ↥U₀- and ↥k.fixingSubgroup-side Evens cochains agree pointwise under the underlying-identity ι₀; the B²-witness of the field-side vanishing pulls back along ι₀ (the DeepDualityK.kerToFixing pattern), and H2ofFun ↥U₀ … = 0 follows.

The two Galois-group views (AbsGalQ2 vs Kummer.GaloisGroup ℚ_[2]) share their group operations at default transparency; all cross-view steps are rfl-bridges in the kerGal idiom (ResidueLift §Plumbing).

Main result: hvanish_involution_ker — consumed by the lemma_6_17_vanish assembly (docs/orchestration/p15f2d-handoff.md §3) at the involution orbits. R : LocalReciprocity and horient : TameUnitOrientation R B.tameF are threaded per the c2c4 consumer note (the hc/hV2 amendment precedent; the architecture review flag).

Axioms: std-3 + {B5 (via R-instantiation downstream), B9, B11a/b (via lemma_6_16), B13 (dyadicUnitFiltration, via hunram_involution)} — the §6.3 involution budget.

The B¹ = 0 extraction: cohomologous scalar cocycles are equal

theorem GQ2.InvolutionSplice.eq_of_H1ofFun_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod 2)] [ContinuousSMul G (ZMod 2)] (htriv : ∀ (g : G) (m : ZMod 2), g • m = m) {φ ψ : G → ZMod 2} (hφ : φ ∈ ContCoh.Z1 G (ZMod 2)) (hψ : ψ ∈ ContCoh.Z1 G (ZMod 2)) (h : H1ofFun G φ = H1ofFun G ψ) : φ = ψ

Trivial-coefficient rigidity: two continuous 1-cocycles with the same H1ofFun class are equal — B¹(G, 𝔽₂) = 0 for the trivial action, so nothing is identified. This dissolves the feared Evens-norm cohomology-invariance gap: the deep-class witness's Kummer cocycle is the block coordinate.

The index-2 bricks

theorem GQ2.InvolutionSplice.mem_or_mul_mem_of_mem_sup {G : Type u_1} [Group G] {N : Subgroup G} [hNn : N.Normal] {ĝ : G} (hĝ2 : ĝ * ĝ ∈ N) {x : G} (hx : x ∈ N ⊔ Subgroup.zpowers ĝ) : x ∈ N ∨ x * ĝ ∈ N

The coset decomposition of N ⊔ ⟨ĝ⟩ for N normal with ĝ² ∈ N: every element is in N or lands there after one more ĝ.

theorem GQ2.InvolutionSplice.index_eq_two_of_decomp {G : Type u_1} [Group G] {U₀ : Subgroup G} {N' : Subgroup ↥U₀} {s : ↥U₀} (hs : s ∉ N') (hdec : ∀ b ∉ N', b * s ∈ N') : N'.index = 2

Index 2 of the kernel inside the involution overgroup, decomposition form: if ⟨ĝ⟩ ∉ N', and every element outside N' returns to it after multiplying by ⟨ĝ⟩, then N' has index 2.

theorem GQ2.InvolutionSplice.subgroupOf_index_eq_two_of_sup {G : Type u_1} [Group G] {N : Subgroup G} [N.Normal] {ĝ : G} (hĝ2 : ĝ * ĝ ∈ N) {U₀ : Subgroup G} (hU₀ : U₀ = N ⊔ Subgroup.zpowers ĝ) (hmem : ĝ ∈ U₀) (hsUnot : ⟨ĝ, hmem⟩ ∉ N.subgroupOf U₀) : (N.subgroupOf U₀).index = 2

Index 2 of a normal subgroup inside its involution overgroup: for N normal with ĝ² ∈ N, the subgroup N has index 2 inside U₀ = N ⊔ ⟨ĝ⟩ (combining the coset decomposition mem_or_mul_mem_of_mem_sup with index_eq_two_of_decomp).

The Galois-view repackaging (the kerGal idiom, for overgroups of ker ρ)

def GQ2.InvolutionSplice.toGalElem (x : AbsGalQ2) : Kummer.GaloisGroup ℚ_[2]

The identity bridge into the AlgEquiv-view Galois group (inverse of ResidueLift.toAbs; keeps mixed-view products elaborable).

Equations

• GQ2.InvolutionSplice.toGalElem x = x

def GQ2.InvolutionSplice.toGal (U : Subgroup AbsGalQ2) : Subgroup (Kummer.GaloisGroup ℚ_[2])

A subgroup of AbsGalQ2, repackaged in the AlgEquiv-view Galois group (the ResidueLift.kerGal idiom: same carrier; the closure proofs cross the two views' default-transparency-equal group structures by rfl-bridges).

Equations

• GQ2.InvolutionSplice.toGal U = { carrier := {x : GQ2.Kummer.GaloisGroup ℚ_[2] | GQ2.ResidueLift.toAbs x ∈ U}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem GQ2.InvolutionSplice.toGal_isOpen_of_ker_le {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] (ρ : AbsGalQ2 →ₜ* C) {U : Subgroup AbsGalQ2} (hle : ρ.ker ≤ U) : IsOpen ↑(toGal U)

toGal of an overgroup of ker ρ is open (it contains the open kerGal ρ).

The generic H²ofFun-vanishing transport along a continuous multiplicative map

theorem GQ2.InvolutionSplice.H2ofFun_eq_zero_comp {G₁ : Type u_1} {G₂ : Type u_2} [Group G₁] [TopologicalSpace G₁] [IsTopologicalGroup G₁] [DistribMulAction G₁ (ZMod 2)] [ContinuousSMul G₁ (ZMod 2)] [Group G₂] [TopologicalSpace G₂] [IsTopologicalGroup G₂] [DistribMulAction G₂ (ZMod 2)] [ContinuousSMul G₂ (ZMod 2)] (e : G₁ →* G₂) (hec : Continuous ⇑e) (htriv₁ : ∀ (g : G₁) (m : ZMod 2), g • m = m) (htriv₂ : ∀ (g : G₂) (m : ZMod 2), g • m = m) {F₁ : G₁ × G₁ → ZMod 2} {F₂ : G₂ × G₂ → ZMod 2} (hcomp : ∀ (p : G₁ × G₁), F₁ p = F₂ (e p.1, e p.2)) (hZ1 : F₁ ∈ ContCoh.Z2 G₁ (ZMod 2)) (hZ2 : F₂ ∈ ContCoh.Z2 G₂ (ZMod 2)) (hvan : H2ofFun G₂ F₂ = 0) : H2ofFun G₁ F₁ = 0

H²ofFun-vanishing pulls back along a continuous multiplicative map (trivial coefficients): if F₁ = F₂ ∘ (e × e) pointwise, F₁ is a 2-cocycle, and F₂ is a 2-cocycle with trivial H²ofFun class, then so is F₁ — the B²-witness ψ of F₂ pulls back to ψ ∘ e (δ¹ commutes with precomposition by multiplicativity; the trivial actions make the smul-terms invisible).

evensNormFun along an index-preserving multiplicative map

theorem GQ2.InvolutionSplice.evensNormFun_comp {G₁ : Type u_1} {G₂ : Type u_2} [Group G₁] [Group G₂] (e : G₁ →* G₂) {U₁ : Subgroup G₁} {U₂ : Subgroup G₂} {s₁ : G₁} {s₂ : G₂} (hmem : ∀ (x : G₁), x ∈ U₁ ↔ e x ∈ U₂) (hs : e s₁ = s₂) (hUi₁ : U₁.index = 2) (hs₁ : s₁ ∉ U₁) (hUi₂ : U₂.index = 2) (hs₂ : s₂ ∉ U₂) (α₁ : ↥U₁ → ZMod 2) (α₂ : ↥U₂ → ZMod 2) (hval : ∀ (x : G₁) (hx : x ∈ U₁), α₁ ⟨x, hx⟩ = α₂ ⟨e x, ⋯⟩) (p : G₁ × G₁) : evensNormFun U₁ s₁ α₁ p = evensNormFun U₂ s₂ α₂ (e p.1, e p.2)

evensNormFun is functorial along a multiplicative map matching the index-2 data: evensAux/bS are membership tests and s-translates only (no transversal choice), so with corresponding memberships (hmem), matched slices (hs), and matched scalar values (hval), the two Evens cochains agree pointwise.

The capstone: the involution hvanish in ker ρ-vocabulary

theorem GQ2.InvolutionSplice.hvanish_involution_ker {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] (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) (α : ↥ρ.ker → ZMod 2) (hαZ1 : α ∈ ContCoh.Z1 (↥ρ.ker) (ZMod 2)) (hdeep : H1ofFun (↥ρ.ker) α ∈ LocalKummer.deepClasses ρ.ker) (ĝ : AbsGalQ2) (hĝN : ĝ ∉ ρ.ker) (hĝ2 : ĝ * ĝ ∈ ρ.ker) (U₀ : Subgroup AbsGalQ2) (hU₀ : U₀ = ρ.ker ⊔ Subgroup.zpowers ĝ) (hmem : ĝ ∈ U₀) : H2ofFun (↥U₀) (evensNormFun (ρ.ker.subgroupOf U₀) ⟨ĝ, hmem⟩ fun (w : ↥(ρ.ker.subgroupOf U₀)) => α ⟨↑↑w, ⋯⟩) = 0

The involution hvanish over ker ρ (the Lemma 6.17 vanishing proof, the U₀-splice): for a deep block coordinate α on N = ker ρ and an involution lift ĝ (ĝ ∉ N, ĝ² ∈ N, U₀ = N ⊔ ⟨ĝ⟩), the Evens-norm inner cochain of the reducer's involution orbit has trivial H²ofFun class. This is the reducer's hvanish-input at the involution orbits, with the inner cochain matching ShapiroRead.hcoh_involution's output verbatim.

Chains: B¹ = 0 extraction (the deep witness's Kummer cocycle equals α), the splitting tower k = fixedField (toGal U₀) ≤ L = splitField ρ with the infinite Galois correspondence, the c2a Kummer package (kummer_presentation_of_index_two), the c2c analytic hunram (hunram_involution), the c2b spine (hvanish_involution = Lemma 6.16 + descent), and the carrier splice pulling the B²-witness back along the underlying-identity ↥U₀ → ↥k.fixingSubgroup.

The square/free hvanish in ker ρ-vocabulary (the deep-cup vanishing)

theorem GQ2.InvolutionSplice.cup11Fun_comp {G₁ : Type u_1} {G₂ : Type u_2} [Group G₁] [Group G₂] [DistribMulAction G₁ (ZMod 2)] [DistribMulAction G₂ (ZMod 2)] (htriv₁ : ∀ (g : G₁) (m : ZMod 2), g • m = m) (htriv₂ : ∀ (g : G₂) (m : ZMod 2), g • m = m) (e : G₁ →* G₂) (α₁ β₁ : G₁ → ZMod 2) (α₂ β₂ : G₂ → ZMod 2) (hα : ∀ (x : G₁), α₁ x = α₂ (e x)) (hβ : ∀ (x : G₁), β₁ x = β₂ (e x)) (p : G₁ × G₁) : ContCoh.cup11Fun AddMonoidHom.mul α₁ β₁ p = ContCoh.cup11Fun AddMonoidHom.mul α₂ β₂ (e p.1, e p.2)

cup11Fun functoriality along a multiplicative map (trivial coefficients): matched scalar values give equal cup cochains under (e × e).

theorem GQ2.InvolutionSplice.hvanish_cup_ker {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] (ρ : AbsGalQ2 →ₜ* C) (α β : ↥ρ.ker → ZMod 2) (hαZ1 : α ∈ ContCoh.Z1 (↥ρ.ker) (ZMod 2)) (hβZ1 : β ∈ ContCoh.Z1 (↥ρ.ker) (ZMod 2)) (hαdeep : H1ofFun (↥ρ.ker) α ∈ LocalKummer.deepClasses ρ.ker) (hβdeep : H1ofFun (↥ρ.ker) β ∈ LocalKummer.deepClasses ρ.ker) : H2ofFun (↥ρ.ker) (ContCoh.cup11Fun AddMonoidHom.mul α β) = 0

The square/free hvanish over ker ρ (the Lemma 6.17 vanishing proof): the cup of two deep block coordinates over N = ker ρ has trivial H²ofFun class. Same tower/carrier splice as hvanish_involution_ker, but with U = N (no lift, no index-2) and the cup in place of the Evens norm; the field-side vanishing is hvanish_cup (eq.-(94) orthogonality).

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

• Lemma 6.16 = ⟦lem-evensvanish⟧