The Γ_A (83)-coordinates — Z¹⧸B¹ in word generator coordinates

Route W brick A-1 (docs/orchestration/p16d6e4aA-gammaA-gauss-design.md §2): the e6 Stage-0 bridge as reusable per-ρ declarations, composed with the banked degree-1 word comparison (WordCohBridge.h1Equiv) into the generator-coordinate model of the Γ_A Gauss domain:

`h1CoordGammaA : Z¹_{Γ_A,ρ'}(V) ⧸ B¹ → H¹_w (markC θ)`      (`θ = ρ.1.1`),  bijective,

so A-3 can evaluate the descended Q̄⁰ as an explicit 𝔽₂-function of word-cocycle classes (Fin 4 → V generator tuples). Contents:

• rhoPrimeGA/thetaGA — the GammaA → GA retypes of the two lower maps (the e6 Stage-0 idiom as top-level declarations), with thetaGA_surjective and the roundtrip roundtripGA; all A-lane objects live uniformly at GA, with ONE defeq-bridge to the GammaA-spelled GaussZResidue statement at the A-4 finale;
• coordHcomp_of_hcompat — the h1OfVQuot compatibility from the θ-compatibility (callers hold the latter as fun _ _ => rfl under the compHom (thetaGA …) letI-pack, the GaussZFinal per-ρ idiom);
• finite_vcocycle_gammaA — Z¹ finiteness, σ-free from Phase140GammaA.hZcard_gammaA;
• hfix_of_simple_nt — the hnt-variant of GaussZReduction.hfix_of_simple: V^{C₀} = 0 from ρ'-surjectivity + hsimple + hnt alone — the W = ⊤ branch contradicts hnt directly, so the NON-block-derivable hfaith (the §9 induction flag) and the [Nontrivial C0] instance are both dropped; the A-lane runs entirely on the prop_8_9 ledger hypotheses;
• h1CoordGammaA + h1CoordGammaA_bijective + card_H1w_gammaA (#H¹_w = #V).

All std-3 (no B-axioms). Consumed by A-3 (the explicit relator quadratic) and A-4 (form identification + gaussZResidue_gammaA_*); A-2 (the iotaB relator-evaluation rule) is independent.

The hnt-variant of the fixed-point freeness (generic; drops hfaith)

theorem GQ2.SectionEight.AffineTLift.hfix_of_simple_nt {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] {D : RadicalCoverData Bg} {DD : DescData D} {Γ : Type} [Group Γ] [TopologicalSpace Γ] {ρ : Γ →ₜ* Bg ⧸ D.M} (hsurj : Function.Surjective fun (γ : Γ) => (rho0 DD ρ) γ) (hsimple : ∀ (W : AddSubgroup DD.Vmod), (∀ (g : DD.C0), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hnt : ∃ (g : DD.C0) (v : DD.Vmod), g • v ≠ v) (v : DD.Vmod) (hv : ∀ (γ : Γ), (rho0 DD ρ) γ • v = v) : v = 0

V^{C₀} = 0 from the ledger hypotheses alone — the hnt-variant of GaussZReduction.hfix_of_simple: faithfulness is NOT needed (nor block-derivable — the the §9 induction coordination flag); in the W = ⊤ branch every C₀-element acts trivially, contradicting hnt directly.

The per-ρ retypes and the coordinate bijection

noncomputable def GQ2.SectionEight.AffineTLift.rhoPrimeGA {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 : RecursionFrame T Blk} (b : ↑GammaA.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : BoundaryLifts b F RF.TC) : WordCohBridge.GA →ₜ* RF.YB ⧸ (En.radData l h).M

The lower map ρ' : Γ_A → Y_B ⧸ M, retyped against the raw quotient GA (the e6 Stage-0 idiom as a declaration).

Equations

• GQ2.SectionEight.AffineTLift.rhoPrimeGA b F En l h ρ = RF.rhoPrime b F (En.radData l h) ⋯ ρ

theorem GQ2.SectionEight.AffineTLift.finite_vcocycle_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 : RecursionFrame T Blk} (b : ↑GammaA.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : BoundaryLifts b F RF.TC) (hsimple : ∀ (W : AddSubgroup En.Vmod), (∀ (g : RF.YC), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hVne : ∃ (v : En.Vmod), v ≠ 0) (hnt : ∃ (g : RF.YC) (v : En.Vmod), g • v ≠ v) : Finite (VCocycle (En.descData l h) (rhoPrimeGA b F En l h ρ))

Z¹ is finite — σ-free from the e6 count (Phase140GammaA.hZcard_gammaA).

noncomputable def GQ2.SectionEight.AffineTLift.thetaGA {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 : RecursionFrame T Blk} (b : ↑GammaA.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (ρ : BoundaryLifts b F RF.TC) : WordCohBridge.GA →ₜ* RF.YC

The boundary-lift head θ = ρ.1.1 : Γ_A → Y_C, retyped against GA — the marking map of the word complex (markC (thetaGA …)).

Equations

• GQ2.SectionEight.AffineTLift.thetaGA b F ρ = ↑↑ρ

theorem GQ2.SectionEight.AffineTLift.thetaGA_surjective {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 : RecursionFrame T Blk} (b : ↑GammaA.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (ρ : BoundaryLifts b F RF.TC) : Function.Surjective ⇑(thetaGA b F ρ)

theorem GQ2.SectionEight.AffineTLift.roundtripGA {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 : RecursionFrame T Blk} (b : ↑GammaA.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : BoundaryLifts b F RF.TC) (γ : WordCohBridge.GA) : (rho0 (En.descData l h) (rhoPrimeGA b F En l h ρ)) γ = (thetaGA b F ρ) γ

The roundtrip rho0 ∘ rhoPrime = θ over GA (rho0_descData_rhoPrime, retyped). Callers derive the h1OfVQuot-compatibility from their letI-pack through this: hcomp γ v := congrArg (· • v) (roundtripGA … γ).symm-composed with the compHom-rfl.

noncomputable def GQ2.SectionEight.AffineTLift.h1CoordGammaA {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 : RecursionFrame T Blk} (b : ↑GammaA.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : BoundaryLifts b F RF.TC) [TopologicalSpace (En.descData l h).Vmod] [DiscreteTopology (En.descData l h).Vmod] [DistribMulAction WordCohBridge.GA (En.descData l h).Vmod] [ContinuousSMul WordCohBridge.GA (En.descData l h).Vmod] [DistribMulAction RF.YC (En.descData l h).Vmod] [Finite (En.descData l h).Vmod] (hcomp : ∀ (γ : WordCohBridge.GA) (v : (En.descData l h).Vmod), γ • v = (rho0 (En.descData l h) (rhoPrimeGA b F En l h ρ)) γ • v) (hcompat : ∀ (γ : WordCohBridge.GA) (v : (En.descData l h).Vmod), γ • v = (thetaGA b F ρ) γ • v) (hA₂ : ∀ (v : (En.descData l h).Vmod), v + v = 0) (x : VCocycle (En.descData l h) (rhoPrimeGA b F En l h ρ) ⧸ vCobRange (En.descData l h) (rhoPrimeGA b F En l h ρ)) : FoxH.H1w (WordCohBridge.markC (thetaGA b F ρ))

The A-1 result: the generator-coordinate model of the Γ_A Gauss domain — the quotient bijection h1OfVQuot into H¹(Γ_A, V) composed with the banked degree-1 word comparison h1Equiv into H¹_w(markC θ) (classes of Fin 4 → V generator tuples). The two compatibility hypotheses are the same fact at the two actions the banked pieces pin (h1OfVQuot: the DescData-internal actVmod; h1Equiv: the ambient Y_C-action): under the caller's letI-pack (compHom (thetaGA …) + the actVmod re-key) both are rfl-flavored (hcompat := fun _ _ => rfl; hcomp via roundtripGA).

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.SectionEight.AffineTLift.h1CoordGammaA_bijective {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 : RecursionFrame T Blk} (b : ↑GammaA.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : BoundaryLifts b F RF.TC) [TopologicalSpace (En.descData l h).Vmod] [DiscreteTopology (En.descData l h).Vmod] [DistribMulAction WordCohBridge.GA (En.descData l h).Vmod] [ContinuousSMul WordCohBridge.GA (En.descData l h).Vmod] [DistribMulAction RF.YC (En.descData l h).Vmod] [Finite (En.descData l h).Vmod] (hcomp : ∀ (γ : WordCohBridge.GA) (v : (En.descData l h).Vmod), γ • v = (rho0 (En.descData l h) (rhoPrimeGA b F En l h ρ)) γ • v) (hcompat : ∀ (γ : WordCohBridge.GA) (v : (En.descData l h).Vmod), γ • v = (thetaGA b F ρ) γ • v) (hA₂ : ∀ (v : (En.descData l h).Vmod), v + v = 0) : Function.Bijective (h1CoordGammaA b F En l h ρ hcomp hcompat hA₂)