theorem
Hex.GraphIso.Nauty.Sparse.RefineSt.Ready.child_singleton
{n : Nat}
{G : SparseGraph n}
{level a : Nat}
{s : RefineSt n}
(h : Ready G level s)
{tc len o : Nat}
(hc : IsCell s.ptn level tc len)
(hb : tc + len ≤ n)
(hn : 1 < len)
(ho : o < len)
(scratch : Scratch)
(hs : Scratch.Bounded n scratch)
(ha : IsCell s.ptn level a 1)
:
A literal native child keeps every older singleton and its vertex.
theorem
Hex.GraphIso.Nauty.Sparse.RefineSt.Ready.child_picked
{n : Nat}
{G : SparseGraph n}
{level : Nat}
{s : RefineSt n}
(h : Ready G level s)
{tc len o : Nat}
(hc : IsCell s.ptn level tc len)
(hb : tc + len ≤ n)
(hn : 1 < len)
(ho : o < len)
(scratch : Scratch)
(hs : Scratch.Bounded n scratch)
:
Individualization creates a singleton holding the chosen vertex; the actual cached refinement retains it at the target position.
theorem
Hex.GraphIso.Nauty.Sparse.DescPath.singleton
{n : Nat}
{G : SparseGraph n}
{base last a : Nat}
{root leaf : RefineSt n}
{path : List (Nat × Nat)}
(h : DescPath G base root path last leaf)
(hr : RefineSt.Ready G base root)
(ha : IsCell root.ptn base a 1)
:
Every native descent keeps its entry singletons at their literal positions, despite cached refinement and later individualizations.
theorem
Hex.GraphIso.Nauty.Sparse.DescPath.picked
{n : Nat}
{G : SparseGraph n}
{base last tc o : Nat}
{root leaf : RefineSt n}
{path : List (Nat × Nat)}
(h : DescPath G base root ((tc, o) :: path) last leaf)
(hr : RefineSt.Ready G base root)
:
A terminal native labelling records the first chosen vertex at its target position.