theorem Hex.GraphIso.Nauty.Sparse.maketargetcell_window {n : Nat} (g : Graph n) (lab ptn : Array Nat) (level tcLevel : Nat) (hint : Int) : have t := maketargetcell g lab ptn level tcLevel hint; t.snd.fst = windowSet n lab t.fst t.snd.snd

The native target bitset is exactly its length-indexed label window.

theorem Hex.GraphIso.Nauty.Sparse.Ready.target_window {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; t.snd.fst = windowSet n st.lab t.fst t.snd.snd.fst

A cached target's fields denote the current label window; this uses cache validity to identify all three fields with fresh native dispatch.

theorem Hex.GraphIso.Nauty.Sparse.NodeInv.visit_vertex {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells v : Nat} {st : State n} (h : NodeInv G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) : have r := visit (Graph.ofGraph G.graph) level numcells st; have f := refine (Graph.ofGraph G.graph) level st.lab st.ptn st.active numcells; have t := maketargetcell (Graph.ofGraph G.graph) f.lab f.ptn level tcLevel (-1); r.fst < n → n < fuel + (r.fst + 1) → t.snd.fst.mem v = true → vertexKey G.graph tcLevel fuel level f.lab f.ptn t.fst f.numcells v = vertexKey G.graph tcLevel fuel level r.snd.snd.lab r.snd.snd.ptn t.fst r.fst v

Each complete child maximum is unchanged when the specification's fresh visit is replaced by the actual cached visit.

theorem Hex.GraphIso.Nauty.Sparse.NodeInv.visit_bound {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells : Nat} {st : State n} {bound : Key n} (h : NodeInv G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (hf : n < fuel + 1 + numcells) : have r := visit (Graph.ofGraph G.graph) level numcells st; have t := maketargetCached (Graph.ofGraph G.graph) r.snd.snd.lab r.snd.snd.ptn level tcLevel (-1) r.snd.snd.canong.scratch; r.fst < n → ((subtreeKey G.graph tcLevel (fuel + 1) level st.lab st.ptn st.active numcells).Le bound ↔ ∀ (v : Nat), t.snd.fst.mem v = true → (prefixKey [r.snd.fst] (vertexKey G.graph tcLevel fuel level r.snd.snd.lab r.snd.snd.ptn t.fst r.fst v)).Le bound)

An internal node is bounded exactly when all children of its actual cached target are bounded. The keys use the actual visit's code, labels and count; sufficient fuel prevents either enumeration from being truncated.

theorem Hex.GraphIso.Nauty.Sparse.NodeInv.visit_attains {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells : Nat} {st : State n} (h : NodeInv G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (hf : n < fuel + 1 + numcells) : have r := visit (Graph.ofGraph G.graph) level numcells st; have t := maketargetCached (Graph.ofGraph G.graph) r.snd.snd.lab r.snd.snd.ptn level tcLevel (-1) r.snd.snd.canong.scratch; r.fst < n → ∃ (v : Nat), t.snd.fst.mem v = true ∧ prefixKey [r.snd.fst] (vertexKey G.graph tcLevel fuel level r.snd.snd.lab r.snd.snd.ptn t.fst r.fst v) = subtreeKey G.graph tcLevel (fuel + 1) level st.lab st.ptn st.active numcells

Some vertex of the actual cached target attains the complete node maximum, with the actual visit's code prefixed to its child maximum.

theorem Hex.GraphIso.Nauty.Sparse.NodeInv.visit_leaf {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells : Nat} {st : State n} {label : Label n} (h : NodeInv G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) : have r := visit (Graph.ofGraph G.graph) level numcells st; r.fst = n → Label.ofArray? n r.snd.snd.lab = some label → subtreeKey G.graph tcLevel (fuel + 1) level st.lab st.ptn st.active numcells = { codes := [r.snd.fst, codeSentinel], graph := G.graph.relabel label.perm }

A discrete actual visit attains exactly the specification's node key, using the literal parsed label and emitted terminal code.