The six-lift and eight-lift trees of Appendix C.1

eq:six-lift-tree with the lifts eq:six-lift-coordinates, and eq:eight-lift-tree with the lifts eq:eight-lift-coordinates (local-ray-restrictions.tex). Each is given as a table poset with its rays; the factorization checks of lem:tree-quotient enter only through the retraction conditions on cover relations (Lemma 8.9), as hypotheses X*/Y* naming the excluded factorizations. Lemma 8.8 then excludes both trees.

The six-lift tree

def MultiplicativeBasisDeformations.RaySys.Tab.t6L : Fin 6 → Fin 6 → Bool

v₁ → v₂ → v₃, v₄ → v₅ → v₂, v₆ → v₅ (indices 0, …, 5).

instance MultiplicativeBasisDeformations.RaySys.Tab.instFactAxT6L : Fact (PosetRep.Ax t6L)

theorem MultiplicativeBasisDeformations.RaySys.Tab.t6L_uniq : PosetRep.UniqOK t6L

theorem MultiplicativeBasisDeformations.RaySys.Tab.t6L_count : PosetRep.CountOK t6L ![1, 2, 1, 1, 2, 1]

def MultiplicativeBasisDeformations.RaySys.Tab.s6V {V : Type} (x y z t : V) : Fin 6 → V

The objects.

def MultiplicativeBasisDeformations.RaySys.Tab.s6G {V R L : Type} [AddCommGroup L] (P : Tab V R L) (γ α β qz : R) : Fin 6 → L

The weights.

def MultiplicativeBasisDeformations.RaySys.Tab.s6ρ {V R L : Type} [AddCommGroup L] (P : Tab V R L) (x y z t : V) (γ α lam β f qy qz aq ζ bq : R) : Fin 6 → Fin 6 → R

The rays.

theorem MultiplicativeBasisDeformations.RaySys.Tab.s6_src {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z t : V} {γ α lam β f qy qz aq ζ bq : R} (γ1 : P.src γ = x) (α1 : P.src α = y) (l1 : P.src lam = z) (β1 : P.src β = t) (hf : P.mul γ α = some f) (hqy : P.mul α lam = some qy) (hqz : P.mul lam α = some qz) (haq1 : P.mul α qz = some aq) (haq2 : P.mul qy α = some aq) (hζ : P.mul β lam = some ζ) (hbq1 : P.mul β qz = some bq) (hbq2 : P.mul ζ α = some bq) (i j : Fin 6) : t6L i j = true → P.src (P.s6ρ x y z t γ α lam β f qy qz aq ζ bq i j) = s6V x y z t i

theorem MultiplicativeBasisDeformations.RaySys.Tab.s6_tgt {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z t : V} {γ α lam β f qy qz aq ζ bq : R} (γ2 : P.tgt γ = y) (α2 : P.tgt α = z) (l2 : P.tgt lam = y) (β2 : P.tgt β = z) (hf : P.mul γ α = some f) (hqy : P.mul α lam = some qy) (hqz : P.mul lam α = some qz) (haq1 : P.mul α qz = some aq) (haq2 : P.mul qy α = some aq) (hζ : P.mul β lam = some ζ) (hbq1 : P.mul β qz = some bq) (hbq2 : P.mul ζ α = some bq) (i j : Fin 6) : t6L i j = true → P.tgt (P.s6ρ x y z t γ α lam β f qy qz aq ζ bq i j) = s6V x y z t j

theorem MultiplicativeBasisDeformations.RaySys.Tab.s6_wt {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z t : V} {γ α lam β f qy qz aq ζ bq : R} (hf : P.mul γ α = some f) (hqy : P.mul α lam = some qy) (hqz : P.mul lam α = some qz) (haq1 : P.mul α qz = some aq) (haq2 : P.mul qy α = some aq) (hζ : P.mul β lam = some ζ) (hbq1 : P.mul β qz = some bq) (hbq2 : P.mul ζ α = some bq) (i j : Fin 6) : t6L i j = true → P.wt (P.s6ρ x y z t γ α lam β f qy qz aq ζ bq i j) = P.s6G γ α β qz j - P.s6G γ α β qz i

theorem MultiplicativeBasisDeformations.RaySys.Tab.s6_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z t : V} {γ α lam β f qy qz aq ζ bq : R} (γ1 : P.src γ = x) (γ2 : P.tgt γ = y) (α1 : P.src α = y) (α2 : P.tgt α = z) (l1 : P.src lam = z) (l2 : P.tgt lam = y) (β1 : P.src β = t) (β2 : P.tgt β = z) (hf : P.mul γ α = some f) (hqy : P.mul α lam = some qy) (hqz : P.mul lam α = some qz) (haq1 : P.mul α qz = some aq) (haq2 : P.mul qy α = some aq) (hζ : P.mul β lam = some ζ) (hbq1 : P.mul β qz = some bq) (hbq2 : P.mul ζ α = some bq) (i j l : Fin 6) : t6L i j = true → t6L j l = true → P.mul (P.s6ρ x y z t γ α lam β f qy qz aq ζ bq i j) (P.s6ρ x y z t γ α lam β f qy qz aq ζ bq j l) = some (P.s6ρ x y z t γ α lam β f qy qz aq ζ bq i l)

theorem MultiplicativeBasisDeformations.RaySys.Tab.s6_retL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z t : V} {γ α lam β f qy qz aq ζ bq : R} (hf : P.mul γ α = some f) (hqy : P.mul α lam = some qy) (hqz : P.mul lam α = some qz) (haq1 : P.mul α qz = some aq) (haq2 : P.mul qy α = some aq) (hζ : P.mul β lam = some ζ) (hbq1 : P.mul β qz = some bq) (hbq2 : P.mul ζ α = some bq) (dγ : 0 < P.deg (P.wt γ)) (dα : 0 < P.deg (P.wt α)) (dl : 0 < P.deg (P.wt lam)) (dβ : 0 < P.deg (P.wt β)) (i j l : Fin 6) (h : R) : PosetRep.covB t6L i j = true → t6L i l = true → P.src h = s6V x y z t j → P.tgt h = s6V x y z t l → P.wt h = P.s6G γ α β qz l - P.s6G γ α β qz j → P.mul (P.s6ρ x y z t γ α lam β f qy qz aq ζ bq i j) h = some (P.s6ρ x y z t γ α lam β f qy qz aq ζ bq i l) → t6L j l = true

theorem MultiplicativeBasisDeformations.RaySys.Tab.s6_retR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z t : V} {γ α lam β f qy qz aq ζ bq : R} (hf : P.mul γ α = some f) (hqy : P.mul α lam = some qy) (hqz : P.mul lam α = some qz) (haq1 : P.mul α qz = some aq) (haq2 : P.mul qy α = some aq) (hζ : P.mul β lam = some ζ) (hbq1 : P.mul β qz = some bq) (hbq2 : P.mul ζ α = some bq) (dγ : 0 < P.deg (P.wt γ)) (dα : 0 < P.deg (P.wt α)) (dl : 0 < P.deg (P.wt lam)) (dβ : 0 < P.deg (P.wt β)) (X1 : ∀ (h : R), P.src h = y → P.tgt h = x → P.mul h γ ≠ some qy) (X2 : ∀ (h : R), P.src h = z → P.tgt h = x → P.mul h γ ≠ some lam) (X3 : ∀ (h : R), P.src h = t → P.tgt h = x → P.mul h γ ≠ some ζ) (X4 : ∀ (h : R), P.src h = t → P.tgt h = y → P.mul h α ≠ some β) (X5 : ∀ (h : R), P.src h = x → P.tgt h = z → P.wt h + P.wt qz = P.wt α + P.wt γ → P.mul h lam ≠ some γ) (X6 : ∀ (h : R), P.src h = y → P.tgt h = t → P.mul h β ≠ some α) (i j l : Fin 6) (h : R) : PosetRep.covB t6L i j = true → t6L l j = true → P.src h = s6V x y z t l → P.tgt h = s6V x y z t i → P.wt h = P.s6G γ α β qz i - P.s6G γ α β qz l → P.mul h (P.s6ρ x y z t γ α lam β f qy qz aq ζ bq i j) = some (P.s6ρ x y z t γ α lam β f qy qz aq ζ bq l j) → t6L l i = true

theorem MultiplicativeBasisDeformations.RaySys.Tab.s6_false {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z t : V} {γ α lam β f qy qz aq ζ bq : R} (γ1 : P.src γ = x) (γ2 : P.tgt γ = y) (α1 : P.src α = y) (α2 : P.tgt α = z) (l1 : P.src lam = z) (l2 : P.tgt lam = y) (β1 : P.src β = t) (β2 : P.tgt β = z) (hf : P.mul γ α = some f) (hqy : P.mul α lam = some qy) (hqz : P.mul lam α = some qz) (haq1 : P.mul α qz = some aq) (haq2 : P.mul qy α = some aq) (hζ : P.mul β lam = some ζ) (hbq1 : P.mul β qz = some bq) (hbq2 : P.mul ζ α = some bq) (dγ : 0 < P.deg (P.wt γ)) (dα : 0 < P.deg (P.wt α)) (dl : 0 < P.deg (P.wt lam)) (dβ : 0 < P.deg (P.wt β)) (X1 : ∀ (h : R), P.src h = y → P.tgt h = x → P.mul h γ ≠ some qy) (X2 : ∀ (h : R), P.src h = z → P.tgt h = x → P.mul h γ ≠ some lam) (X3 : ∀ (h : R), P.src h = t → P.tgt h = x → P.mul h γ ≠ some ζ) (X4 : ∀ (h : R), P.src h = t → P.tgt h = y → P.mul h α ≠ some β) (X5 : ∀ (h : R), P.src h = x → P.tgt h = z → P.wt h + P.wt qz = P.wt α + P.wt γ → P.mul h lam ≠ some γ) (X6 : ∀ (h : R), P.src h = y → P.tgt h = t → P.mul h β ≠ some α) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) : False

The six-lift tree is excluded (eq:six-lift-tree).

The eight-lift tree

def MultiplicativeBasisDeformations.RaySys.Tab.t8L : Fin 8 → Fin 8 → Bool

Arms (3,3,1) around v₃ (indices 0, …, 7 for v₁, …, v₈).

instance MultiplicativeBasisDeformations.RaySys.Tab.instFactAxT8L : Fact (PosetRep.Ax t8L)

theorem MultiplicativeBasisDeformations.RaySys.Tab.t8L_uniq : PosetRep.UniqOK t8L

theorem MultiplicativeBasisDeformations.RaySys.Tab.t8L_count : PosetRep.CountOK t8L ![2, 2, 4, 3, 3, 2, 1, 1]

def MultiplicativeBasisDeformations.RaySys.Tab.s8V {V : Type} (x y z t : V) : Fin 8 → V

The objects.

def MultiplicativeBasisDeformations.RaySys.Tab.s8G {V R L : Type} [AddCommGroup L] (P : Tab V R L) (γ α β qy qz : R) : Fin 8 → L

The weights.

def MultiplicativeBasisDeformations.RaySys.Tab.s8ρ {V R L : Type} [AddCommGroup L] (P : Tab V R L) (x y z t : V) (γ α η β f qy qz γq bq : R) : Fin 8 → Fin 8 → R

The rays.

theorem MultiplicativeBasisDeformations.RaySys.Tab.s8_src {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z t : V} {γ α η β f qy qz γq bq : R} (γ1 : P.src γ = x) (α1 : P.src α = y) (η1 : P.src η = x) (β1 : P.src β = t) (qy1 : P.src qy = y) (qz1 : P.src qz = z) (hγq : P.mul γ qy = some γq) (hf : P.mul γ α = some f) (hbq : P.mul β qz = some bq) (i j : Fin 8) : t8L i j = true → P.src (P.s8ρ x y z t γ α η β f qy qz γq bq i j) = s8V x y z t i

theorem MultiplicativeBasisDeformations.RaySys.Tab.s8_tgt {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z t : V} {γ α η β f qy qz γq bq : R} (γ2 : P.tgt γ = y) (α2 : P.tgt α = z) (η2 : P.tgt η = t) (β2 : P.tgt β = z) (qy2 : P.tgt qy = y) (qz2 : P.tgt qz = z) (hγq : P.mul γ qy = some γq) (hf : P.mul γ α = some f) (hbq : P.mul β qz = some bq) (i j : Fin 8) : t8L i j = true → P.tgt (P.s8ρ x y z t γ α η β f qy qz γq bq i j) = s8V x y z t j

theorem MultiplicativeBasisDeformations.RaySys.Tab.s8_wt {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z t : V} {γ α η β f qy qz γq bq : R} (hγq : P.mul γ qy = some γq) (hf : P.mul γ α = some f) (hf' : P.mul η β = some f) (hbq : P.mul β qz = some bq) (i j : Fin 8) : t8L i j = true → P.wt (P.s8ρ x y z t γ α η β f qy qz γq bq i j) = P.s8G γ α β qy qz j - P.s8G γ α β qy qz i

theorem MultiplicativeBasisDeformations.RaySys.Tab.s8_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z t : V} {γ α η β f qy qz γq bq : R} (γ1 : P.src γ = x) (γ2 : P.tgt γ = y) (α1 : P.src α = y) (α2 : P.tgt α = z) (η1 : P.src η = x) (η2 : P.tgt η = t) (β1 : P.src β = t) (β2 : P.tgt β = z) (qy1 : P.src qy = y) (qy2 : P.tgt qy = y) (qz1 : P.src qz = z) (qz2 : P.tgt qz = z) (hγq : P.mul γ qy = some γq) (hf : P.mul γ α = some f) (hbq : P.mul β qz = some bq) (i j l : Fin 8) : t8L i j = true → t8L j l = true → P.mul (P.s8ρ x y z t γ α η β f qy qz γq bq i j) (P.s8ρ x y z t γ α η β f qy qz γq bq j l) = some (P.s8ρ x y z t γ α η β f qy qz γq bq i l)

theorem MultiplicativeBasisDeformations.RaySys.Tab.s8_retL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z t : V} {γ α η β f qy qz γq bq : R} (hγq : P.mul γ qy = some γq) (hf : P.mul γ α = some f) (hf' : P.mul η β = some f) (hbq : P.mul β qz = some bq) (dγ : 0 < P.deg (P.wt γ)) (dα : 0 < P.deg (P.wt α)) (dη : 0 < P.deg (P.wt η)) (dβ : 0 < P.deg (P.wt β)) (dqy : 0 < P.deg (P.wt qy)) (dqz : 0 < P.deg (P.wt qz)) (Y1 : ∀ (h : R), P.src h = y → P.tgt h = z → P.mul qy h ≠ some α) (Y2 : ∀ (h : R), P.src h = z → P.tgt h = y → P.mul α h ≠ some qy) (Y3 : ∀ (h : R), P.src h = y → P.tgt h = t → P.mul γ h ≠ some η) (Y4 : ∀ (h : R), P.src h = t → P.tgt h = y → P.mul η h ≠ some γ) (i j l : Fin 8) (h : R) : PosetRep.covB t8L i j = true → t8L i l = true → P.src h = s8V x y z t j → P.tgt h = s8V x y z t l → P.wt h = P.s8G γ α β qy qz l - P.s8G γ α β qy qz j → P.mul (P.s8ρ x y z t γ α η β f qy qz γq bq i j) h = some (P.s8ρ x y z t γ α η β f qy qz γq bq i l) → t8L j l = true

theorem MultiplicativeBasisDeformations.RaySys.Tab.s8_retR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z t : V} {γ α η β f qy qz γq bq : R} (hγq : P.mul γ qy = some γq) (hf : P.mul γ α = some f) (hf' : P.mul η β = some f) (hbq : P.mul β qz = some bq) (dγ : 0 < P.deg (P.wt γ)) (dα : 0 < P.deg (P.wt α)) (dη : 0 < P.deg (P.wt η)) (dβ : 0 < P.deg (P.wt β)) (dqy : 0 < P.deg (P.wt qy)) (dqz : 0 < P.deg (P.wt qz)) (Y5 : ∀ (h : R), P.src h = x → P.tgt h = y → P.wt h + P.wt qy = P.wt γ → P.mul h qy ≠ some γ) (Y6 : ∀ (h : R), P.src h = z → P.tgt h = y → P.mul h α ≠ some qz) (Y7 : ∀ (h : R), P.src h = t → P.tgt h = y → P.mul h α ≠ some bq) (Y8 : ∀ (h : R), P.src h = x → P.tgt h = x → P.mul h γ ≠ some γq) (Y9 : ∀ (h : R), P.src h = y → P.tgt h = x → P.mul h γ ≠ some qy) (Y10 : ∀ (h : R), P.src h = x → P.tgt h = z → P.wt h + P.wt qz = P.wt α + P.wt γ → P.mul h qz ≠ some f) (Y11 : ∀ (h : R), P.src h = y → P.tgt h = z → P.mul h qz ≠ some α) (i j l : Fin 8) (h : R) : PosetRep.covB t8L i j = true → t8L l j = true → P.src h = s8V x y z t l → P.tgt h = s8V x y z t i → P.wt h = P.s8G γ α β qy qz i - P.s8G γ α β qy qz l → P.mul h (P.s8ρ x y z t γ α η β f qy qz γq bq i j) = some (P.s8ρ x y z t γ α η β f qy qz γq bq l j) → t8L l i = true

theorem MultiplicativeBasisDeformations.RaySys.Tab.s8_false {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z t : V} {γ α η β f qy qz γq bq : R} (γ1 : P.src γ = x) (γ2 : P.tgt γ = y) (α1 : P.src α = y) (α2 : P.tgt α = z) (η1 : P.src η = x) (η2 : P.tgt η = t) (β1 : P.src β = t) (β2 : P.tgt β = z) (qy1 : P.src qy = y) (qy2 : P.tgt qy = y) (qz1 : P.src qz = z) (qz2 : P.tgt qz = z) (hγq : P.mul γ qy = some γq) (hf : P.mul γ α = some f) (hf' : P.mul η β = some f) (hbq : P.mul β qz = some bq) (dγ : 0 < P.deg (P.wt γ)) (dα : 0 < P.deg (P.wt α)) (dη : 0 < P.deg (P.wt η)) (dβ : 0 < P.deg (P.wt β)) (dqy : 0 < P.deg (P.wt qy)) (dqz : 0 < P.deg (P.wt qz)) (Y1 : ∀ (h : R), P.src h = y → P.tgt h = z → P.mul qy h ≠ some α) (Y2 : ∀ (h : R), P.src h = z → P.tgt h = y → P.mul α h ≠ some qy) (Y3 : ∀ (h : R), P.src h = y → P.tgt h = t → P.mul γ h ≠ some η) (Y4 : ∀ (h : R), P.src h = t → P.tgt h = y → P.mul η h ≠ some γ) (Y5 : ∀ (h : R), P.src h = x → P.tgt h = y → P.wt h + P.wt qy = P.wt γ → P.mul h qy ≠ some γ) (Y6 : ∀ (h : R), P.src h = z → P.tgt h = y → P.mul h α ≠ some qz) (Y7 : ∀ (h : R), P.src h = t → P.tgt h = y → P.mul h α ≠ some bq) (Y8 : ∀ (h : R), P.src h = x → P.tgt h = x → P.mul h γ ≠ some γq) (Y9 : ∀ (h : R), P.src h = y → P.tgt h = x → P.mul h γ ≠ some qy) (Y10 : ∀ (h : R), P.src h = x → P.tgt h = z → P.wt h + P.wt qz = P.wt α + P.wt γ → P.mul h qz ≠ some f) (Y11 : ∀ (h : R), P.src h = y → P.tgt h = z → P.mul h qz ≠ some α) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) : False

The eight-lift tree with arms (3,3,1) is excluded (eq:eight-lift-tree).

The proper six-tree eq:proper-six-tree

def MultiplicativeBasisDeformations.RaySys.Tab.tQ6 : Fin 6 → Fin 6 → Bool

B₀ → B₁ → B₂ → B₃, B₁ → Y₊, Y₋ → B₂ (indices 0, …, 3, 4 = Y₊, 5 = Y₋).

instance MultiplicativeBasisDeformations.RaySys.Tab.instFactAxTQ6 : Fact (PosetRep.Ax tQ6)

theorem MultiplicativeBasisDeformations.RaySys.Tab.tQ6_uniq : PosetRep.UniqOK tQ6

theorem MultiplicativeBasisDeformations.RaySys.Tab.tQ6_count : PosetRep.CountOK tQ6 ![1, 2, 2, 1, 1, 1]

def MultiplicativeBasisDeformations.RaySys.Tab.q6V {V : Type} (b y : V) : Fin 6 → V

The objects.

def MultiplicativeBasisDeformations.RaySys.Tab.q6G {V R L : Type} [AddCommGroup L] (P : Tab V R L) (q1 q2 q3 e l : R) : Fin 6 → L

The weights.

def MultiplicativeBasisDeformations.RaySys.Tab.q6ρ {V R L : Type} [AddCommGroup L] (P : Tab V R L) (b y : V) (q1 q2 q3 e qe l lq : R) : Fin 6 → Fin 6 → R

The rays.

theorem MultiplicativeBasisDeformations.RaySys.Tab.q6_src {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {b y : V} {q1 q2 q3 e qe l lq : R} (q11 : P.src q1 = b) (e1 : P.src e = b) (l1 : P.src l = y) (h11 : P.mul q1 q1 = some q2) (h12 : P.mul q1 q2 = some q3) (hqe : P.mul q1 e = some qe) (hlq : P.mul l q1 = some lq) (i j : Fin 6) : tQ6 i j = true → P.src (P.q6ρ b y q1 q2 q3 e qe l lq i j) = q6V b y i

theorem MultiplicativeBasisDeformations.RaySys.Tab.q6_tgt {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {b y : V} {q1 q2 q3 e qe l lq : R} (q12 : P.tgt q1 = b) (e2 : P.tgt e = y) (l2 : P.tgt l = b) (h11 : P.mul q1 q1 = some q2) (h12 : P.mul q1 q2 = some q3) (hqe : P.mul q1 e = some qe) (hlq : P.mul l q1 = some lq) (i j : Fin 6) : tQ6 i j = true → P.tgt (P.q6ρ b y q1 q2 q3 e qe l lq i j) = q6V b y j

theorem MultiplicativeBasisDeformations.RaySys.Tab.q6_wt {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {b y : V} {q1 q2 q3 e qe l lq : R} (h11 : P.mul q1 q1 = some q2) (h12 : P.mul q1 q2 = some q3) (hqe : P.mul q1 e = some qe) (hlq : P.mul l q1 = some lq) (i j : Fin 6) : tQ6 i j = true → P.wt (P.q6ρ b y q1 q2 q3 e qe l lq i j) = P.q6G q1 q2 q3 e l j - P.q6G q1 q2 q3 e l i

theorem MultiplicativeBasisDeformations.RaySys.Tab.q6_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {b y : V} {q1 q2 q3 e qe l lq : R} (q11 : P.src q1 = b) (q12 : P.tgt q1 = b) (e1 : P.src e = b) (e2 : P.tgt e = y) (l1 : P.src l = y) (l2 : P.tgt l = b) (h11 : P.mul q1 q1 = some q2) (h12 : P.mul q1 q2 = some q3) (h21 : P.mul q2 q1 = some q3) (hqe : P.mul q1 e = some qe) (hlq : P.mul l q1 = some lq) (i j m : Fin 6) : tQ6 i j = true → tQ6 j m = true → P.mul (P.q6ρ b y q1 q2 q3 e qe l lq i j) (P.q6ρ b y q1 q2 q3 e qe l lq j m) = some (P.q6ρ b y q1 q2 q3 e qe l lq i m)

theorem MultiplicativeBasisDeformations.RaySys.Tab.q6_retL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {b y : V} {q1 q2 q3 e qe l lq : R} (h11 : P.mul q1 q1 = some q2) (h12 : P.mul q1 q2 = some q3) (hqe : P.mul q1 e = some qe) (hlq : P.mul l q1 = some lq) (dq : 0 < P.deg (P.wt q1)) (de : 0 < P.deg (P.wt e)) (dl : 0 < P.deg (P.wt l)) (Z1 : ∀ (h : R), P.src h = b → P.tgt h = y → P.mul q1 h ≠ some e) (Z2 : ∀ (h : R), P.src h = y → P.tgt h = b → P.mul e h ≠ some q1) (Z3 : ∀ (h : R), P.src h = y → P.tgt h = b → P.wt h + P.wt e + P.wt q1 = P.wt q3 → False) (i j m : Fin 6) (h : R) : PosetRep.covB tQ6 i j = true → tQ6 i m = true → P.src h = q6V b y j → P.tgt h = q6V b y m → P.wt h = P.q6G q1 q2 q3 e l m - P.q6G q1 q2 q3 e l j → P.mul (P.q6ρ b y q1 q2 q3 e qe l lq i j) h = some (P.q6ρ b y q1 q2 q3 e qe l lq i m) → tQ6 j m = true

theorem MultiplicativeBasisDeformations.RaySys.Tab.q6_retR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {b y : V} {q1 q2 q3 e qe l lq : R} (h11 : P.mul q1 q1 = some q2) (h12 : P.mul q1 q2 = some q3) (hqe : P.mul q1 e = some qe) (hlq : P.mul l q1 = some lq) (dq : 0 < P.deg (P.wt q1)) (de : 0 < P.deg (P.wt e)) (dl : 0 < P.deg (P.wt l)) (Z4 : ∀ (h : R), P.src h = y → P.tgt h = b → P.wt h + P.wt q2 = P.wt q1 + P.wt l → False) (Z5 : ∀ (h : R), P.src h = b → P.tgt h = y → P.wt h + P.wt l + P.wt q1 = P.wt q2 → False) (Z6 : ∀ (h : R), P.src h = b → P.tgt h = y → P.wt h + P.wt l = P.wt q2 → False) (i j m : Fin 6) (h : R) : PosetRep.covB tQ6 i j = true → tQ6 m j = true → P.src h = q6V b y m → P.tgt h = q6V b y i → P.wt h = P.q6G q1 q2 q3 e l i - P.q6G q1 q2 q3 e l m → P.mul h (P.q6ρ b y q1 q2 q3 e qe l lq i j) = some (P.q6ρ b y q1 q2 q3 e qe l lq m j) → tQ6 m i = true

theorem MultiplicativeBasisDeformations.RaySys.Tab.q6_false {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {b y : V} {q1 q2 q3 e qe l lq : R} (q11 : P.src q1 = b) (q12 : P.tgt q1 = b) (e1 : P.src e = b) (e2 : P.tgt e = y) (l1 : P.src l = y) (l2 : P.tgt l = b) (h11 : P.mul q1 q1 = some q2) (h12 : P.mul q1 q2 = some q3) (h21 : P.mul q2 q1 = some q3) (hqe : P.mul q1 e = some qe) (hlq : P.mul l q1 = some lq) (dq : 0 < P.deg (P.wt q1)) (de : 0 < P.deg (P.wt e)) (dl : 0 < P.deg (P.wt l)) (Z1 : ∀ (h : R), P.src h = b → P.tgt h = y → P.mul q1 h ≠ some e) (Z2 : ∀ (h : R), P.src h = y → P.tgt h = b → P.mul e h ≠ some q1) (Z3 : ∀ (h : R), P.src h = y → P.tgt h = b → P.wt h + P.wt e + P.wt q1 = P.wt q3 → False) (Z4 : ∀ (h : R), P.src h = y → P.tgt h = b → P.wt h + P.wt q2 = P.wt q1 + P.wt l → False) (Z5 : ∀ (h : R), P.src h = b → P.tgt h = y → P.wt h + P.wt l + P.wt q1 = P.wt q2 → False) (Z6 : ∀ (h : R), P.src h = b → P.tgt h = y → P.wt h + P.wt l = P.wt q2 → False) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) : False

The proper six-tree is excluded (eq:proper-six-tree).

The complementary-path tree (Appendix C.2, Step 3)

def MultiplicativeBasisDeformations.RaySys.Tab.c6V {V : Type} (x y z : V) : Fin 6 → V

The objects.

def MultiplicativeBasisDeformations.RaySys.Tab.c6G {V R L : Type} [AddCommGroup L] (P : Tab V R L) (g f r s : R) : Fin 6 → L

The weights.

def MultiplicativeBasisDeformations.RaySys.Tab.c6ρ {V R L : Type} [AddCommGroup L] (P : Tab V R L) (x y z : V) (g f r s qx qz gq gr sg : R) : Fin 6 → Fin 6 → R

The rays.

theorem MultiplicativeBasisDeformations.RaySys.Tab.c6_src {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z : V} {g f r s qx qz gq gr sg : R} (g1 : P.src g = z) (f1 : P.src f = x) (r1 : P.src r = x) (s1 : P.src s = y) (hgf : P.mul g f = some qz) (hfg : P.mul f g = some qx) (hgq : P.mul g qx = some gq) (hgr : P.mul g r = some gr) (hsg : P.mul s g = some sg) (i j : Fin 6) : tQ6 i j = true → P.src (P.c6ρ x y z g f r s qx qz gq gr sg i j) = c6V x y z i

theorem MultiplicativeBasisDeformations.RaySys.Tab.c6_tgt {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z : V} {g f r s qx qz gq gr sg : R} (g2 : P.tgt g = x) (f2 : P.tgt f = z) (r2 : P.tgt r = y) (s2 : P.tgt s = z) (hgf : P.mul g f = some qz) (hfg : P.mul f g = some qx) (hgq : P.mul g qx = some gq) (hgr : P.mul g r = some gr) (hsg : P.mul s g = some sg) (i j : Fin 6) : tQ6 i j = true → P.tgt (P.c6ρ x y z g f r s qx qz gq gr sg i j) = c6V x y z j

theorem MultiplicativeBasisDeformations.RaySys.Tab.c6_wt {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z : V} {g f r s qx qz gq gr sg : R} (hgf : P.mul g f = some qz) (hfg : P.mul f g = some qx) (hgq : P.mul g qx = some gq) (hgr : P.mul g r = some gr) (hsg : P.mul s g = some sg) (i j : Fin 6) : tQ6 i j = true → P.wt (P.c6ρ x y z g f r s qx qz gq gr sg i j) = P.c6G g f r s j - P.c6G g f r s i

theorem MultiplicativeBasisDeformations.RaySys.Tab.c6_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z : V} {g f r s qx qz gq gr sg : R} (g1 : P.src g = z) (g2 : P.tgt g = x) (f1 : P.src f = x) (f2 : P.tgt f = z) (r1 : P.src r = x) (r2 : P.tgt r = y) (s1 : P.src s = y) (s2 : P.tgt s = z) (hgf : P.mul g f = some qz) (hfg : P.mul f g = some qx) (hgq : P.mul g qx = some gq) (hqg : P.mul qz g = some gq) (hgr : P.mul g r = some gr) (hsg : P.mul s g = some sg) (i j m : Fin 6) : tQ6 i j = true → tQ6 j m = true → P.mul (P.c6ρ x y z g f r s qx qz gq gr sg i j) (P.c6ρ x y z g f r s qx qz gq gr sg j m) = some (P.c6ρ x y z g f r s qx qz gq gr sg i m)

theorem MultiplicativeBasisDeformations.RaySys.Tab.c6_retL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z : V} {g f r s qx qz gq gr sg : R} (hgf : P.mul g f = some qz) (hfg : P.mul f g = some qx) (hgq : P.mul g qx = some gq) (hgr : P.mul g r = some gr) (hsg : P.mul s g = some sg) (dg : 0 < P.deg (P.wt g)) (df : 0 < P.deg (P.wt f)) (dr : 0 < P.deg (P.wt r)) (ds : 0 < P.deg (P.wt s)) (W1 : ∀ (h : R), P.src h = z → P.tgt h = y → P.mul f h ≠ some r) (W2 : ∀ (h : R), P.src h = y → P.tgt h = z → P.wt r + P.wt h = P.wt f → False) (W3 : ∀ (h : R), P.src h = y → P.tgt h = x → P.mul r h ≠ some qx) (i j m : Fin 6) (h : R) : PosetRep.covB tQ6 i j = true → tQ6 i m = true → P.src h = c6V x y z j → P.tgt h = c6V x y z m → P.wt h = P.c6G g f r s m - P.c6G g f r s j → P.mul (P.c6ρ x y z g f r s qx qz gq gr sg i j) h = some (P.c6ρ x y z g f r s qx qz gq gr sg i m) → tQ6 j m = true

theorem MultiplicativeBasisDeformations.RaySys.Tab.c6_retR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z : V} {g f r s qx qz gq gr sg : R} (hgf : P.mul g f = some qz) (hfg : P.mul f g = some qx) (hgq : P.mul g qx = some gq) (hgr : P.mul g r = some gr) (hsg : P.mul s g = some sg) (dg : 0 < P.deg (P.wt g)) (df : 0 < P.deg (P.wt f)) (dr : 0 < P.deg (P.wt r)) (ds : 0 < P.deg (P.wt s)) (W4 : ∀ (h : R), P.src h = y → P.tgt h = x → P.mul h f ≠ some s) (W5 : ∀ (h : R), P.src h = x → P.tgt h = y → P.wt h + P.wt s = P.wt f → False) (W6 : ∀ (h : R), P.src h = z → P.tgt h = y → P.mul h s ≠ some qz) (i j m : Fin 6) (h : R) : PosetRep.covB tQ6 i j = true → tQ6 m j = true → P.src h = c6V x y z m → P.tgt h = c6V x y z i → P.wt h = P.c6G g f r s i - P.c6G g f r s m → P.mul h (P.c6ρ x y z g f r s qx qz gq gr sg i j) = some (P.c6ρ x y z g f r s qx qz gq gr sg m j) → tQ6 m i = true

theorem MultiplicativeBasisDeformations.RaySys.Tab.c6_false {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x y z : V} {g f r s qx qz gq gr sg : R} (g1 : P.src g = z) (g2 : P.tgt g = x) (f1 : P.src f = x) (f2 : P.tgt f = z) (r1 : P.src r = x) (r2 : P.tgt r = y) (s1 : P.src s = y) (s2 : P.tgt s = z) (hgf : P.mul g f = some qz) (hfg : P.mul f g = some qx) (hgq : P.mul g qx = some gq) (hqg : P.mul qz g = some gq) (hgr : P.mul g r = some gr) (hsg : P.mul s g = some sg) (dg : 0 < P.deg (P.wt g)) (df : 0 < P.deg (P.wt f)) (dr : 0 < P.deg (P.wt r)) (ds : 0 < P.deg (P.wt s)) (W1 : ∀ (h : R), P.src h = z → P.tgt h = y → P.mul f h ≠ some r) (W2 : ∀ (h : R), P.src h = y → P.tgt h = z → P.wt r + P.wt h = P.wt f → False) (W3 : ∀ (h : R), P.src h = y → P.tgt h = x → P.mul r h ≠ some qx) (W4 : ∀ (h : R), P.src h = y → P.tgt h = x → P.mul h f ≠ some s) (W5 : ∀ (h : R), P.src h = x → P.tgt h = y → P.wt h + P.wt s = P.wt f → False) (W6 : ∀ (h : R), P.src h = z → P.tgt h = y → P.mul h s ≠ some qz) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) : False

The complementary-path tree is excluded (Appendix C.2, Step 3).