theorem
Hex.GraphIso.Nauty.Sparse.CodePath.code_prefix
{n : Nat}
{G : SparseGraph n}
{base last level : Nat}
{root leaf current : RefineSt n}
{path xs : List (Nat × Nat)}
{codes : List Nat}
(h : CodePath G base root path last leaf codes)
(hr : RefineSt.Ready G base root)
(hshape : NodeShape n base root.ptn)
(hp : DescPath G base root xs level current)
(hprefix : List.map Prod.fst xs <+: List.map Prod.fst path)
:
Below a cheap-shaped node, following a prefix of a saved descent's targets gives its exact refinement code at the reached depth. Offsets, native row orders and bounded scratch contents may differ.
theorem
Hex.GraphIso.Nauty.Sparse.FirstRef.code
{n : Nat}
{G : SparseGraph n}
{tcLevel base level : Nat}
{root current : RefineSt n}
{st : State n}
{xs : List (Nat × Nat)}
(h : FirstRef G tcLevel base root st)
(hdepth : level ≤ h.last)
(hr : RefineSt.Ready G base root)
(hshape : NodeShape n base root.ptn)
(hp : DescPath G base root xs level current)
(ht : Targets st.firsttc base (List.map Prod.fst xs))
:
The exact code reached along stored targets below a cheap ancestor is the code the native first descent wrote at that depth.