Magnitude conjecture

MagnitudeConjecture.Combinatorics.DirectedDeletion

Numerical kernel of directed primitive deletion #

This file formalizes the live manuscript's direct vertex--arrow--mesh count. If q vertices are deleted, aH arrows have both endpoints in the deleted part, z arrows cross the boundary, p objects of the deleted factor are tau-projective, newArrows arrows are gained downstairs, and newMeshes meshes are new downstairs, then

epsilon = 2*q - aH - p - 1,
newMeshes = z - (p - 1),
sigma(A) - sigma(B) = epsilon + newArrows - newMeshes.

No block inverse or Schur complement enters this count. Nonnegativity is exposed as the two representation-theoretic obligations 0 ≤ epsilon and newMeshes ≤ newArrows.

source
def MagnitudeConjecture.DirectedDeletion.intrinsicEulerExcess {H : Type v} [Fintype H] (Phi : Matrix H H ℤ) :
ℤ

Intrinsic Euler excess of the finite strict tau-factor.

Instances For
    source
    def MagnitudeConjecture.DirectedDeletion.deletionCost {H : Type v} [Fintype H] (Phi : Matrix H H ℤ) (newArrows newMeshes : ℤ) :
    ℤ

    The directed-deletion correction in the live manuscript.

    Instances For
      source
      def MagnitudeConjecture.DirectedDeletion.translationQuiverSurplus (vertices simples arrows : ℤ) :
      ℤ

      Surplus expressed using the vertex, simple, and arrow counts of a finite Auslander--Reiten translation quiver.

      Instances For
        source
        theorem MagnitudeConjecture.DirectedDeletion.surplus_eq_translationQuiverSurplus {H : Type v} [Fintype H] (arrowMultiplicity : H → H → ℕ) (IsProjective : H → Prop) [DecidablePred IsProjective] :
        ARCount.surplus arrowMultiplicity IsProjective = translationQuiverSurplus ARCount.vertexCount (ARCount.projectiveCount IsProjective) (ARCount.arrowCount arrowMultiplicity)

        The usual Auslander--Reiten surplus is the translation-quiver surplus formed from its literal vertex, projective, and arrow counts.

        source
        theorem MagnitudeConjecture.DirectedDeletion.translationQuiverSurplus_difference_eq_deletionCost {H : Type v} [Fintype H] (Phi : Matrix H H ℤ) (vA nA aA vB nB aB q a0 aH z p newArrows newMeshes : ℤ) (vertexCount : vA = vB + q) (simpleCount : nA = nB + 1) (ambientArrowCount : aA = a0 + aH + z) (quotientArrowCount : aB = a0 + newArrows) (factorEulerCount : intrinsicEulerExcess Phi = 2 * q - aH - p - 1) (newMeshCount : newMeshes = z - (p - 1)) :
        translationQuiverSurplus vA nA aA - translationQuiverSurplus vB nB aB = deletionCost Phi newArrows newMeshes

        The live manuscript's direct deletion identity. The hypotheses are the literal vertex, simple, ambient-arrow, quotient-arrow, factor-Euler, and crossing-mesh counts appearing in the proof.

        source
        theorem MagnitudeConjecture.DirectedDeletion.translationQuiverSurplus_difference_nonnegative {H : Type v} [Fintype H] (Phi : Matrix H H ℤ) (vA nA aA vB nB aB q a0 aH z p newArrows newMeshes : ℤ) (vertexCount : vA = vB + q) (simpleCount : nA = nB + 1) (ambientArrowCount : aA = a0 + aH + z) (quotientArrowCount : aB = a0 + newArrows) (factorEulerCount : intrinsicEulerExcess Phi = 2 * q - aH - p - 1) (newMeshCount : newMeshes = z - (p - 1)) (factorExcess_nonnegative : 0 ≤ intrinsicEulerExcess Phi) (newMeshes_le_newArrows : newMeshes ≤ newArrows) :
        0 ≤ translationQuiverSurplus vA nA aA - translationQuiverSurplus vB nB aB

        The directed deletion is monotone once the factor Euler excess is nonnegative and new meshes inject into gained arrow occurrences.

        source
        theorem MagnitudeConjecture.DirectedDeletion.equality_iff_zero_factorExcess_and_equal_correction {H : Type v} [Fintype H] (Phi : Matrix H H ℤ) (newArrows newMeshes : ℤ) (factorExcess_nonnegative : 0 ≤ intrinsicEulerExcess Phi) (newMeshes_le_newArrows : newMeshes ≤ newArrows) :
        deletionCost Phi newArrows newMeshes = 0 ↔ intrinsicEulerExcess Phi = 0 ∧ newArrows = newMeshes

        Equality in a directed deletion forces both nonnegative contributions to vanish separately.