Uniform indegree bounds for the actual interval algebra

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalIndegreeFinite {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.intervalIndegreeNoetherian {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)ᵐᵒᵖ

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalIndegreeBound {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : ℕ

A single bound for all interval lengths and all targets.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalSkeleton_indegree_le {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) : ∑ a : Fin (S.standardFormIntervalSkeleton m).n, FiniteTauMatrix.arrowMultiplicity (ofFGFamily (fun (a : S.standardFormSupportedLabel m) => (S.standardFormIntervalAlgebraEquivalence m).inverse.obj (S.standardFormSupportedFamily m a)) ⋯ ⋯ ⋯).finiteTauCategoryData.toFiniteRightTauCategoryData a j ≤ S.standardFormIntervalIndegreeBound

Total official arrow multiplicity into each interval vertex is uniformly bounded, including at the two boundaries.