Numbered interval arrows and allowed-shift quotient dimensions

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.numberedIntervalFinite {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.numberedIntervalNoetherian {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.standardFormIntervalLabelEquiv {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) : Fin (S.standardFormIntervalSkeleton m).n ≃ S.standardFormSupportedLabel m

The exact enumeration used by the actual interval skeleton.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalSkeleton_arrowMultiplicity_eq {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (i j : Fin (S.standardFormIntervalSkeleton m).n) : FiniteTauMatrix.arrowMultiplicity (ofFGFamily (fun (a : S.standardFormSupportedLabel m) => (S.standardFormIntervalAlgebraEquivalence m).inverse.obj (S.standardFormSupportedFamily m a)) ⋯ ⋯ ⋯).finiteTauCategoryData.toFiniteRightTauCategoryData i j = Module.finrank k (CategoricalIrreducible.Space k (S.standardFormSupportedFamily m ((Fintype.equivFin (S.standardFormSupportedLabel m)).symm i)) (S.standardFormSupportedFamily m ((Fintype.equivFin (S.standardFormSupportedLabel m)).symm j)))

Every numbered interval arrow multiplicity is the intrinsic quotient dimension at the corresponding literal allowed shifts.