Intrinsic matrix excess in terms of the direct height

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instDecidablePred : DecidablePred fun (p : Prop) => p

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_intrinsicExcess {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) : DirectedDeletion.intrinsicEulerExcess (FiniteTauMatrix.meshMatrix (S.factorFiniteTauCategoryData K)) = ↑(B.directFactorHeight D.sink) - (ARCount.projectiveCount (S.factorFiniteTauCategoryData K).IsProjective - 1)

The literal matrix-defined intrinsic excess is L−(p−1), where L is the direct sink height and p counts projective factor vertices.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_intrinsicExcess_nonnegative_iff {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) : 0 ≤ DirectedDeletion.intrinsicEulerExcess (FiniteTauMatrix.meshMatrix (S.factorFiniteTauCategoryData K)) ↔ ARCount.projectiveCount (S.factorFiniteTauCategoryData K).IsProjective - 1 ≤ ↑(B.directFactorHeight D.sink)

The remaining numerical inequality is exactly the projective-count bound on the direct sink height.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_intrinsicExcess_eq_zero_iff {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) : DirectedDeletion.intrinsicEulerExcess (FiniteTauMatrix.meshMatrix (S.factorFiniteTauCategoryData K)) = 0 ↔ ↑(B.directFactorHeight D.sink) = ARCount.projectiveCount (S.factorFiniteTauCategoryData K).IsProjective - 1

Vanishing intrinsic excess is exactly equality in the height bound.