The dévissage counts are bounded

A killing diagram bounds the two counts of a dévissage state. The killing is whiskered by the base and read as module-level vanishing for the free module on the object; the decomposition carries it to the mixed free part; and there the nonvanishing of the mixed sum forces the diagram to contain the cell recording the two counts.

theorem RS.devissage_bound {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (P : SchurPackage) (P₀ : SchurPackage) (L : OddLine D) (X : D) {lam : YoungDiagram} (hcard : lam.card ≠ 0) (hkill : SchurKilled P X lam) (st : DevissageState D L X) : st.units + st.lines ≤ 2 * lam.card

The counts of a dévissage state are bounded by the killing diagram.