A uniform count of incoming indecomposable sources

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportedIncomingLabel {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {m : ℕ} (b : S.standardFormSupportedLabel m) : Type

Labels admitting a nonzero map to a fixed supported representative.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportedIncomingLabel_card_le {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 = ⊥) {m : ℕ} (b : S.standardFormSupportedLabel m) : Nat.card (S.standardFormSupportedIncomingLabel b) ≤ S.n * (h + 1)

At most h + 1 shifts of each original indecomposable can map to a fixed interval target. This includes targets at either boundary.