The traced chain rows and the trivial-module self-duality for r_R (⟦lem:stokes⟧, ⟦lem:trivial⟧) #
The Γ_R counterparts of GQ2.FoxHeisenberg.Traced's wild chain-map rows and
GQ2.TrivialSelfDual's base case of the Prop. 5.15 dévissage, for the Roe candidate word
r_R = (x₀^σ)⁻¹ · (x₀⁻³τ)^{ω₂} · x₁² · [x₁, x₁^{σ₂}] (GQ2.Roe.Words).
The traced chain rows (⟦lem:stokes⟧, Prop 5.8) #
prop_5_8_left_R/prop_5_8_right_R: the traced mixed coordinate mixedB_R
(GQ2.Roe.FoxBasic) at a coboundary d⁰a splits into the dual first-relation Fox rows,
B_{R,ρ,A}(d⁰a, y) = ⟨a, L^{A^∨}_t(y) + L^{A^∨}_w(y)⟩. The tame row (mixedB_tameRow_R) is
Γ_A's verbatim (the tame relator is shared, d1FunR_fst); the wild row (mixedB_wildRow_R) runs
the Roe wild bridge bridge_wildR through the generic finite-word Stokes formula lemma_5_7_left,
its two ε-corrections y_τ(τ·a) matching the tame ones because the Roe wild ε-vector is
(0,1,0,0) at the odd ω₂-representative (R23's expMod2_wildValueExpR_odd at
omega2Exp_exponent_heis_cast) — the endpoint condition ⟦lem:stokes⟧.
The trivial module (⟦lem:trivial⟧) #
For V = 𝔽₂ with trivial action, d¹_R(a,b,c,d) = (b,b) (R21's d1R_of_trivial), so
Z¹_R = {x | x₁ = 0} has coordinates (a,c,d) = (x₀,x₂,x₃) and B¹_R = ⊥, giving the two card
clauses. The degree-one pairing is the scalar Gram ⟦eq:scalarform⟧
⟨(a,c,d),(a',c',d')⟩ = a·c' + c·a' + d·d', matrix [[0,1,0],[1,0,0],[0,0,1]] (⟦eq:cupmatrix⟧),
whose closed form mixedB_cocycle_R is the Roe twin of mixedB_cocycle
(GQ2.MixedBilinear) — cleaner: the honest diagonal d·d' on the (3,3) slot comes from the
square x₁², and the opaque ω₂ scalar aR.z is confined to the (2,2) slot (with Γ_A's
u₁.z moved from (3,3) to (2,2) by the x₀ ↔ x₁ wild-column swap), killed on the single-slot
duals used for nondegeneracy. Nonsingularity is a 3×3 unit-determinant decide.
The traced chain rows of Prop 5.8 for r_R (⟦lem:stokes⟧) #
The tame row of Prop 5.8 (41) for r_R — Γ_A's mixedB_tameRow reused verbatim: the
tame relator is shared, so its mixed central coordinate is unchanged, and the first Fox component
(d1FunR t y).1 = (d1Fun t y).1 (d1FunR_fst).
The wild hr for r_R: the free Roe word wildValueExpR freeMarking (omega2Exp N) has
trivial lower value at N = exponent (H(A)⋊C), from WildRelR — the Γ_R twin of
lift_markVec_wildValueExp_eq_one, with the two ω₂-subword orders (σ, x₀⁻³τ) dividing N.
The wild .l-bridge for r_R: the .l-coordinate of the y-only Roe-wild evaluation is
d¹_R's wild row on the dual (the Γ_R analogue of stokesEval_wild_l).
The wild row of Prop 5.8 (41) for r_R: the wild summand at the coboundary d⁰a equals
the pairing ⟨a, L^{A^∨}_w(y)⟩ plus the ε-correction y_τ(τ·a) — the same correction as the tame
row, because the Roe wild ε-vector reduces to (0,1,0,0) at the odd ω₂-representative
(expMod2_wildValueExpR_odd at omega2Exp_exponent_heis_cast, ⟦lem:stokes⟧).
Prop 5.8, display (41) for r_R: B_{R,ρ,A}(d⁰a, y) = ⟨a, L^{A^∨}_t(y) + L^{A^∨}_w(y)⟩,
the dual first-relation Fox rows. Assembled exactly as Γ_A's prop_5_8_left: the two
y_τ(τ·a) ε-corrections cancel in char 2 (⟦lem:stokes⟧, "Their sum is zero").
The tame row of Prop 5.8 (42) for r_R (dual form) — Γ_A's mixedB_tameRow_right
reused: shared tame relator, d1FunR_fst.
The .a-bridge for r_R: the .a-coordinate of the x-only Roe-wild evaluation is d¹_R's
wild row on A (the Γ_R analogue of stokesEval_wild_a; the A⋊C exponent divisibility is
re-derived through the public section secWA so no private helper is needed).
The wild row of Prop 5.8 (42) for r_R (dual form): ⟨L^A_w(x), λ⟩ + λ(x_τ).
Prop 5.8, display (42) for r_R: B_{R,ρ,A}(x, d⁰λ) = ⟨L_t(x)+L_w(x), λ⟩. Assembled as
Γ_A's prop_5_8_right: the two λ(x_τ) corrections cancel (char 2).
The trivial module 𝔽₂ is self-dual for r_R (⟦lem:trivial⟧) #
On the trivial module Z¹_R = {x | x₁ = 0} (the note's coordinates (a,c,d) = (x₀,x₂,x₃)).
On the trivial module range d¹_R = Δ (the diagonal a ↦ (a,a)), of cardinality #A.
Card clause for H²_R: #H²_R = #A on the trivial module (H²_R = (A×A)/Δ).
Card clause for Z¹_R: #Z¹_R = (#A)³ on the trivial module (Z¹_R = {x | x₁ = 0}).
The wild .z peel on cocycles (⟦lem:trivial⟧, the Gram closed form) #
The Roe wild word wildValueR = (x₀^σ)⁻¹ · aR · x₁² · cR (aR = (x₀⁻³τ)^{ω₂}) evaluated at
heisMarking t x y on the split cocycles {x₁ = 0, y₁ = 0}, peeled factor-by-factor with the
generic HeisLift API (every .g acts trivially via htriv). The honest diagonal y₃(x₃)
comes from x₁²; the symplectic y₂(x₀) − y₀(x₂) from (x₀^σ)⁻¹; cR cancels in char 2; and
the opaque ω₂ scalar aR.z is confined to the (2,2) slot.
Wild .z, the x₁² factor: the honest Heisenberg diagonal y₃(x₃) — the (3,3) Gram
entry. x₁.a = x₃, x₁.l = y₃, x₁.z = 0, so (x₁·x₁).z = y₃(x₃).
Wild .z, the cR = [x₁, x₁^{σ₂}] factor vanishes on the trivial module: the two
symplectic commutator terms y₃(x₃) + y₃(x₃) cancel in char 2 (U = σ₂ acts trivially; the
general-cocycle analogue of R24's heisMarking_cR_z_split_cancels).
The .a-coordinate of aR at heisMarking is its primal Fox derivative on A
(the agHom-projection to liftMarking): aR.a = (liftMarking t x).aR.u.
Wild .z assembly on cocycles: peeling wildValueR = (x₀^σ)⁻¹ · aR · x₁² · cR keeps the
symplectic y₂(x₀) − y₀(x₂) (from (x₀^σ)⁻¹, its inv_z diagonal y₂(x₂) cancelling the
aR-cross-term −y₂(aR.a) = −y₂(x₂) because aR.a = x₂), the honest diagonal y₃(x₃) (from
x₁²), the opaque ω₂ scalar aR.z (the (2,2) slot), and cR.z = 0.
aR.z = 0 when y₂ = 0 (on cocycles): aR = powOmega2((x₀⁻³τ)) and the base has l = z = 0,
so its powers do too — the Γ_R analogue of heisMarking_u1_z_of_y3_zero, on the (2,2) slot.
aR.z = 0 when x₂ = 0 (on cocycles), dually (heisLift_pow_a_z_zero).
The trivial-module degree-one pairing on cocycles (⟦lem:trivial⟧, ⟦eq:scalarform⟧):
mixedB_R t x y = y₂(x₀) − y₀(x₂) + y₃(x₃) + aR.z, the tame part vanishing
(stokesEval_tame_z_trivial_cocycle) and the wild part from the peel. The opaque aR.z is the
ω₂ scalar, confined to the (2,2) slot (killed on single-slot duals with y₂ = 0 or x₂ = 0);
the scalar Gram is [[0,1,0],[1,0,0],[0,0,1]] (scalarGramR_nonsingular).
The Roe self-duality package (Γ_R twin of IsSelfDual, over the r_R complex d¹_R):
the display-(56) numerics and a perfect degree-one pairing descending mixedB_R. This is the
base-case return type of the r_R dévissage entry point (consumed by R26).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The r_R dévissage base case (⟦lem:trivial⟧): the trivial module 𝔽₂ is self-dual for the
Roe complex. Both card clauses (card_H2wR_trivial/card_Z1wR_trivial with
card_fixedPts_elemDual_trivial) and the degree-one pairing (the scalar Gram ⟦eq:scalarform⟧) hold:
mixedB_R descends to H¹_R = Z¹_R (since B¹_R = ⊥), its closed form mixedB_cocycle_R has
unit-determinant Gram [[0,1,0],[1,0,0],[0,0,1]] (the ω₂ scalar aR.z sits only on the (2,2)
slot, killed by the paired single-slot dual), and elemDual_separates supplies the witnesses.
Consumed by R26's selfDual_of_simple_R/prop_5_15_of_simple_R.
Nonsingularity of the scalar Gram (⟦eq:scalarform⟧/⟦eq:cupmatrix⟧) #
The cup–Bockstein form ⟨(a,c,d),(a',c',d')⟩ = a·c' + c·a' + d·d' on H¹_R(𝔽₂) = 𝔽₂³ has matrix
[[0,1,0],[1,0,0],[0,0,1]] (⟦eq:cupmatrix⟧); a decide confirms it is nonsingular (left and right
nondegenerate), the finite 𝔽₂-linear-algebra stress test underlying trivialSelfDual_R.
The scalar cup–Bockstein form on H¹_R(𝔽₂) in coordinates (a,c,d) (⟦eq:scalarform⟧).
Equations
- GQ2.FoxH.scalarGramR v w = v 0 * w 1 + v 1 * w 0 + v 2 * w 2
Instances For
Nonsingularity of the scalar Gram (⟦eq:cupmatrix⟧, the 3×3 unit-determinant check): the
form a·c' + c·a' + d·d' is left- and right-nondegenerate over ZMod 2, by decide.