The two-middle bound on the quotient-algebra skeleton

The literal Butler--Ringel boundary calculation lives in the contravariant finite-module category of right string modules. The quotient-category algebra skeleton pulls back to covariant finite modules. We therefore send its chosen right almost-split map through coefficient duality, rotate the resulting left almost-split monomorphism across its cokernel, classify that cokernel by a literal string, and compare minimal right almost-split middle terms. Finally, ordinary projective-generator equivalence transports the arity bound back to the algebra skeleton.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.algebraSkeletonArityFiniteDimensional {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) : FiniteDimensional k P.quotientCategoryAlgebra

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.algebraSkeletonArityNoetherian {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) : IsNoetherianRing P.quotientCategoryAlgebraᵐᵒᵖ

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.rightMiddleArity_le_two_of_not_projective {k A Q : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : P.ArrowPolarization) (T : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) (i : Fin T.n) (hi : ¬T.finiteTauCategoryData.IsProjective i) : FiniteTauMatrix.rightMiddleArity T.finiteTauCategoryData.toFiniteRightTauCategoryData i ≤ 2

Every nonprojective quotient-algebra skeleton label has incoming Auslander--Reiten arity at most two. The estimate is the literal string boundary theorem transported through coefficient duality and the finite projective-generator equivalence.