Global Euler counts from concrete translation slices

The concrete level fibers partition all surviving indecomposables. Since official arrow multiplicities are supported only on adjacent levels, the sum of the adjacent slice counts is the global arrow count. These two facts identify the mesh-matrix total with the graded Euler expression used by the intrinsic factor-excess theorem.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.standardFactorLevelSigmaEquiv {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} (B : S.PrimitiveDirectedBoundaryData D) : S.SurvivingLabel K ≃ (j : Fin (B.standardFactorLength + 1)) × B.StandardFactorLevelVertex ↑j

Every surviving label, tagged by its concrete level.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.standardFactorVertexTotal_eq_vertexCount {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} (B : S.PrimitiveDirectedBoundaryData D) : (GradedTreeExcess.vertexTotal fun (j : Fin (B.standardFactorLength + 1)) => B.standardFactorVertexCount ↑j) = ARCount.vertexCount

The sum of the concrete level-fiber cardinalities is the global factor vertex count.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.standardFactorArrowCount_length {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} (B : S.PrimitiveDirectedBoundaryData D) : B.standardFactorArrowCount B.standardFactorLength = 0

There is no adjacent arrow slice above the top concrete level.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.standardFactorArrowTotal_eq_arrowCount {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} (B : S.PrimitiveDirectedBoundaryData D) : (GradedTreeExcess.arrowTotal fun (j : Fin B.standardFactorLength) => B.standardFactorArrowCount ↑j) = ARCount.arrowCount (FiniteTauMatrix.arrowMultiplicity (S.factorFiniteTauCategoryData K).toFiniteRightTauCategoryData)

Summing the concrete adjacent-level slices recovers the global official arrow multiplicity count.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.standardFactorProjectiveCount_eq_projectivePoset_card_add_one {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} (B : S.PrimitiveDirectedBoundaryData D) : ARCount.projectiveCount (S.factorFiniteTauCategoryData K).IsProjective = ↑(Fintype.card B.ProjectivePoset) + 1

The global tau-projective count is the root plus the cardinality of the projective poset used in the realization.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.standardFactorMeshEulerTotal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} (B : S.PrimitiveDirectedBoundaryData D) : ARCount.matrixTotal (FiniteTauMatrix.meshMatrix (S.factorFiniteTauCategoryData K)) = ((GradedTreeExcess.vertexTotal fun (j : Fin (B.standardFactorLength + 1)) => B.standardFactorVertexCount ↑j) - GradedTreeExcess.arrowTotal fun (j : Fin B.standardFactorLength) => B.standardFactorArrowCount ↑j) + ((GradedTreeExcess.vertexTotal fun (j : Fin (B.standardFactorLength + 1)) => B.standardFactorVertexCount ↑j) - ARCount.projectiveCount (S.factorFiniteTauCategoryData K).IsProjective)

The factor mesh-matrix total is exactly the global Euler expression obtained by summing the concrete level slices.