structure Hex.GraphIso.Nauty.Generation.CanonPast {n : Nat} {κ : Type} (level pos : Nat) (cursor : Option Nat) (st : SearchState 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 : Nat} {κ : Type} {level pos : Nat} {st : SearchState 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 : Nat} {κ : Type} {level pos tv : Nat} {cursor : Option Nat} {st : SearchState 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 : Nat} {κ : Type} {level pos tv : Nat} {cursor : Option Nat} {st : SearchState 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 : Nat} {κ : Type} {level pos : Nat} {cursor : Option Nat} {st out : SearchState 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.