The magnitude theorem with a direct simple-module count

The original endpoint computes the simple count using indecomposable projectives. This public interface exposes module-theoretic simplicity directly and uses the proved simple-top bijection to connect the two counts.

noncomputable def MagnitudeConjecture.RightModule.simpleModuleCount {k A : Type u} [Field k] [Ring A] [Algebra k A] (hA : IsRepresentationFinite k A) : ℕ

The number of simple right-module isomorphism classes, counted by testing module-theoretic simplicity on the complete indecomposable family.

theorem MagnitudeConjecture.RightModule.simpleModuleCount_eq_numberOfSimpleModules {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (hA : IsRepresentationFinite k A) : ↑(simpleModuleCount hA) = numberOfSimpleModules hA

The direct simple count agrees with the original projective-count interface.

theorem MagnitudeConjecture.RightModule.magnitudeConjecture_simpleCount {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] (hA : IsRepresentationFinite k A) : ↑(simpleModuleCount hA) ≤ moduleCategoryMagnitude hA ∧ (moduleCategoryMagnitude hA = ↑(simpleModuleCount hA) ↔ BoundQuiver.IsSpecialBiserial k A)

The magnitude inequality and equality characterization with the simple count defined directly through simple right modules.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.magnitudeConjecture_simpleCount {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : ↑S.simpleCount ≤ FiniteTauMatrix.categoryMagnitude S.finiteTauCategoryData ∧ (FiniteTauMatrix.categoryMagnitude S.finiteTauCategoryData = ↑S.simpleCount ↔ BoundQuiver.IsSpecialBiserial k A)

The same theorem on any complete finite indecomposable family.