structure Hex.GraphIso.Nauty.Sparse.Max.Parent.Guided {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (p : Parent n) : Prop

A suspended parent retains coverage of references pointing to its own sweep. These are previously completed child keys, in its actual ordering at suspension.

• canonical : CanonGuide p.node.level p.tc p.state (key G tcLevel p) (State.key G p.bs p.state) p.state
• first : p.state.gcaFirst = p.node.level → Covers (key G tcLevel p p.state.firstlab[p.tc]!) (State.key G p.bs p.state) ∧ cellsPerm p.state.ptn p.node.level p.state.lab p.state.firstlab

theorem Hex.GraphIso.Nauty.Sparse.Max.Parent.Guided.vacuous {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {p : Parent n} (hf : p.state.gcaFirst < p.node.level) (hc : p.state.gcaCanon < p.node.level) : Guided G tcLevel p

structure Hex.GraphIso.Nauty.Sparse.Max.Guides {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (st : State n) (parents : Parents n) : Prop

A reference still pointing to a suspended ancestor is literally the reference retained there. Covered-reference data is stored at suspension; incumbent growth is supplied separately by the established native scope.

• saved (t : Nat) (p : Parent n) : parents t = some p → Parent.Guided G tcLevel p
• first (t : Nat) (p : Parent n) : parents t = some p → st.gcaFirst ≤ t → st.gcaFirst = p.state.gcaFirst ∧ st.firstlab = p.state.firstlab
• canonical (t : Nat) (p : Parent n) : parents t = some p → st.gcaCanon ≤ t → st.gcaCanon = p.state.gcaCanon ∧ st.canonlab = p.state.canonlab

theorem Hex.GraphIso.Nauty.Sparse.Max.Guides.root {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (st : State n) : Guides G tcLevel st fun (x : Nat) => none

theorem Hex.GraphIso.Nauty.Sparse.Max.Guides.fields {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {st out : State n} {parents : Parents n} (h : Guides G tcLevel st parents) (hf : out.firstlab = st.firstlab) (hg : out.gcaFirst = st.gcaFirst) (hc : out.canonlab = st.canonlab) (ha : out.gcaCanon = st.gcaCanon) : Guides G tcLevel out parents

Native local operations preserving the reference labels and their ancestor counters retain all covered-reference associations.

theorem Hex.GraphIso.Nauty.Sparse.Max.Guides.child {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {p : Parent n} {parents : Parents n} (h : Guides G tcLevel p.state parents) (hp : Parent.Guided G tcLevel p) : Guides G tcLevel (Parent.child G tcLevel p).entry (parents.push p)

Suspending a covered parent and performing the actual sparse child operation extends the reference associations. Cache invalidation and first-path coset bookkeeping do not change either reference.

theorem Hex.GraphIso.Nauty.Sparse.Max.Guides.change {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {bs : List Nat} {st out : State n} {parents : Parents n} (h : Guides G.graph tcLevel st parents) (hs : Scope G tcLevel f bs st parents) (hf : out.gcaFirst = st.gcaFirst ∧ out.firstlab = st.firstlab ∨ f.level ≤ out.gcaFirst) (hc : out.gcaCanon < f.level → out.gcaCanon = st.gcaCanon ∧ out.canonlab = st.canonlab) : Guides G.graph tcLevel out parents

A return retains earlier references whenever its counters still name them. A first-child update points to the current level and therefore cannot be mistaken for a reference belonging to an older suspended parent.