The Γ_A ledger identity: obs(varCoc u) = mixedB #
The edge-specific half of the Γ_A half-torsor proof. For a primal crossed cocycle w : Z¹(Γ_A, T) (packaged as
u : TCocycle) and the shifted-edge dual cocycle φf : Z¹(Γ_A, T^∨), the WordCoh2
obstruction of the variation class varCoc u equals the Fox–Heisenberg mixed pairing:
obs(varCoc u) = mixedB (markC ρ) (eval w) (eval φf).
The proof is the near-definitional edge unfold varCoc u (a,b) = kappaHeis (H a) (H b) (where
H is the graph hom of the pair (w, φf) into WordLift (T × T^∨) C) fed into the two generic
cores MixedBObs.obs_inflation and MixedBObs.mixedB_eq_relZPair.
The graph hom of the pair (w, φf) into WordLift (T × T^∨) C.
Equations
- GQ2.SectionEight.LedgerGammaA.pairHom D ρ hcompat hcompatD w φf = GQ2.WordCohBridge.wordHom ρ ⋯ ⟨fun (γ : GQ2.WordCohBridge.GA) => (↑w γ, ↑φf γ), ⋯⟩
Instances For
The nonzero variation class (the Γ_A half-torsor proof hvar). If the mixed pairing of the primal cocycle
w against the shifted-edge dual φf is nonzero, the variation class [varCoc u] is a nonzero
element of H²(Γ_A, 𝔽₂): a trivial class would be a coboundary, on which obs — hence mixedB
by the ledger — vanishes.
The shifted-edge dual cocycle (reconstruction of c3's φf) #
φf γ = (s ↦ ε̄(ρ γ)(γ⁻¹ · s)) is the dual 1-cocycle carrying the edge; it is nonzero in H¹
exactly when the cover does not descend (NoDescent). This is c3's internal construction,
re-exposed so the ledger identity can consume it.