The centre corner of E₈ in characteristic two (Appendix B)

characteristic-two-mesh-calculations.tex. In R₅ = k⟨x, y⟩/(x⁵, y³, (x + y)²) over a ring with 2 = 0, put ω₃ = yx³y, ω₄ = yx⁴y, ω₅ = ω₄x³y. "The following words span R₅: xⁱ, xⁱyxʲ (j ≤ 4), xⁱω₃, xⁱω₄xʲ (j ≤ 3), xⁱω₅. Their span contains 1 and is closed under multiplication on the right by x, y. … The highest word degree in the list is fourteen." We prove the closure (spn_mul_x, spn_mul_y), so that every word of degree n lies in the span spn n of the listed words of degree n, and spn n = 0 for n ≥ 15.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.R5.ω3 {S : Type u_1} [Ring S] (x y : S) : S

ω₃ = yx³y.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.R5.ω4 {S : Type u_1} [Ring S] (x y : S) : S

ω₄ = yx⁴y.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.R5.ω5 {S : Type u_1} [Ring S] (x y : S) : S

ω₅ = ω₄x³y.

def MultiplicativeBasisDeformations.R5.Gen {S : Type u_1} [Ring S] (x y : S) (n : ℕ) : Set S

The listed words of word degree n.

def MultiplicativeBasisDeformations.R5.spn {S : Type u_1} [Ring S] (x y : S) (n : ℕ) : AddSubgroup S

Their additive span.

structure MultiplicativeBasisDeformations.R5.Hyp {S : Type u_1} [Ring S] (x y : S) : Prop

• x5 : x ^ 5 = 0
• y3 : y ^ 3 = 0
• d1 : y * y + y * x + x * y + x * x = 0
• two : 2 = 0

theorem MultiplicativeBasisDeformations.R5.add_self {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) (a : S) : a + a = 0

theorem MultiplicativeBasisDeformations.R5.neg_self {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) (a : S) : -a = a

theorem MultiplicativeBasisDeformations.R5.xpow_big {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) (k : ℕ) (hk : 5 ≤ k) : x ^ k = 0

The word identities in characteristic two

theorem MultiplicativeBasisDeformations.R5.Ry0 {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) : y * y = y * x + x * y + x ^ 2

theorem MultiplicativeBasisDeformations.R5.Ry1 {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) : y * x * y = x * y * x + x ^ 3

theorem MultiplicativeBasisDeformations.R5.Ry2 {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) : y * x ^ 2 * y = y * x ^ 3 + x * y * x ^ 2 + x ^ 2 * y * x + x ^ 3 * y

theorem MultiplicativeBasisDeformations.R5.Z2 {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) : y * x * y - x * y * x - x ^ 3 = 0

theorem MultiplicativeBasisDeformations.R5.Z3 {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) : y * x ^ 2 * y + y * x ^ 3 + x * y * x ^ 2 + x ^ 2 * y * x + x ^ 3 * y + (x ^ 4 + x ^ 4) = 0

theorem MultiplicativeBasisDeformations.R5.Rω3x {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) : ω3 x y * x = ω4 x y + x * ω3 x y + x ^ 2 * y * x ^ 3 + x ^ 3 * y * x ^ 2

F: ω₃x = ω₄ + xω₃ + x²yx³ + x³yx².

theorem MultiplicativeBasisDeformations.R5.Rω3y {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) : ω3 x y * y = x * ω3 x y + x ^ 2 * y * x ^ 3 + x ^ 3 * y * x ^ 2

theorem MultiplicativeBasisDeformations.R5.Rω4y {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) : ω4 x y * y = ω4 x y * x

theorem MultiplicativeBasisDeformations.R5.Rω4xy {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) : ω4 x y * x * y = 0

theorem MultiplicativeBasisDeformations.R5.Rω4x2y {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) : ω4 x y * x ^ 2 * y = ω4 x y * x ^ 3

theorem MultiplicativeBasisDeformations.R5.mono0 {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) (a b : ℕ) (h : 5 ≤ a ∨ 5 ≤ b) : x ^ a * y * x ^ b = 0

theorem MultiplicativeBasisDeformations.R5.Rω4x4 {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) : ω4 x y * x ^ 4 = x * ω4 x y * x ^ 3 + x ^ 2 * ω4 x y * x ^ 2 + x ^ 3 * ω4 x y * x + x ^ 4 * ω4 x y

theorem MultiplicativeBasisDeformations.R5.Rω5x {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) : ω5 x y * x = x * ω5 x y + x ^ 2 * ω4 x y * x ^ 3 + x ^ 4 * ω4 x y * x

theorem MultiplicativeBasisDeformations.R5.Rω5y {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) : ω5 x y * y = 0

Closure of the span

theorem MultiplicativeBasisDeformations.R5.gen_mem {S : Type u_1} [Ring S] (x y : S) {n : ℕ} {r : S} (h : r ∈ Gen x y n) : r ∈ spn x y n

theorem MultiplicativeBasisDeformations.R5.m1 {S : Type u_1} [Ring S] {x y : S} (n : ℕ) : x ^ n ∈ spn x y n

theorem MultiplicativeBasisDeformations.R5.m2 {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) (j n : ℕ) (h : j + 1 = n) : y * x ^ j ∈ spn x y n

theorem MultiplicativeBasisDeformations.R5.m3 {S : Type u_1} [Ring S] {x y : S} : ω3 x y ∈ spn x y 5

theorem MultiplicativeBasisDeformations.R5.m4 {S : Type u_1} [Ring S] {x y : S} (j n : ℕ) (hj : j ≤ 3) (h : j + 6 = n) : ω4 x y * x ^ j ∈ spn x y n

theorem MultiplicativeBasisDeformations.R5.m5 {S : Type u_1} [Ring S] {x y : S} : ω5 x y ∈ spn x y 10

theorem MultiplicativeBasisDeformations.R5.Lx_gen {S : Type u_1} [Ring S] {x y : S} {n : ℕ} {r : S} (h : r ∈ Gen x y n) : x * r ∈ spn x y (n + 1)

theorem MultiplicativeBasisDeformations.R5.Lx {S : Type u_1} [Ring S] {x y : S} {n : ℕ} {r : S} (h : r ∈ spn x y n) : x * r ∈ spn x y (n + 1)

theorem MultiplicativeBasisDeformations.R5.Lxpow {S : Type u_1} [Ring S] {x y : S} (i : ℕ) {n : ℕ} {r : S} (h : r ∈ spn x y n) : x ^ i * r ∈ spn x y (n + i)

theorem MultiplicativeBasisDeformations.R5.spn_congr {S : Type u_1} [Ring S] {x y : S} {n n' : ℕ} (h : n = n') {r : S} (hr : r ∈ spn x y n) : r ∈ spn x y n'

The core words times x and y

theorem MultiplicativeBasisDeformations.R5.core_y {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) (j : ℕ) (hj : j ≤ 4) : y * x ^ j * x ∈ spn x y (j + 2) ∧ y * x ^ j * y ∈ spn x y (j + 2)

theorem MultiplicativeBasisDeformations.R5.core_ω3 {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) : ω3 x y * x ∈ spn x y 6 ∧ ω3 x y * y ∈ spn x y 6

theorem MultiplicativeBasisDeformations.R5.core_ω4 {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) (j : ℕ) (hj : j ≤ 3) : ω4 x y * x ^ j * x ∈ spn x y (j + 7) ∧ ω4 x y * x ^ j * y ∈ spn x y (j + 7)

theorem MultiplicativeBasisDeformations.R5.core_ω5 {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) : ω5 x y * x ∈ spn x y 11 ∧ ω5 x y * y ∈ spn x y 11

theorem MultiplicativeBasisDeformations.R5.gen_mul {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) {n : ℕ} {r : S} (h : r ∈ Gen x y n) : r * x ∈ spn x y (n + 1) ∧ r * y ∈ spn x y (n + 1)

theorem MultiplicativeBasisDeformations.R5.spn_mul {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) {n : ℕ} {r : S} (h : r ∈ spn x y n) (u : S) (hu : u = x ∨ u = y) : r * u ∈ spn x y (n + 1)

The span is closed under right multiplication by x and y.

theorem MultiplicativeBasisDeformations.R5.spn_big {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) {n : ℕ} (hn : 15 ≤ n) {r : S} (h : r ∈ spn x y n) : r = 0

Words of degree at least fifteen vanish.

theorem MultiplicativeBasisDeformations.R5.prod_mem {S : Type u_1} [Ring S] {x y : S} (H : Hyp x y) (l : List S) (hl : ∀ u ∈ l, u = x ∨ u = y ∨ u = x + y) : l.prod ∈ spn x y l.length

Products of n letters x, y, x + y lie in the span of degree n.