theorem
Hex.GraphIso.Nauty.Sparse.Target.count_map
{n a first : Nat}
(G H : SparseGraph n)
(p : Perm n)
(hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v)
(lab ptn : Array Nat)
(level : Nat)
(s t : Scratch)
(hp : lab.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 (Array.map (renamingOf p).toFun lab) ptn level t.cellstart t.cellend)
(ha : a ∈ nontrivial (cells ptn level n))
(hf : first < n)
:
List.count a (row (Graph.ofGraph H) (Array.map (renamingOf p).toFun lab) t first) = List.count a (row (Graph.ofGraph G) lab s first)
A graph isomorphism preserves native target-row counts after transporting the labelling and its valid cell index.
theorem
Hex.GraphIso.Nauty.Sparse.Target.score_map
{n first : Nat}
(G H : SparseGraph n)
(p : Perm n)
(hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v)
(lab ptn : Array Nat)
(level : Nat)
(s t : Scratch)
(hp : lab.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 (Array.map (renamingOf p).toFun lab) ptn level t.cellstart t.cellend)
(hf : first ∈ nontrivial (cells ptn level n))
:
score (Graph.ofGraph H) (Array.map (renamingOf p).toFun lab) t (nontrivial (cells ptn level n)) first = score (Graph.ofGraph G) lab s (nontrivial (cells ptn level n)) first
Partial-join scores commute with relabelling, independently of native neighbour order and admissible scratch contents.
theorem
Hex.GraphIso.Nauty.Sparse.bestcell_map
{n : Nat}
(G H : SparseGraph n)
(p : Perm n)
(hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v)
(lab ptn : Array Nat)
(level : Nat)
(s t : Scratch)
(hp : lab.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 (Array.map (renamingOf p).toFun lab) ptn level t.cellstart t.cellend)
:
bestcell (Graph.ofGraph H) (Array.map (renamingOf p).toFun lab) ptn level = bestcell (Graph.ofGraph G) lab ptn level
Sparse best-cell selection commutes with the transported graph and labelling, retaining its native first-maximum tie rule.
theorem
Hex.GraphIso.Nauty.Sparse.targetcell_map
{n : Nat}
(G H : SparseGraph n)
(p : Perm n)
(hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v)
(lab ptn : Array Nat)
(level tcLevel : Nat)
(hint : Int)
(s t : Scratch)
(hp : lab.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 (Array.map (renamingOf p).toFun lab) ptn level t.cellstart t.cellend)
:
targetcell (Graph.ofGraph H) (Array.map (renamingOf p).toFun lab) ptn level tcLevel hint = targetcell (Graph.ofGraph G) lab ptn level tcLevel hint
All sparse target-dispatch arms commute with relabelling.