Direct heights increase along nonzero nonisomorphisms

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorHeight_lt_of_hom {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} (B : S.PrimitiveDirectedBoundaryData D) {X Y : S.SurvivingLabel K} (f : S.factorObject K X ⟶ S.factorObject K Y) (hf : f ≠ 0) (hn : ¬CategoryTheory.IsIso f) : B.directFactorHeight X < B.directFactorHeight Y

Induction through incoming meshes makes the directly constructed height strictly increase on every nonzero nonisomorphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorHeight_lt_of_ne {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} (B : S.PrimitiveDirectedBoundaryData D) {X Y : S.SurvivingLabel K} (hXY : X ≠ Y) (f : S.factorObject K X ⟶ S.factorObject K Y) (hf : f ≠ 0) : B.directFactorHeight X < B.directFactorHeight Y

A nonzero map between distinct selected factor objects increases height.