Uniform surplus error for the actual finite interval algebras

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

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInterval_surplus_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) : |(S.standardFormIntervalSkeleton m).ambientARSurplus - (↑m + 1) * S.ambientARSurplus| ≤ 2 * |∑ i : Fin S.n, (↑(S.standardFormSupportWindow i).upper - ↑(S.standardFormSupportWindow i).lower)| + (↑S.standardFormBoundaryArrowBound + 2 * ↑S.standardFormIntervalControlHeight * ARCount.arrowCount (FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData))

The official interval surplus has the ambient surplus as its linear slope, with an error bounded independently of interval length.