Commutative squares give nonzero maps into the almost-split kernel

theorem MagnitudeConjecture.CategoryTheory.exists_nonzero_weakKernel_map_of_square {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) (hS : QuotientSubmoduleEquidistribution.Iyama.ShortComplex.IsWeakKernel S) (hg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit S.g) {X V W : C} (a : X ⟶ V) (b : V ⟶ S.X₃) (c : X ⟶ W) (d : W ⟶ S.X₃) (ha : a ≠ 0) (hb : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism b) (hd : ¬CategoryTheory.IsSplitEpi d) (hWV : ∀ (f : W ⟶ V), f = 0) (hsquare : CategoryTheory.CategoryStruct.comp a b = CategoryTheory.CategoryStruct.comp c d) : ∃ (f : X ⟶ S.X₁), f ≠ 0

A commutative square with distinct orthogonal middle objects produces a nonzero map to the weak kernel of a right almost-split terminal map.