Magnitude conjecture

MagnitudeConjecture.Combinatorics.DegreeOneDimension

A dimension function supported in degree one #

theorem MagnitudeConjecture.degreeOne_function_formula (q : ℤ → ℤ → ℕ) (D : ℕ) (hone : ∀ (t : ℤ), q (t + 1) t = D) (hlow : ∀ (s t : ℤ), s ≤ t → q s t = 0) (hhigh : ∀ (t : ℤ) (n : ℕ), 0 < n → q (t + ↑n + 1) t = 0) (s t : ℤ) :
q s t = if s = t + 1 then D else 0

Three degree ranges determine a dimension function supported on adjacent shifts.