The ι_Γ ↔ inv_{ℚ₂} obstruction bridge

The master-count / keystone layer measures the base-class obstruction with the abstract coboundary indicator iotaB (GQ2/PhaseObstruction.lean); the §6 base-determinant layer measures it with the Tate invariant map iotaF ∘ H²ofFun (GQ2/SectionSix.lean, Q0loc). On continuous 2-cocycles over G_ℚ₂ the two agree, because #H²(G_ℚ₂,𝔽₂) = 2 and iotaF D is the invariant-map isomorphism. This is the bridge that lets prop_6_18's Q0loc-Gauss-sum feed the QZero source-Gauss residue (the Prop. 8.9 assembly; design docs/orchestration/p16d6e4a-evaluation-design.md §1(C)).

iotaB_eq_iotaF_of_injective is stated with the injectivity of iotaF D as an explicit hypothesis — a self-contained, reusable form. The injectivity itself (iotaF D = D.inv ∘ mapCoeff2 muTwoOfF2, both factors injective) is the enumerated remaining sub-obligation mapCoeff2_injective (the degree-2 analog of DeepPart.mapCoeff1_injective).

theorem GQ2.SectionEight.iotaB_eq_iotaF_of_injective (D : TateDuality 2) (hinj : Function.Injective ⇑(SectionSix.iotaF D)) {φ : AbsGalQ2 × AbsGalQ2 → ZMod 2} (hφ : φ ∈ ContCoh.Z2 AbsGalQ2 (ZMod 2)) : iotaB φ = (SectionSix.iotaF D) (H2ofFun AbsGalQ2 φ)

The abstract↔invariant obstruction bridge (the Prop. 8.9 assembly §1(C)): on a continuous 2-cocycle φ over G_ℚ₂, the abstract coboundary indicator iotaB φ equals the Tate invariant iotaF D (H²ofFun φ), given iotaF D injective. Both vanish exactly on B², and a ZMod 2 value is determined by whether it is 0.

The injectivity of iotaF — mapCoeff2 of a coefficient bijection

iotaF D = D.inv ∘ mapCoeff2 muTwoOfF2; D.inv is an AddEquiv and muTwoOfF2 is the 𝔽₂ ≅ μ₂ coefficient bijection, so the missing piece is the degree-2 analog of DeepPart.mapCoeff1_injective — coboundaries pull back along the (automatically continuous, discrete-coefficient) inverse. Homed here rather than Cohomology.lean to avoid a foundational-file rebuild; generic over AbsGalQ2-coefficient bijections.

theorem GQ2.SectionEight.mapCoeff2_injective {A B : Type} [AddCommGroup A] [AddCommGroup B] [TopologicalSpace A] [TopologicalSpace B] [DiscreteTopology A] [DiscreteTopology B] [DistribMulAction AbsGalQ2 A] [ContinuousSMul AbsGalQ2 A] [DistribMulAction AbsGalQ2 B] [ContinuousSMul AbsGalQ2 B] (f : A →+ B) (hf : Continuous ⇑f) (hcompat : ∀ (g : AbsGalQ2) (a : A), f (g • a) = g • f a) (hinj : Function.Injective ⇑f) (hsurj : Function.Surjective ⇑f) : Function.Injective ⇑(ContCoh.mapCoeff2 f hf hcompat)

mapCoeff2 of an equivariant additive bijection is injective (the degree-2 DeepPart.mapCoeff1_injective): a B²-witness on the target pulls back along the inverse, which is continuous because the coefficients are discrete.

theorem GQ2.SectionEight.muTwoOfF2_surjective : Function.Surjective ⇑SectionSix.muTwoOfF2

muTwoOfF2 is surjective (𝔽₂ ≅ μ₂, via DeepPart.zmodTwoEquivMuTwo).

theorem GQ2.SectionEight.iotaF_injective (D : TateDuality 2) : Function.Injective ⇑(SectionSix.iotaF D)

iotaF D is injective: D.inv is an equivalence and mapCoeff2 muTwoOfF2 is injective (mapCoeff2_injective at the 𝔽₂ ≅ μ₂ bijection).

theorem GQ2.SectionEight.iotaB_eq_iotaF (D : TateDuality 2) {φ : AbsGalQ2 × AbsGalQ2 → ZMod 2} (hφ : φ ∈ ContCoh.Z2 AbsGalQ2 (ZMod 2)) : iotaB φ = (SectionSix.iotaF D) (H2ofFun AbsGalQ2 φ)

The abstract↔invariant obstruction bridge, unconditional (the Prop. 8.9 assembly §1(C) closed): iotaB φ = iotaF D (H²ofFun φ) on continuous 2-cocycles over G_ℚ₂.