The types E in characteristic two (Appendix B)

characteristic-two-mesh-calculations.tex: "Lemma A.2 now bounds the possible positive correction degrees. Ordinary degree d requires s ∣ (d/2 − 1); for d = 4, 8, 16, 28 these integers are 1, 3, 7, 13. … Period one is excluded in every case by the central D₄ deletion and Lemma A.5. … For each fixed component, the list permits at most one degree, d = 2s + 2, spanned by a single central row path."

A row of word degree j occurs with twist θ^n only when j = 1 + n s. With s ≥ 2, the candidate degrees 4, 8, 14 (ordinary) and 5 (reflection of E₆) force n = 1, so j = s + 1.

theorem MultiplicativeBasisDeformations.StarTrace.prime_cases (n s j : ℕ) (hs : 2 ≤ s) (hj : j = 1 + n * s) (hc : j = 4 ∨ j = 8 ∨ j = 14) : n = 1 ∧ j = s + 1

theorem MultiplicativeBasisDeformations.StarTrace.e_cokerSpan {V : Type v'} [Quiver V] [Fintype V] [DecidableEq V] [∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype ↑Q.nonprojective] {k : Type u} [Field k] (c : MeshCoefficients k Q) (hbrick : ScalarMeshCategory.BrickHypothesis c) (hchar : 2 = 0) (L : Fin 3 → ℕ) (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (hEL : ∃ (a : Fin 3) (b : Fin 3) (c : Fin 3), a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ L a = 0 ∧ L b = 1 ∧ 1 ≤ L c ∧ L c ≤ 3) : ∃ (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0), 0 < c0 ∧ ρ none = none ∧ (∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) ∧ (∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (StarGauge.gZ ρ hρ c0 hρp)^[n] X ∨ X = (StarGauge.gZ ρ hρ c0 hρp)^[n] Y) ∧ ∃ (W₀ : List (Fin 3)), W₀.length = c0 / 2 + 1 ∧ ScalarMeshCategory.CokerSpan c (candRow hQ π W₀) ∧ ScalarMeshCategory.TwoRows Q (candRow hQ π W₀)

The types E in characteristic two: on a periodic star model of type E, the cokernels are spanned by the row of one word of length c₀/2 + 1 at the centre, under the brick hypothesis.