Documentation

GQ2.Phase140.GammaA.Hsep

The Γ_A separation and partial-count assembly #

The word-side separator, private assembly helpers, and the final hsep calculation.

See GQ2.Phase140.GammaA for the paper-facing overview and architectural notes.

The word-side right-slot separator (the hpartial_A stage-6 engine) #

The Γ_A replacement for the local cup11_dualEval_right_separating (which runs on B6 Tate duality): 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 wordHom (MixedBObs.obs_inflation), so its WordCoh2.obs equals the traced mixed pairing mixedB (markC θ) (eval z) (eval ξ) (mixedB_eq_relZPair); obs kills (obs_B2_eq_zero), so all word pairings vanish, and prop_5_15's clause-3 RIGHT-slot nondegeneracy forces [eval ξ]_w = 0; eval_dZero + z1Equiv-injectivity pull the word coboundary back to a continuous one. No B-axioms.

Generic helpers for the hsep_gammaA/hpartial_gammaA decompositions #

hsep for Γ_A: the (T^∨)^C-separation via the marking route #

theorem GQ2.Phase140GammaA.hsep_gammaA {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : SectionEight.RecursionFrame T Blk} (b : GammaA.toProfinite.toTop →ₜ* boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l RF.zeroDR) (Dsc : SectionEight.AffineTLift.Descent (En.radData l h)) (ρ : BoundaryLifts b F RF.TC) (c : SectionEight.AffineTLift.VCocycle (En.descData l h) (RF.rhoPrime b F (En.radData l h) ρ)) (hc : ∀ (χ : (SectionEight.AffineTLift.TCharC (En.radData l h))), SectionEight.AffineTLift.betaChi (SectionEight.descSections En l h Dsc) χ c = 0) :

hsep for Γ_A — the (T^∨)^C-separation at the candidate source: a V-coordinate whose χ-obstructions all vanish is T-liftable. The Γ_A twin of Phase140Local.hsep_local, by the marking route (the local prop_5_16 cup20 route has no Γ_A analog): each nonzero invariant character's vanishing obstruction produces a lift through its 𝔽₂-cover (exists_lift_charCover), which forces χ-agreement of the relator values of a set-lift marking (redValues_eq_of_coverLift); sep_word (the prop_5_15 trace-span) converts total agreement into word-level corrections; the corrected marking kills both relators (corrected_tameValue/corrected_wildValue + T-elementarity) and descends (mlift_of_relatorFree_marking) to the direct M-lift.

theorem GQ2.Phase140GammaA.hpartial_gammaA {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : SectionEight.RecursionFrame T Blk} (b : GammaA.toProfinite.toTop →ₜ* boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l RF.zeroDR) (Dsc : SectionEight.AffineTLift.Descent (En.radData l h)) (ρ : BoundaryLifts b F RF.TC) (χ : (SectionEight.AffineTLift.TCharC (En.radData l h))) ( : χ 0) :

hpartial for Γ_A — nondegeneracy of the obstruction pairing in the character: every nonzero χ ∈ (T^∨)^C is detected by some V-coordinate. The Γ_A twin of Phase140Local.hpartial_local, stages 1–5 and 7–9 mirrored verbatim (they are frame-level or Γ-generic); the ONE divergent stage is the right-slot separation (local stage 6, B6 Tate duality), replaced by the word-side b1_of_pair_cochain_B2 (prop_5_15 clause-3 right-nondegeneracy through the obs/mixedB ledger). All std-3, no B-axioms.