Lemma 8.8 with one zero relation

lem:dimension-infinity with F = d_p d_r for a single zero relation p → m → r of length two in a poset with unique paths: the linearization of the bound incidence table (RaySys.incZ, zero set {(x, z) | x ≤ p, r ≤ z}) is representation-infinite when ∑ d_v² + d_p d_r ≤ ∑_{x → y} d_x d_y and d ≠ 0. This is the form needed for Case 2 of Lemma 8.11 (local-ray-geometry.tex, N = 22, D = 21, F = 1).

The module of a point of the zero set is a module over the bound algebra, through the matrix units of the incidence algebra; isomorphisms of such modules are conjugations (conj_of_iso), and OrbitDim.orbits_not_finite applies with the F entries of the composite along the relation.

def MultiplicativeBasisDeformations.PosetRep.Zr {P : Type} [PartialOrder P] (p r x z : P) : Prop

The zero set of the relation p → m → r.

@[instance_reducible]

instance MultiplicativeBasisDeformations.PosetRep.instDecidableRelZr {P : Type} [PartialOrder P] [DecidableLE P] (p r : P) : DecidableRel (Zr p r)

theorem MultiplicativeBasisDeformations.PosetRep.zr_zeroSet {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (hE : ∀ (x y : P), E x y → x < y) {p m r : P} (hpm : E p m) (hmr : E m r) : RaySys.ZeroSet P (Zr p r)

theorem MultiplicativeBasisDeformations.PosetRep.T_zero {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) {M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} (hM : M m r hmr ∘ₗ M p m hpm = 0) {x z : P} (hz : Zr p r x z) : T d hex M x z = 0

The transport vanishes on the zero set.

theorem MultiplicativeBasisDeformations.PosetRep.act_sgl_zero {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) {M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} (hM : M m r hmr ∘ₗ M p m hpm = 0) {x z : P} (hxz : x ≤ z) (hz : Zr p r x z) (w : (v : P) → Sp k d v) : act d hex M (sgl x z hxz) w = 0

The bound algebra acting on a point of the zero set

theorem MultiplicativeBasisDeformations.PosetRep.sgl_mul {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] (x y y' z : P) (h : x ≤ y) (h' : y' ≤ z) : sgl x y h * sgl y' z h' = if hy : y = y' then sgl x z ⋯ else 0

noncomputable def MultiplicativeBasisDeformations.PosetRep.actE {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) (a : IncidenceAlgebra k P) : Module.End k ((v : P) → Sp k d v)

The action of an incidence function, as an endomorphism of the carrier.

theorem MultiplicativeBasisDeformations.PosetRep.actE_apply {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} (a : IncidenceAlgebra k P) (w : (v : P) → Sp k d v) : (actE d hex M a) w = act d hex M a w

noncomputable def MultiplicativeBasisDeformations.PosetRep.actA {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) : IncidenceAlgebra k P →ₗ[k] Module.End k ((v : P) → Sp k d v)

The action is linear in the incidence function.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.PosetRep.BAlg (k : Type u) [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (hE : ∀ (x y : P), E x y → x < y) {p m r : P} (hpm : E p m) (hmr : E m r) : Subalgebra k (Matrix (RaySys.IPZ P (Zr p r)) (RaySys.IPZ P (Zr p r)) k)

The bound algebra of the relation.

noncomputable def MultiplicativeBasisDeformations.PosetRep.ιB {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (hE : ∀ (x y : P), E x y → x < y) {p m r : P} (hpm : E p m) (hmr : E m r) : ↥(BAlg k hE hpm hmr) →ₗ[k] IncidenceAlgebra k P

Matrix units of the bound algebra in the incidence algebra.

theorem MultiplicativeBasisDeformations.PosetRep.ιB_b {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (hE : ∀ (x y : P), E x y → x < y) {p m r : P} (hpm : E p m) (hmr : E m r) (q : RaySys.IPZ P (Zr p r)) : (ιB hE hpm hmr) ((RaySys.incZ ⋯).b k q) = sgl (↑q).1 (↑q).2 ⋯

theorem MultiplicativeBasisDeformations.PosetRep.ιB_one {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (hE : ∀ (x y : P), E x y → x < y) {p m r : P} (hpm : E p m) (hmr : E m r) : (ιB hE hpm hmr) 1 = 1

noncomputable def MultiplicativeBasisDeformations.PosetRep.ψ0 {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) (M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y) : ↥(BAlg k hE hpm hmr) →ₗ[k] Module.End k ((v : P) → Sp k d v)

The action of the bound algebra.

theorem MultiplicativeBasisDeformations.PosetRep.ψ0_mul {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) {M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} (hM : M m r hmr ∘ₗ M p m hpm = 0) (b b' : ↥(BAlg k hE hpm hmr)) : (ψ0 d hE hex hpm hmr M) (b * b') = (ψ0 d hE hex hpm hmr M) b' * (ψ0 d hE hex hpm hmr M) b

theorem MultiplicativeBasisDeformations.PosetRep.ψ0_one' {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) {M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} : (ψ0 d hE hex hpm hmr M) 1 = 1

noncomputable def MultiplicativeBasisDeformations.PosetRep.ψ {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) {M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} (hM : M m r hmr ∘ₗ M p m hpm = 0) : (↥(BAlg k hE hpm hmr))ᵐᵒᵖ →+* Module.End k ((v : P) → Sp k d v)

The bound algebra acting on a point of the zero set (a right module).

noncomputable def MultiplicativeBasisDeformations.PosetRep.repObjB {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) {M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} (hM : M m r hmr ∘ₗ M p m hpm = 0) : RightModuleCat ↥(BAlg k hE hpm hmr)

The module of a point of the zero set over the bound algebra.

theorem MultiplicativeBasisDeformations.PosetRep.repObjB_smul {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) {M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} (hM : M m r hmr ∘ₗ M p m hpm = 0) (b : (↥(BAlg k hE hpm hmr))ᵐᵒᵖ) (w : ↑(repObjB d hE huniq hex hpm hmr hM)) : b • w = act d hex M ((ιB hE hpm hmr) (MulOpposite.unop b)) w

def MultiplicativeBasisDeformations.PosetRep.toP {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) {M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} {hM : M m r hmr ∘ₗ M p m hpm = 0} (w : ↑(repObjB d hE huniq hex hpm hmr hM)) (v : P) : Sp k d v

Elements of the module of a point as tuples of vectors.

theorem MultiplicativeBasisDeformations.PosetRep.toP_smul {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) {M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} {hM : M m r hmr ∘ₗ M p m hpm = 0} (c : k) (w : ↑(repObjB d hE huniq hex hpm hmr hM)) : toP d hE huniq hex hpm hmr (c • w) = c • toP d hE huniq hex hpm hmr w

def MultiplicativeBasisDeformations.PosetRep.toPiB {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) {M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} (hM : M m r hmr ∘ₗ M p m hpm = 0) : ↑(repObjB d hE huniq hex hpm hmr hM) →ₗ[k] (v : P) → Sp k d v

The identification with ∏ k^{d v} is k-linear.

theorem MultiplicativeBasisDeformations.PosetRep.repObjB_finite {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) {M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} (hM : M m r hmr ∘ₗ M p m hpm = 0) : Module.Finite k ↑(repObjB d hE huniq hex hpm hmr hM)

theorem MultiplicativeBasisDeformations.PosetRep.finrank_repObjB_le {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) {M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} (hM : M m r hmr ∘ₗ M p m hpm = 0) : Module.finrank k ↑(repObjB d hE huniq hex hpm hmr hM) ≤ ∑ v : P, d v

theorem MultiplicativeBasisDeformations.PosetRep.incidence_eq_sum {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] (a : IncidenceAlgebra k P) : a = ∑ q : { x : P × P // x.1 ≤ x.2 }, a (↑q).1 (↑q).2 • sgl (↑q).1 (↑q).2 ⋯

An incidence function as a combination of matrix units.

def MultiplicativeBasisDeformations.PosetRep.ofP {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) {M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} {hM : M m r hmr ∘ₗ M p m hpm = 0} (w : (v : P) → Sp k d v) : ↑(repObjB d hE huniq hex hpm hmr hM)

Tuples of vectors as elements of the module of a point.

theorem MultiplicativeBasisDeformations.PosetRep.act_eq_sum {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {M : (x y : P) → E x y → Sp k d x →ₗ[k] Sp k d y} (a : IncidenceAlgebra k P) (w : (v : P) → Sp k d v) : act d hex M a w = ∑ q : { x : P × P // x.1 ≤ x.2 }, a (↑q).1 (↑q).2 • act d hex M (sgl (↑q).1 (↑q).2 ⋯) w

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.PosetRep.ZC {k : Type u} [Field k] {P : Type} {E : P → P → Prop} (d : P → ℕ) {p m r : P} (hpm : E p m) (hmr : E m r) (y : OrbitDim.Coord d src tgt → k) : Prop

The zero condition for a point.

theorem MultiplicativeBasisDeformations.PosetRep.hom_act {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) [DecidableRel E] (x y : OrbitDim.Coord d src tgt → k) (hx : ZC d hpm hmr x) (hy : ZC d hpm hmr y) (φ : repObjB d hE huniq hex hpm hmr hx ⟶ repObjB d hE huniq hex hpm hmr hy) (a : IncidenceAlgebra k P) (w : (v : P) → Sp k d v) : toP d hE huniq hex hpm hmr ((CategoryTheory.ConcreteCategory.hom φ) (ofP d hE huniq hex hpm hmr (act d hex (Mpt d x) a w))) = act d hex (Mpt d y) a (toP d hE huniq hex hpm hmr ((CategoryTheory.ConcreteCategory.hom φ) (ofP d hE huniq hex hpm hmr w)))

A module map between points of the zero set commutes with the incidence algebra.

theorem MultiplicativeBasisDeformations.PosetRep.conj_of_isoB {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) [DecidableRel E] (x y : OrbitDim.Coord d src tgt → k) (hx : ZC d hpm hmr x) (hy : ZC d hpm hmr y) (L : repObjB d hE huniq hex hpm hmr hx ≅ repObjB d hE huniq hex hpm hmr hy) : ∃ (g : (v : P) → GL (Fin (d v)) k), y = OrbitDim.act g x

Isomorphic modules over the bound algebra are conjugate points.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.PosetRep.amr {P : Type} {E : P → P → Prop} {m r : P} (hmr : E m r) : Arr E

The arrow m → r.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.PosetRep.apm {P : Type} {E : P → P → Prop} {p m : P} (hpm : E p m) : Arr E

The arrow p → m.

noncomputable def MultiplicativeBasisDeformations.PosetRep.relPoly {k : Type u} [Field k] {P : Type} {E : P → P → Prop} (d : P → ℕ) {p m r : P} (hpm : E p m) (hmr : E m r) (ij : Fin (d r * d p)) : MvPolynomial (OrbitDim.Coord d src tgt) k

The entries of the composite along the relation, as polynomials.

theorem MultiplicativeBasisDeformations.PosetRep.eval_relPoly {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) {p m r : P} (hpm : E p m) (hmr : E m r) [DecidableRel E] (y : OrbitDim.Coord d src tgt → k) (ij : Fin (d r * d p)) : (MvPolynomial.eval y) (relPoly d hpm hmr ij) = (OrbitDim.mat y (amr hmr) * OrbitDim.mat y (apm hpm)) (finProdFinEquiv.symm ij).1 (finProdFinEquiv.symm ij).2

theorem MultiplicativeBasisDeformations.PosetRep.zc_iff {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) {p m r : P} (hpm : E p m) (hmr : E m r) [DecidableRel E] (y : OrbitDim.Coord d src tgt → k) : ZC d hpm hmr y ↔ ∀ (ij : Fin (d r * d p)), (MvPolynomial.eval y) (relPoly d hpm hmr ij) = 0

theorem MultiplicativeBasisDeformations.PosetRep.relPoly_stab {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) {p m r : P} (hpm : E p m) (hmr : E m r) [DecidableRel E] (g : (v : P) → GL (Fin (d v)) k) (y : OrbitDim.Coord d src tgt → k) (hy : ∀ (ij : Fin (d r * d p)), (MvPolynomial.eval y) (relPoly d hpm hmr ij) = 0) (ij : Fin (d r * d p)) : (MvPolynomial.eval (OrbitDim.act g y)) (relPoly d hpm hmr ij) = 0

noncomputable def MultiplicativeBasisDeformations.PosetRep.ObjB {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (hE : ∀ (x y : P), E x y → x < y) {p m r : P} (hpm : E p m) (hmr : E m r) {N : ℕ} (X : Fin N → RightModuleCat ↥(BAlg k hE hpm hmr)) (B : ℕ) (τ : (m : Fin (B + 1)) × (Fin ↑m → Fin N)) : RightModuleCat ↥(BAlg k hE hpm hmr)

The labelled biproducts of the bound algebra.

theorem MultiplicativeBasisDeformations.PosetRep.not_isRepresentationFinite_bound {k : Type u} [Field k] {P : Type} [PartialOrder P] [Fintype P] [DecidableEq P] [LocallyFiniteOrder P] [DecidableLE P] {E : P → P → Prop} (d : P → ℕ) (hE : ∀ (x y : P), E x y → x < y) (huniq : ∀ (x y : P), Subsingleton (EPath E x y)) (hex : ∀ (x y : P), x ≤ y → Nonempty (EPath E x y)) {p m r : P} (hpm : E p m) (hmr : E m r) [DecidableRel E] [IsAlgClosed k] (hd : ∃ (v : P), 0 < d v) (hN : ∑ v : P, d v ^ 2 + d r * d p ≤ ∑ a : Arr E, d (tgt a) * d (src a)) : ¬IsRepresentationFinite k ↥(BAlg k hE hpm hmr)

Lemma 8.8 with one zero relation: if d ≠ 0 and ∑ d_v² + d_p d_r ≤ ∑_{x → y} d_x d_y, the bound incidence algebra is representation-infinite.