Multiplicity one on both primitive factor boundaries

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjective_primitiveMultiplicity_eq_one_finiteKernel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (D : PrimitiveIdempotentData e) (p : S.FactorProjectiveLabel (S.primitiveKilledLabels D)) : S.primitiveMultiplicity D ↑↑p = 1

Finite kernels and duality give multiplicity one on the projective boundary of the literal primitive factor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorInjective_primitiveMultiplicity_eq_one_finiteKernel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (D : PrimitiveIdempotentData e) (p : S.FactorInjectiveLabel (S.primitiveKilledLabels D)) : S.primitiveMultiplicity D ↑↑p = 1

Finite kernels give multiplicity one on the injective boundary of the literal primitive factor.

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

The complete boundary input is supplied by finite kernels, independently of the stronger translation-difference coordinate estimate.