Exceptional twisted traces in characteristic two (Appendix B)

characteristic-two-mesh-calculations.tex. For a star of type E with short arm a (L a = 0), medium arm b (L b = 1) and long arm c, write x, y for the closed paths along c, b; then x^m = y³ = (x + y)² = 0 with m = L c + 2.

• Ordinary traces (trace_E_c2): in word degree n, every trace is a multiple of the candidate yx, yx³, (yx³)², (yx³)(yx⁴)² for n = 2, 4, 8, 14, and zero otherwise.
• The reflection of E₆ (L b = L c = 1, twist exchanging b, c): "Twisted cuts are xw = wy and yw = wx. … In degree three, use xw = wy with w = x², xy to obtain [ξ₁] = [ξ₂] = 0, and use yw = wx with w = x² to obtain [ξ₃] = 0. In degree four, the first relation with w = ξ₁ gives [ξ₄] = 0, and the second with w = ξ₃ gives [ξ₅] = 0. Degree five is already spanned by ξ₆." (trace_E6_twist_c2).

theorem MultiplicativeBasisDeformations.TraceAlg.neg_c {L : Fin 3 → ℕ} (r : Rc L) : -r = r

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

theorem MultiplicativeBasisDeformations.TraceAlg.r5hyp {L : Fin 3 → ℕ} {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 = 1 ∨ L c = 2 ∨ L c = 3) : R5.Hyp (z L c) (z L b)

The relations of the centre corner in Rc.

theorem MultiplicativeBasisDeformations.TraceAlg.word_mem_span {L : Fin 3 → ℕ} {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (w : List (Fin 3)) : (List.map (z L) w).prod ∈ E78.span (z L c) (z L b) w.length

Ordinary traces

def MultiplicativeBasisDeformations.TraceAlg.candE (b c : Fin 3) : ℕ → List (Fin 3)

The candidate words of degrees 2, 4, 8, 14.

theorem MultiplicativeBasisDeformations.TraceAlg.length_candE_2 {b c : Fin 3} : (candE b c 2).length = 2

theorem MultiplicativeBasisDeformations.TraceAlg.length_candE_4 {b c : Fin 3} : (candE b c 4).length = 4

theorem MultiplicativeBasisDeformations.TraceAlg.length_candE_8 {b c : Fin 3} : (candE b c 8).length = 8

theorem MultiplicativeBasisDeformations.TraceAlg.length_candE_14 {b c : Fin 3} : (candE b c 14).length = 14

theorem MultiplicativeBasisDeformations.TraceAlg.trace_E_c2 {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) (h2 : ∀ (m : M), m + 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 = 1 ∨ L c = 2 ∨ L c = 3) (hθ : ∀ (i : Fin 3), D.θ i = i) (w : List (Fin 3)) (hw : 1 ≤ w.length) : ∃ (z : ℤ), D.tr w = z • if w.length = 2 ∨ w.length = 4 ∨ w.length = 8 ∨ w.length = 14 then D.tr (candE b c w.length) else 0

Ordinary traces of the types E in characteristic two.

The reflection of E₆

theorem MultiplicativeBasisDeformations.TraceAlg.trace_E6_twist_c2 {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) (h2 : ∀ (m : M), m + 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 = 1) (hθb : D.θ b = c) (hθc : D.θ c = b) (w : List (Fin 3)) : (w.length = 3 ∨ w.length = 4 ∨ 6 ≤ w.length → D.tr w = 0) ∧ (w.length = 5 → ∃ (z : ℤ), D.tr w = z • D.tr [c, c, b, c, c])

Reflection-twisted traces of E₆ in characteristic two: they vanish in word degrees three, four and at least six, and are multiples of [x²yx²] in degree five.