Kupisch cyclicity for distributive Hom spaces

If endpoint-stable subspaces of one Hom space are linearly ordered, compare the source-radical and target-radical parts of the principal bimodule. Split residue maps and nilpotence of the endpoint Jacobson radicals then show that the principal bimodule is cyclic on one side. Equivalently, the morphism allows transit or cotransit in the sense used by BGRS.

This is the Mathlib-generic part of the corresponding Cartan-determinant argument, reproduced here without its split-basic or ray-category imports.

theorem MagnitudeConjecture.transit_or_cotransit_of_homSubbimodule_comparable {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X Y : C} (f : X ⟶ Y) [IsArtinianRing (CategoryTheory.End X)] [IsArtinianRing (CategoryTheory.End Y)] (sourceResidue : CategoryTheory.End X →ₐ[k] k) (targetResidue : CategoryTheory.End Y →ₐ[k] k) (sourceResidue_zero : ∀ (a : CategoryTheory.End X), sourceResidue a = 0 ↔ a ∈ Ring.jacobson (CategoryTheory.End X)) (targetResidue_zero : ∀ (b : CategoryTheory.End Y), targetResidue b = 0 ↔ b ∈ Ring.jacobson (CategoryTheory.End Y)) (hcomparable : ∀ (S T : Submodule k (X ⟶ Y)), IsHomSubbimodule S → IsHomSubbimodule T → S ≤ T ∨ T ≤ S) : AllowsTransit f ∨ AllowsCotransit f

Kupisch's cyclicity argument: linearly ordered endpoint-stable subspaces, split residue maps, and nilpotent endpoint radicals force every morphism to allow transit or cotransit.