Documentation

GQ2.MixedBilinear

Bilinearity of the traced mixed coordinate mixedB #

The degree-one pairing mixedB t x y = (heisMarking t x y).tameValue.z + (…).wildValue.z is bilinear in the offsets (x, y). Via bridge_tame/bridge_wild this reduces to bilinearity of (stokesEval c x y r).z for an arbitrary free-group word r, which is an induction on r using the HeisLift coordinate cocycle rules: the .a-coordinate depends only on x, the .l-coordinate only on y, the .g-coordinate on neither, and the .z-coordinate is the bilinear cross-term Σ λ_left(a_right).

This is the general-offset toolkit consumed by the trivial-module Gram matrix (the Prop. 5.15 proof part i) and the ramified mixed Hessian (the §5 proof layer).

theorem GQ2.FoxH.stokesEval_a_indep {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] {n : } (c : Fin nC) (x : Fin nA) (y y' : Fin nElemDual A) (r : FreeGroup (Fin n)) :
((stokesEval c x y) r).a = ((stokesEval c x y') r).a

The .a-coordinate of a Stokes evaluation is independent of the dual offsets y.

theorem GQ2.FoxH.stokesEval_l_indep {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] {n : } (c : Fin nC) (x x' : Fin nA) (y : Fin nElemDual A) (r : FreeGroup (Fin n)) :
((stokesEval c x y) r).l = ((stokesEval c x' y) r).l

The .l-coordinate of a Stokes evaluation is independent of the primal offsets x.

theorem GQ2.FoxH.stokesEval_a_zero_dual {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] {n : } (c : Fin nC) (x : Fin nA) (y : Fin nElemDual A) (r : FreeGroup (Fin n)) :
((stokesEval c x y) r).a = ((stokesEval c x 0) r).a

Canonical form of stokesEval_a_indep (dual offsets set to 0).

theorem GQ2.FoxH.stokesEval_l_zero_prim {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] {n : } (c : Fin nC) (x : Fin nA) (y : Fin nElemDual A) (r : FreeGroup (Fin n)) :
((stokesEval c x y) r).l = ((stokesEval c 0 y) r).l

Canonical form of stokesEval_l_indep (primal offsets set to 0).

theorem GQ2.FoxH.stokesEval_a_add {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] {n : } (c : Fin nC) (x x' : Fin nA) (y : Fin nElemDual A) (r : FreeGroup (Fin n)) :
((stokesEval c (x + x') y) r).a = ((stokesEval c x y) r).a + ((stokesEval c x' y) r).a

The .a-coordinate is additive in the primal offsets x.

theorem GQ2.FoxH.stokesEval_l_add {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] {n : } (c : Fin nC) (x : Fin nA) (y y' : Fin nElemDual A) (r : FreeGroup (Fin n)) :
((stokesEval c x (y + y')) r).l = ((stokesEval c x y) r).l + ((stokesEval c x y') r).l

The .l-coordinate is additive in the dual offsets y.

theorem GQ2.FoxH.stokesEval_z_add_left {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] {n : } (c : Fin nC) (x x' : Fin nA) (y : Fin nElemDual A) (r : FreeGroup (Fin n)) :
((stokesEval c (x + x') y) r).z = ((stokesEval c x y) r).z + ((stokesEval c x' y) r).z

.z is additive in the primal offsets x.

theorem GQ2.FoxH.stokesEval_z_add_right {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] {n : } (c : Fin nC) (x : Fin nA) (y y' : Fin nElemDual A) (r : FreeGroup (Fin n)) :
((stokesEval c x (y + y')) r).z = ((stokesEval c x y) r).z + ((stokesEval c x y') r).z

.z is additive in the dual offsets y.

theorem GQ2.FoxH.mixedB_add_left {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) (x x' : Fin 4A) (y : Fin 4ElemDual A) :
mixedB t (x + x') y = mixedB t x y + mixedB t x' y

mixedB is additive in the primal offsets x.

theorem GQ2.FoxH.mixedB_add_right {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) (x : Fin 4A) (y y' : Fin 4ElemDual A) :
mixedB t x (y + y') = mixedB t x y + mixedB t x y'

mixedB is additive in the dual offsets y.

The tame .z in closed form (trivial action) #

For a trivial C-action, fgTame = g₀⁻¹ g₁ g₀ g₁⁻² evaluates (untwisted Heisenberg) to the bilinear form below. Crucially every term carries an index-1 (τ) factor, so it vanishes on the split cocycles {x₁ = 0} — i.e. the trivial-module degree-one pairing is carried entirely by the wild relator, not the tame one.

theorem GQ2.FoxH.stokesEval_tame_z_trivial_cocycle {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (htriv : ∀ (g : C) (a : A), g a = a) (c : Fin 4C) (x : Fin 4A) (y : Fin 4ElemDual A) (hx : x 1 = 0) (hy : y 1 = 0) :
((stokesEval c x y) fgTame).z = 0

The tame .z (trivial action) vanishes on the split cocycles x₁ = 0, y₁ = 0.

theorem GQ2.FoxH.conjP_z_of_alzero {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p g : HeisLift A C) (hga : g.a = 0) (hgl : g.l = 0) :
(conjP p g).z = p.z

Conjugation by an a=l-slice element g (g.a = g.l = 0) fixes the central coordinate, even when g.z ≠ 0 and the base acts nontrivially: (conjP p g).z = p.z. (The two g.z contributions cancel in ZMod 2.) Strengthens conjP_z_of_slice by dropping g.z = 0 — needed because on general offsets g₀ = σ₂² has g₀.z = y₀(x₀) ≠ 0.

Wild .z, piece 1: the x₁^σ = σ⁻¹x₁σ factor (trivial action) #

One factor of the wild relator wildValue = h₀·u₁⁻¹·x₁^σ·c₀. Its central coordinate is the symplectic pairing of the σ- and x₁-slots, y₃(x₀) − y₀(x₃) — the (0,3)/(3,0) Gram entries.

theorem GQ2.FoxH.heisMarking_c0_z_cocycle {C : Type u_3} [Group C] [Finite C] {V : Type u_4} [AddCommGroup V] [DistribMulAction C V] [Finite V] (htriv : ∀ (g : C) (a : V), g a = a) (hV₂ : ∀ (v : V), v + v = 0) (t : Marking C) (x : Fin 4V) (y : Fin 4ElemDual V) (hx1 : x 1 = 0) (hy1 : y 1 = 0) :
(heisMarking t x y).c0.z = 0

Wild .z, piece 2: c₀ = [d₀,z₀] ↦ 0 on cocycles. The symplectic commutator vanishes because d₀.a = d₀.l = 0 there (liftMarking_d0_u = x₁ = 0). Same argument as heisMarking_c0_z, with x₁ = y₁ = 0 in place of x₀-support.

theorem GQ2.FoxH.heisMarking_h0_z_cocycle {C : Type u_3} [Group C] [Finite C] {V : Type u_4} [AddCommGroup V] [DistribMulAction C V] [Finite V] (htriv : ∀ (g : C) (a : V), g a = a) (hV₂ : ∀ (v : V), v + v = 0) (t : Marking C) (x : Fin 4V) (y : Fin 4ElemDual V) (hx1 : x 1 = 0) (hy1 : y 1 = 0) :
(heisMarking t x y).h0.z = (y 2) (x 2)

Wild .z, piece 3: h₀ ↦ y₂(x₂) on cocycles — the main term, giving the (2,2) Gram entry. Mirrors heisMarking_h0_z (the x₀-supported ↦ λ(c)) with x₁=y₁=0 in place of x₀-support: the d₀-derived leaf coords still vanish (liftMarking_d0_u = x₁ = 0), the ω₂ in d₀.z cancels via the dg·d₀ pair in char 2, and g₀ = σ₂² is a=l-slice (char-2 doubling) so conjP_z_of_alzero handles its nonzero .z.

theorem GQ2.FoxH.heisMarking_wildValue_z_cocycle {C : Type u_3} [Group C] [Finite C] {V : Type u_4} [AddCommGroup V] [DistribMulAction C V] [Finite V] (htriv : ∀ (g : C) (a : V), g a = a) (hV₂ : ∀ (v : V), v + v = 0) (t : Marking C) (x : Fin 4V) (y : Fin 4ElemDual V) (hx1 : x 1 = 0) (hy1 : y 1 = 0) :
(heisMarking t x y).wildValue.z = (y 2) (x 2) + (y 3) (x 0) - (y 0) (x 3) + (heisMarking t x y).u1.z

Wild .z assembly on cocycles: peeling wildValue = h₀·u₁⁻¹·(x₁^σ)·c₀ keeps the sum of the four factor .z's plus one cross-term. The u₁.l-terms — from inv_z (u₁⁻¹.z = u₁.z + u₁.l(u₁.a)) and from the (x₁^σ)-cross ((h₀u₁⁻¹).l = −u₁.l) — cancel because u₁.a = (x₁^σ).a = x₃ (both are the same primal Fox derivative), leaving the opaque u₁.z (the ω₂ scalar) confined to the (3,3) slot.

theorem GQ2.FoxH.mixedB_cocycle {C : Type u_3} [Group C] [Finite C] {V : Type u_4} [AddCommGroup V] [DistribMulAction C V] [Finite V] (htriv : ∀ (g : C) (a : V), g a = a) (hV₂ : ∀ (v : V), v + v = 0) (t : Marking C) (x : Fin 4V) (y : Fin 4ElemDual V) (hx1 : x 1 = 0) (hy1 : y 1 = 0) :
mixedB t x y = (y 2) (x 2) + (y 3) (x 0) - (y 0) (x 3) + (heisMarking t x y).u1.z

The trivial-module degree-one pairing on cocycles: mixedB t x y = y₂(x₂) + y₃(x₀) − y₀(x₃) + u₁.z, the tame part vanishing (stokesEval_tame_z_trivial_cocycle) and the wild part from the peel. The opaque u₁.z is the ω₂ scalar, confined to the (3,3) slot.

u₁.z is confined to the (3,3) slot #

theorem GQ2.FoxH.heisLift_pow_l_z_zero {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (w : HeisLift A C) (hl : w.l = 0) (hz : w.z = 0) (k : ) :
(w ^ k).l = 0 (w ^ k).z = 0

In the l = 0 subgroup of H(A)⋊C the .z is additive, so a power keeps l = 0, z = 0.

theorem GQ2.FoxH.heisLift_pow_a_z_zero {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (w : HeisLift A C) (ha : w.a = 0) (hz : w.z = 0) (k : ) :
(w ^ k).a = 0 (w ^ k).z = 0

In the a = 0 subgroup the .z is additive, so a power keeps a = 0, z = 0.

theorem GQ2.FoxH.heisMarking_u1_z_of_y3_zero {C : Type u_3} [Group C] {V : Type u_4} [AddCommGroup V] [DistribMulAction C V] (htriv : ∀ (g : C) (a : V), g a = a) (t : Marking C) (x : Fin 4V) (y : Fin 4ElemDual V) (hx1 : x 1 = 0) (hy1 : y 1 = 0) (hy3 : y 3 = 0) :
(heisMarking t x y).u1.z = 0

u₁.z = 0 when y₃ = 0 (on cocycles): u₁ = powOmega2(x₁τ) and x₁τ has l = 0, z = 0, so its powers do too.

theorem GQ2.FoxH.heisMarking_u1_z_of_x3_zero {C : Type u_3} [Group C] {V : Type u_4} [AddCommGroup V] [DistribMulAction C V] (htriv : ∀ (g : C) (a : V), g a = a) (t : Marking C) (x : Fin 4V) (y : Fin 4ElemDual V) (hx1 : x 1 = 0) :
y 1 = 0∀ (hx3 : x 3 = 0), (heisMarking t x y).u1.z = 0

u₁.z = 0 when x₃ = 0 (on cocycles), dually.