Primitive multiplicity on the projective boundary

This file formalizes the boundary reduction in the frozen manuscript. A tau-projective object of the literal primitive factor is either already ambient projective or its ambient Auslander--Reiten translate was killed. The manuscript's exact coordinate estimate then forces its primitive multiplicity to be one.

MultiplicityCoordinateEstimate is an intermediate interface for the manuscript's boundary-coordinate lemma. The final theorem must construct it; this file does not treat it as an unexplained headline hypothesis.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.MultiplicityCoordinateEstimate {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) : Prop

The exact numerical coordinate estimate used by the manuscript. It says that the multiplicity of a simple in an indecomposable projective or injective is at most one, and that multiplicities change by at most one under ambient Auslander--Reiten translation.

• projective_le_one (x : Fin S.n) : CategoryTheory.Projective (S.fgObj x) → D.multiplicity x ≤ 1
• injective_le_one (x : Fin S.n) : CategoryTheory.Injective (S.fgObj x) → D.multiplicity x ≤ 1
• translation_difference_le_one (z : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : |↑(D.multiplicity ↑z) - ↑(D.multiplicity (S.rightTranslationLabel z))| ≤ 1

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.MultiplicityCoordinateEstimate.ofMiddleSupport {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] {e : A} (D : PrimitiveIdempotentData e) (R : S.MiddleSupportCartanData D) (B : S.SchurianBoundaryData) : S.MultiplicityCoordinateEstimate (S.primitiveMultiplicityInput D)

The repaired Appendix A data constructs the numerical estimate for a literal primitive idempotent. The projective and injective clauses are the schurian corner bounds, while the translation clause comes from the Cartan form on the sequence-dependent middle-term support algebra.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.factorProjective_ambient_projective_or_translation_killed {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) (x : S.SurvivingLabel K) (hx : (S.factorFiniteTauCategoryData K).IsProjective x) : CategoryTheory.Projective (S.fgObj ↑x) ∨ ∃ (hnp : ¬CategoryTheory.Projective (S.fgObj ↑x)), S.rightTranslationLabel ⟨↑x, hnp⟩ ∈ K

A tau-projective surviving label is either ambient projective or its ambient right translate belongs to the killed set.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.factorProjective_multiplicity_eq_one {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) (E : S.MultiplicityCoordinateEstimate D) (p : S.FactorProjectiveLabel K) : D.multiplicity ↑↑p = 1

The manuscript's coordinate estimate forces multiplicity one on every tau-projective surviving label of the literal primitive factor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.factorInjective_ambient_injective_or_inverse_translation_killed {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) (x : S.SurvivingLabel K) (hx : (S.factorFiniteTauCategoryData K).IsInjective x) : CategoryTheory.Injective (S.fgObj ↑x) ∨ ∃ (hni : ¬CategoryTheory.Injective (S.fgObj ↑x)), ↑(S.rightTranslationEquiv.symm ⟨↑x, hni⟩) ∈ K

A tau-injective surviving label is either ambient injective or its ambient inverse right translate belongs to the killed set.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.factorInjective_multiplicity_eq_one {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) (E : S.MultiplicityCoordinateEstimate D) (i : S.FactorInjectiveLabel K) : D.multiplicity ↑↑i = 1

The manuscript's dual coordinate estimate forces multiplicity one on every tau-injective surviving label of the literal primitive factor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.ofCoordinateEstimate {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) (hacyclic : S.HasAcyclicNonzeroNonisomorphisms) (E : S.MultiplicityCoordinateEstimate D) : S.PrimitiveDirectedBoundaryData D

Ambient directedness and the coordinate estimate construct the complete boundary data required by the primitive projective-poset realization.