Nonnegative surplus by directed primitive deletion

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientARSurplus_nonnegative_of_directed {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) : 0 ≤ S.ambientARSurplus

A representation-directed algebra has nonnegative AR surplus. The proof uses primitive deletion and induction on the number of indecomposables.