Incoming sums for the actual interval skeleton

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.incomingIntervalFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) : FiniteDimensional k (S.standardFormIntervalAlgebra m)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.incomingIntervalNoetherian {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) : IsNoetherianRing (S.standardFormIntervalAlgebra m)ᵐᵒᵖ

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalSkeleton_incoming_sum {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (j : Fin (S.standardFormIntervalSkeleton m).n) : ∑ i : Fin (Fintype.card (S.standardFormSupportedLabel m)), FiniteTauMatrix.arrowMultiplicity (ofFGFamily (fun (a : S.standardFormSupportedLabel m) => (S.standardFormIntervalAlgebraEquivalence m).inverse.obj (S.standardFormSupportedFamily m a)) ⋯ ⋯ ⋯).finiteTauCategoryData.toFiniteRightTauCategoryData i j = ∑ a : S.standardFormSupportedLabel m, Module.finrank k (CategoricalIrreducible.Space k (S.standardFormSupportedFamily m a) (S.standardFormSupportedFamily m ((Fintype.equivFin (S.standardFormSupportedLabel m)).symm j)))

The actual numbered interval incoming sum equals the supported-family sum.