theorem Hex.GraphIso.Nauty.Sparse.classify_internal_state {n : Nat} {g : Graph n} {level numcells : Nat} {st : State n} (h : (classify g level numcells st).fst = Generic.Leaf.internal) : classify g level numcells st = (Generic.Leaf.internal, st)

An internal native classifier leaves its input state unchanged.

theorem Hex.GraphIso.Nauty.Sparse.Ready.target_phase {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells : Nat} {st : State n} (h : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (hc : numcells < n) : have t := chooseTarget false (Graph.ofGraph G.graph) tcLevel level numcells st; t.snd.snd.snd.compCanon ≤ 0 ∨ (t.snd.fst.nextElem none).isSome = true

A positive canonical code comparison selects a nonempty native cell. Consequently the sweep executes a child before it can return settled codes.

theorem Hex.GraphIso.Nauty.Sparse.CodeEntry.recorded {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells : Nat} {st : State n} (h : CodeEntry G tcLevel level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (hc : (prepareOther (Graph.ofGraph G.graph) tcLevel level numcells st).fst < n) : have p := prepareOther (Graph.ofGraph G.graph) tcLevel level numcells st; CheapRecorded level p.snd.snd.fst.toNat p.snd.snd.snd.snd.snd ∧ RouteRecorded G.graph tcLevel level p.snd.snd.fst.toNat p.snd.snd.snd.snd.snd

Native off-path preparation records both the general guided target choice and the stronger saved-target condition used in cheap subtrees.