theorem Hex.GraphIso.Nauty.admit_gca {n : Nat} {κ : Type} (st : SearchState n κ) : (admit st).gcaFirst = st.gcaFirst

Admitting a generator retains the first-path ancestor.

theorem Hex.GraphIso.Nauty.leafExit_gca {n : Nat} {κ : Type} (leaf : Leaf) (level : Nat) (st : SearchState n κ) : (leafExit leaf level st).snd.gcaFirst = st.gcaFirst

Leaf actions preserve the ancestor shared with the first path.

theorem Hex.GraphIso.Nauty.admit_canon {n : Nat} {κ : Type} (st : SearchState n κ) : (admit st).gcaCanon = st.gcaCanon

Admitting a generator retains the canonical ancestor.

theorem Hex.GraphIso.Nauty.admit_ref {n : Nat} {κ : Type} (st : SearchState n κ) : (admit st).canonlab = st.canonlab

Admitting a generator retains the canonical labelling.

theorem Hex.GraphIso.Nauty.autoCanon_ref {n : Nat} {κ : Type} (level : Nat) (st : SearchState n κ) : (leafExit Generic.Leaf.autoCanon level st).snd.canonlab = st.canonlab

A canonical automorphism return retains its reference labelling.

theorem Hex.GraphIso.Nauty.autoCanon_ancestor {n : Nat} {κ : Type} (level : Nat) (st : SearchState n κ) : (leafExit Generic.Leaf.autoCanon level st).snd.gcaCanon = st.gcaCanon

A canonical automorphism return retains its canonical ancestor.

theorem Hex.GraphIso.Nauty.pruneReturn_canon {n : Nat} {κ : Type} (level : Nat) (st : SearchState n κ) : (pruneReturn level st).snd.gcaCanon = st.gcaCanon

The shared prune tail retains the canonical ancestor.

theorem Hex.GraphIso.Nauty.recover_ref {n : Nat} {κ : Type} (inf level : Nat) (st : SearchState n κ) : (recover inf level st).canonlab = st.canonlab

Parent recovery retains the stored canonical labelling.

theorem Hex.GraphIso.Nauty.compare_canon {n : Nat} {κ : Type} (level code : Nat) (st : SearchState n κ) : (compareCodes level code st).gcaCanon = st.gcaCanon

Code comparison retains the ancestor of the canonical path.

theorem Hex.GraphIso.Nauty.target_canon {n : Nat} (first : Bool) (ctx : Ctx n) (tcLevel level numcells : Nat) (st : Search n) : (chooseTarget first ctx tcLevel level numcells st).snd.snd.snd.gcaCanon = st.gcaCanon

Target selection retains the ancestor of the canonical path.

theorem Hex.GraphIso.Nauty.classify_canon {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : Search n) : (classify ctx level numcells st).snd.gcaCanon = st.gcaCanon

Classification retains the ancestor of the canonical path.

theorem Hex.GraphIso.Nauty.cheap_canon {n : Nat} {κ : Type} (first : Bool) (level : Nat) (st : SearchState n κ) : (cheapCheck first level st).gcaCanon = st.gcaCanon

Testing a small cell retains the ancestor of the canonical path.

theorem Hex.GraphIso.Nauty.recover_canon {n : Nat} {κ : Type} {inf : Nat} (level : Nat) (st : SearchState n κ) : (recover inf level st).gcaCanon = min level st.gcaCanon

Recovery clamps the canonical ancestor to the receiving sweep.

theorem Hex.GraphIso.Nauty.recover_canon_le {n : Nat} {κ : Type} {inf : Nat} (level : Nat) (st : SearchState n κ) : (recover inf level st).gcaCanon ≤ level

The recovered canonical ancestor is no deeper than its sweep.

theorem Hex.GraphIso.Nauty.gcaPolicy {n : Nat} (ctx : Ctx n) (inf tcLevel : Nat) : Generic.ReferencePolicy ctx inf tcLevel fun (st : Search n) => st.gcaFirst

Outside the first descent the first-path ancestor is a fixed frame.

theorem Hex.GraphIso.Nauty.node_gca {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : Search n) : (node false ctx inf tcLevel fuel level numcells st).snd.gcaFirst = st.gcaFirst

An off-path node retains its first-path ancestor throughout its return.

theorem Hex.GraphIso.Nauty.sweep_gca {n : Nat} (first : Bool) (ctx : Ctx n) (inf tcLevel fuel cfuel level numcells tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (st : Search n) (hpast : Generic.Past first tv1 cursor) : (sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd.gcaFirst = st.gcaFirst

Once past the first child, a sweep retains its first-path ancestor.