The κ⁰ ledger for the Γ_A Gauss residue

The supported section, coordinate transport, and split and ramified wild-value calculations.

See GQ2.GaussZ.FinalGammaA for the paper-facing overview, source citations, and deviations.

A-4.1: the x₀-supported section of H¹_w (generic marking level)

The paper's "only x₀ varies" gauge (Prop 6.5's normalization), as a bijective parametrization V ≃ H¹_w: membership and bijectivity fall out of the banked lemma_5_13_split shape characterizations (Z¹_w = {x₁-row = x₃-row = 0}, B¹_w = σ-row of coboundaries). Ramified twin in the next increment via lemma_5_13_ramified.

theorem GQ2.SectionEight.AffineTLift.x0Supported_mem_Z1w_split {C : Type u_1} [Group C] [Finite C] {V : Type u_2} [AddCommGroup V] [DistribMulAction C V] (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (hV₂ : ∀ (v : V), v + v = 0) (hsimple : FoxH.IsSimpleModTwo C V) [Finite V] (hcore : t.Pro2Core) (htau : ∀ (v : V), t.τ • v = v) (hU : ∀ (v : V), t.sigma2 • v = v) (hVS : ∀ (v : V), t.σ • v = v → v = 0) (v : V) : FoxH.x0Supported v ∈ FoxH.Z1w t

The x₀-supported tuples are word cocycles (split regime): immediate from the lemma_5_13_split Z¹-shape (x 1 = x 3 = 0).

theorem GQ2.SectionEight.AffineTLift.h1wMk_eq_iff {C : Type u_1} [Group C] [Finite C] {V : Type u_2} [AddCommGroup V] [DistribMulAction C V] {t : Marking C} [Finite V] (x y : ↥(FoxH.Z1w t)) : FoxH.h1wMk t x = FoxH.h1wMk t y ↔ ↑(x - y) ∈ FoxH.B1w t

The H¹_w-class equality criterion in h1wMk vocabulary (H1w is a semireducible def, so the quotient lemmas do not elaborate against it directly — the GaussZLocal.H1mk_eq_iff idiom).

theorem GQ2.SectionEight.AffineTLift.x0Section_bijective_split {C : Type u_1} [Group C] [Finite C] {V : Type u_2} [AddCommGroup V] [DistribMulAction C V] (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (hV₂ : ∀ (v : V), v + v = 0) (hsimple : FoxH.IsSimpleModTwo C V) [Finite V] (hcore : t.Pro2Core) (htau : ∀ (v : V), t.τ • v = v) (hU : ∀ (v : V), t.sigma2 • v = v) (hVS : ∀ (v : V), t.σ • v = v → v = 0) : Function.Bijective fun (v : V) => FoxH.h1wMk t ⟨FoxH.x0Supported v, ⋯⟩

The x₀-supported section of H¹_w is bijective (split regime): injectivity from the B¹-shape (coboundaries live in the σ-row, so an x₀-row difference must vanish); surjectivity by normalizing the σ-row away ((σ − 1) is onto by hVS + finiteness).

theorem GQ2.SectionEight.AffineTLift.x0Section_bijective_ramified {C : Type u_1} [Group C] [Finite C] {V : Type u_2} [AddCommGroup V] [DistribMulAction C V] (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (hV₂ : ∀ (v : V), v + v = 0) [Finite V] (hx0 : ∀ (v : V), t.x₀ • v = v) (hx1 : ∀ (v : V), t.x₁ • v = v) (htau : ∀ (v : V), t.τ • v = v → v = 0) (hTodd : ∀ (v : V), powOmega2 t.τ • v = v) : Function.Bijective fun (v : V) => FoxH.h1wMk t ⟨FoxH.x0Supported v, ⋯⟩

The x₀-supported section of H¹_w is bijective (ramified regime): both halves from lemma_5_13_ramified's unique normal form.

A-4.2: the κ⁰-ledger, tame value — the base-slice section

The tame relator only walks the σ/τ-slots; on the x₀-supported gauge those have zero V-part, and κ⁰ vanishes when both arguments do (f_zero_left + m_zero), so the whole walk stays in the image of the base-slice section hom sdSec : C →* CentExt κ⁰ — the κ⁰-analog of the mixed ledger's secHom. Hence the tame fibre is 0.

noncomputable def GQ2.SectionEight.AffineTLift.sdSec {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) : C →* WordCoh2.CentExt (kappa0Cocycle dat hdat)

The base-slice section cc ↦ ((0, cc), 0) is a homomorphism into CentExt κ⁰.

Equations

• GQ2.SectionEight.AffineTLift.sdSec dat hdat = { toFun := fun (cc : C) => (GQ2.SectionEight.AffineTLift.Sd.mk 0 cc, 0), map_one' := ⋯, map_mul' := ⋯ }

theorem GQ2.SectionEight.AffineTLift.liftMark_kappa0_tameValue_fib {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (t : Marking (Sd C V)) (hσ : t.σ.v = 0) (hτ : t.τ.v = 0) : (WordCoh2.liftMark t (kappa0Cocycle dat hdat)).tameValue.fib = 0

The tame κ⁰-value is base-slice: at any lifted marking whose σ/τ-slots have zero V-part, the tame relator value is the sdSec-image of the C-level tame value — its fibre vanishes (no TameRel needed).

theorem GQ2.SectionEight.AffineTLift.relZPair_kappa0_fst_eq_zero {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) [Finite C] [Finite V] (t : Marking (Sd C V)) (hσ : t.σ.v = 0) (hτ : t.τ.v = 0) : (WordCoh2.relZPair t (kappa0Cocycle dat hdat)).1 = 0

The A-3 interface form: the FIRST relator-z component vanishes on base-slice σ/τ-slots.

A-4.3a: the coordinate transport toolkit

The Sd-parts of the wild-word factors transport to the BANKED liftMarking_*_u V-part ledger through the carrier identification Sd C V ≅ WordLift V C (same semidirect law), and the CentExt κ⁰-factors project to the Sd-factors through CentExt.proj — so every base coordinate in the κ⁰-peel is already computed. The fibre cells are then CentExt.mul_fib + the evaluated κ⁰-values; the first (and quadratically decisive) cell is the x₀-square q(v) + m_{P}(v).

noncomputable def GQ2.SectionEight.AffineTLift.sdToWL {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] : Sd C V →* FoxH.WordLift V C

The carrier identification Sd C V →* WordLift V C (the two semidirect laws agree).

Equations

• GQ2.SectionEight.AffineTLift.sdToWL = { toFun := fun (p : GQ2.SectionEight.AffineTLift.Sd C V) => { u := p.v, g := p.cc }, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def GQ2.SectionEight.AffineTLift.sdBaseMarking {C : Type u_1} {V : Type u_2} (tS : Marking (Sd C V)) : Marking C

The C-level base marking of an Sd-marking.

Equations

• GQ2.SectionEight.AffineTLift.sdBaseMarking tS = { σ := tS.σ.cc, τ := tS.τ.cc, x₀ := tS.x₀.cc, x₁ := tS.x₁.cc }

noncomputable def GQ2.SectionEight.AffineTLift.sdOffsets {C : Type u_1} {V : Type u_2} (tS : Marking (Sd C V)) : Fin 4 → V

The V-offset tuple of an Sd-marking.

Equations

• GQ2.SectionEight.AffineTLift.sdOffsets tS = ![tS.σ.v, tS.τ.v, tS.x₀.v, tS.x₁.v]

theorem GQ2.SectionEight.AffineTLift.sdToWL_marking {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] (tS : Marking (Sd C V)) : Marking.map sdToWL tS = FoxH.liftMarking (sdBaseMarking tS) (sdOffsets tS)

Under the carrier identification, an Sd-marking IS the liftMarking of its base marking at its offset tuple.

theorem GQ2.SectionEight.AffineTLift.sd_d0_v {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] [Finite C] [Finite V] (tS : Marking (Sd C V)) : tS.d0.v = (FoxH.liftMarking (sdBaseMarking tS) (sdOffsets tS)).d0.u

d₀'s V-part transports to the banked WordLift ledger.

theorem GQ2.SectionEight.AffineTLift.liftMark_d0_base {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) [Finite C] [Finite V] (tS : Marking (Sd C V)) : (WordCoh2.liftMark tS (kappa0Cocycle dat hdat)).d0.base = tS.d0

The CentExt κ⁰-level factors project to the Sd-level factors (d₀ case; the projection is liftMark_map_proj + word functoriality).

A-4.3b: conjugation and base-slice fibre cells + the m-calculus

The κ⁰-peel's step lemmas: on V-part-zero prefixes the fibre accumulates only m-corrections (f dies on a zero slot); conjugation by an sdSec-image shifts the fibre by one m-value; m at squares/inverses of V-fixing elements vanishes/reflects (m_mul + char 2). These are the CentExt κ⁰-analogs of the HeisLift.mul_z_of_trivial family.

theorem GQ2.SectionEight.AffineTLift.mul_fib_of_v_zero {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (p r : WordCoh2.CentExt (kappa0Cocycle dat hdat)) (hp : p.base.v = 0) : (p * r).fib = p.fib + r.fib + dat.m p.base.cc r.base.v

The fibre step on a V-part-zero left factor: only the m-correction survives.

theorem GQ2.SectionEight.AffineTLift.mul_fib_of_v_zero_right {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (p r : WordCoh2.CentExt (kappa0Cocycle dat hdat)) (hr : r.base.v = 0) : (p * r).fib = p.fib + r.fib

The fibre step on a V-part-zero RIGHT factor: κ⁰(·, v-part 0) dies entirely.

theorem GQ2.SectionEight.AffineTLift.conjP_sdSec_base {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (x : WordCoh2.CentExt (kappa0Cocycle dat hdat)) (w : C) : (conjP x ((sdSec dat hdat) w)).base = conjP x.base (Sd.mk 0 w)

The base of a conjugate by an sdSec-image (through CentExt.proj).

theorem GQ2.SectionEight.AffineTLift.sd_conjP_v {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] (p : Sd C V) (w : C) : (conjP p (Sd.mk 0 w)).v = w⁻¹ • p.v

The V-part of an Sd-conjugate by a V-part-zero element: the w⁻¹-twist.

theorem GQ2.SectionEight.AffineTLift.conjP_sdSec_fib {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (x : WordCoh2.CentExt (kappa0Cocycle dat hdat)) (w : C) : (conjP x ((sdSec dat hdat) w)).fib = x.fib + dat.m w⁻¹ x.base.v

The conjugation fibre cell: conjugating by an sdSec-image shifts the fibre by the single m-correction m_{w⁻¹} at the V-part.

theorem GQ2.SectionEight.AffineTLift.m_inv_of_fixed {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (w : C) (v : V) (hfix : w • v = v) : dat.m w⁻¹ v = dat.m w v

m at an inverse of a V-fixing element reflects (from m_mul + m_one + char 2).

theorem GQ2.SectionEight.AffineTLift.m_sq_of_fixed {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (w : C) (v : V) (hfix : w • v = v) : dat.m (w * w) v = 0

m at a square of a V-fixing element vanishes.

A-4.3c: the split wild value = the x₀-square

With the structural pack (x₀.cc = x₁.cc = 1 from the tame factorization, τ.cc of odd order — prep doc §6), d₀ has base 1, hence is CENTRAL in CentExt κ⁰: the whole wild word collapses (d₀² = 1, d_g = d₀, h_c = c₀ = 1, u₁ = 1, x₁^σ = 1, and h₀ = x₀² on the nose — the paper's p. 15 "replacing h₀ by x₀²"). The split wild fibre is therefore the x₀-square q(v), with every starred m-entry dying on m_one.

noncomputable def GQ2.SectionEight.AffineTLift.sdCcHom {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] : Sd C V →* C

The C-component projection Sd C V →* C.

Equations

• GQ2.SectionEight.AffineTLift.sdCcHom = { toFun := GQ2.SectionEight.AffineTLift.Sd.cc, map_one' := ⋯, map_mul' := ⋯ }

theorem GQ2.SectionEight.AffineTLift.central_of_base_one {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (p : WordCoh2.CentExt (kappa0Cocycle dat hdat)) (hp : p.base = 1) (x : WordCoh2.CentExt (kappa0Cocycle dat hdat)) : p * x = x * p

Base-1 elements of CentExt κ⁰ are central (κ⁰ dies against 1 on both sides).

theorem GQ2.SectionEight.AffineTLift.liftMark_kappa0_wildValue_fib_split {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) [Finite C] [Finite V] (tS : Marking (Sd C V)) (hσv : tS.σ.v = 0) (hτv : tS.τ.v = 0) (hx1v : tS.x₁.v = 0) (hx0cc : tS.x₀.cc = 1) (hx1cc : tS.x₁.cc = 1) (hV₂ : ∀ (w : V), w + w = 0) (htau : ∀ (w : V), tS.τ.cc • w = w) (hU : ∀ (w : V), (sdBaseMarking tS).sigma2 • w = w) (hτodd : Odd (orderOf tS.τ.cc)) : (WordCoh2.liftMark tS (kappa0Cocycle dat hdat)).wildValue.fib = q tS.x₀.v

The split wild κ⁰-value is the x₀-square (paper (83), T = 1 case): with the structural pack, the lifted wild relator value has fibre q(x₀.v) — every starred m-entry dies on m_one, and the base-central d₀ collapses the word to x₀².

A-4.4: the ramified wild value = the Wall double

Ramified regime (V^T = 0): the structural pack persists, so d₀ still has cc = 1, but its V-part is now a := x₀.v (liftMarking_d0_u_ramified). The cc = 1 elements form the abelian V-slice, whose CentExt is the E_f-Heisenberg: commutators produce the polar form (commP_fib_cc_one), so c₀ = [d₀,z₀] ↦ B(a, U⁻¹a) — the p. 15 table's ramified entry. The h₀-peel telescopes to q(g₀⁻¹a) on one f_cocycle + f_diag + f_polar, and q-invariance gives q(a). Total: q(a) + B(a, U⁻¹a).

theorem GQ2.SectionEight.AffineTLift.sd_mul_comm_cc_one {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] (p r : Sd C V) (hp : p.cc = 1) (hr : r.cc = 1) : p * r = r * p

Sd-elements with cc = 1 commute (the abelian V-slice).

theorem GQ2.SectionEight.AffineTLift.sd_commP_cc_one {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] (p r : Sd C V) (hp : p.cc = 1) (hr : r.cc = 1) : commP p r = 1

commP of two V-slice elements of Sd is 1.

theorem GQ2.SectionEight.AffineTLift.kappa0_cc_one {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (p r : Sd C V) (hp : p.cc = 1) : (kappa0Cocycle dat hdat).κ p r = dat.f p.v r.v

The κ⁰-value on two V-slice bases is the bare f-value.

theorem GQ2.SectionEight.AffineTLift.inv_cc_one {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (p : WordCoh2.CentExt (kappa0Cocycle dat hdat)) (hp : p.base.cc = 1) (hV₂ : ∀ (w : V), w + w = 0) : p⁻¹.base = p.base ∧ p⁻¹.fib = p.fib + q p.base.v

The inverse of a V-slice CentExt-element: same base (char 2), fibre shifted by q of the V-part.

theorem GQ2.SectionEight.AffineTLift.commP_fib_cc_one {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (p r : WordCoh2.CentExt (kappa0Cocycle dat hdat)) (hp : p.base.cc = 1) (hr : r.base.cc = 1) (hV₂ : ∀ (w : V), w + w = 0) : (commP p r).fib = QuadraticFp2.polar q p.base.v r.base.v

The V-slice commutator fibre is the polar form (the [d₀,z₀]-cell): for CentExt κ⁰-elements over cc = 1 bases, commP has base 1 and fibre polar q of the V-parts.

theorem GQ2.SectionEight.AffineTLift.liftMark_ramified_h0_fib {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) (A X Dg D F : WordCoh2.CentExt (kappa0Cocycle dat hdat)) (a b : V) (mA fD : ZMod 2) (hV₂ : ∀ (w : V), w + w = 0) (hAv : A.base.v = a) (hAcc : A.base.cc = 1) (hAf : A.fib = mA) (hXv : X.base.v = b) (hXcc : X.base.cc = 1) (hXf : X.fib = 0) (hDgv : Dg.base.v = a) (hDgcc : Dg.base.cc = 1) (hDgf : Dg.fib = fD + mA) (hDv : D.base.v = b) (hDcc : D.base.cc = 1) (hDf : D.fib = fD) (hFbase : F.base = 1) (hFf : F.fib = QuadraticFp2.polar q a b) : (A * X * Dg * D * D ^ 2 * F).base.v = 0 ∧ (A * X * Dg * D * D ^ 2 * F).base.cc = 1 ∧ (A * X * Dg * D * D ^ 2 * F).fib = mA + dat.f a b + (fD + mA) + dat.f (a + b) a + fD + q b + q b + QuadraticFp2.polar q a b

The ramified h₀-telescope fibre (V^T = 0 prefix peel): for the six-factor wild prefix A · X · Dg · D · D² · F over cc = 1 bases — A, Dg on the V-part a, X, D on b, and F slice-trivial (base = 1) — the base collapses to (0, 1) and each kappa0_cc_one step deposits one f-atom, giving the accumulated fibre below. This is the V^T = 0 analog of the split h₀ = x₀² collapse: nothing is central here.

theorem GQ2.SectionEight.AffineTLift.liftMark_kappa0_wildValue_fib_ramified {C : Type u_1} {V : Type u_2} [Group C] [AddCommGroup V] [DistribMulAction C V] {q : V → ZMod 2} (dat : FactorSet C V) (hdat : IsEquivariantFactorSet q dat) [Finite C] [Finite V] (tS : Marking (Sd C V)) (hσv : tS.σ.v = 0) (hτv : tS.τ.v = 0) (hx1v : tS.x₁.v = 0) (hx0cc : tS.x₀.cc = 1) (hx1cc : tS.x₁.cc = 1) (hV₂ : ∀ (w : V), w + w = 0) (htauf : ∀ (w : V), tS.τ.cc • w = w → w = 0) (hτodd : Odd (orderOf tS.τ.cc)) (hqg0 : q ((sdBaseMarking tS).g0⁻¹ • tS.x₀.v) = q tS.x₀.v) : (WordCoh2.liftMark tS (kappa0Cocycle dat hdat)).wildValue.fib = q tS.x₀.v + QuadraticFp2.polar q tS.x₀.v ((sdBaseMarking tS).sigma2⁻¹ • tS.x₀.v)

The ramified wild κ⁰-value is the Wall double (paper (83), V^T = 0 case): with the structural pack, the lifted wild relator value has fibre q(x₀.v) + polar q x₀.v (σ₂⁻¹ • x₀.v). Unlike the split case d₀ is no longer central — it carries the V-coordinate x₀.v (the banked ramified row liftMarking_d0_u_ramified) — but every h₀-factor stays in the abelian V-slice (cc = 1), so the peel proceeds by kappa0_cc_one steps: the [d₀,z₀]-commutator c₀ contributes the polar term (commP_fib_cc_one), and the h₀-telescope closes on q(g₀⁻¹ • x₀.v) = q(x₀.v) by the q-invariance hypothesis hqg0.