@[reducible, inline]

abbrev Hex.GraphIso.Nauty.PathInv {n k : Nat} (G : Colored n k) (ctx : Ctx n) (level : Nat) (st : Search n) : Prop

The individualized path consists of singleton cells and transports root-stabilizing automorphisms to the current partition.

Equations

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

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

Bookkeeping that preserves the partition and fixed vertices preserves the path.

theorem Hex.GraphIso.Nauty.PathInv.visit {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st : Search n} (h : PathInv G ctx level st) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hgsz : ctx.g.size = n) (hok : SearchOk G level numcells st) (hstarts : ∀ (v : Nat), st.active.mem v = true → v = 0 ∨ st.ptn[v - 1]! ≤ level) : PathInv G ctx level (Nauty.visit ctx level numcells st).snd.snd

Refinement transports the path when its active positions are cell starts.

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

Code comparison preserves the current path.

theorem Hex.GraphIso.Nauty.PathInv.target {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level : Nat} {st : Search n} (h : PathInv G ctx level st) (first : Bool) (tcLevel numcells : Nat) : PathInv G ctx level (chooseTarget first ctx tcLevel level numcells st).snd.snd.snd

Target selection changes neither the path nor the partition.

theorem Hex.GraphIso.Nauty.PathInv.classify {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level : Nat} {st : Search n} (h : PathInv G ctx level st) (numcells : Nat) : PathInv G ctx level (Nauty.classify ctx level numcells st).snd

Classification leaves the individualized path unchanged.

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

Admissions and incumbent installation preserve the current path.

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

The cheap guard changes only its recorded boundary.

theorem Hex.GraphIso.Nauty.PathInv.child {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells tc tv : Nat} {st : Search n} {cell : VSet n} (h : PathInv G ctx level st) (first : Bool) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (htarget : Generic.Target (fun (st : Search n) => st) level tc cell st) (htv : cell.mem tv = true) : PathInv G ctx (level + 1) (Nauty.child first level tc tv st)

Individualizing a target vertex extends the partition-stabilization condition to automorphisms fixing that vertex.

theorem Hex.GraphIso.Nauty.child_starts {n level tc tv : Nat} {st : Search n} {cell : VSet n} (first : Bool) (htarget : Generic.Target (fun (st : Search n) => st) level tc cell st) (htv : cell.mem tv = true) : have out := child first level tc tv st; ∀ (v : Nat), out.active.mem v = true → v = 0 ∨ out.ptn[v - 1]! ≤ level + 1

A child's singleton active set names a cell start in its new partition.

theorem Hex.GraphIso.Nauty.PathInv.recover {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st out : Search n} (h : PathInv G ctx level st) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (hout : SearchOut G level level st out) (hf : out.fixedpts = st.fixedpts) : PathInv G ctx level (Nauty.recover (n + 2) level out)

A recovered parent keeps its path once cleanup restores its fixed set.

theorem Hex.GraphIso.Nauty.PathInv.pairs {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level : Nat} {st : Search n} (h : PathInv G ctx level st) (hp : PairsOk G ctx st) : LocalAutos ctx level st

The path and root ledger give precisely the conditional pair ledger read by long and short pruning at the current partition.

theorem Hex.GraphIso.Nauty.initial_pathInv {n k : Nat} (G : Colored n k) (ctx : Ctx n) : PathInv G ctx 1 (initial n (initialPartition G).fst (initialPartition G).snd)

The initial partition is its own stabilization frame and has no fixed vertices.