The degree-one irreducible quotient is the degree-one mesh Hom space

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_degreeOne_radical_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 : ℤ) : CategoricalIrreducible.radical k { obj := S.standardFormGradedVertexFunctor.obj X, degree := t + 1 } { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t } = ⊤

All maps between adjacent shifts are radical.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_degreeOne_radicalSquare_bot {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 : ℤ) : CategoricalIrreducible.radicalSquare k { obj := S.standardFormGradedVertexFunctor.obj X, degree := t + 1 } { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t } = ⊥

The intrinsic radical square vanishes between adjacent shifts.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_degreeOne_irreducibleEquiv {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 : ℤ) : CategoricalIrreducible.Space k { obj := S.standardFormGradedVertexFunctor.obj X, degree := t + 1 } { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t } ≃ₗ[k] ↥(S.standardFormIntegerHomGrading.component X Y 1)

The degree-one intrinsic quotient retains precisely the degree-one mesh component.