One-middle meshes in a finite tau-category

The frozen manuscript writes E₁ for the number of almost split meshes whose middle term has exactly one indecomposable occurrence. This file packages that literal finite type and records the numerical reduction of the AR surplus when every nonprojective mesh has at most two middle occurrences.

@[instance_reducible]

noncomputable def MagnitudeConjecture.FiniteTauMatrix.instDecidablePredIsProjective_magnitudeConjecture {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) : DecidablePred T.IsProjective

@[reducible, inline]

abbrev MagnitudeConjecture.FiniteTauMatrix.OneMiddleMesh {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) : Type w

Nonprojective right meshes having exactly one indecomposable middle-term occurrence. Repeated isomorphic summands would be separate occurrences, so the equality to one has the manuscript's multiplicity convention.

noncomputable def MagnitudeConjecture.FiniteTauMatrix.oneMiddleMeshCount {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) : ℕ

The manuscript's E₁.

noncomputable def MagnitudeConjecture.FiniteTauMatrix.projectiveIncomingArity {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) : ℕ

Total incoming-arrow multiplicity at tau-projective targets.

theorem MagnitudeConjecture.FiniteTauMatrix.oneMiddleMeshCount_eq_natCard_of_equiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) {α : Type u_1} [Finite α] (e : α ≃ OneMiddleMesh T) : oneMiddleMeshCount T = Nat.card α

An explicit equivalence with the one-middle mesh type computes E₁.

theorem MagnitudeConjecture.FiniteTauMatrix.sum_oneMiddleIndicator_eq_oneMiddleMeshCount {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) : (∑ Y : Ind, if ¬T.IsProjective Y ∧ rightMiddleArity T.toFiniteRightTauCategoryData Y = 1 then 1 else 0) = ↑(oneMiddleMeshCount T)

The one-middle indicator sums to E₁.

theorem MagnitudeConjecture.FiniteTauMatrix.sum_projectiveIncomingIndicator_eq_projectiveIncomingArity {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) : (∑ Y : Ind, if T.IsProjective Y then ↑(rightMiddleArity T.toFiniteRightTauCategoryData Y) else 0) = ↑(projectiveIncomingArity T)

The projective incoming-arity indicator sums to the integer form of the projective incoming count.

theorem MagnitudeConjecture.FiniteTauMatrix.localDensity_eq_oneMiddleIndicator_sub_projectiveIncoming {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (hbound : ∀ (Y : Ind), ¬T.IsProjective Y → rightMiddleArity T.toFiniteRightTauCategoryData Y ≤ 2) (Y : Ind) : ARCount.localDensity (arrowMultiplicity T.toFiniteRightTauCategoryData) T.IsProjective Y = (if ¬T.IsProjective Y ∧ rightMiddleArity T.toFiniteRightTauCategoryData Y = 1 then 1 else 0) - if T.IsProjective Y then ↑(rightMiddleArity T.toFiniteRightTauCategoryData Y) else 0

Under the two-middle bound, local AR density is 1 precisely at a one-middle mesh, is minus the incoming arity at a projective, and is zero at every other vertex.

theorem MagnitudeConjecture.FiniteTauMatrix.surplus_eq_oneMiddleMeshCount_sub_projectiveIncomingArity {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (hbound : ∀ (Y : Ind), ¬T.IsProjective Y → rightMiddleArity T.toFiniteRightTauCategoryData Y ≤ 2) : ARCount.surplus (arrowMultiplicity T.toFiniteRightTauCategoryData) T.IsProjective = ↑(oneMiddleMeshCount T) - ↑(projectiveIncomingArity T)

If every nonprojective mesh has at most two middle occurrences, the AR surplus is E₁ minus the total incoming multiplicity at projectives. This is the manuscript's E₁ - ell reduction without introducing a separate E₂.