1. Hom and mesh matrices
Almost-split sequences supply an inverse for the Hom-dimension matrix and a combinatorial formula for magnitude.
Matrix and numerical interfaceMathematical navigation
The graded-interval proof
The proof studies the difference between magnitude and the simple count. Finite graded intervals connect directed deletion to the general theorem.
2. Finite kernels and direct heights
Finite kernels bound the primitive-factor boundaries. Direct heights and generated relations realize the associated poset spaces.
Poset realization3. Directed deletion
The intrinsic excess and Ext compensation control deletion. The equality argument uses commutative squares and a simultaneous basis for two filtrations.
Directed surplus4. Finite graded intervals
Every graded indecomposable is a unique shift of a standard representative. Finite interval algebras have a uniform surplus estimate, which proves the lower bound.
Interval inequality5. Equality and almost-split transfer
Separated interval packing forces zero surplus and thinness. The control interval is biserial, and supported almost-split maps transfer its nonprojective middle-summand bound.
One-sided transfer6. The full theorem
The beta characterization gives special biseriality. The proved socle/string converse and Morita reduction complete the theorem.
Full proofEntry points
MagnitudeConjecture.MainResults provides the theorem, direct simple count and independent statement. The root MagnitudeConjecture also imports supporting results. Public and expanded axiom audits check both levels.
Selected direct imports around the public interface
Arrows point from a module to a module it imports. The graph is generated from source; other dependencies are omitted.
Paper correspondence
The formalization proves the main theorem of Magnitude of module categories and special biserial algebras. It uses the direct arguments in Appendix A, directed deletion and standard-form interval algebras. The correspondence explains these constructions and beta transfer to one control interval, and identifies the precise scope of each Lean result.