Ordinary traces of E_7 and E_8 in characteristic two (Appendix B)

characteristic-two-mesh-calculations.tex: "Apply Lemma A.6(1) in characteristic two. For a = yx³ and b = yx⁴, its block relations and 3[ab] = 0 give [a²W] = 0 (W ≠ 1), [abW] = [baW] (W ≠ 1), [ab] = 0, [b^q] = 0 (q ≥ 2). Words with two a's and at least three blocks vanish by bringing the a's together. With exactly one a, only ab² can remain: abʳ has word degree greater than fourteen for r ≥ 3. For the one-y words, the identities 3[yx²] = 0 and 5[yx⁴] = 0 still hold, whereas no vanishing follows from 2[yx] = 2[yx³] = 0. Thus the ordinary positive trace is spanned by yx, yx³, (yx³)², (yx³)(yx⁴)² in word degrees 2, 4, 8, 14."

We run the induction of Lemma A.6 on the number of y's in a fixed word degree n, with values in a subgroup A of the target containing the candidate class of degree n (all_mem).

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

The hypotheses in characteristic two.

• x5 : x ^ 5 = 0
• y3 : y ^ 3 = 0
• d1 : y * y + y * x + x * y + x * x = 0
• two : 2 = 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

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.r5 {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) : R5.Hyp x y

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.tr_self {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) (r : S) : tr r + tr r = 0

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.tr_eq_neg {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) (r : S) : tr (-r) = tr r

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

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.tr_bump {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 ℕ) (h j : ℕ) : tr (x ^ j * E78.blk x y (g₀ ++ [h])) = tr (E78.blk x y (g₀ ++ [h + j]))

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

Gap reductions in characteristic two

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

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

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

Words with one y

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.t2_zero {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) : tr (y * x ^ 2) = 0

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.t4_zero {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) : tr (y * x ^ 4) = 0

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

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

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.Zs_zero {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) {A : AddSubgroup M} (n : ℕ) (hn : 1 ≤ n) : Zs x y tr n 0 A

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.single {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) {A : AddSubgroup M} (h : ℕ) (h2 : h = 1 → tr (E78.blk x y [1]) ∈ A) (h4 : h = 3 → tr (E78.blk x y [3]) ∈ A) : tr (E78.blk x y [h]) ∈ A

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.blk_zero_of_mem {S : Type u_1} [Ring S] {x y : S} (g : List ℕ) (e : ℕ) (he : e ∈ g) (hx : x ^ e = 0) : E78.blk x y g = 0

Bad gaps

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

A gap of length at most two, or at least five, reduces to fewer y's.

Words in a = yx³ and b = yx⁴

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

F x^k W: blk (3 :: (k+1) :: g) = blk (4 :: k :: g) + ….

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.aa_mem {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) {A : AddSubgroup M} {n K : ℕ} (hK : 1 ≤ K) (hZ : Zs x y tr n K A) (g : List ℕ) (hlen : g.length + 1 = K) (hs : K + 7 + g.sum = n) (h8 : g = [] → tr (E78.blk x y [3, 3]) ∈ A) : tr (E78.blk x y (3 :: 3 :: g)) ∈ A

[a²W] ∈ A for nonempty W; [a²] is the candidate of degree eight.

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

[abW] - [baW] ∈ A for nonempty W.

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.ab_zero {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) : tr (E78.blk x y [3, 4]) = 0

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.bb_eq {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 (E78.blk x y (4 :: 4 :: g)) = tr (x ^ 1 * E78.blk x y (3 :: 4 :: g))

[b²W] = [x a b W].

The degree bound

def MultiplicativeBasisDeformations.TraceAlg.E78c.blkL {S : Type u_1} (x y : S) (g : List ℕ) : List S

A gap word as a list of letters.

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.blkL_prod {S : Type u_1} [Ring S] {x y : S} (g : List ℕ) : (blkL x y g).prod = E78.blk x y g

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.blkL_length {S : Type u_1} [Ring S] {x y : S} (g : List ℕ) : (blkL x y g).length = g.length + g.sum

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.blk_big15 {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 ℕ) (hg : 15 ≤ g.length + g.sum) : E78.blk x y g = 0

Words of degree at least fifteen vanish (R5.spn_big).

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

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

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.blocks_mem {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) {A : AddSubgroup M} {n K : ℕ} (hK : 1 ≤ K) (hZ : Zs x y tr n K A) (h8 : n = 8 → tr (E78.blk x y [3, 3]) ∈ A) (h14 : n = 14 → tr (E78.blk x y [3, 4, 4]) ∈ A) (g : List ℕ) (hlen : g.length = K + 1) (hg : ∀ e ∈ g, e = 3 ∨ e = 4) (hs : K + 1 + g.sum = n) : tr (E78.blk x y g) ∈ A

Cyclic words in a, b.

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.all_mem {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) {A : AddSubgroup M} (n : ℕ) (hn : 1 ≤ n) (h2 : n = 2 → tr (E78.blk x y [1]) ∈ A) (h4 : n = 4 → tr (E78.blk x y [3]) ∈ A) (h8 : n = 8 → tr (E78.blk x y [3, 3]) ∈ A) (h14 : n = 14 → tr (E78.blk x y [3, 4, 4]) ∈ A) (K : ℕ) : Zs x y tr n K A

The ordinary traces in characteristic two, by word degree: in word degree n, every gap word has trace in any subgroup containing the candidate of degree n.

theorem MultiplicativeBasisDeformations.TraceAlg.E78c.span_mem {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : Hyp x y tr) {A : AddSubgroup M} (n : ℕ) (hn : 1 ≤ n) (h2 : n = 2 → tr (E78.blk x y [1]) ∈ A) (h4 : n = 4 → tr (E78.blk x y [3]) ∈ A) (h8 : n = 8 → tr (E78.blk x y [3, 3]) ∈ A) (h14 : n = 14 → tr (E78.blk x y [3, 4, 4]) ∈ A) {r : S} (hr : r ∈ E78.span x y n) : tr r ∈ A