theorem Hex.GraphIso.Nauty.Sparse.split_distances_equiv {n : Nat} (σ : Renaming n) (level : Nat) (s t : RefineSt n) (hs : RefineSt.Valid level s) (ht : RefineSt.Valid level t) (hv : ∀ (v : Nat), v < n → s.hits[v]! ≤ n) (hw : ∀ (v : Nat), v < n → t.hits[v]! ≤ n) (hkeys : ∀ (v : Nat), v < n → t.hits[σ.toFun v]! = s.hits[v]!) (he : RefineSt.Equiv σ level s t) : have run := fun (s : RefineSt n) => (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 : PUnit) (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 PUnit.unit state else __do_jp PUnit.unit state have state : RefineSt n := __s.fst pure state).run; RefineSt.Equiv σ level (run s) (run t)

The complete literal distance-cell loop preserves all refinement observations under renaming, given transported native distances.