Uniform incoming Hom bounds for the graded standard form

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_incoming_shift_bounds {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (h : ℕ) (hb : ∀ (X Y : S.StandardFormMeshCategory) (d : ℤ), d < 0 ∨ ↑h < d → S.standardFormIntegerHomGrading.component X Y d = ⊥) (X Y : S.StandardFormMeshCategory) (s t : ℤ) (f : { obj := S.standardFormGradedVertexFunctor.obj X, degree := s } ⟶ { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t }) (hf : f ≠ 0) : t ≤ s ∧ s ≤ t + ↑h

A common bound on homogeneous degrees bounds the source shift of every nonzero incoming map, including maps between equal vertex labels.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_hom_finrank_le {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) (s t : ℤ) : Module.finrank k ({ obj := S.standardFormGradedVertexFunctor.obj X, degree := s } ⟶ { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t }) ≤ Module.finrank k (X ⟶ Y)

Hom dimensions of shifted vertex modules are bounded by the fixed ungraded mesh Hom dimension, independently of both shifts.