Separated degree intervals

def MagnitudeConjecture.GradedInterval.InBlock (r h j : ℕ) (d : ℤ) : Prop

Membership in the j-th retained interval, with h omitted degrees between successive intervals of length r+1.

theorem MagnitudeConjecture.GradedInterval.block_gap (r h : ℕ) {i j : ℕ} {x y : ℤ} (hij : i < j) (hx : InBlock r h i x) (hy : InBlock r h j y) : ↑h < y - x

Degrees in different retained blocks differ by more than the Hom bound.

theorem MagnitudeConjecture.GradedInterval.block_index_eq_of_close (r h : ℕ) {i j : ℕ} {x y : ℤ} (hx : InBlock r h i x) (hy : InBlock r h j y) (hclose : |y - x| ≤ ↑h) : i = j

A nonzero Hom degree can connect only one retained block.

theorem MagnitudeConjecture.GradedInterval.inBlock_of_between (r h j : ℕ) {x y z : ℤ} (hx : InBlock r h j x) (hy : InBlock r h j y) (hxz : x ≤ z) (hzy : z ≤ y) : InBlock r h j z

Intermediate degrees between two degrees of a retained block stay in that block.

def MagnitudeConjecture.GradedInterval.Retained (r h q : ℕ) (d : ℤ) : Prop

The retained degrees for q separated copies of [0,r].

theorem MagnitudeConjecture.GradedInterval.retained_of_between_close (r h q : ℕ) {x y z : ℤ} (hx : Retained r h q x) (hy : Retained r h q y) (hclose : |y - x| ≤ ↑h) (hxz : x ≤ z) (hzy : z ≤ y) : Retained r h q z

A degree between close retained endpoints is retained.