Finite coordinates for separated interval blocks

def MagnitudeConjecture.GradedInterval.packingEnd (r h q : ℕ) : ℕ

The last retained degree for q positive blocks.

theorem MagnitudeConjecture.GradedInterval.packingEnd_eq (r h q : ℕ) (hq : 1 ≤ q) : packingEnd r h q = q * (r + h + 1) - h - 1

This endpoint agrees with the manuscript's q(r+h+1)-h-1.

def MagnitudeConjecture.GradedInterval.blockPoint (r h q : ℕ) (j : Fin q) (t : Fin (r + 1)) : Fin (packingEnd r h q + 1)

The degree of a point in one of the retained blocks.

theorem MagnitudeConjecture.GradedInterval.blockPoint_inBlock (r h q : ℕ) (j : Fin q) (t : Fin (r + 1)) : InBlock r h ↑j ↑↑(blockPoint r h q j t)

Each block coordinate lies in its specified retained block.

theorem MagnitudeConjecture.GradedInterval.blockPoint_injective (r h q : ℕ) : Function.Injective fun (p : Fin q × Fin (r + 1)) => blockPoint r h q p.1 p.2

The pair of block number and offset is recovered from its degree.

theorem MagnitudeConjecture.GradedInterval.exists_blockPoint_of_retained (r h q : ℕ) (d : Fin (packingEnd r h q + 1)) (hd : Retained r h q ↑↑d) : ∃ (p : Fin q × Fin (r + 1)), blockPoint r h q p.1 p.2 = d

Every retained finite degree has a block coordinate.

noncomputable def MagnitudeConjecture.GradedInterval.retainedDegreeEquiv (r h q : ℕ) : Fin q × Fin (r + 1) ≃ { d : Fin (packingEnd r h q + 1) // Retained r h q ↑↑d }

The retained degree set is exactly q copies of the finite interval.