Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardBoundaryCount

A uniform count of boundary targets in supported intervals #

source
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportedBoundaryLabel {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
Type

Targets outside the common interior range for radical-square comparison.

Instances For
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportedBoundaryLabel_card_le {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
    Nat.card (S.standardFormSupportedBoundaryLabel m) ≤ S.n * (3 * S.standardFormIntervalControlHeight)

    The number of actual boundary targets is bounded independently of interval length.