The ι_{Γ_A}-computation rule

The F-brick of the (83)-for-Γ_A seam (docs/orchestration/p16d6e4aA-gammaA-gauss-design.md §2): the coboundary indicator ι_Γ (SectionEight.iotaB, the Q⁰-valuation) is computed, over the raw candidate carrier GA = F₄ ⧸ N_A, by the word-relator obstruction of the Γ_A half-torsor proof degree-2 presentation-comparison:

• iotaB_eq_obs — ι_{Γ_A} φ = obs φ for every continuous 2-cocycle φ: both are 𝔽₂-valued with the same vanishing locus (iotaB_eq_zero_iff vs the c4 keystone WordCoh2.obs_ker_eq_B2), hence equal.
• iotaB_eq_levelFactor_obs — the evaluation form: ι_{Γ_A} φ is the (tame + wild) relator obstruction F.obs = relZPair(…).1 + relZPair(…).2 of any finite-admissible-level factorization F of the (1,1)-normalization of φ (obsFun_eq well-definedness).
• QZero_eq_obs / QZero_eq_levelFactor_obs — the same, specialized to the base determinant form: Q⁰_{Γ_A,ρ'}(c) is the relator obstruction of any level factorization of the (normalized) graph pullback graphPullback DD.dat ρ'₀ c.c — the A-3 interface: brick A-3 constructs an explicit LevelFactor for the graph pullback in the e6 generator coordinates and reads the two relator values off the factor-set expansion.

Everything is glue over proved technology (iotaB = the B²-indicator, PhaseObstruction.lean:51; obs/obs_ker_eq_B2/obsFun_eq, WordCoh2.lean §CardBound; graphPullback_mem_Z2_of_cocycle, KeystoneDelta.lean:1516, generic-Γ) — std-3, no axioms, no sorries.

theorem GQ2.IotaGammaA.iotaB_eq_obs [DistribMulAction WordCohBridge.GA (ZMod 2)] (htriv : ∀ (x : WordCohBridge.GA) (m : ZMod 2), x • m = m) (φ : ↥(ContCoh.Z2 WordCohBridge.GA (ZMod 2))) : SectionEight.iotaB ↑φ = (WordCoh2.obs htriv) φ

The ι_{Γ_A}-computation rule (A-2 core): the coboundary indicator agrees with the the Γ_A half-torsor proof word-relator obstruction on every continuous 2-cocycle — both are 𝔽₂-valued with kernel exactly B²(Γ_A, 𝔽₂).

theorem GQ2.IotaGammaA.iotaB_eq_levelFactor_obs [DistribMulAction WordCohBridge.GA (ZMod 2)] (htriv : ∀ (x : WordCohBridge.GA) (m : ZMod 2), x • m = m) (φ : ↥(ContCoh.Z2 WordCohBridge.GA (ZMod 2))) (F : WordCoh2.LevelFactor (WordCoh2.normalizeCochain ↑φ)) : SectionEight.iotaB ↑φ = F.obs

The evaluation form (the A-3 interface, cocycle-level): ι_{Γ_A} φ is the (tame + wild) relator obstruction of any finite-admissible-level factorization of the (1,1)-normalization of φ.

theorem GQ2.IotaGammaA.QZero_eq_obs [DistribMulAction WordCohBridge.GA (ZMod 2)] (htriv : ∀ (x : WordCohBridge.GA) (m : ZMod 2), x • m = m) {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : SectionEight.RadicalCoverData Bg} {DD : SectionEight.AffineTLift.DescData D} {ρM : WordCohBridge.GA →ₜ* Bg ⧸ D.M} (c : SectionEight.AffineTLift.VCocycle DD ρM) : SectionEight.AffineTLift.QZero DD ρM c = (WordCoh2.obs htriv) ⟨graphPullback DD.dat (fun (γ : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) => (SectionEight.AffineTLift.rho0 DD ρM) γ) c.c, ⋯⟩

Q⁰ over Γ_A is the word-relator obstruction (A-2 → A-3 handoff, packaged form): the base determinant form evaluates through obs at the graph pullback.

theorem GQ2.IotaGammaA.QZero_eq_levelFactor_obs [DistribMulAction WordCohBridge.GA (ZMod 2)] (htriv : ∀ (x : WordCohBridge.GA) (m : ZMod 2), x • m = m) {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : SectionEight.RadicalCoverData Bg} {DD : SectionEight.AffineTLift.DescData D} {ρM : WordCohBridge.GA →ₜ* Bg ⧸ D.M} (c : SectionEight.AffineTLift.VCocycle DD ρM) (F : WordCoh2.LevelFactor (WordCoh2.normalizeCochain (graphPullback DD.dat (fun (γ : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) => (SectionEight.AffineTLift.rho0 DD ρM) γ) c.c))) : SectionEight.AffineTLift.QZero DD ρM c = F.obs

The A-3 consumable: Q⁰_{Γ_A,ρ'}(c) is the (tame + wild) relator obstruction of any finite-admissible-level factorization of the normalized graph pullback. A-3 supplies an explicit LevelFactor in the e6 generator coordinates and expands F.obs along the two relator words.