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.