Full radical concentration in the primitive factor's direct height

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_radical_concentration {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 : B.directFactorHeight X < B.directFactorHeight Y) : ((S.factorFiniteTauCategoryData K).radical.ideal.pow (B.directFactorHeight Y - B.directFactorHeight X)).hom (S.factorObject K X) (S.factorObject K Y) = ⊤ ∧ ((S.factorFiniteTauCategoryData K).radical.ideal.pow (B.directFactorHeight Y - B.directFactorHeight X + 1)).hom (S.factorObject K X) (S.factorObject K Y) = ⊥

At positive height difference, the full Hom space is concentrated in that radical layer.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_radical_concentration_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} (hXY : X ≠ Y) (f : S.factorObject K X ⟶ S.factorObject K Y) (hf : f ≠ 0) : 0 < B.directFactorHeight Y - B.directFactorHeight X ∧ ((S.factorFiniteTauCategoryData K).radical.ideal.pow (B.directFactorHeight Y - B.directFactorHeight X)).hom (S.factorObject K X) (S.factorObject K Y) = ⊤ ∧ ((S.factorFiniteTauCategoryData K).radical.ideal.pow (B.directFactorHeight Y - B.directFactorHeight X + 1)).hom (S.factorObject K X) (S.factorObject K Y) = ⊥

For distinct labels with a nonzero map, the height difference is positive, the corresponding radical power is the whole Hom group, and the next vanishes.