Radical powers determined by a finite tau-category height

theorem MagnitudeConjecture.FiniteTauMatrix.hom_mem_radical_pow_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 → ℕ) (hstep : ∀ (y : Ind) (i : Fin (rightMiddleArity T y)), height (rightMiddleLabel T y i) + 1 = height y) (n : ℕ) {x y : Ind} (hgap : height x + n ≤ height y) (f : T.obj x ⟶ T.obj y) : f ∈ (T.radical.ideal.pow n).hom (T.obj x) (T.obj y)

Recursive incoming factorization places every Hom in its height power.

theorem MagnitudeConjecture.FiniteTauMatrix.radical_pow_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) (n : ℕ) {x y : Ind} (hgap : height y < height x + n) (f : T.obj x ⟶ T.obj y) (hf : f ∈ (T.radical.ideal.pow n).hom (T.obj x) (T.obj y)) : f = 0

Powers beyond the available strict height increase vanish.