Exact total interior arrow contribution in the supported family

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupported_interior_arrowSum {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (hm : 2 * S.standardFormIntervalControlHeight ≤ m) : ∑ b : { b : S.standardFormSupportedLabel m // 0 ≤ ↑b.snd ∧ ↑b.snd ≤ ↑m - 2 * ↑S.standardFormIntervalControlHeight }, ∑ a : (i : Fin S.n) × ↥(GradedInterval.allowedShifts m (S.standardFormSupportWindow i).lower (S.standardFormSupportWindow i).upper), Module.finrank k (CategoricalIrreducible.Space k (S.standardFormSupportedFamily m a) (S.standardFormSupportedFamily m ↑b)) = (m - 2 * S.standardFormIntervalControlHeight + 1) * ∑ i : Fin S.n, ∑ i_1 : Fin S.n, FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData i_1 i

The supported-family interior arrow sum repeats the ordinary total arrow multiplicity once for each interior shift.