theorem Hex.GraphIso.Nauty.Sparse.Index.Valid.agree {lab ptn starts ends starts' ends' : Array Nat} {n level : Nat} (h : Valid n lab ptn level starts ends) (h' : Valid n lab ptn level starts' ends') (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (l : Label n) (hl : Label.ofArray? n lab = some l) : starts = starts' ∧ ∀ (a : Nat), a < n → a = 0 ∨ ptn[a - 1]! ≤ level → ends[a]! = ends'[a]!

Two admissible caches agree on every vertex index and every cell endpoint that the executable reads. Unused endpoint entries may differ.

theorem Hex.GraphIso.Nauty.Sparse.bestcellCached_max {n : Nat} (G : SparseGraph n) (lab ptn : Array Nat) (level : Nat) (s : Scratch) (l : Label n) (hl : Label.ofArray? n lab = some l) (hptn : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hidx : Index.Valid n lab ptn level s.cellstart s.cellend) (hsize : s.hits.size = n) (hne : Target.nontrivial (cells ptn level n) ≠ []) : Target.FirstMax (Target.score (Graph.ofGraph G) lab s (Target.nontrivial (cells ptn level n))) (Target.nontrivial (cells ptn level n)) (bestcellCached (Graph.ofGraph G) lab s).fst

The executed cached selector returns the first maximal partial-join cell.

theorem Hex.GraphIso.Nauty.Sparse.bestcellCached_congr {n : Nat} (G : SparseGraph n) (lab ptn : Array Nat) (level : Nat) (s t : Scratch) (l : Label n) (hl : Label.ofArray? n lab = some l) (hptn : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hs : Index.Valid n lab ptn level s.cellstart s.cellend) (hss : s.hits.size = n) (ht : Index.Valid n lab ptn level t.cellstart t.cellend) (hts : t.hits.size = n) : (bestcellCached (Graph.ofGraph G) lab s).fst = (bestcellCached (Graph.ofGraph G) lab t).fst

Initial hit values and unused cache entries do not affect the selected cell. Both admissible caches compute the same complete join-score sequence.