Graded irreducible dimensions in terms of ordinary arrow multiplicities

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_irreducible_arrowMultiplicity {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X Y : S.StandardFormMeshCategory) (s t : ℤ) : Module.finrank k (CategoricalIrreducible.Space k { obj := S.standardFormGradedVertexFunctor.obj X, degree := s } { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t }) = if s = t + 1 then FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData X.as Y.as else 0

Shift difference one contributes the ordinary arrow multiplicity; every other shift difference contributes zero.