theorem
Hex.GraphIso.Nauty.Sparse.firstPath_rows
{n : Nat}
{g : Graph n}
{tcLevel fuel level numcells last : Nat}
{st leaf : State n}
(path : Generic.FirstPath g tcLevel fuel level numcells st last leaf)
:
Before the first leaf, the actual first descent retains the literal canonical row allocation while refinement continues to reuse its scratch.
theorem
Hex.GraphIso.Nauty.Sparse.blank_prefix
{n : Nat}
(G : SparseGraph n)
(l : Label n)
:
(Graph.ofGraph G).blank.Prefix (G.relabel l.perm) 0
The native initial allocation is a valid empty prefix for every label of its input graph. Its capacity equals the graph's directed edge count.
theorem
Hex.GraphIso.Nauty.Sparse.firstterminal_store
{n : Nat}
(G : SparseGraph n)
(level : Nat)
(st : State n)
(l : Label n)
(hl : Label.ofArray? n st.lab = some l)
(hb : st.canong.toRows = (Graph.ofGraph G).blank)
:
Store G (firstterminal level st)
The first terminal installs its checked current label with an empty prefix in the retained initial allocation.
theorem
Hex.GraphIso.Nauty.Sparse.firstPath_store
{n k : Nat}
{G : Sparse.Colored n k}
(hn : 0 < n)
{tcLevel fuel level numcells last : Nat}
{st leaf : State n}
(path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel level numcells st last leaf)
(hl : 1 ≤ level)
(h : NodeInv G level numcells st)
(hb : st.canong.toRows = (Graph.ofGraph G.graph).blank)
:
Store G.graph (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd
The first descent initializes the native store at its first leaf; the already-proved recursive store contract covers every later sibling.