The global equality implication through a single graded interval

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.beta_le_two_of_ambientARSurplus_eq_zero_by_intervals {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hz : S.ambientARSurplus = 0) : FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData ≤ 2

Zero ambient surplus bounds the original nonprojective middle count by two through the interval of length given by the control height plus two.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.isSpecialBiserial_of_ambientARSurplus_eq_zero_by_intervals {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hz : S.ambientARSurplus = 0) : BoundQuiver.IsSpecialBiserial k A

The manuscript's global equality implication, using finite intervals, separated packing, and the one-sided almost-split transfer.