The Γ_R ledger identity: obs_R(varCoc u) = mixedB_R #
The edge-specific half of the Γ_R half-torsor proof. For a primal crossed cocycle
w : Z¹(Γ_R, T) (packaged as u : TCocycle) and the shifted-edge dual cocycle
φf : Z¹(Γ_R, T^∨), the WordCoh2R
obstruction of the variation class varCoc u equals the Fox–Heisenberg mixed pairing:
obs_R(varCoc u) = mixedB_R (markC_R ρ) (evalR w) (evalR φ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 MixedBObsR.obs_inflation_R and MixedBObsR.mixedB_eq_relZPairR.
The graph hom of the pair (w, φf) into WordLift (T × T^∨) C.
Equations
- GQ2.SectionEight.LedgerGammaR.pairHomR D ρ hcompat hcompatD w φf = GQ2.WordCohBridgeR.wordHomR ρ ⋯ ⟨fun (γ : GQ2.WordCohBridgeR.GR) => (↑w γ, ↑φf γ), ⋯⟩
Instances For
The nonzero variation class (the Γ_R 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²(Γ_R, 𝔽₂): a trivial class would be a coboundary, on which obs_R — hence mixedB_R
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.