The exact indecomposable count for the actual finite interval algebra

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardIntervalSkeletonFinite {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.standardIntervalSkeletonNoetherian {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.standardFormIntervalSkeleton {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) : FiniteIndecomposableSkeleton k (S.standardFormIntervalAlgebra m)

The exact finite right-module skeleton of the interval algebra.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalSkeleton_card {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (hm : S.standardFormSupportHeight ≤ m) : ↑(S.standardFormIntervalSkeleton m).n = ↑S.n * (↑m + 1) - ∑ i : Fin S.n, (↑(S.standardFormSupportWindow i).upper - ↑(S.standardFormSupportWindow i).lower)

The count of actual interval indecomposables has the fixed support-width correction.