The actual factor's weighted-height arrow sum

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_weighted_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) : have a := fun (X Y : S.SurvivingLabel K) => ↑(FiniteTauMatrix.arrowMultiplicity (S.factorFiniteTauCategoryData K).toFiniteRightTauCategoryData X Y); have h := fun (X : S.SurvivingLabel K) => ↑(B.directFactorHeight X); ∑ X : S.SurvivingLabel K, ∑ Y : S.SurvivingLabel K, a X Y = ∑ Y : S.SurvivingLabel K, h Y * ∑ X : S.SurvivingLabel K, a X Y - ∑ X : S.SurvivingLabel K, h X * ∑ Y : S.SurvivingLabel K, a X Y

The direct height gives the weighted incoming-minus-outgoing identity for the actual official arrow multiplicities.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_boundary_difference {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 : { x : S.SurvivingLabel K // (S.factorFiniteTauCategoryData K).IsInjective x }, ↑(B.directFactorHeight ↑x) - ∑ x : { x : S.SurvivingLabel K // (S.factorFiniteTauCategoryData K).IsProjective x }, ↑(B.directFactorHeight ↑x) = 2 * (↑(Fintype.card (S.SurvivingLabel K)) - ↑(Fintype.card { x : S.SurvivingLabel K // (S.factorFiniteTauCategoryData K).IsProjective x }))

The actual translation identifies the boundary height difference with twice the number of nonprojective vertices.