def Hex.GraphIso.Nauty.Sparse.State.best {n : Nat} (G : SparseGraph n) (st : State n) : Option (Key n)

Read an installed native incumbent from its stable code array and checked label. This semantic observation does not expand sparse rows.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.Sparse.State.key {n : Nat} (G : SparseGraph n) (bs : List Nat) (st : State n) : Option (Key n)

During code overwriting, the semantic incumbent retains its complete saved code sequence. Its graph is still the actual saved native label.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.best_eq_key {n : Nat} {G : SparseGraph n} {cs bs : List Nat} {st : State n} {comparison : Int} (h : CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon comparison) (hne : comparison ≠ 1) : State.best G st = State.key G bs st

A stable canonical code array reads exactly the semantic sparse key.

theorem Hex.GraphIso.Nauty.Sparse.settled_read {n : Nat} {G : SparseGraph n} {cs bs : List Nat} {st : State n} (h : Settled cs bs st) : State.best G st = State.key G bs st

Either settled leaf verdict exposes the same native incumbent.

theorem Hex.GraphIso.Nauty.Sparse.firstterminal_best {n : Nat} {G : SparseGraph n} {cs : List Nat} {st : State n} {l : Label n} (h : Codes cs cs (firstterminal cs.length st)) (hne : cs ≠ []) (hl : Label.ofArray? n st.lab = some l) : State.best G (firstterminal cs.length st) = some { codes := cs ++ [codeSentinel], graph := G.relabel l.perm }

Installing the first leaf exposes precisely its executed code chain and sparse relabelling, once the code machine has been initialized.