structure Hex.GraphIso.Nauty.Sparse.DistanceState {n : Nat} (level : Nat) (before s : RefineSt n) (first : Nat) : Prop

The actual distance-cell scan preserves unprocessed cells while making every completed cell constant in the captured distance array.

• valid : RefineSt.Valid level s
• step : RefineSt.Step level before s
• bound : first ≤ n
• suffix : RefinePrefix level first before.ptn s.ptn
• constant : ConstantPrefix n level first (fun (v : Nat) => before.hits[v]!) s.lab s.ptn
• hits : s.hits = before.hits
• active : Activation n level before.ptn s.ptn before.active s.active

theorem Hex.GraphIso.Nauty.Sparse.DistanceState.initial {n level : Nat} {s : RefineSt n} (h : RefineSt.Valid level s) : DistanceState level s s 0

theorem Hex.GraphIso.Nauty.Sparse.DistanceState.cell {n level first : Nat} {before s : RefineSt n} (h : DistanceState level before s first) (hf : first < n) : IsCell s.ptn level first (s.cellend[first]! + 1 - first) ∧ first ≤ s.cellend[first]! ∧ s.cellend[first]! < n

theorem Hex.GraphIso.Nauty.Sparse.DistanceState.singleton {n level first : Nat} {before s : RefineSt n} (h : DistanceState level before s first) (hf : first < n) (he : s.cellend[first]! = first) : DistanceState level before s (first + 1)

theorem Hex.GraphIso.Nauty.Sparse.DistanceState.counts {n level first : Nat} {before s : RefineSt n} (h : DistanceState level before s first) (hbefore : RefineSt.Valid level before) (hv : ∀ (v : Nat), v < n → before.hits[v]! ≤ n) (hf : first < n) : DistanceState level before (splitCounts level first true s) (s.cellend[first]! + 1)