Total interior arrows for the actual interval skeleton

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.interiorTotalIntervalFinite {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.interiorTotalIntervalNoetherian {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_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) : ∑ j : { j : Fin (Fintype.card (S.standardFormSupportedLabel m)) // 0 ≤ ↑((Fintype.equivFin (S.standardFormSupportedLabel m)).symm j).snd ∧ ↑((Fintype.equivFin (S.standardFormSupportedLabel m)).symm j).snd ≤ ↑m - 2 * ↑S.standardFormIntervalControlHeight }, ∑ 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 = (m - 2 * S.standardFormIntervalControlHeight + 1) * ∑ i : Fin S.n, ∑ i_1 : Fin S.n, FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData i_1 i

The actual interval skeleton's interior contribution is the ordinary arrow total repeated once for each interior shift.