The actual graded incoming maps are minimal right almost split

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.gradedIncomingASQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Quiver (Fin S.n)

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.gradedIncomingASArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) : Fintype (x ⟶ y)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardGradedIncomingRecoveryIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormMeshRawFunctor.mapMat_.comp (S.standardFormGradedFunctor.comp Graded.FiniteGradedModule.underlyingFG) ≅ S.standardFormAdditiveRestrictedYonedaFunctor.comp S.standardFormProjectiveVertexModuleAlgebraEquivalence.functor

The actual incoming matrix has the same finitely generated realization as the established recovered mesh.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardGradedRecoveryIncoming_rightAlmostSplit {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (S.standardFormAdditiveRestrictedYonedaFunctor.map (S.standardFormRightMeshData.additiveIncomingMap z))

Before the endpoint identification, the recovered incoming matrix is almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardGradedRecoveryIncoming_rightMinimal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) : QuotientSubmoduleEquidistribution.IsRightMinimal (S.standardFormAdditiveRestrictedYonedaFunctor.map (S.standardFormRightMeshData.additiveIncomingMap z))

Before the endpoint identification, the recovered incoming matrix is right minimal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedIncomingMap_rightAlmostSplit {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (t : ℤ) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (S.standardFormGradedIncomingMap z t)

The degree-one incoming map is almost split in the full graded module category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedIncomingMap_rightMinimal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (t : ℤ) : QuotientSubmoduleEquidistribution.IsRightMinimal (S.standardFormGradedIncomingMap z t)

The same concrete map is right minimal after grading and shifting.