Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardIntervalSurplusSlope

The interval surplus constant and its nonnegative-slope consequence #

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.surplusSlopeIntervalFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
FiniteDimensional k (S.standardFormIntervalAlgebra m)
source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.surplusSlopeIntervalNoetherian {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) :
IsNoetherianRing (S.standardFormIntervalAlgebra m)ᵐᵒᵖ
source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalSurplusErrorBound {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
ℤ

A fixed bound for all sufficiently long interval surplus errors.

Instances For
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInterval_surplus_error_uniform {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (hm : 2 * S.standardFormIntervalControlHeight ≤ m) :
    |(S.standardFormIntervalSkeleton m).ambientARSurplus - (↑m + 1) * S.ambientARSurplus| ≤ S.standardFormIntervalSurplusErrorBound

    The error bound is independent of the interval length.

    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientARSurplus_nonnegative_of_interval_nonnegative {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hpos : ∀ (m : ℕ), 0 ≤ (S.standardFormIntervalSkeleton m).ambientARSurplus) :
    0 ≤ S.ambientARSurplus

    Once the directed interval nonnegativity input is supplied, the interval slope argument proves the ambient surplus nonnegative.