The literal primitive-deletion layer

For a primitive idempotent e, the indecomposable modules over A / AeA are already present in the ambient skeleton: they are exactly the labels on which AeA acts by zero. This file records that identification at the level needed by the new-mesh/new-arrow argument and fixes one ambient Krull--Schmidt multiplicity function for all subsequent counts.

No second quotient-only counting model is introduced. In particular, the multiplicity of a summand in a Hoshino torsion middle term is measured by the same ambient skeleton that defines the ambient arrow multiplicities.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveQuotientLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : Type

The ambient skeleton labels which are literal indecomposables over the primitive quotient A / AeA.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientLabelObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (x : S.PrimitiveQuotientLabel D) : PrimitiveQuotientSubcategory e

A primitive-quotient label, bundled in the full subcategory of ambient modules annihilated by AeA.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveDeletedSimple {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : FinitelyGeneratedCategory A

The deleted simple E = S_e, realized as the top of its primitive projective cover.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveDeletedSimpleProjection {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : S.fgObj (S.primitiveSourceLabel D) ⟶ S.primitiveDeletedSimple D

The canonical projective-cover map onto the deleted simple.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveDeletedSimple_primitiveSinkHom_finrank_eq_one {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} {D : PrimitiveIdempotentData e} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) : Module.finrank k (S.primitiveDeletedSimple D ⟶ S.fgObj (S.primitiveSinkLabel D)) = 1

The deleted simple maps one-dimensionally into the distinguished primitive injective.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveDeletedSimpleToSink {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} {D : PrimitiveIdempotentData e} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) : S.primitiveDeletedSimple D ⟶ S.fgObj (S.primitiveSinkLabel D)

A chosen nonzero embedding of the deleted simple into its distinguished primitive injective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveDeletedSimpleToSink_ne_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} {D : PrimitiveIdempotentData e} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) : S.primitiveDeletedSimpleToSink H ≠ 0

The chosen map from the deleted simple to the primitive injective is nonzero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveDeletedSimpleToSink_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} {D : PrimitiveIdempotentData e} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) : Function.Injective ⇑(ModuleCat.Hom.hom (S.primitiveDeletedSimpleToSink H).hom)

The chosen nonzero map from the simple E is monic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.hom_to_primitiveDeletedSimple_eq_zero_of_inAdd {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} {D : PrimitiveIdempotentData e} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (M : FinitelyGeneratedCategory A) (hM : S.almostSplitSkeleton.InAdd (S.primitiveKilledLabels D) M) (f : M ⟶ S.primitiveDeletedSimple D) : f = 0

Every map from a killed additive object to the deleted simple is zero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.hom_primitiveDeletedSimple_to_primitiveQuotientLabel_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (x : S.PrimitiveQuotientLabel D) (f : S.primitiveDeletedSimple D ⟶ S.fgObj ↑x) : f = 0

There are no maps from the deleted simple to an indecomposable module over A/AeA.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.hom_primitiveDeletedSimple_eq_zero_of_inAdd {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} {D : PrimitiveIdempotentData e} (M : FinitelyGeneratedCategory A) (hM : S.almostSplitSkeleton.InAdd (S.primitiveKilledLabels D) M) (f : S.primitiveDeletedSimple D ⟶ M) : f = 0

Every map from the deleted simple to a killed additive object is zero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.isAnnihilatedBy_primitiveIdeal_middle_of_exact {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) {Q E N : FinitelyGeneratedCategory A} (i : Q ⟶ E) (q : E ⟶ N) (hexact : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom i) ⇑(CategoryTheory.ConcreteCategory.hom q)) (hQ : IsAnnihilatedBy (primitiveIdeal e) Q) (hN : IsAnnihilatedBy (primitiveIdeal e) N) : IsAnnihilatedBy (primitiveIdeal e) E

For an idempotent generator, the full subcategory annihilated by AeA is extension closed.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.decompositionLabel_mem_primitiveKilledLabels {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (M : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy (primitiveIdeal e) M) {n : ℕ} {label : Fin n → Fin S.n} (d : M ≅ ⨁ fun (i : Fin n) => S.fgObj (label i)) (i : Fin n) : label i ∈ S.primitiveKilledLabels D

Every displayed ambient decomposition of an AeA-annihilated module uses only primitive-quotient labels.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.inAdd_primitiveKilledLabels_of_isAnnihilatedBy {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (M : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy (primitiveIdeal e) M) : S.almostSplitSkeleton.InAdd (S.primitiveKilledLabels D) M

Hence every AeA-annihilated module belongs to the additive closure of the primitive-quotient labels in the ambient skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.chosenLabelDecomposition_label_mem_primitiveKilledLabels {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (M : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy (primitiveIdeal e) M) (i : Fin (S.chosenLabelDecomposition M).n) : (S.chosenLabelDecomposition M).label i ∈ S.primitiveKilledLabels D

The ambient decomposition chosen by the tau-category construction also uses only primitive-quotient labels on an annihilated module.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecomposableMultiplicity {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (M : FinitelyGeneratedCategory A) : ℕ

Multiplicity of one ambient skeleton label in the fixed displayed Krull--Schmidt decomposition of a finitely generated module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecomposableMultiplicity_eq_of_decomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (M : FinitelyGeneratedCategory A) {n : ℕ} {label : Fin n → Fin S.n} (d : M ≅ ⨁ fun (i : Fin n) => S.fgObj (label i)) : S.indecomposableMultiplicity p M = ∑ i : Fin n, if label i = p then 1 else 0

The fixed multiplicity agrees with the occurrence count in any other displayed decomposition into the same ambient skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecomposableMultiplicity_eq_of_fintype_decomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (M : FinitelyGeneratedCategory A) {I : Type} [Fintype I] [Finite I] {label : I → Fin S.n} (d : M ≅ ⨁ fun (i : I) => S.fgObj (label i)) : S.indecomposableMultiplicity p M = ∑ i : I, if label i = p then 1 else 0

The fixed multiplicity agrees with a decomposition indexed by any finite type. This is the index-neutral form used by almost-split decompositions, whose index is stored as a FintypeCat.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecomposableMultiplicity_iso_invariant {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) {M N : FinitelyGeneratedCategory A} (d : M ≅ N) : S.indecomposableMultiplicity p M = S.indecomposableMultiplicity p N

Ambient indecomposable multiplicity is invariant under module isomorphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecomposableMultiplicity_biprod {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (M N : FinitelyGeneratedCategory A) : S.indecomposableMultiplicity p (M ⊞ N) = S.indecomposableMultiplicity p M + S.indecomposableMultiplicity p N

Ambient indecomposable multiplicity is additive across a binary biproduct.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecomposableMultiplicity_fgObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p q : Fin S.n) : S.indecomposableMultiplicity p (S.fgObj q) = if q = p then 1 else 0

The multiplicity of a skeleton label in one displayed indecomposable is the corresponding Kronecker delta.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecomposableMultiplicity_meshRightMiddle {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p z : Fin S.n) : S.indecomposableMultiplicity p (S.meshRightAlmostSplitAt z).middle = FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData p z

At every ambient endpoint, including the projective boundary, the fixed object multiplicity of the standard right-mesh middle term is exactly the ambient arrow multiplicity.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecomposableMultiplicity_eq_zero_of_isAnnihilatedBy {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (p : Fin S.n) (hp : p ∉ S.primitiveKilledLabels D) (M : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy (primitiveIdeal e) M) : S.indecomposableMultiplicity p M = 0

A label outside the primitive quotient has multiplicity zero in every AeA-annihilated module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveTorsionFGObj_inAdd_primitiveKilledLabels {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (M : FinitelyGeneratedCategory A) : S.almostSplitSkeleton.InAdd (S.primitiveKilledLabels D) (primitiveTorsionFGObj e M)

Every Hoshino torsion radical decomposes entirely into literal primitive-quotient labels.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecomposableMultiplicity_primitiveTorsion_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (p : Fin S.n) (hp : p ∉ S.primitiveKilledLabels D) (M : FinitelyGeneratedCategory A) : S.indecomposableMultiplicity p (primitiveTorsionFGObj e M) = 0

Consequently, labels deleted from the literal quotient never occur in a Hoshino torsion middle term.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientARShortComplex {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)

The ambient Auslander--Reiten sequence at an arbitrary nonprojective selected label, with its kernel identified with the selected translate.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientARShortComplex_shortExact {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : (S.ambientARShortComplex z).ShortExact

Every displayed ambient Auslander--Reiten sequence is short exact.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : Type

A right endpoint whose relative Auslander--Reiten mesh is new after primitive deletion. Its endpoint is an A/AeA-module, it is nonprojective in that literal quotient category, and its ambient translate lies outside the quotient subcategory.

• label : S.PrimitiveQuotientLabel D
• ambient_nonprojective : ¬CategoryTheory.Projective (S.fgObj ↑self.label)
• quotient_nonprojective : ¬CategoryTheory.Projective (S.primitiveQuotientLabelObj D self.label)
• translation_not_mem : S.rightTranslationLabel ⟨↑self.label, ⋯⟩ ∉ S.primitiveKilledLabels D

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.ambientLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (N : S.PrimitiveNewRightMeshEndpoint D) : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }

The endpoint as an ambient nonprojective label.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.rightMarker {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (N : S.PrimitiveNewRightMeshEndpoint D) : S.SurvivingLabel (S.primitiveKilledLabels D)

The deleted ambient translate q_N = τ_A N, bundled as a surviving label of the factor category mod A / [mod (A/AeA)].

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.rightMarker_isInjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (N : S.PrimitiveNewRightMeshEndpoint D) : (S.factorFiniteTauCategoryData (S.primitiveKilledLabels D)).IsInjective N.rightMarker

The marker q_N = τ_A N is tau-injective in the factor category: its ambient inverse translate is the quotient label N, which is killed in the factor.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.rightMarkerInjectiveLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (N : S.PrimitiveNewRightMeshEndpoint D) : S.FactorInjectiveLabel (S.primitiveKilledLabels D)

The factor-injective boundary label supplied by a new mesh endpoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.rightMarker_primitiveMultiplicity_eq_one {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D)) (N : S.PrimitiveNewRightMeshEndpoint D) : S.primitiveMultiplicity D ↑N.rightMarker = 1

The boundary coordinate theorem gives the marker multiplicity [q_N : S_e] = 1.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.IsPositive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (N : S.PrimitiveNewRightMeshEndpoint D) : Prop

The manuscript's positive boundary test, expressed in the form used by the new-arrow construction: Hom_A(S_e,q_N)=0. Complementarity with the left marker is proved at the later boundary-correspondence layer.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.hom_primitiveDeletedSimple_to_ambientMiddle_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (N : S.PrimitiveNewRightMeshEndpoint D) (hpositive : N.IsPositive) (f : S.primitiveDeletedSimple D ⟶ (S.minimalRightAlmostSplitAt ↑N.label).middle) : f = 0

At a positive new mesh, the deleted simple has no map to the ambient AR middle term.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.sourceModule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (N : S.PrimitiveNewRightMeshEndpoint D) : FinitelyGeneratedCategory A

The Hoshino torsion radical of the ambient translate is the source of the new relative mesh.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.middleModule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (N : S.PrimitiveNewRightMeshEndpoint D) : FinitelyGeneratedCategory A

The middle term of the new relative mesh is the torsion radical of the ambient right almost-split middle term.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.rightKernelMap_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (N : S.PrimitiveNewRightMeshEndpoint D) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (S.rightKernelMap N.ambientLabel))

Ambient injectivity of the transported AR-kernel inclusion.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.fgShortComplex {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (N : S.PrimitiveNewRightMeshEndpoint D) : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)

The ambient FG-module short complex underlying the new relative mesh. Its terms are R(τ_A N), R(V_N), and N.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.fgShortComplex_shortExact {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (N : S.PrimitiveNewRightMeshEndpoint D) : N.fgShortComplex.ShortExact

Hoshino's comparison makes the displayed new relative mesh short exact.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.sourceModule_not_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (N : S.PrimitiveNewRightMeshEndpoint D) : ¬CategoryTheory.Injective N.sourceModule

The Hoshino torsion kernel which starts the new relative mesh is not injective even in the ambient module category.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.sourceAmbientLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (he : IsIdempotentElem e) (N : S.PrimitiveNewRightMeshEndpoint D) : Fin S.n

The source label selected from Hoshino's indecomposable torsion radical.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.sourceIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (he : IsIdempotentElem e) (N : S.PrimitiveNewRightMeshEndpoint D) : N.sourceModule ≅ S.fgObj (sourceAmbientLabel H he N)

The selected source label represents the actual torsion kernel R(τ_A N).

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.sourceAmbientLabel_mem {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (he : IsIdempotentElem e) (N : S.PrimitiveNewRightMeshEndpoint D) : sourceAmbientLabel H he N ∈ S.primitiveKilledLabels D

The source of a new relative mesh is itself a literal A/AeA-indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.sourceAmbientLabel_not_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (he : IsIdempotentElem e) (N : S.PrimitiveNewRightMeshEndpoint D) : ¬CategoryTheory.Injective (S.fgObj (sourceAmbientLabel H he N))

The selected ambient source label is noninjective.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.sourceLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (he : IsIdempotentElem e) (N : S.PrimitiveNewRightMeshEndpoint D) : S.PrimitiveQuotientLabel D

The source M of the new relative mesh, bundled in the same literal quotient label type as its endpoint N.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.sourceNoninjectiveLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (he : IsIdempotentElem e) (N : S.PrimitiveNewRightMeshEndpoint D) : { x : Fin S.n // ¬CategoryTheory.Injective (S.fgObj x) }

The source M as an ambient noninjective label, so that its inverse Auslander--Reiten translate is defined.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.leftMarkerAmbientLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (he : IsIdempotentElem e) (N : S.PrimitiveNewRightMeshEndpoint D) : Fin S.n

The ambient inverse-translation label underlying the manuscript's left marker p_M = τ_A⁻¹M. The later boundary theorem proves that it lies outside the primitive quotient label set.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.relativeArrowMultiplicity {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (source : S.PrimitiveQuotientLabel D) (N : S.PrimitiveNewRightMeshEndpoint D) : ℕ

Relative arrow multiplicity into N, computed in the existing ambient skeleton from the Hoshino torsion middle term.