Ordinary traces of types E_7 and E_8 (Lemma A.6)

lem:e78-traces (periodic-mesh-calculations.tex). Write x, y for the closed paths along the long and medium arms; the short arm gives (x + y)² = 0, and x⁵ = y³ = 0. The word identities y² = -yx - xy - x², yxy = xyx + x³, yx²y = -yx³ - xyx² - x²yx - x³y - 2x⁴ and F = yx³yx + yx⁴y + xyx³y - x²yx³ - x³yx² = 0 reduce cyclic words by their gaps (the numbers of x's between successive y's): "If a gap has length zero, one or two, apply the corresponding one of the first three identities. Each resulting term has fewer y's." The remaining words are cyclic words in a = yx³, b = yx⁴, and the relations [a²W] = 0, [abW] = -[baW], [b^q] = 0 dispose of them.

With two invertible only degrees three, five and nine survive (part (2)); we record the vanishing in all other word degrees, which is what the period exclusion uses. A word y x^{g₁} ⋯ y x^{g_k} is blk [g₁, …, g_k]; the induction runs on the number k of y's, in a fixed word degree.

def MultiplicativeBasisDeformations.TraceAlg.E78.blk {S : Type u_1} [Ring S] (x y : S) : List ℕ → S

The word y x^{g₁} y x^{g₂} ⋯ y x^{g_k}.

structure MultiplicativeBasisDeformations.TraceAlg.E78.Hyp0 {S : Type u_1} [Ring S] (x y : S) {M : Type u_2} [AddCommGroup M] (tr : S →+ M) : Prop

The hypotheses of Lemma A.6 over any coefficient ring.

• x5 : x ^ 5 = 0
• y3 : y ^ 3 = 0
• d1 : y * y + y * x + x * y + x * x = 0
• rot (p q : S) : tr (p * q) = tr (q * p)
• xp (q : ℕ) : 1 ≤ q → tr (x ^ q) = 0
• ty : tr y = 0
• ty2 : tr (y * y) = 0

structure MultiplicativeBasisDeformations.TraceAlg.E78.Hyp {S : Type u_1} [Ring S] (x y : S) {M : Type u_2} [AddCommGroup M] (tr : S →+ M) extends MultiplicativeBasisDeformations.TraceAlg.E78.Hyp0 x y tr : Prop

The hypotheses of Lemma A.6 with two invertible.

• x5 : x ^ 5 = 0
• y3 : y ^ 3 = 0
• d1 : y * y + y * x + x * y + x * x = 0
• rot (p q : S) : tr (p * q) = tr (q * p)
• xp (q : ℕ) : 1 ≤ q → tr (x ^ q) = 0
• ty : tr y = 0
• ty2 : tr (y * y) = 0
• two (m : M) : m + m = 0 → m = 0

theorem MultiplicativeBasisDeformations.TraceAlg.E78.blk_append {S : Type u_1} [Ring S] {x y : S} (g₁ g₂ : List ℕ) : blk x y (g₁ ++ g₂) = blk x y g₁ * blk x y g₂

theorem MultiplicativeBasisDeformations.TraceAlg.E78.tr_blk_rotate {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H₀ : Hyp0 x y tr) (g₁ g₂ : List ℕ) : tr (blk x y (g₁ ++ g₂)) = tr (blk x y (g₂ ++ g₁))

theorem MultiplicativeBasisDeformations.TraceAlg.E78.blk_snoc_mul {S : Type u_1} [Ring S] {x y : S} (g₀ : List ℕ) (h j : ℕ) : blk x y (g₀ ++ [h]) * x ^ j = blk x y (g₀ ++ [h + j])

theorem MultiplicativeBasisDeformations.TraceAlg.E78.tr_bump {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H₀ : Hyp0 x y tr) (g₀ : List ℕ) (h j : ℕ) : tr (x ^ j * blk x y (g₀ ++ [h])) = tr (blk x y (g₀ ++ [h + j]))

Leading x's rotate into the last gap.

theorem MultiplicativeBasisDeformations.TraceAlg.E78.blk_big {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H₀ : Hyp0 x y tr) (e : ℕ) (he : 5 ≤ e) (g : List ℕ) : blk x y (e :: g) = 0

The word identities

theorem MultiplicativeBasisDeformations.TraceAlg.E78.I1 {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H₀ : Hyp0 x y tr) (T : S) : y * (y * T) = -(y * (x * T)) - x * (y * T) - x * (x * T)

theorem MultiplicativeBasisDeformations.TraceAlg.E78.d2 {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H₀ : Hyp0 x y tr) : y * x * y - x * y * x - x ^ 3 = 0

theorem MultiplicativeBasisDeformations.TraceAlg.E78.I2 {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H₀ : Hyp0 x y tr) (T : S) : y * (x * (y * T)) = x * (y * (x * T)) + x * (x * (x * T))

theorem MultiplicativeBasisDeformations.TraceAlg.E78.d3 {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H₀ : Hyp0 x y tr) : y * x ^ 2 * y + y * x ^ 3 + x * y * x ^ 2 + x ^ 2 * y * x + x ^ 3 * y + 2 * x ^ 4 = 0

theorem MultiplicativeBasisDeformations.TraceAlg.E78.I3 {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H₀ : Hyp0 x y tr) (T : S) : y * (x * (x * (y * T))) = -(y * (x * (x * (x * T)))) - x * (y * (x * (x * T))) - x * (x * (y * (x * T))) - x * (x * (x * (y * T))) - 2 * (x * (x * (x * (x * T))))

theorem MultiplicativeBasisDeformations.TraceAlg.E78.F_eq {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H₀ : Hyp0 x y tr) : y * x ^ 3 * y * x + y * x ^ 4 * y + x * y * x ^ 3 * y - x ^ 2 * y * x ^ 3 - x ^ 3 * y * x ^ 2 = 0

Gap reductions

theorem MultiplicativeBasisDeformations.TraceAlg.E78.red0 {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H₀ : Hyp0 x y tr) (h : ℕ) (g : List ℕ) : blk x y (0 :: h :: g) = -blk x y ((h + 1) :: g) - x ^ 1 * blk x y (h :: g) - x ^ (h + 2) * blk x y g

Gap zero (y² = -yx - xy - x²).

theorem MultiplicativeBasisDeformations.TraceAlg.E78.red1 {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H₀ : Hyp0 x y tr) (h : ℕ) (g : List ℕ) : blk x y (1 :: h :: g) = x ^ 1 * blk x y ((h + 1) :: g) + x ^ (h + 3) * blk x y g

Gap one (yxy = xyx + x³).

theorem MultiplicativeBasisDeformations.TraceAlg.E78.red2 {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H₀ : Hyp0 x y tr) (h : ℕ) (g : List ℕ) : blk x y (2 :: h :: g) = -blk x y ((h + 3) :: g) - x ^ 1 * blk x y ((h + 2) :: g) - x ^ 2 * blk x y ((h + 1) :: g) - x ^ 3 * blk x y (h :: g) - 2 * (x ^ (h + 4) * blk x y g)

Gap two.

def MultiplicativeBasisDeformations.TraceAlg.E78.Z {S : Type u_1} [Ring S] (x y : S) {M : Type u_2} [AddCommGroup M] (tr : S →+ M) (n K : ℕ) : Prop

All words of word degree n with at most K letters y have zero trace.

theorem MultiplicativeBasisDeformations.TraceAlg.E78.Z_zero {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) (n : ℕ) (hn : 1 ≤ n) : Z x y tr n 0

theorem MultiplicativeBasisDeformations.TraceAlg.E78.bad_zero {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) {n K : ℕ} (hK : 1 ≤ K) (hZ : Z x y tr n K) (g : List ℕ) (hg : g.length = K + 1) (hs : K + 1 + g.sum = n) (e : ℕ) (he : e ∈ g) (hbad : e ≤ 2 ∨ 5 ≤ e) : tr (blk x y g) = 0

A gap of length at most two, or at least five, gives zero trace.

theorem MultiplicativeBasisDeformations.TraceAlg.E78.Z.blk {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} {n K : ℕ} (hZ : Z x y tr n K) (g : List ℕ) (h1 : g.length ≤ K) (h2 : g.length + g.sum = n) : tr (E78.blk x y g) = 0

Words in a = yx³ and b = yx⁴

theorem MultiplicativeBasisDeformations.TraceAlg.E78.nil_or_snoc {α : Type u_3} (g : List α) : g = [] ∨ ∃ (g₀ : List α) (h : α), g = g₀ ++ [h]

theorem MultiplicativeBasisDeformations.TraceAlg.E78.aa {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) {n K : ℕ} (hK : 1 ≤ K) (hZ : Z x y tr n K) (g : List ℕ) (hlen : g.length + 1 = K) (hs : K + 7 + g.sum = n) : tr (blk x y (3 :: 3 :: g)) = 0

[a²W] = 0, from the trace of F x² W.

theorem MultiplicativeBasisDeformations.TraceAlg.E78.ab_ba {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) {n K : ℕ} (hK : 1 ≤ K) (hZ : Z x y tr n K) (g : List ℕ) (hne : g ≠ []) (hlen : g.length + 1 = K) (hs : K + 8 + g.sum = n) : tr (blk x y (3 :: 4 :: g)) = -tr (blk x y (4 :: 3 :: g))

[abW] = -[baW] for nonempty W, from the trace of F x³ W.

theorem MultiplicativeBasisDeformations.TraceAlg.E78.bb {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) (g : List ℕ) : tr (blk x y (4 :: 4 :: g)) = -tr (x ^ 1 * blk x y (3 :: 4 :: g))

[b²W] = -[x a b W], from the trace of F x⁴ W.

theorem MultiplicativeBasisDeformations.TraceAlg.E78.cases34 (l : List ℕ) (hl : ∀ e ∈ l, e = 3 ∨ e = 4) : l = List.replicate l.length 4 ∨ ∃ (r : ℕ) (l' : List ℕ), l = List.replicate r 4 ++ 3 :: l'

theorem MultiplicativeBasisDeformations.TraceAlg.E78.chain {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) {n K : ℕ} (hK : 1 ≤ K) (hZ : Z x y tr n K) (r : ℕ) (g : List ℕ) (hlen : r + g.length + 1 = K) (hs : K + 7 + 4 * r + g.sum = n) : tr (blk x y (3 :: (List.replicate r 4 ++ 3 :: g))) = 0

Two a's are brought together using [abW] = -[baW].

theorem MultiplicativeBasisDeformations.TraceAlg.E78.blocks_zero {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) {n K : ℕ} (hK : 1 ≤ K) (hZ : Z x y tr n K) (h9 : n = 9 → tr (blk x y [3, 4]) = 0) (g : List ℕ) (hlen : g.length = K + 1) (hg : ∀ e ∈ g, e = 3 ∨ e = 4) (hs : K + 1 + g.sum = n) : tr (blk x y g) = 0

Cyclic words in a, b with at least two blocks vanish outside word degree nine.

theorem MultiplicativeBasisDeformations.TraceAlg.E78.single {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) (j : ℕ) (hj : j ≠ 2) (hj4 : j = 4 → tr (blk x y [4]) = 0) : tr (blk x y [j]) = 0

Words with one y: t_j = [yx^j] vanishes for j = 0, 1, 3 and j ≥ 5.

theorem MultiplicativeBasisDeformations.TraceAlg.E78.all_zero {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) (n : ℕ) (hn : 1 ≤ n) (h3 : n ≠ 3) (h5 : n = 5 → tr (blk x y [4]) = 0) (h9 : n = 9 → tr (blk x y [3, 4]) = 0) (K : ℕ) : Z x y tr n K

Lemma A.6 with two invertible, by word degree: in word degree n ∉ {3}, every word in x, y has zero trace, provided [yx⁴] = 0 in degree five and [ab] = 0 in degree nine.

Words as combinations of gap words

def MultiplicativeBasisDeformations.TraceAlg.E78.span {S : Type u_1} [Ring S] (x y : S) (n : ℕ) : AddSubgroup S

The span of the gap words of word degree n.

theorem MultiplicativeBasisDeformations.TraceAlg.E78.span_mul_left {S : Type u_1} [Ring S] {x y : S} (n : ℕ) {u r : S} (hu : ∀ (j : ℕ) (g : List ℕ), j + g.length + g.sum = n → u * (x ^ j * blk x y g) ∈ span x y (n + 1)) (hr : r ∈ span x y n) : u * r ∈ span x y (n + 1)

theorem MultiplicativeBasisDeformations.TraceAlg.E78.x_mul_mem {S : Type u_1} [Ring S] {x y : S} (n : ℕ) {r : S} (hr : r ∈ span x y n) : x * r ∈ span x y (n + 1)

theorem MultiplicativeBasisDeformations.TraceAlg.E78.y_mul_mem {S : Type u_1} [Ring S] {x y : S} (n : ℕ) {r : S} (hr : r ∈ span x y n) : y * r ∈ span x y (n + 1)

theorem MultiplicativeBasisDeformations.TraceAlg.E78.span_zero {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) (n : ℕ) (hn : 1 ≤ n) (h3 : n ≠ 3) (h5 : n = 5 → tr (blk x y [4]) = 0) (h9 : n = 9 → tr (blk x y [3, 4]) = 0) {r : S} (hr : r ∈ span x y n) : tr r = 0

Vanishing on the span in word degrees other than three.

Application to the twisted traces of E_7 and E_8

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.tw2_id {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) (hθ : ∀ (i : Fin 3), D.θ i = i) (r : R2 L) : D.tw2 r = r

theorem MultiplicativeBasisDeformations.TraceAlg.trace_E78 {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) (h2 : ∀ (m : M), m + m = 0 → m = 0) {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 1) (hLc : L c = 2 ∨ L c = 3) (hθ : ∀ (i : Fin 3), D.θ i = i) (w : List (Fin 3)) (hw : 1 ≤ w.length) (h3 : w.length ≠ 3) (h59 : L c = 3 → w.length ≠ 5 ∧ w.length ≠ 9) : D.tr w = 0

Ordinary traces of E_7 and E_8 vanish outside word degrees 3, 5, 9 (Lemma A.6(2)); for E_7 only word degree three remains.