Excluding periods by the brick hypothesis

Appendix A (periodic-mesh-calculations.tex): "Delete all lifts of the two outer vertices of the long arms. The retained vertices are closed under translation, and (5.2) identifies the object quotient with the D₄ mesh category of the same period. Its degree-four closed paths … remain nonzero, so it has no brick." In general: if every retained vertex carries a closed path whose lift is nonzero in Π(Δ) modulo the deleted vertices, then every retained object of the object quotient has a nonzero radical endomorphism besides the identity, and the brick hypothesis fails for that quotient.

theorem MultiplicativeBasisDeformations.OrientedTree.not_brick {D : Type v} (T : OrientedTree D) [Fintype D] [DecidableEq D] [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [Field k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (hπ : π.IsCovering) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (Dset : Set V) (Del : Set T.Dbl) (hD : ∀ (Z : T.ZVert), π.obj Z ∈ Dset → T.toDbl Z.v ∈ Del) (hsurj : ∀ (x : V), ∃ (X : T.ZVert), π.obj X = x) (x₀ : V) (hx₀ : x₀ ∉ Dset) (hgood : ∀ (X : T.ZVert), π.obj X ∉ Dset → ∃ (E : T.ZVert) (P : Quiver.Path X E), X ≠ E ∧ π.obj E = π.obj X ∧ LinearPaths.path (T.forget.mapPath P) ∉ ((T.preproj k).del Del).ideal (LinearPaths.obj (T.forget.obj X)) (LinearPaths.obj (T.forget.obj E)) ∧ LinearPaths.path Quiver.Path.nil ∉ ((T.preproj k).del Del).ideal (LinearPaths.obj (T.forget.obj X)) (LinearPaths.obj (T.forget.obj X))) : ¬ScalarMeshCategory.BrickHypothesis c

No brick after deletion. Let D be a set of vertices of Q whose lifts lie over the deleted vertices Del of Δ. If every lift X of a retained vertex starts a path P to another lift E of the same vertex such that the image of P in Π(Δ) modulo Del is nonzero (and e_X is nonzero there), then the brick hypothesis fails.