theorem Hex.GraphIso.Nauty.Sparse.chooseTarget_unhinted {n : Nat} {g : Graph n} {tcLevel level numcells : Nat} {st : State n} (first : Bool) (hc : numcells < n) (hh : first = true ∨ 0 ≤ st.compCanon) : (chooseTarget first g tcLevel level numcells st).fst.toNat = (maketargetCached g st.lab st.ptn level tcLevel (-1) st.canong.scratch).fst

The native first path and nonnegative canonical comparisons use the literal unhinted cached target.

def Hex.GraphIso.Nauty.Sparse.Max.Frame.Choice {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) (tc : Nat) (best : Option (Key n)) : Prop

An actual target is the original unhinted target or its entire code prefix is dominated. The latter also bounds descendants of a hinted target.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Choice.grow {n : Nat} {G : SparseGraph n} {tcLevel tc : Nat} {f : Frame n} {before after : Option (Key n)} (h : Choice G tcLevel f tc before) (hg : Grows before after) : Choice G tcLevel f tc after

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.first_target {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {f : Frame n} (hc : (visit (Graph.ofGraph G) f.level f.numcells f.entry).fst < n) : (Generic.prepareFirst (Graph.ofGraph G) tcLevel f.level f.numcells f.entry).snd.fst.toNat = (target G tcLevel f).tc

First-path preparation records the unhinted target before the actual cheap check and child selection.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.choice {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {bs fs : List Nat} (h : Valid G f) (hc : Comparison G.graph f.codes bs fs f.entry) (hi : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n) : have p := prepareOther (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry; Choice G.graph tcLevel f p.snd.snd.fst.toNat (State.key G.graph bs p.snd.snd.snd.snd.snd)

The actual off-path preparation establishes the choice alternative from its executed code comparison. No assumption about a hinted subtree's maximum is needed.