theorem
Hex.GraphIso.Nauty.Sparse.targetcell_mem
{n : Nat}
(G : SparseGraph n)
(lab ptn : Array Nat)
(level tcLevel : Nat)
(hint : Int)
(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)
(hne : Target.nontrivial (cells ptn level n) ≠ [])
:
Every dispatch arm selects a nontrivial cell: valid hints, the shallow partial-join maximum, and the first open position at greater depth.
theorem
Hex.GraphIso.Nauty.Sparse.maketargetCached_eq
{n : Nat}
(G : SparseGraph n)
(lab ptn : Array Nat)
(level tcLevel : Nat)
(hint : Int)
(s : Scratch)
(l : Label n)
(hl : Label.ofArray? n lab = some l)
(hptn : ptn.size = n)
(hend : ptn[n - 1]! ≤ level)
(hs : Scratch.Valid n lab ptn level s)
(hne : Target.nontrivial (cells ptn level n) ≠ [])
:
have out := maketargetCached (Graph.ofGraph G) lab ptn level tcLevel hint s;
(out.fst, out.snd.fst, out.snd.snd.fst) = maketargetcell (Graph.ofGraph G) lab ptn level tcLevel hint
Cached dispatch has exactly the fresh target position, vertex set, and size, including hints and both sides of the configured depth cutoff.