theorem Hex.GraphIso.Nauty.Sparse.bestcellCached_eq {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) : (bestcellCached (Graph.ofGraph G) lab s).fst = bestcell (Graph.ofGraph G) lab ptn level

Fresh and cached sparse best-cell selection agree for any admissible cache, including arbitrary initial count values and empty partitions.

theorem Hex.GraphIso.Nauty.Sparse.Target.open_of_mem {ptn : Array Nat} {n level a : Nat} (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (ha : a ∈ nontrivial (cells ptn level n)) : ptn[a]! > level ∧ (a = 0 ∨ ptn[a - 1]! ≤ level)

theorem Hex.GraphIso.Nauty.Sparse.Target.mem_of_open {ptn : Array Nat} {n level a : Nat} (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (ha : a < n) (ho : ptn[a]! > level) (hb : a = 0 ∨ ptn[a - 1]! ≤ level) : a ∈ nontrivial (cells ptn level n)

theorem Hex.GraphIso.Nauty.Sparse.Target.first_mem {ptn : Array Nat} {n level : Nat} (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hne : nontrivial (cells ptn level n) ≠ []) : (List.find? (fun (i : Nat) => decide (ptn[i]! > level)) (List.range n)).getD 0 ∈ nontrivial (cells ptn level n)

The first open position is the start of the first nontrivial cell.