theorem Hex.GraphIso.Nauty.Sparse.Rows.Prefix.relabel_zero {n : Nat} {G : SparseGraph n} {R : Rows n} {l c : Label n} {same : Nat} (h : R.Prefix (G.relabel c.perm) same) : R.Prefix (G.relabel l.perm) 0

A store with the graph's edge capacity is a valid empty prefix for every other labelling of the same graph. No rows are read.

theorem Hex.GraphIso.Nauty.Sparse.classify_prefix {n : Nat} (G : SparseGraph n) (level numcells : Nat) (st : State n) (l c : Label n) (hl : Label.ofArray? n st.lab = some l) (hc : Label.ofArray? n st.canonlab = some c) (h : st.canong.Prefix (G.relabel c.perm) st.samerows) : have r := classify (Graph.ofGraph G) level numcells st; r.snd.canong.Prefix (G.relabel c.perm) r.snd.samerows ∧ ∀ (sr : Nat), r.fst = Generic.Leaf.better sr → r.snd.canong.Prefix (G.relabel l.perm) sr

Native classification retains the incumbent's valid row prefix. A better verdict carries exactly the candidate prefix needed by installation, including the zero-prefix code-order branches and raw unsorted cached rows.