theorem Hex.GraphIso.Nauty.Sparse.Target.score_perm {n first : 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) (hf : first ∈ nontrivial (cells ptn level n)) : score (Graph.ofGraph G) lab s (nontrivial (cells ptn level n)) first = score (Graph.ofGraph G) out t (nontrivial (cells ptn level n)) first

In an equitable partition the partial-join score is unchanged by reordering vertices inside cells, even when the representative changes.