The Γ_R separation and partial-count assembly #
The Roe-candidate twin of GQ2/Phase140/GammaA/Hsep.lean: the word-side right-slot separator,
the private assembly helpers, and the final hsep/hpartial calculations.
See GQ2.Phase140.GammaR for the paper-facing overview and architectural notes.
The word-side right-slot separator (the hpartial_gammaR stage-6 engine) #
The Γ_R replacement for the local cup11_dualEval_right_separating (which runs on B6 Tate
duality), and the exact twin of Phase140GammaA.b1_of_pair_cochain_B2 on the Roe spine: a
continuous dual 1-cocycle ξ whose pair cochain (a,b) ↦ ξ(a)(a • z(b)) is a continuous
coboundary against EVERY A-cocycle z is itself a coboundary. Route: the pair cochain is the
kappaHeis-inflation of the paired wordHomR (MixedBObsR.obs_inflation_R), so its
WordCoh2R.obs_R equals the traced mixed pairing mixedB_R (markC_R θ) (evalR z) (evalR ξ)
(mixedB_eq_relZPairR); obs_R kills B² (obs_B2_eq_zero_R), so all word pairings vanish, and
prop_5_15_R's clause-3 RIGHT-slot nondegeneracy forces [evalR ξ]_w = 0; eval_dZeroR +
z1EquivR-injectivity pull the word coboundary back to a continuous one. No B-axioms.
Generic helpers for the hsep_gammaR/hpartial_gammaR decompositions #
These are the Γ-free (or retype-only) private helpers of Phase140GammaA.Hsep; they are
private there, hence restated here rather than imported. Statements are binder-for-binder the
Γ_A ones, with GA → GR, GammaA → GammaR, and Marking.push → Marking.pushR /
wildValue → wildValueR where a relator is read.
hsep for Γ_R: the (T^∨)^C-separation via the marking route #
hsep for Γ_R — the (T^∨)^C-separation at the Roe candidate source: a V-coordinate
whose χ-obstructions all vanish is T-liftable. The Γ_R twin of
Phase140GammaA.hsep_gammaA, by the same marking route: each nonzero invariant character's
vanishing obstruction produces a lift through its 𝔽₂-cover (the abstract-Γ
exists_lift_charCover, reused), which forces χ-agreement of the tame and Roe-wild relator
values of a set-lift marking (redValues_eq_of_coverLift_R); sep_word_R (the prop_5_15_R
trace-span) converts total agreement into word-level corrections; the corrected marking kills both
Γ_R relators (corrected_tameValue/corrected_wildValueR + T-elementarity) and descends
(mlift_of_relatorFree_markingR) to the direct M-lift.
hpartial for Γ_R: nondegeneracy of the obstruction pairing in the character #
hpartial for Γ_R — nondegeneracy of the obstruction pairing in the character: every
nonzero χ ∈ (T^∨)^C is detected by some V-coordinate. The Γ_R twin of
Phase140GammaA.hpartial_gammaA, stages 1, 3–5 and 8–9 mirrored verbatim (they are frame-level or
Γ-generic); the two source-specific stages are stage 2 (cupChi_iotaB_eq_zero_R, on the
unconditional Γ_R leaf card_H2_gammaR) and stages 6–7, the word-side right-slot separation
b1_of_pair_cochain_B2_R (prop_5_15_R clause-3 right-nondegeneracy through the
obs_R/mixedB_R ledger). All std-3, no B-axioms.