theorem
Hex.GraphIso.Nauty.Sparse.maketargetcell_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)
(hp : lab.toList.Perm (List.range n))
(hs : ptn.size = n)
(hend : ptn[n - 1]! ≤ level)
(hc : bcount ptn level n < n)
:
have a := maketargetcell (Graph.ofGraph G) lab ptn level tcLevel hint;
maketargetcell (Graph.ofGraph H) (Array.map (renamingOf p).toFun lab) ptn level tcLevel hint = (a.fst, VSet.image (renamingOf p).toFun a.snd.fst, a.snd.snd)
The full fresh target transports its vertex set and retains its position and size under graph relabelling. Valid index witnesses are constructed.
theorem
Hex.GraphIso.Nauty.Sparse.maketargetCached_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 : Scratch.Valid n lab ptn level s)
(hj : Scratch.Valid n (Array.map (renamingOf p).toFun lab) ptn level t)
(hc : bcount ptn level n < n)
:
have a := maketargetCached (Graph.ofGraph G) lab ptn level tcLevel hint s;
have b := maketargetCached (Graph.ofGraph H) (Array.map (renamingOf p).toFun lab) ptn level tcLevel hint t;
(b.fst, b.snd.fst, b.snd.snd.fst) = (a.fst, VSet.image (renamingOf p).toFun a.snd.fst, a.snd.snd.fst)
Admissible caches agree on all observable target fields after relabelling, including invalid-cache fallback, valid hints, and the depth cutoff.
theorem
Hex.GraphIso.Nauty.Sparse.maketargetCached_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 : Scratch.Valid n lab ptn level s)
(hj : Scratch.Valid n out ptn level t)
(heq : Equitable (Graph.context G) level lab ptn)
(hperm : cellsPerm ptn level lab out)
(hc : bcount ptn level n < n)
:
Cached targets are independent of the ordering within equitable cells; the cache's flag and scratch contents may differ between the two calls.