theorem Hex.GraphIso.Nauty.Sparse.Target.best_congr (keys : List Nat) (left right : Nat → Nat) (empty : Nat) (h : ∀ (a : Nat), a ∈ keys → left a = right a) : best keys left empty = best keys right empty

Equal scores on the candidate list give the same first maximum.

theorem Hex.GraphIso.Nauty.Sparse.bestcell_perm {n : Nat} (G : SparseGraph n) (lab out ptn : Array Nat) (level : Nat) (s t : Scratch) (hp : lab.toList.Perm (List.range n)) (hq : out.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hi : Index.Valid n lab ptn level s.cellstart s.cellend) (hj : Index.Valid n out ptn level t.cellstart t.cellend) (heq : Equitable (Graph.context G) level lab ptn) (hperm : cellsPerm ptn level lab out) : bestcell (Graph.ofGraph G) lab ptn level = bestcell (Graph.ofGraph G) out ptn level

The executed fresh best-cell selector is invariant under reordering inside equitable cells. Cache witnesses are supplied by the proved indexer.

theorem Hex.GraphIso.Nauty.Sparse.targetcell_perm {n : Nat} (G : SparseGraph n) (lab out ptn : Array Nat) (level tcLevel : Nat) (hint : Int) (s t : Scratch) (hp : lab.toList.Perm (List.range n)) (hq : out.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hi : Index.Valid n lab ptn level s.cellstart s.cellend) (hj : Index.Valid n out ptn level t.cellstart t.cellend) (heq : Equitable (Graph.context G) level lab ptn) (hperm : cellsPerm ptn level lab out) : targetcell (Graph.ofGraph G) lab ptn level tcLevel hint = targetcell (Graph.ofGraph G) out ptn level tcLevel hint

Valid hints, best-cell selection, and the depth cutoff all respect within-cell permutations of an equitable partition.

theorem Hex.GraphIso.Nauty.Sparse.maketargetcell_perm {n : Nat} (G : SparseGraph n) (lab out ptn : Array Nat) (level tcLevel : Nat) (hint : Int) (s t : Scratch) (hp : lab.toList.Perm (List.range n)) (hq : out.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hi : Index.Valid n lab ptn level s.cellstart s.cellend) (hj : Index.Valid n out ptn level t.cellstart t.cellend) (heq : Equitable (Graph.context G) level lab ptn) (hperm : cellsPerm ptn level lab out) (hc : bcount ptn level n < n) : maketargetcell (Graph.ofGraph G) lab ptn level tcLevel hint = maketargetcell (Graph.ofGraph G) out ptn level tcLevel hint

Target position, vertex set, and size are all invariant under within-cell permutations of an equitable nondiscrete partition.