theorem Hex.GraphIso.Nauty.Sparse.split_distances {n : Nat} (level : Nat) (s : RefineSt n) (h : RefineSt.Valid level s) (hv : ∀ (v : Nat), v < n → s.hits[v]! ≤ n) : have t := (have state := s; have first := 0; do let __s ← forIn [:n] (state, first) fun (x : Nat) (__s : RefineSt n × Nat) => have state := __s.fst; have first := __s.snd; if first ≥ n then pure (ForInStep.done (state, first)) else have last := state.cellend[first]!; have __do_jp := fun (__r : Unit) (state : RefineSt n) => have first := last + 1; pure (ForInStep.yield (state, first)); if first < last then have state := splitCounts level first true state; __do_jp () state else __do_jp () state have state : RefineSt n := __s.fst pure state).run; DistanceState level s t n

The literal distance-cell loop reaches the end of the partition and establishes constant distance keys and the fragment activation rule everywhere.