Forbidden bound configurations

A configuration (Tab.ConfZ) of a table poset with one zero relation p → m → r of length two, whose dimension count ∑ d_v² + d_p d_r ≤ ∑_{x → y} d_x d_y holds (checked by decide), contradicts finite representation type (Lemmas 8.8 and 8.9).

theorem MultiplicativeBasisDeformations.RaySys.Tab.bound_false {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) {n : ℕ} {le : Fin n → Fin n → Bool} [Fact (PosetRep.Ax le)] (hu : PosetRep.UniqOK le) {p m r : Fin n} (hpm : PosetRep.covB le p m = true) (hmr : PosetRep.covB le m r = true) (d : Fin n → ℕ) (hd : ∃ (i : Fin n), 0 < d i) (hN : ∑ i : Fin n, d i ^ 2 + d r * d p ≤ ∑ i : Fin n, ∑ j : Fin n, if PosetRep.covB le i j = true then d i * d j else 0) (C : P.ConfZ (PosetRep.Pos n le) (PosetRep.Zr { v := p } { v := r })) : False

A forbidden bound configuration.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.Tab.ZT {n : ℕ} (le : Fin n → Fin n → Bool) (p r i j : Fin n) : Prop

The zero condition of a table relation.

theorem MultiplicativeBasisDeformations.RaySys.Tab.hmulZ_strict {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {n : ℕ} {le : Fin n → Fin n → Bool} [Fact (PosetRep.Ax le)] (p r : Fin n) (v : Fin n → V) (ρt : Fin n → Fin n → R) (hsrc : ∀ (i j : Fin n), le i j = true → ¬ZT le p r i j → P.src (ρt i j) = v i) (htgt : ∀ (i j : Fin n), le i j = true → ¬ZT le p r i j → P.tgt (ρt i j) = v j) (hρe : ∀ (i : Fin n), ρt i i = P.e (v i)) (hmul' : ∀ (i j l : Fin n), le i j = true → le j l = true → i ≠ j → j ≠ l → ¬ZT le p r i l → P.mul (ρt i j) (ρt j l) = some (ρt i l)) (i j l : Fin n) : le i j = true → le j l = true → ¬ZT le p r i l → P.mul (ρt i j) (ρt j l) = some (ρt i l)

theorem MultiplicativeBasisDeformations.RaySys.Tab.zt_iff {n : ℕ} {le : Fin n → Fin n → Bool} [Fact (PosetRep.Ax le)] (p r i j : Fin n) : PosetRep.Zr { v := p } { v := r } { v := i } { v := j } ↔ ZT le p r i j

def MultiplicativeBasisDeformations.RaySys.Tab.ConfZ.ofTable {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {n : ℕ} {le : Fin n → Fin n → Bool} [Fact (PosetRep.Ax le)] (p r : Fin n) (v : Fin n → V) (g : Fin n → L) (ρt : Fin n → Fin n → R) (hsrc : ∀ (i j : Fin n), le i j = true → ¬ZT le p r i j → P.src (ρt i j) = v i) (htgt : ∀ (i j : Fin n), le i j = true → ¬ZT le p r i j → P.tgt (ρt i j) = v j) (hwt : ∀ (i j : Fin n), le i j = true → ¬ZT le p r i j → P.wt (ρt i j) = g j - g i) (hρe : ∀ (i : Fin n), ρt i i = P.e (v i)) (hmul' : ∀ (i j l : Fin n), le i j = true → le j l = true → i ≠ j → j ≠ l → ¬ZT le p r i l → P.mul (ρt i j) (ρt j l) = some (ρt i l)) (hmulZ : ∀ (i j l : Fin n), le i j = true → le j l = true → ¬ZT le p r i j → ¬ZT le p r j l → ZT le p r i l → P.mul (ρt i j) (ρt j l) = none) (hretL : ∀ (i j l : Fin n) (h : R), PosetRep.covB le i j = true → le i l = true → ¬ZT le p r i l → P.src h = v j → P.tgt h = v l → P.wt h = g l - g j → P.mul (ρt i j) h = some (ρt i l) → le j l = true) (hretR : ∀ (i j l : Fin n) (h : R), PosetRep.covB le i j = true → le l j = true → ¬ZT le p r l j → P.src h = v l → P.tgt h = v i → P.wt h = g i - g l → P.mul h (ρt i j) = some (ρt l j) → le l i = true) : P.ConfZ (PosetRep.Pos n le) (PosetRep.Zr { v := p } { v := r })

The bound configuration of a table poset given by a table of rays.