Uniform support bounds for the actual standard-form graded modules

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedObject_component_eq_bot {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (d : ℤ) (hd : ∀ (X Y : S.StandardFormMeshCategory), S.standardFormIntegerHomGrading.component X Y d = ⊥) (X : CategoryTheory.Mat_ S.StandardFormMeshCategory) : (S.standardFormGradedObject ⋯ X).grading.component d = ⊥

A vanishing mesh degree also vanishes in every represented graded module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_support_bound {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : ∃ (h : ℕ), 1 ≤ h ∧ ∀ (X : S.StandardFormMeshCategory), ∀ d ∈ (S.standardFormGradedVertex ⋯ X).grading.support, 0 ≤ d ∧ d ≤ ↑h

A single positive bound contains the support of every standard-form graded vertex.