theorem Hex.GraphIso.Nauty.Sparse.bestcell_spec {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) : bestcell (Graph.ofGraph G) lab ptn level = Target.best (Target.nontrivial (cells ptn level n)) (Target.score (Graph.ofGraph G) lab s (Target.nontrivial (cells ptn level n))) n

The fresh selector's compact indices compute the same native score fold as the cached selector, including the first maximum tie rule.