theorem
Hex.GraphIso.Nauty.Sparse.Index.Valid.starts_map
{n : Nat}
{lab ptn : Array Nat}
{level : Nat}
{starts ends out other final : Array Nat}
{v : Nat}
(σ : Renaming n)
(hs : Valid n lab ptn level starts ends)
(ht : Valid n out ptn level other final)
(hp : lab.toList.Perm (List.range n))
(hsize : ptn.size = n)
(hend : ptn[n - 1]! ≤ level)
(hcell : cellsPerm ptn level out (Array.map σ.toFun lab))
(hv : v < n)
:
Admissible vertex-to-cell caches commute with vertex renaming and within-cell permutation, including the singleton sentinel.
theorem
Hex.GraphIso.Nauty.Sparse.Index.Valid.ends_congr
{n : Nat}
{lab ptn : Array Nat}
{level : Nat}
{starts ends out other final : Array Nat}
{a len : Nat}
(hs : Valid n lab ptn level starts ends)
(ht : Valid n out ptn level other final)
(hc : IsCell ptn level a len)
(hb : a + len ≤ n)
:
At cell starts, any two valid endpoint caches agree literally. Values at other positions need not agree.