Uniform total arrow contribution at interval boundaries

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

A constant bounding the entire exceptional-target arrow contribution.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInterval_boundaryArrowSum_le {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) : ∑ a : { a : Fin (S.standardFormIntervalSkeleton m).n // ¬(0 ≤ ↑((S.standardFormIntervalLabelEquiv m) a).snd ∧ ↑((S.standardFormIntervalLabelEquiv m) a).snd ≤ ↑m - 2 * ↑S.standardFormIntervalControlHeight) }, ∑ a_1 : 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_1 ↑a ≤ S.n * (3 * S.standardFormIntervalControlHeight) * S.standardFormIntervalIndegreeBound

The sum of actual interval arrow multiplicities into all boundary targets is bounded by a constant independent of the interval length.