Exact boundary degrees for the direct height count

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directCount_incoming_eq_one {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) (Y : S.SurvivingLabel K) (hprojective : (S.factorFiniteTauCategoryData K).IsProjective Y) (hsource : Y ≠ D.source) : ∑ X : S.SurvivingLabel K, ↑(FiniteTauMatrix.arrowMultiplicity (S.factorFiniteTauCategoryData K).toFiniteRightTauCategoryData X Y) = 1

A tau-projective vertex other than the distinguished source has exactly one incoming official arrow occurrence.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directCount_outgoing_eq_one {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 : S.SurvivingLabel K) (hinjective : (S.factorFiniteTauCategoryData K).IsInjective X) (hsink : X ≠ D.sink) : ∑ Y : S.SurvivingLabel K, ↑(FiniteTauMatrix.arrowMultiplicity (S.factorFiniteTauCategoryData K).toFiniteRightTauCategoryData X Y) = 1

A tau-injective vertex other than the distinguished sink has exactly one outgoing official arrow occurrence.