structure Hex.GraphIso.Nauty.Sparse.Index.Complete (n first last : Nat) (oldlab hits oldstarts oldends : Array Nat) (s : RefineSt n) : Prop

The cache describes every count run and retains entries outside the original cell. Label permutation is retained for subsequent cache accesses.

• window : «Sort».Window oldlab s.lab first (last + 1)
• runs : Runs n first last (last + 1) s.lab hits s.cellstart s.cellend
• frame : Frame n first last oldlab s.lab oldstarts s.cellstart oldends s.cellend

theorem Hex.GraphIso.Nauty.Sparse.Index.Complete.iff {n first last : Nat} {oldlab hits oldstarts oldends : Array Nat} {s : RefineSt n} : Complete n first last oldlab hits oldstarts oldends s ↔ «Sort».Window oldlab s.lab first (last + 1) ∧ Runs n first last (last + 1) s.lab hits s.cellstart s.cellend ∧ Frame n first last oldlab s.lab oldstarts s.cellstart oldends s.cellend

theorem Hex.GraphIso.Nauty.Sparse.Index.Complete.of_tail {n first last : Nat} {oldlab hits oldstarts oldends : Array Nat} {s : RefineSt n} (h : Tail n first last last oldlab hits oldstarts oldends s) : Complete n first last oldlab hits oldstarts oldends s

theorem Hex.GraphIso.Nauty.Sparse.Index.Complete.transfer {n first last : Nat} {oldlab hits oldstarts oldends : Array Nat} {s t : RefineSt n} (h : Complete n first last oldlab hits oldstarts oldends s) (hl : t.lab = s.lab) (hs : t.cellstart = s.cellstart) (he : t.cellend = s.cellend) : Complete n first last oldlab hits oldstarts oldends t

theorem Hex.GraphIso.Nauty.Sparse.Index.Complete.constant {oldlab : Array Nat} {first last : Nat} {oldstarts oldends : Array Nat} {n : Nat} {hits : Array Nat} {value : Nat} {s : RefineSt n} (hw : «Sort».Window oldlab s.lab first (last + 1)) (hs : s.cellstart = oldstarts) (he : s.cellend = oldends) (hss : oldstarts.size = n) (hes : oldends.size = n) (hl : last < s.lab.size) (hf : first ≤ last) (hend : oldends[first]! = last) (hv : ∀ (q : Nat), first ≤ q → q ≤ last → oldstarts[oldlab[q]!]! = if first = last then n else first) (hk : ∀ (q : Nat), first ≤ q → q ≤ last → hits[s.lab[q]!]! = value) : Complete n first last oldlab hits oldstarts oldends s

A constant cell leaves its original endpoint and vertex indices valid, including the singleton sentinel. A within-cell permutation is harmless.

theorem Hex.GraphIso.Nauty.Sparse.Index.Complete.valid {n first last : Nat} {oldlab hits oldstarts oldends : Array Nat} {s : RefineSt n} {level : Nat} {before : Array Nat} (h : Complete n first last oldlab hits oldstarts oldends s) (hp : CountPartition level first last s.lab hits before s.ptn) (hc : IsCell before level first (last + 1 - first)) (hi : Valid n oldlab before level oldstarts oldends) : Valid n s.lab s.ptn level s.cellstart s.cellend

theorem Hex.GraphIso.Nauty.Sparse.Index.Complete.of_two {lab : Array Nat} {first last v2 w1 w2 cap : Nat} {starts : Array Nat} {n : Nat} {s : RefineSt n} (hm : Minima.Permuted s.lab lab s.hits first last v2 last last w1 w2 cap) (ht : Two n first v2 last last lab starts) (hf : Frame n first (last - 1) s.lab lab s.cellstart starts s.cellend s.cellend) (hv : v2 < last) (hb : last ≤ n) (he : s.cellend.size = n) : Complete n first (last - 1) s.lab s.hits s.cellstart s.cellend { lab := lab, ptn := s.ptn, active := s.active, queue := s.queue, cellstart := starts, cellend := (s.cellend.setIfInBounds first (v2 - 1)).setIfInBounds v2 (last - 1), indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp, numcells := s.numcells, longcode := s.longcode }

theorem Hex.GraphIso.Nauty.Sparse.Index.Complete.of_scatter {lab : Array Nat} {first last v2 w1 w2 cap : Nat} {starts : Array Nat} {n : Nat} {s : RefineSt n} (hm : Minima.Permuted s.lab lab s.hits first last v2 last last w1 w2 cap) (ht : Two n first v2 last (v2 + (last - v2)) lab starts) (hf : Frame n first s.cellend[first]! s.lab lab s.cellstart starts s.cellend s.cellend) (hlast : s.cellend[first]! + 1 = last) (hv : v2 < last) (hb : last ≤ n) (he : s.cellend.size = n) : «Sort».Window s.lab lab first last ∧ Runs n first s.cellend[first]! last lab s.hits starts ((s.cellend.setIfInBounds first (v2 - 1)).setIfInBounds v2 (last - 1)) ∧ Frame n first s.cellend[first]! s.lab lab s.cellstart starts s.cellend ((s.cellend.setIfInBounds first (v2 - 1)).setIfInBounds v2 (last - 1))

The completed second-fragment scatter establishes the return cache when there is no larger-count tail.

theorem Hex.GraphIso.Nauty.Sparse.Index.Tail.initial {lab : Array Nat} {first last v2 v3 w1 w2 cap : Nat} {starts : Array Nat} {n : Nat} {s : RefineSt n} (hm : Minima.Permuted s.lab lab s.hits first last v2 v3 last w1 w2 cap) (ht : Two n first v2 v3 v3 lab starts) (hf : Frame n first (last - 1) s.lab lab s.cellstart starts s.cellend s.cellend) (hv : v2 < v3) (hb : last ≤ n) (he : s.cellend.size = n) : Tail n first (last - 1) (v3 - 1) s.lab s.hits s.cellstart s.cellend { lab := «Sort».indirect lab s.hits v3 (last - v3), ptn := s.ptn, active := s.active, queue := s.queue, cellstart := starts, cellend := (s.cellend.setIfInBounds first (v2 - 1)).setIfInBounds v2 (v3 - 1), indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp, numcells := s.numcells, longcode := s.longcode }

Sorting the larger-count tail leaves the first two indexed runs intact and establishes the invariant for the executed tail scan.