Interior factorizations reduce to supported indecomposable intermediates

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInterior_factorization_decomposition {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.n) (t : ℤ) (ht0 : 0 ≤ t) (htm : t ≤ ↑m - 2 * ↑S.standardFormIntervalControlHeight) {X M : Graded.FiniteGradedModule.ShiftedModule} (a : X ⟶ M) (b : M ⟶ { obj := S.standardFormGradedFamily j, degree := t }) : ∃ (d : CategoryTheory.FiniteIndecomposableDecomposition M), (∀ (q : d.IncomingIndex b), Graded.FiniteGradedModule.SupportedIn m (d.summand ↑q)) ∧ CategoryTheory.CategoryStruct.comp a b = ∑ q : d.IncomingIndex b, CategoryTheory.CategoryStruct.comp (d.outgoingComponent a ↑q) (d.incomingComponent b ↑q)

A factorization to an interior target is a finite sum through supported indecomposables. The component maps are obtained by composing the original factors with the displayed summand projections and inclusions.