theorem Hex.GraphIso.Nauty.Sparse.Ready.cached_cell {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (hc : numcells < n) (tcLevel : Nat) (hint : Int) : have t := maketargetCached (Graph.ofGraph G.graph) st.lab st.ptn level tcLevel hint st.canong.scratch; IsCell st.ptn level t.fst t.snd.snd.fst ∧ 1 < t.snd.snd.fst ∧ t.fst + t.snd.snd.fst ≤ n

Native cached target coordinates delimit a complete nonsingleton cell.

def Hex.GraphIso.Nauty.Sparse.Max.Frame.target {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) : Cell n

The complete unhinted target computed from the frozen entry's actual cached visit, before mutable target filtering or sibling reordering.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.target {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} (h : Valid G f) (hc : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n) : Cell.Valid G (Frame.target G.graph tcLevel f)

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.target_cover {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {best : Option (Key n)} (h : Valid G f) (hc : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n) : Covers (key G.graph tcLevel f) best ↔ ∀ (v : Nat), (Frame.target G.graph tcLevel f).vertices.mem v = true → Covers (Cell.key G.graph tcLevel (Frame.target G.graph tcLevel f) v) best

Frozen node coverage is precisely coverage of its complete actual cached target's vertex keys. Both sides include every ancestor code.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.small_key {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {v : Nat} (h : Valid G f) (hc : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n) (hshape : NodeShape n f.level (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).snd.snd.ptn) (hv : (Frame.target G.graph tcLevel f).vertices.mem v = true) : key G.graph tcLevel f = Cell.key G.graph tcLevel (Frame.target G.graph tcLevel f) v

With the cheap shape, any complete native target child attains the whole frozen node maximum. This supplies the coverage step needed when a return skips the remaining children of a cheap ancestor.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.cheap_child {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {st : State n} {v : Nat} (h : Valid G f) (hc : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n) (hguard : cheapautom (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).snd.snd.ptn f.level n = true) (he : FrameOut G f.level f.level (Frame.target G.graph tcLevel f).entry st) (hs : Ready G f.level (Frame.target G.graph tcLevel f).numcells st) (hv : (Frame.target G.graph tcLevel f).vertices.mem v = true) (first : Bool) : key G.graph tcLevel f = key G.graph tcLevel ((Frame.target G.graph tcLevel f).child first st v)

A passing native cheap guard makes an actual individualized child attain its parent's whole key, including after sibling reordering.