The trichotomy, unconditionally

Both steps of the dévissage are constructions, the trichotomy and the exit are theorems, and a killing diagram bounds the counts, so the recursion runs to completion from the initial state: an object killed by some Schur functor is locally a mixed sum of the unit and the odd line.

theorem RS.prop29 {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (P : SchurPackage) (P₀ : SchurPackage) (L : OddLine (CategoryTheory.Ind C)) (X Y : CategoryTheory.Ind C) [CategoryTheory.ExactPairing X Y] (h1 : ¬CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C))) : Prop29Statement P L X

The trichotomy of Deligne 2.9, discharged: an object with an exact pairing that is killed by some Schur functor is locally a mixed sum of the unit and the odd line.