Uniform total incoming irreducible dimension in supported intervals

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupported_uniform_indegree_bound {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : ∃ (B : ℕ), ∀ (m : ℕ) (b : S.standardFormSupportedLabel m), ∑ a : S.standardFormSupportedLabel m, Module.finrank k (CategoricalIrreducible.Space k (S.standardFormSupportedFamily m a) (S.standardFormSupportedFamily m b)) ≤ B

Total incoming irreducible dimension is bounded independently of the interval length, including all boundary targets.