The exact simple-module count of the standard-form interval algebra

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardIntervalSimpleBaseFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : FiniteDimensional k (S.standardFormAlgebra ⋯)

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInterval_simpleCount {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (T : FiniteIndecomposableSkeleton k (S.standardFormIntervalAlgebra m)) : T.simpleCount = S.simpleCount * (m + 1)

Every degree contributes one simple for each original simple class.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalSkeleton_simpleCount {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) : (S.standardFormIntervalSkeleton m).simpleCount = S.simpleCount * (m + 1)

The constructed interval skeleton realizes the exact simple-count formula.