theorem Hex.GraphIso.Nauty.Sparse.codes_compare (xs ys : List Nat) : listCmp compare xs ys = compare xs ys

The shared code machine and the native sparse key use the same lexicographic order on refinement codes.

theorem Hex.GraphIso.Nauty.Sparse.codes_less {n : Nat} {cs bs : List Nat} {st : State n} (h : CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon (-1)) (ext : List Nat) (A B : SparseGraph n) : { codes := cs ++ ext, graph := A }.cmp { codes := bs ++ [codeSentinel], graph := B } = Ordering.lt

A frozen code rejection dominates every continuation, independently of the native sparse rows below it.

theorem Hex.GraphIso.Nauty.Sparse.codes_greater {n : Nat} {cs bs : List Nat} {st : State n} (h : CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon 1) (ext : List Nat) (A B : SparseGraph n) : { codes := cs ++ ext, graph := A }.cmp { codes := bs ++ [codeSentinel], graph := B } = Ordering.gt

A frozen positive comparison dominates the incumbent before any sparse adjacency row is read.

theorem Hex.GraphIso.Nauty.Sparse.codes_short {n : Nat} {cs bs : List Nat} {st : State n} (h : CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon 0) (hlen : cs.length < bs.length) (A B : SparseGraph n) : { codes := cs ++ [codeSentinel], graph := A }.cmp { codes := bs ++ [codeSentinel], graph := B } = Ordering.gt

At a shorter tied leaf, the sentinel wins against the next real incumbent code. This uses only the shared code-order theorem.

theorem Hex.GraphIso.Nauty.Sparse.codes_tied {n : Nat} {cs bs : List Nat} {st : State n} (h : CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon 0) (hlen : cs.length = bs.length) (A B : SparseGraph n) : { codes := cs ++ [codeSentinel], graph := A }.cmp { codes := bs ++ [codeSentinel], graph := B } = graphCmp A B

Equal complete code sequences hand the verdict to sparse row order.

theorem Hex.GraphIso.Nauty.Sparse.Key.max_eq_left {n : Nat} {a b : Key n} (h : b.Le a) : a.max b = a

theorem Hex.GraphIso.Nauty.Sparse.Key.max_eq_right {n : Nat} {a b : Key n} (h : b.cmp a = Ordering.gt) : a.max b = b