Lemma A.7: closed paths of degree sixteen in Π(E₇)

lem:e7-sixteen-return (periodic-mesh-calculations.tex): "Every vertex of Π(E₇) has a nonzero closed path of path degree sixteen, over every field. … Thus U_0, …, U_8 are nonnegative. The same recurrence gives U_9 = U_7. Its reversibility implies U_{8+j} = U_{8-j} for 0 ≤ j ≤ 8. In particular U_16 = I and all preceding matrices are nonnegative. Apply (A.17)."

The matrices U_d are integer matrices determined by the recurrence; we list them in a fixed labelling of the vertices and check the recurrence, the nonnegativity and U_16 = I by direct computation.

def MultiplicativeBasisDeformations.E7Return.A7 : Matrix (Fin 7) (Fin 7) ℤ

The adjacency matrix of E₇ in the labelling: centre 0; arm of length one 1; arm of length two 2, 3; arm of length three 4, 5, 6.

def MultiplicativeBasisDeformations.E7Return.Ulit : ℕ → Matrix (Fin 7) (Fin 7) ℤ

The matrices U_0, …, U_16 of E_7 in the labelling e7.

theorem MultiplicativeBasisDeformations.E7Return.U0 : UBound.U A7 0 = Ulit 0

theorem MultiplicativeBasisDeformations.E7Return.U1 : UBound.U A7 1 = Ulit 1

theorem MultiplicativeBasisDeformations.E7Return.U2 : UBound.U A7 2 = Ulit 2

theorem MultiplicativeBasisDeformations.E7Return.U3 : UBound.U A7 3 = Ulit 3

theorem MultiplicativeBasisDeformations.E7Return.U4 : UBound.U A7 4 = Ulit 4

theorem MultiplicativeBasisDeformations.E7Return.U5 : UBound.U A7 5 = Ulit 5

theorem MultiplicativeBasisDeformations.E7Return.U6 : UBound.U A7 6 = Ulit 6

theorem MultiplicativeBasisDeformations.E7Return.U7 : UBound.U A7 7 = Ulit 7

theorem MultiplicativeBasisDeformations.E7Return.U8 : UBound.U A7 8 = Ulit 8

theorem MultiplicativeBasisDeformations.E7Return.U9 : UBound.U A7 9 = Ulit 9

theorem MultiplicativeBasisDeformations.E7Return.U10 : UBound.U A7 10 = Ulit 10

theorem MultiplicativeBasisDeformations.E7Return.U11 : UBound.U A7 11 = Ulit 11

theorem MultiplicativeBasisDeformations.E7Return.U12 : UBound.U A7 12 = Ulit 12

theorem MultiplicativeBasisDeformations.E7Return.U13 : UBound.U A7 13 = Ulit 13

theorem MultiplicativeBasisDeformations.E7Return.U14 : UBound.U A7 14 = Ulit 14

theorem MultiplicativeBasisDeformations.E7Return.U15 : UBound.U A7 15 = Ulit 15

theorem MultiplicativeBasisDeformations.E7Return.U16 : UBound.U A7 16 = Ulit 16

theorem MultiplicativeBasisDeformations.E7Return.U_eq_Ulit (d : ℕ) : d ≤ 16 → UBound.U A7 d = Ulit d

theorem MultiplicativeBasisDeformations.E7Return.Ulit_nonneg (d : ℕ) : d ≤ 16 → ∀ (a b : Fin 7), 0 ≤ Ulit d a b

theorem MultiplicativeBasisDeformations.E7Return.Ulit_16 : Ulit 16 = 1

The labelling of an E₇ star

def MultiplicativeBasisDeformations.E7Return.e7 {L : Fin 3 → ℕ} {a b c : Fin 3} (hLa : L a = 0) (hLb : L b = 1) (hLc : L c = 2) : Fin 7 → StarV L

The vertices 0, …, 6 of the star.

theorem MultiplicativeBasisDeformations.E7Return.e7_injective {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 = 2) : Function.Injective (e7 hLa hLb hLc)

theorem MultiplicativeBasisDeformations.E7Return.e7_surjective {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 = 2) : Function.Surjective (e7 hLa hLb hLc)

noncomputable def MultiplicativeBasisDeformations.E7Return.E7eqv {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 = 2) : Fin 7 ≃ (starTree L).Dbl

The labelling as an equivalence.

theorem MultiplicativeBasisDeformations.E7Return.adjM_e7 {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 = 2) (n m : Fin 7) : (starTree L).adjM (e7 hLa hLb hLc n) (e7 hLa hLb hLc m) = A7 n m

theorem MultiplicativeBasisDeformations.E7Return.U_submatrix {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 = 2) (d : ℕ) : (UBound.U (starTree L).adjM d).submatrix ⇑(E7eqv hab hac hbc hLa hLb hLc) ⇑(E7eqv hab hac hbc hLa hLb hLc) = UBound.U A7 d

theorem MultiplicativeBasisDeformations.E7Return.e7_return {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 = 2) {k : Type u_1} [Field k] (v : (starTree L).Dbl) : ∃ (p : Quiver.Path v v), p.length = 16 ∧ LinearPaths.path p ∉ (starTree L).Id k v v

Lemma A.7: every vertex of Π(E₇) carries a closed path of degree sixteen outside the ideal, over every field.