Adjacent-height morphisms are irreducible

theorem MagnitudeConjecture.FiniteTauMatrix.radical_comp_eq_zero_of_height_gap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind) (height : Ind → ℕ) (hh : ∀ {x y : Ind} (f : T.obj x ⟶ T.obj y), f ≠ 0 → ¬CategoryTheory.IsIso f → height x < height y) {x y : Ind} (hgap : height y ≤ height x + 1) {M : C} (g : T.obj x ⟶ M) (h : M ⟶ T.obj y) (hg : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism g) (hh' : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism h) : CategoryTheory.CategoryStruct.comp g h = 0

A composite of radical maps cannot connect heights differing by at most one.

theorem MagnitudeConjecture.FiniteTauMatrix.isIrreducible_of_height_eq_add_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind) (height : Ind → ℕ) (hh : ∀ {x y : Ind} (f : T.obj x ⟶ T.obj y), f ≠ 0 → ¬CategoryTheory.IsIso f → height x < height y) {x y : Ind} (hgap : height y = height x + 1) (f : T.obj x ⟶ T.obj y) (hf : f ≠ 0) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f

Every nonzero map across one height step is irreducible.