Q⁰ over Γ_R as a Roe relator value in the κ⁰-extension #
The Γ_R twin of GQ2/GaussZ/RelatorGammaA.lean's GammaA section (the A-3 keystone,
obligation ii.7): over the raw candidate carrier GR = F₄ ⧸ N_R, the base determinant form
Q⁰ of a crossed V-cocycle is the Roe relator pair value in the concrete
κ⁰-extension:
Q⁰_{Γ_R,ρ'}(c) = relZPairR (graph-marking) κ⁰-cocycle |₁ + |₂,
where the graph marking is the image of the Γ_R-generator marking gammaGenR under the
graph homomorphism — the four explicit pairs (c(gᵢ), ρ'₀(gᵢ)) ∈ V ⋊ C. The route is the
Γ_A one verbatim: A-2 over Γ_R (IotaGammaR.QZero_eq_levelFactor_obsR, the R31c layer)
at the explicit LevelFactorR through the κ⁰-cocycle (kernel level of the graph hom),
transported by the Roe level-change naturality (WordCoh2R.relZPairR_comap).
The carrier Sd C V, the cocycle kappa0Cocycle, and the graph homomorphism graphSdHom
are generic in Γ and imported from GQ2/GaussZ/RelatorGammaA.lean, never cloned; the
only genuine clone is the 15-line continuity lemma continuous_vcocycle_c_R (its Γ_A
original is stated against ρM : ContinuousMonoidHom GA _).
All std-3; no axioms, no sorries.
A crossed cocycle's underlying function is continuous into the (discrete) module — the
Γ_R retyping of continuous_vcocycle_c (GQ2/GaussZ/RelatorGammaA.lean; the original is
pinned to GA-typed lower maps).
The A-3 keystone over Γ_R: the base determinant form Q⁰ of a crossed V-cocycle
is the Roe relator value in the concrete κ⁰-extension: the (tame + Roe wild)
relator-z pair of the κ⁰-cocycle on V ⋊ C at the marking graph(gammaGenR) — the four
explicit pairs (c(gᵢ), ρ'₀(gᵢ)). (A-2 over Γ_R — QZero_eq_levelFactor_obsR — at the
kernel level of the graph hom, transported by relZPairR_comap.)