@[reducible, inline]

abbrev Hex.GraphIso.Nauty.Sparse.PathInv {n k : Nat} (G : Sparse.Colored n k) (level : Nat) (st : State n) : Prop

The current individualized vertices are singleton cells, and every root-colour stabilizer fixing them stabilizes the current partition.

Equations

• Hex.GraphIso.Nauty.Sparse.PathInv G level st = Hex.GraphIso.Nauty.PathInv G.toDense (Hex.GraphIso.Nauty.Sparse.Graph.context G.graph) level st.frame

theorem Hex.GraphIso.Nauty.Sparse.PathInv.fields {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st out : State n} (h : PathInv G level st) (hl : out.lab = st.lab) (hp : out.ptn = st.ptn) (hf : out.fixedpts = st.fixedpts) : PathInv G level out

theorem Hex.GraphIso.Nauty.Sparse.PathInv.visit {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : PathInv G level st) (hi : NodeInv G level numcells st) : PathInv G level (Sparse.visit (Graph.ofGraph G.graph) level numcells st).snd.snd

Refinement uses the native cached equivariance theorem for the path stabilizer, together with literal preservation of fixed singletons.

theorem Hex.GraphIso.Nauty.Sparse.PathInv.record {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st : State n} (h : PathInv G level st) (code : Nat) : PathInv G level (recordFirst level code st)

theorem Hex.GraphIso.Nauty.Sparse.PathInv.compare {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st : State n} (h : PathInv G level st) (code : Nat) : PathInv G level (compareCodes level code st)

theorem Hex.GraphIso.Nauty.Sparse.PathInv.target {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st : State n} (h : PathInv G level st) (first : Bool) (tcLevel numcells : Nat) : PathInv G level (chooseTarget first (Graph.ofGraph G.graph) tcLevel level numcells st).snd.snd.snd

theorem Hex.GraphIso.Nauty.Sparse.PathInv.classify {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st : State n} (h : PathInv G level st) (numcells : Nat) : PathInv G level (Sparse.classify (Graph.ofGraph G.graph) level numcells st).snd

theorem Hex.GraphIso.Nauty.Sparse.PathInv.terminal {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st : State n} (h : PathInv G level st) : PathInv G level (firstterminal level st)

theorem Hex.GraphIso.Nauty.Sparse.PathInv.leaf {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st : State n} (h : PathInv G level st) (leaf : Leaf) : PathInv G level (leafExit leaf level st).snd

theorem Hex.GraphIso.Nauty.Sparse.PathInv.cheap {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st : State n} (h : PathInv G level st) (first : Bool) : PathInv G level (cheapCheck first level st)

theorem Hex.GraphIso.Nauty.Sparse.PathInv.child {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : PathInv G level st) (hn : 0 < n) (hl : 1 ≤ level) (hr : Ready G level numcells st) (first : Bool) {tc tv : Nat} {cell : VSet n} (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) : PathInv G (level + 1) (Generic.Policy.child first level tc tv st)

Individualization supplies path stabilization for automorphisms fixing the selected vertex, without changing the sparse child operation.

theorem Hex.GraphIso.Nauty.Sparse.PathInv.recover {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st out : State n} (h : PathInv G level st) (hn : 0 < n) (hl : 1 ≤ level) (hr : Ready G level numcells st) (hx : FrameOut G level level st out) (he : out.fixedpts = st.fixedpts) : PathInv G level (Generic.Policy.recover (n + 2) level out)

Parent recovery transports the path stabilizer along the actual frame and the exactly restored fixed-point set.

theorem Hex.GraphIso.Nauty.Sparse.PathInv.child_return {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : PathInv G level st) (hn : 0 < n) (hl : 1 ≤ level) (hr : Ready G level numcells st) (first descendFirst : Bool) (tcLevel fuel tc tv : Nat) (cell : VSet n) (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) : have child := Generic.Policy.child first level tc tv st; have out := (Generic.node descendFirst (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1) child).snd; PathInv G level (Generic.Policy.recover (n + 2) level (Generic.Policy.leaveChild tv out))

A complete native child call, including first descent or a nonlocal exit, restores the parent's path invariant when its receiving frame is recovered.

theorem Hex.GraphIso.Nauty.Sparse.initial_pathInv {n k : Nat} (G : Sparse.Colored n k) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; PathInv G 1 (initial (Graph.ofGraph G.graph) p.fst p.snd)

Stable colour initialization has no fixed vertices and is its own root stabilization frame. This statement also includes the empty graph.