The direct height formula for the actual factor's arrow count

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_arrow_count {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, ∑ Y : S.SurvivingLabel K, ↑(FiniteTauMatrix.arrowMultiplicity (S.factorFiniteTauCategoryData K).toFiniteRightTauCategoryData X Y) = 2 * ↑(Fintype.card (S.SurvivingLabel K)) - ↑(B.directFactorHeight D.sink) - 2