Uniform arrow-count error for the actual finite interval algebras

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInterval_arrow_error_bound {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) : |ARCount.arrowCount (FiniteTauMatrix.arrowMultiplicity (ofFGFamily (fun (a : S.standardFormSupportedLabel m) => (S.standardFormIntervalAlgebraEquivalence m).inverse.obj (S.standardFormSupportedFamily m a)) ⋯ ⋯ ⋯).finiteTauCategoryData.toFiniteRightTauCategoryData) - (↑m + 1) * ARCount.arrowCount (FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData)| ≤ ↑S.standardFormBoundaryArrowBound + 2 * ↑S.standardFormIntervalControlHeight * ARCount.arrowCount (FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData)

The actual interval arrow count differs from (m+1) times the ordinary arrow count by a constant independent of m.