theorem
Hex.GraphIso.Nauty.Sparse.CodePath.codes_lt
{n : Nat}
{G : SparseGraph n}
{base last : Nat}
{root leaf : RefineSt n}
{path : List (Nat × Nat)}
{codes : List Nat}
(h : CodePath G base root path last leaf codes)
(hr : root.longcode < codeSentinel)
(c : Nat)
:
c ∈ codes → c < codeSentinel
Every code recorded by a native descent is a real refinement code, strictly below the sentinel later written by leaf installation.