Intrinsic irreducible quotients compute the official arrow multiplicity

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intrinsicIrreducible_finrank_eq_arrowMultiplicity {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (source target : Fin S.n) : Module.finrank k (CategoricalIrreducible.Space k (S.fgObj source) (S.fgObj target)) = FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData source target

Over an algebraically closed field the dimension of the intrinsic categorical irreducible quotient is the literal finite-tau arrow multiplicity, including arrows into projective vertices.