structure Hex.GraphIso.Nauty.Generation.CanonPast {n : Nat} (level pos : Nat) (cursor : Option Nat) (st : SearchSt n) : Prop

A canonical reference belonging to the current frame comes from a child already behind its cursor. An older ancestor reference has no local source obligation.

• cap : st.gcaCanon ≤ level
• source : st.gcaCanon = level → ¬After cursor st.canonlab[pos]!

theorem Hex.GraphIso.Nauty.Generation.CanonPast.start {n level pos : Nat} {st : SearchSt n} (h : st.gcaCanon < level) : CanonPast level pos none st

An ancestor reference imposes no source obligation at a fresh frame.

theorem Hex.GraphIso.Nauty.Generation.CanonPast.advance {n level pos tv : Nat} {cursor : Option Nat} {st : SearchSt n} (h : CanonPast level pos cursor st) (ha : After cursor tv) : CanonPast level pos (some tv) st

Advancing a sweep cursor retains every older canonical source.

theorem Hex.GraphIso.Nauty.Generation.CanonPast.before {n level pos tv : Nat} {cursor : Option Nat} {st : SearchSt n} {tcell : VSet n} (h : CanonPast level pos cursor st) (hnext : tcell.nextElem cursor = some tv) (he : st.gcaCanon = level) : st.canonlab[pos]! < tv

The reference child is strictly earlier than the next visited child.

theorem Hex.GraphIso.Nauty.Generation.CanonPast.stateEq {n level pos : Nat} {cursor : Option Nat} {st out : SearchSt n} (h : CanonPast level pos cursor st) (hgca : out.gcaCanon = st.gcaCanon) (hlab : out.canonlab = st.canonlab) : CanonPast level pos cursor out

Updates to unrelated bookkeeping preserve the canonical source.

theorem Hex.GraphIso.Nauty.Generation.CanonPast.recover {n inf level pos tv : Nat} {cursor : Option Nat} {st child out : SearchSt n} (h : CanonPast level pos cursor st) (ha : After cursor tv) (hgca : child.gcaCanon = st.gcaCanon) (hlab : child.canonlab = st.canonlab) (hguide : GuideRel (level + 1) child out) (hcell : IsCell child.ptn (level + 1) pos 1) (hat : child.lab[pos]! = tv) : CanonPast level pos (some tv) (Nauty.recover n inf level out)

Recovering after a child visit keeps an old source or records the visited child as the new source. The old/new disjunction is used directly; no cell-location assertion is made about an old ancestor reference.

theorem Hex.GraphIso.Nauty.Generation.canon_old {n level : Nat} {st out : SearchSt n} (h : GuideRel level st out) (hbelow : out.gcaCanon < level) : out.gcaCanon = st.gcaCanon ∧ out.canonlab = st.canonlab

A child return below its entry keeps the old canonical reference whenever its canonical guide is also below that entry.

theorem Hex.GraphIso.Nauty.Generation.CanonPast.locate {n : Nat} {ctx : Ctx n} {tcLevel specFuel level tc len numcells tv : Nat} {codes : List Nat} {rsLab rsPtn : Array Nat} {cursor : Option Nat} {tcell : VSet n} {st child out : SearchSt n} {best : Option (Key n)} (h : CanonPast level tc cursor st) (hnext : tcell.nextElem cursor = some tv) (hrefs : FrameRefs ctx tcLevel specFuel level codes rsLab rsPtn tc len numcells st best) (hgca : child.gcaCanon = st.gcaCanon) (hlab : child.canonlab = st.canonlab) (hguide : GuideRel (level + 1) child out) (hat : out.gcaCanon = level) : ∃ (o : Nat), o < len ∧ out.canonlab[tc]! = rsLab[tc + o]! ∧ rsLab[tc + o]! < tv ∧ cellsPerm rsPtn level rsLab out.canonlab

A canonical return to this frame names an earlier original child. The return tag and old-reference alternative recover its location from the existing frame references, including after target-set pruning.