Type D traces in every characteristic (Appendix B)

characteristic-two-mesh-calculations.tex: "In word degree j < N the alternating words w_j, w'_j, starting with x, y, span; in degree N they satisfy w_N + w'_N = 0. Multiplying this relation by x and y shows that both alternating words of degree N + 1 are zero. … In the ordinary trace, the one-letter classes vanish …. An odd alternating word of length at least three rotates to a word containing a square. For even j, rotation identifies w_j and w'_j. … If ι interchanges the two short arms, twisted rotation turns an even alternating word into a word containing a square, while in odd degree the two alternating words become equal."

We record this without assumptions on the characteristic: every positive trace is an integer multiple of the trace of the alternating word altE starting with x; that trace vanishes in odd degree for the trivial twist, in even degree for the interchange, and in degree above N = L c + 2, where c is the long arm.

def MultiplicativeBasisDeformations.TraceAlg.altE {S : Type u_1} [Ring S] (p q : S) (n : ℕ) : S

The alternating word of length n starting with p.

theorem MultiplicativeBasisDeformations.TraceAlg.altE_even {S : Type u_1} [Ring S] (p q : S) (r : ℕ) : altE p q (2 * r) = (p * q) ^ r

theorem MultiplicativeBasisDeformations.TraceAlg.altE_odd {S : Type u_1} [Ring S] (p q : S) (r : ℕ) : altE p q (2 * r + 1) = (p * q) ^ r * p

theorem MultiplicativeBasisDeformations.TraceAlg.altE_succ_even {S : Type u_1} [Ring S] (p q : S) (r : ℕ) : altE p q (2 * r + 1) = altE p q (2 * r) * p

theorem MultiplicativeBasisDeformations.TraceAlg.altE_succ_odd {S : Type u_1} [Ring S] (p q : S) (r : ℕ) : altE p q (2 * r + 2) = altE p q (2 * r + 1) * q

theorem MultiplicativeBasisDeformations.TraceAlg.altE_eq_zero_of_le {S : Type u_1} [Ring S] (p q : S) (n : ℕ) (hn : altE p q n = 0) (n' : ℕ) : n ≤ n' → altE p q n' = 0

theorem MultiplicativeBasisDeformations.TraceAlg.altE_zero_of_pow {S : Type u_1} [Ring S] {p q : S} (hp : p * p = 0) (hq : q * q = 0) {N : ℕ} (hN : 1 ≤ N) (hpow : (p + q) ^ N = 0) (n : ℕ) : N + 1 ≤ n → altE p q n = 0

Alternating words above the nilpotency degree vanish: if (p + q)^N = 0, then altE (N + 1) = 0.

theorem MultiplicativeBasisDeformations.TraceAlg.xa_sq {L : Fin 3 → ℕ} {a : Fin 3} (hLa : L a = 0) : x L a * x L a = 0

theorem MultiplicativeBasisDeformations.TraceAlg.xb_sq {L : Fin 3 → ℕ} {b : Fin 3} (hLb : L b = 0) : x L b * x L b = 0

theorem MultiplicativeBasisDeformations.TraceAlg.xc_eq {L : Fin 3 → ℕ} {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) : x L c = -(x L a + x L b)

theorem MultiplicativeBasisDeformations.TraceAlg.altE_zero {L : Fin 3 → ℕ} {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 0) (n : ℕ) (hn : L c + 3 ≤ n) : altE (x L a) (x L b) n = 0

Alternating words vanish above degree N = L c + 2.

theorem MultiplicativeBasisDeformations.TraceAlg.trace_D_span {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 0) (hθ : D.θ a = a ∧ D.θ b = b ∨ D.θ a = b ∧ D.θ b = a) {w : List (Fin 3)} (hw : w ≠ []) : ∃ (z : ℤ), D.tr w = z • D.trR (altE (x L a) (x L b) w.length)

Every positive trace is a multiple of the trace of the alternating word.

theorem MultiplicativeBasisDeformations.TraceAlg.trace_altE_odd {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) {a b : Fin 3} (hLa : L a = 0) (hLb : L b = 0) (ha : D.θ a = a) (hb : D.θ b = b) (r : ℕ) : D.trR (altE (x L a) (x L b) (2 * r + 1)) = 0

With the trivial twist on the short arms, odd alternating words have zero trace.

theorem MultiplicativeBasisDeformations.TraceAlg.trace_altE_even {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) {a b : Fin 3} (hLb : L b = 0) (ha : D.θ a = b) (r : ℕ) (hr : 1 ≤ r) : D.trR (altE (x L a) (x L b) (2 * r)) = 0

With the short-arm interchange, even alternating words have zero trace.