structure Hex.GraphIso.Nauty.CanonOut {n : Nat} (level : Nat) (st out : Search n) : Prop

A retained reference cannot acquire a deeper ancestor. An installed reference belongs to the current partition and cannot return above it. Recovery may lower either ancestor only as far as the current level.

• floor : min level st.gcaCanon ≤ out.gcaCanon
• source : out.gcaCanon ≤ st.gcaCanon ∧ out.canonlab = st.canonlab ∨ level ≤ out.gcaCanon ∧ out.canonlab.size = st.lab.size ∧ cellsPerm st.ptn level st.lab out.canonlab

theorem Hex.GraphIso.Nauty.CanonOut.refl {n : Nat} (level : Nat) (st : Search n) : CanonOut level st st

Retaining the canonical reference is a reflexive effect.

theorem Hex.GraphIso.Nauty.CanonOut.fields {n level : Nat} {st out result : Search n} (h : CanonOut level st out) (hc : result.canonlab = out.canonlab) (hg : result.gcaCanon = out.gcaCanon) : CanonOut level st result

Bookkeeping that retains the reference and ancestor preserves its effect.

theorem Hex.GraphIso.Nauty.CanonOut.trans {n k : Nat} {G : Colored n k} {level : Nat} {st mid out : Search n} (h : CanonOut level st mid) (hnext : CanonOut level mid out) (he : SearchOut G level level st mid) : CanonOut level st out

Canonical effects compose using the partition effect of the first call.

theorem Hex.GraphIso.Nauty.CanonOut.lift {n level next : Nat} {st mid out : Search n} (h : CanonOut next mid out) (hlevel : level ≤ next) (hc : mid.canonlab = st.canonlab) (hg : mid.gcaCanon = st.gcaCanon) (hs : mid.lab.size = st.lab.size) (hp : cellsPerm st.ptn level st.lab mid.lab) (hlift : ∀ (lab : Array Nat), lab.size = mid.lab.size → cellsPerm mid.ptn next mid.lab lab → cellsPerm st.ptn level mid.lab lab) : CanonOut level st out

Transport a reference through a finer partition while retaining its ancestor bounds and the alternative of an unchanged reference.

theorem Hex.GraphIso.Nauty.CanonOut.within {n level : Nat} {st out : Search n} (h : CanonOut level st out) (hg : st.gcaCanon < out.gcaCanon) : out.canonlab.size = st.lab.size ∧ cellsPerm st.ptn level st.lab out.canonlab

An ancestor deeper than the incoming one binds the reference to this call.

theorem Hex.GraphIso.Nauty.CanonOut.old {n level : Nat} {st out : Search n} (h : CanonOut level st out) (hg : out.gcaCanon < level) : out.gcaCanon = st.gcaCanon ∧ out.canonlab = st.canonlab

A reference pointing above the call retains its incoming labelling and ancestor, even when that labelling is also reachable in this subtree.

theorem Hex.GraphIso.Nauty.CanonOut.visit {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st out : Search n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (h : CanonOut level (Nauty.visit ctx level numcells st).snd.snd out) : CanonOut level st out

Refinement transports a canonical effect to the node's entry partition.

theorem Hex.GraphIso.Nauty.child_store {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells tc tv : Nat} {st : Search n} {lab : Array Nat} {cell : VSet n} (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) (hsaved : lab.size = (child first level tc tv st).lab.size ∧ cellsPerm (child first level tc tv st).ptn (level + 1) (child first level tc tv st).lab lab) : lab.size = st.lab.size ∧ cellsPerm st.ptn level st.lab lab ∧ lab[tc]! = tv

A reference stored within the child retains the chosen vertex at the target position and lies within the parent's cells.

theorem Hex.GraphIso.Nauty.CanonOut.child {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells tc tv : Nat} {st out : Search n} {cell : VSet n} (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) (h : CanonOut (level + 1) (Nauty.child first level tc tv st) out) : CanonOut level st out

A child's newly installed reference lies within its parent's cells.

theorem Hex.GraphIso.Nauty.canon_leaf {n : Nat} (leaf : Leaf) (level : Nat) (st : Search n) : CanonOut level st (leafExit leaf level st).snd

Leaf installation is the only leaf action that raises the canonical ancestor.

theorem Hex.GraphIso.Nauty.CanonOut.recover {n level : Nat} {st out : Search n} (h : CanonOut level st out) (inf : Nat) : CanonOut level st (Nauty.recover inf level out)

Recovery lowers the canonical ancestor and keeps its stored labelling.

theorem Hex.GraphIso.Nauty.CanonOut.afterSweep {n level : Nat} {st out : Search n} (h : CanonOut level st out) (first : Bool) (size index : Nat) : CanonOut level st (Nauty.afterSweep first level size index out)

Finishing a sweep changes only the all-same level.