Euler excess of a category with tree slices

This file formalizes the numerical part of the factor-excess argument in the frozen manuscript. Suppose a graded translation quiver has levels 0,...,L, singleton source and sink levels, and every bipartite arrow slice is a tree. If v j is the number of vertices at level j, the number of arrows in slice j is v j + v (j+1) - 1. Summing gives

arrows = 2 * vertices - L - 2.

With one mesh for each nonprojective and p projective vertices, the intrinsic Euler excess is therefore L - (p - 1). Positivity is reduced exactly to the realization-theoretic bound p - 1 ≤ L.

def MagnitudeConjecture.GradedTreeExcess.vertexTotal {L : ℕ} (verticesAt : Fin (L + 1) → ℤ) : ℤ

Total number of graded vertices, represented in ℤ.

def MagnitudeConjecture.GradedTreeExcess.arrowTotal {L : ℕ} (arrowsAt : Fin L → ℤ) : ℤ

Total arrow multiplicity across adjacent graded slices.

theorem MagnitudeConjecture.GradedTreeExcess.arrowTotal_eq_two_mul_vertexTotal_sub_length_sub_two {L : ℕ} (verticesAt : Fin (L + 1) → ℤ) (arrowsAt : Fin L → ℤ) (source_singleton : verticesAt 0 = 1) (sink_singleton : verticesAt (Fin.last L) = 1) (slice_tree_edges : ∀ (j : Fin L), arrowsAt j = verticesAt j.castSucc + verticesAt j.succ - 1) : arrowTotal arrowsAt = 2 * vertexTotal verticesAt - ↑L - 2

Summing the tree edge formula over all slices.

def MagnitudeConjecture.GradedTreeExcess.intrinsicExcessFromCounts (vertices arrows projectives : ℤ) : ℤ

Euler expression with one mesh for each of the vertices - projectives nonprojective vertices, followed by the -1 normalization in the intrinsic factor excess.

theorem MagnitudeConjecture.GradedTreeExcess.intrinsicExcessFromCounts_eq_length_sub_projectives_sub_one {L : ℕ} (verticesAt : Fin (L + 1) → ℤ) (arrowsAt : Fin L → ℤ) (projectives : ℤ) (source_singleton : verticesAt 0 = 1) (sink_singleton : verticesAt (Fin.last L) = 1) (slice_tree_edges : ∀ (j : Fin L), arrowsAt j = verticesAt j.castSucc + verticesAt j.succ - 1) : intrinsicExcessFromCounts (vertexTotal verticesAt) (arrowTotal arrowsAt) projectives = ↑L - (projectives - 1)

The tree-slice count identifies intrinsic excess with the difference between grading length and the number of non-root projectives.

theorem MagnitudeConjecture.GradedTreeExcess.intrinsicExcessFromCounts_nonnegative {L : ℕ} (verticesAt : Fin (L + 1) → ℤ) (arrowsAt : Fin L → ℤ) (projectives : ℤ) (source_singleton : verticesAt 0 = 1) (sink_singleton : verticesAt (Fin.last L) = 1) (slice_tree_edges : ∀ (j : Fin L), arrowsAt j = verticesAt j.castSucc + verticesAt j.succ - 1) (realization_length_bound : projectives - 1 ≤ ↑L) : 0 ≤ intrinsicExcessFromCounts (vertexTotal verticesAt) (arrowTotal arrowsAt) projectives

The realization bound projectives - 1 ≤ L is precisely what makes the intrinsic factor excess nonnegative.

theorem MagnitudeConjecture.GradedTreeExcess.intrinsicExcessFromCounts_eq_zero_iff {L : ℕ} (verticesAt : Fin (L + 1) → ℤ) (arrowsAt : Fin L → ℤ) (projectives : ℤ) (source_singleton : verticesAt 0 = 1) (sink_singleton : verticesAt (Fin.last L) = 1) (slice_tree_edges : ∀ (j : Fin L), arrowsAt j = verticesAt j.castSucc + verticesAt j.succ - 1) : intrinsicExcessFromCounts (vertexTotal verticesAt) (arrowTotal arrowsAt) projectives = 0 ↔ ↑L = projectives - 1

Under the tree-slice hypotheses, vanishing of the factor excess is equivalent to sharpness of the realization length bound.

theorem MagnitudeConjecture.GradedTreeExcess.intrinsicExcessFromCounts_pos {L : ℕ} (verticesAt : Fin (L + 1) → ℤ) (arrowsAt : Fin L → ℤ) (projectives : ℤ) (source_singleton : verticesAt 0 = 1) (sink_singleton : verticesAt (Fin.last L) = 1) (slice_tree_edges : ∀ (j : Fin L), arrowsAt j = verticesAt j.castSucc + verticesAt j.succ - 1) (thick_length_bound : projectives ≤ ↑L) : 0 < intrinsicExcessFromCounts (vertexTotal verticesAt) (arrowTotal arrowsAt) projectives

The strengthened bound projectives ≤ L, supplied in the manuscript by a thick indecomposable poset-space, makes the intrinsic excess strictly positive.

theorem MagnitudeConjecture.GradedTreeExcess.matrixIntrinsicEulerExcess_eq_length_sub_projectives_sub_one {ι : Type u} [Fintype ι] (Phi : Matrix ι ι ℤ) {L : ℕ} (verticesAt : Fin (L + 1) → ℤ) (arrowsAt : Fin L → ℤ) (projectives : ℤ) (source_singleton : verticesAt 0 = 1) (sink_singleton : verticesAt (Fin.last L) = 1) (slice_tree_edges : ∀ (j : Fin L), arrowsAt j = verticesAt j.castSucc + verticesAt j.succ - 1) (meshEulerTotal : ARCount.matrixTotal Phi = vertexTotal verticesAt - arrowTotal arrowsAt + (vertexTotal verticesAt - projectives)) : DirectedDeletion.intrinsicEulerExcess Phi = ↑L - (projectives - 1)

Bridge from the graded count to the matrix-defined intrinsic factor excess used by directed deletion.

theorem MagnitudeConjecture.GradedTreeExcess.matrixIntrinsicEulerExcess_nonnegative {ι : Type u} [Fintype ι] (Phi : Matrix ι ι ℤ) {L : ℕ} (verticesAt : Fin (L + 1) → ℤ) (arrowsAt : Fin L → ℤ) (projectives : ℤ) (source_singleton : verticesAt 0 = 1) (sink_singleton : verticesAt (Fin.last L) = 1) (slice_tree_edges : ∀ (j : Fin L), arrowsAt j = verticesAt j.castSucc + verticesAt j.succ - 1) (meshEulerTotal : ARCount.matrixTotal Phi = vertexTotal verticesAt - arrowTotal arrowsAt + (vertexTotal verticesAt - projectives)) (realization_length_bound : projectives - 1 ≤ ↑L) : 0 ≤ DirectedDeletion.intrinsicEulerExcess Phi

Matrix form of nonnegative intrinsic factor excess.

theorem MagnitudeConjecture.GradedTreeExcess.matrixIntrinsicEulerExcess_eq_zero_iff {ι : Type u} [Fintype ι] (Phi : Matrix ι ι ℤ) {L : ℕ} (verticesAt : Fin (L + 1) → ℤ) (arrowsAt : Fin L → ℤ) (projectives : ℤ) (source_singleton : verticesAt 0 = 1) (sink_singleton : verticesAt (Fin.last L) = 1) (slice_tree_edges : ∀ (j : Fin L), arrowsAt j = verticesAt j.castSucc + verticesAt j.succ - 1) (meshEulerTotal : ARCount.matrixTotal Phi = vertexTotal verticesAt - arrowTotal arrowsAt + (vertexTotal verticesAt - projectives)) : DirectedDeletion.intrinsicEulerExcess Phi = 0 ↔ ↑L = projectives - 1

Matrix form of the sharp equality criterion for the length bound.