Directed deletion from the direct count and graded factor positivity #
This file combines the live manuscript's vertex--arrow--mesh deletion count with the graded translation-slice proof that the factor Euler excess is nonnegative. The remaining representation-theoretic input is visible: new meshes must inject into gained arrow occurrences.
theorem
MagnitudeConjecture.DirectedDeletion.translationQuiverSurplus_difference_nonnegative_of_translationRecurrence
{H : Type v}
[Fintype H]
(Phi : Matrix H H ℤ)
(vA nA aA vB nB aB q a0 aH z newArrows newMeshes : ℤ)
{L : ℕ}
(vertices arrows tauInjectives tauProjectives : ℕ → ℤ)
(projectives : ℤ)
(vertexCount : vA = vB + q)
(simpleCount : nA = nB + 1)
(ambientArrowCount : aA = a0 + aH + z)
(quotientArrowCount : aB = a0 + newArrows)
(factorEulerCount : intrinsicEulerExcess Phi = 2 * q - aH - projectives - 1)
(newMeshCount : newMeshes = z - (projectives - 1))
(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 = ((GradedTreeExcess.vertexTotal fun (j : Fin (L + 1)) => vertices ↑j) - GradedTreeExcess.arrowTotal fun (j : Fin L) => arrows ↑j) + ((GradedTreeExcess.vertexTotal fun (j : Fin (L + 1)) => vertices ↑j) - projectives))
(realization_length_bound : projectives - 1 ≤ ↑L)
(newMeshes_le_newArrows : newMeshes ≤ newArrows)
:
0 ≤ translationQuiverSurplus vA nA aA - translationQuiverSurplus vB nB aB
The directed-deletion inequality after supplying the literal direct counts and replacing abstract factor-excess nonnegativity by the graded translation recurrence and realization bound.
theorem
MagnitudeConjecture.DirectedDeletion.translationQuiverSurplus_difference_eq_zero_iff_of_translationRecurrence
{H : Type v}
[Fintype H]
(Phi : Matrix H H ℤ)
(vA nA aA vB nB aB q a0 aH z newArrows newMeshes : ℤ)
{L : ℕ}
(vertices arrows tauInjectives tauProjectives : ℕ → ℤ)
(projectives : ℤ)
(vertexCount : vA = vB + q)
(simpleCount : nA = nB + 1)
(ambientArrowCount : aA = a0 + aH + z)
(quotientArrowCount : aB = a0 + newArrows)
(factorEulerCount : intrinsicEulerExcess Phi = 2 * q - aH - projectives - 1)
(newMeshCount : newMeshes = z - (projectives - 1))
(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 = ((GradedTreeExcess.vertexTotal fun (j : Fin (L + 1)) => vertices ↑j) - GradedTreeExcess.arrowTotal fun (j : Fin L) => arrows ↑j) + ((GradedTreeExcess.vertexTotal fun (j : Fin (L + 1)) => vertices ↑j) - projectives))
(realization_length_bound : projectives - 1 ≤ ↑L)
(newMeshes_le_newArrows : newMeshes ≤ newArrows)
:
translationQuiverSurplus vA nA aA - translationQuiverSurplus vB nB aB = 0 ↔ ↑L = projectives - 1 ∧ newArrows = newMeshes
The sharp directed-deletion equality criterion under the same direct count and graded translation hypotheses. Equality separates into sharp realization length and bijectivity of the new-mesh/new-arrow injection.
theorem
MagnitudeConjecture.DirectedDeletion.finrank_eq_one_of_translationQuiverSurplus_difference_eq_zero_of_translationRecurrence_and_posetSpace
{H : Type v}
[Fintype H]
(Phi : Matrix H H ℤ)
(vA nA aA vB nB aB q a0 aH z newArrows newMeshes : ℤ)
{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)
(vertexCount : vA = vB + q)
(simpleCount : nA = nB + 1)
(ambientArrowCount : aA = a0 + aH + z)
(quotientArrowCount : aB = a0 + newArrows)
(factorEulerCount : intrinsicEulerExcess Phi = 2 * q - aH - projectives - 1)
(newMeshCount : newMeshes = z - (projectives - 1))
(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 = ((GradedTreeExcess.vertexTotal fun (j : Fin (L + 1)) => vertices ↑j) - GradedTreeExcess.arrowTotal fun (j : Fin L) => arrows ↑j) + ((GradedTreeExcess.vertexTotal fun (j : Fin (L + 1)) => vertices ↑j) - projectives))
(realization_length_bound : projectives - 1 ≤ ↑L)
(newMeshes_le_newArrows : newMeshes ≤ newArrows)
(hzero : translationQuiverSurplus vA nA aA - translationQuiverSurplus vB nB aB = 0)
(X : PosetSpace.Obj k T)
(hX : PosetSpace.IsSchur k T X)
:
Module.finrank k X.carrier = 1
Equality in the complete direct deletion count makes the poset-space realization sharp, so every Schur realization object is one-dimensional.