Higher-degree maps vanish in the intrinsic irreducible quotient

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_higherDegree_radicalSquare_top {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X Y : S.StandardFormMeshCategory) (t : ℤ) (n : ℕ) (hn : 0 < n) : CategoricalIrreducible.radicalSquare k { obj := S.standardFormGradedVertexFunctor.obj X, degree := t + ↑n + 1 } { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t } = ⊤

Every graded Hom of degree at least two belongs to the actual radical square.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_higherDegree_irreducible_finrank_zero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X Y : S.StandardFormMeshCategory) (t : ℤ) (n : ℕ) (hn : 0 < n) : Module.finrank k (CategoricalIrreducible.Space k { obj := S.standardFormGradedVertexFunctor.obj X, degree := t + ↑n + 1 } { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t }) = 0

Higher-degree graded irreducible quotient dimensions are zero.