Interior incoming sums equal the ordinary indegree

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupported_interior_indegree {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {m : ℕ} (b : S.standardFormSupportedLabel m) (ht0 : 0 ≤ ↑b.snd) (htm : ↑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)) = ∑ i : Fin S.n, FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData i b.fst

The incoming irreducible sum at an interior supported target is exactly its ordinary skeleton indegree.