Translation recurrence for graded slice counts

The frozen manuscript proves that every adjacent level slice in the finite strict tau-factor has the edge count of a tree. Its induction has a purely numerical core: remove the tau-injective leaves from one slice, translate the remaining arrows, and attach the new tau-projective leaves in the next slice.

This file proves that the corresponding arrow and vertex recurrences propagate the tree edge formula. It then feeds that formula into the intrinsic Euler excess theorems. Establishing the two recurrences from an actual translation quiver remains a separate categorical obligation.

theorem MagnitudeConjecture.GradedTreeExcess.sliceEdgeCount_of_translationRecurrence {L : ℕ} (vertices arrows tauInjectives tauProjectives : ℕ → ℤ) (firstSlice : arrows 0 = vertices 0 + vertices 1 - 1) (arrowStep : ∀ (j : ℕ), j + 1 < L → arrows (j + 1) = arrows j - tauInjectives j + tauProjectives (j + 2)) (vertexStep : ∀ (j : ℕ), j + 1 < L → vertices (j + 2) = vertices j - tauInjectives j + tauProjectives (j + 2)) (j : ℕ) : j < L → arrows j = vertices j + vertices (j + 1) - 1

The pruning/translation/attachment recurrence propagates the tree edge count from the first slice to every slice below L.

theorem MagnitudeConjecture.GradedTreeExcess.finiteSliceEdgeCount_of_translationRecurrence {L : ℕ} (vertices arrows tauInjectives tauProjectives : ℕ → ℤ) (firstSlice : arrows 0 = vertices 0 + vertices 1 - 1) (arrowStep : ∀ (j : ℕ), j + 1 < L → arrows (j + 1) = arrows j - tauInjectives j + tauProjectives (j + 2)) (vertexStep : ∀ (j : ℕ), j + 1 < L → vertices (j + 2) = vertices j - tauInjectives j + tauProjectives (j + 2)) (j : Fin L) : arrows ↑j = vertices ↑j.castSucc + vertices ↑j.succ - 1

Finite-level form of the propagated slice edge count.

theorem MagnitudeConjecture.GradedTreeExcess.arrowTotal_eq_of_translationRecurrence {L : ℕ} (vertices arrows tauInjectives tauProjectives : ℕ → ℤ) (source_singleton : vertices 0 = 1) (sink_singleton : vertices L = 1) (firstSlice : arrows 0 = vertices 0 + vertices 1 - 1) (arrowStep : ∀ (j : ℕ), j + 1 < L → arrows (j + 1) = arrows j - tauInjectives j + tauProjectives (j + 2)) (vertexStep : ∀ (j : ℕ), j + 1 < L → vertices (j + 2) = vertices j - tauInjectives j + tauProjectives (j + 2)) : (arrowTotal fun (j : Fin L) => arrows ↑j) = (2 * vertexTotal fun (j : Fin (L + 1)) => vertices ↑j) - ↑L - 2

The translation recurrence gives the manuscript's total arrow count.

theorem MagnitudeConjecture.GradedTreeExcess.intrinsicExcessFromCounts_eq_of_translationRecurrence {L : ℕ} (vertices arrows tauInjectives tauProjectives : ℕ → ℤ) (projectives : ℤ) (source_singleton : vertices 0 = 1) (sink_singleton : vertices L = 1) (firstSlice : arrows 0 = vertices 0 + vertices 1 - 1) (arrowStep : ∀ (j : ℕ), j + 1 < L → arrows (j + 1) = arrows j - tauInjectives j + tauProjectives (j + 2)) (vertexStep : ∀ (j : ℕ), j + 1 < L → vertices (j + 2) = vertices j - tauInjectives j + tauProjectives (j + 2)) : intrinsicExcessFromCounts (vertexTotal fun (j : Fin (L + 1)) => vertices ↑j) (arrowTotal fun (j : Fin L) => arrows ↑j) projectives = ↑L - (projectives - 1)

Under the translation recurrence, the intrinsic factor excess is the grading length minus the number of non-root projectives.

theorem MagnitudeConjecture.GradedTreeExcess.matrixIntrinsicEulerExcess_nonnegative_of_translationRecurrence {ι : Type u} [Fintype ι] (Phi : Matrix ι ι ℤ) {L : ℕ} (vertices arrows tauInjectives tauProjectives : ℕ → ℤ) (projectives : ℤ) (source_singleton : vertices 0 = 1) (sink_singleton : vertices L = 1) (firstSlice : arrows 0 = vertices 0 + vertices 1 - 1) (arrowStep : ∀ (j : ℕ), j + 1 < L → arrows (j + 1) = arrows j - tauInjectives j + tauProjectives (j + 2)) (vertexStep : ∀ (j : ℕ), j + 1 < L → vertices (j + 2) = vertices j - tauInjectives j + tauProjectives (j + 2)) (meshEulerTotal : ARCount.matrixTotal Phi = ((vertexTotal fun (j : Fin (L + 1)) => vertices ↑j) - arrowTotal fun (j : Fin L) => arrows ↑j) + ((vertexTotal fun (j : Fin (L + 1)) => vertices ↑j) - projectives)) (realization_length_bound : projectives - 1 ≤ ↑L) : 0 ≤ DirectedDeletion.intrinsicEulerExcess Phi

Matrix form: the translation recurrence and realization-length bound discharge the intrinsic nonnegativity hypothesis of directed deletion.

theorem MagnitudeConjecture.GradedTreeExcess.matrixIntrinsicEulerExcess_eq_zero_iff_of_translationRecurrence {ι : Type u} [Fintype ι] (Phi : Matrix ι ι ℤ) {L : ℕ} (vertices arrows tauInjectives tauProjectives : ℕ → ℤ) (projectives : ℤ) (source_singleton : vertices 0 = 1) (sink_singleton : vertices L = 1) (firstSlice : arrows 0 = vertices 0 + vertices 1 - 1) (arrowStep : ∀ (j : ℕ), j + 1 < L → arrows (j + 1) = arrows j - tauInjectives j + tauProjectives (j + 2)) (vertexStep : ∀ (j : ℕ), j + 1 < L → vertices (j + 2) = vertices j - tauInjectives j + tauProjectives (j + 2)) (meshEulerTotal : ARCount.matrixTotal Phi = ((vertexTotal fun (j : Fin (L + 1)) => vertices ↑j) - arrowTotal fun (j : Fin L) => arrows ↑j) + ((vertexTotal fun (j : Fin (L + 1)) => vertices ↑j) - projectives)) : DirectedDeletion.intrinsicEulerExcess Phi = 0 ↔ ↑L = projectives - 1

Matrix equality criterion under the translation recurrence.

theorem MagnitudeConjecture.GradedTreeExcess.matrixIntrinsicEulerExcess_nonnegative_of_translationRecurrence_and_posetSpace {ι : Type u} [Fintype ι] (Phi : Matrix ι ι ℤ) {L : ℕ} (vertices arrows tauInjectives tauProjectives : ℕ → ℤ) (projectives : ℤ) {k T : Type w} [Field k] [PartialOrder T] [Fintype T] (projectives_eq : projectives = ↑(Fintype.card T) + 1) (grading : PosetSpace.PositiveGrading (PosetSpace.Obj k T) (PosetSpace.IsSchur k T) L) (source_singleton : vertices 0 = 1) (sink_singleton : vertices L = 1) (firstSlice : arrows 0 = vertices 0 + vertices 1 - 1) (arrowStep : ∀ (j : ℕ), j + 1 < L → arrows (j + 1) = arrows j - tauInjectives j + tauProjectives (j + 2)) (vertexStep : ∀ (j : ℕ), j + 1 < L → vertices (j + 2) = vertices j - tauInjectives j + tauProjectives (j + 2)) (meshEulerTotal : ARCount.matrixTotal Phi = ((vertexTotal fun (j : Fin (L + 1)) => vertices ↑j) - arrowTotal fun (j : Fin L) => arrows ↑j) + ((vertexTotal fun (j : Fin (L + 1)) => vertices ↑j) - projectives)) : 0 ≤ DirectedDeletion.intrinsicEulerExcess Phi

The poset-space realization and its positive grading construct the realization-length bound, so the translation recurrence alone then gives nonnegative intrinsic factor excess.

theorem MagnitudeConjecture.GradedTreeExcess.finrank_eq_one_of_matrixIntrinsicEulerExcess_eq_zero_of_translationRecurrence_and_posetSpace {ι : Type u} [Fintype ι] (Phi : Matrix ι ι ℤ) {L : ℕ} (vertices arrows tauInjectives tauProjectives : ℕ → ℤ) (projectives : ℤ) {k T : Type w} [Field k] [PartialOrder T] [Fintype T] (projectives_eq : projectives = ↑(Fintype.card T) + 1) (grading : PosetSpace.PositiveGrading (PosetSpace.Obj k T) (PosetSpace.IsSchur k T) L) (source_singleton : vertices 0 = 1) (sink_singleton : vertices L = 1) (firstSlice : arrows 0 = vertices 0 + vertices 1 - 1) (arrowStep : ∀ (j : ℕ), j + 1 < L → arrows (j + 1) = arrows j - tauInjectives j + tauProjectives (j + 2)) (vertexStep : ∀ (j : ℕ), j + 1 < L → vertices (j + 2) = vertices j - tauInjectives j + tauProjectives (j + 2)) (meshEulerTotal : ARCount.matrixTotal Phi = ((vertexTotal fun (j : Fin (L + 1)) => vertices ↑j) - arrowTotal fun (j : Fin L) => arrows ↑j) + ((vertexTotal fun (j : Fin (L + 1)) => vertices ↑j) - projectives)) (hzero : DirectedDeletion.intrinsicEulerExcess Phi = 0) (X : PosetSpace.Obj k T) (hX : PosetSpace.IsSchur k T X) : Module.finrank k X.carrier = 1

Vanishing intrinsic excess makes the realization bound sharp and hence forces every Schur poset space to be one-dimensional.