def Hex.GraphIso.Nauty.Sparse.Max.Cosets {n : Nat} (st : State n) (parents : Parents n) : Prop

An active first ancestor identifies its suspended selected vertex with the coset index used by native early-return bookkeeping.

Equations

• Hex.GraphIso.Nauty.Sparse.Max.Cosets st parents = ∀ (t : Nat) (p : Hex.GraphIso.Nauty.Sparse.Max.Parent n), parents t = some p → st.gcaFirst = t → p.first = true ∧ st.cosetindex = p.chosen

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

theorem Hex.GraphIso.Nauty.Sparse.Max.Cosets.fields {n : Nat} {st out : State n} {parents : Parents n} (h : Cosets st parents) (hf : out.gcaFirst = st.gcaFirst) (hc : out.cosetindex = st.cosetindex) : Cosets out parents

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.firstParent_coset {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) (bs : List Nat) (tv : Nat) : (firstParent G tcLevel f bs tv).state.cosetindex = f.entry.cosetindex

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.otherParent_coset {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) (bs : List Nat) (tv : Nat) : (otherParent G tcLevel f bs tv).state.cosetindex = f.entry.cosetindex

theorem Hex.GraphIso.Nauty.Sparse.Max.Cosets.first_prepare {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {f : Frame n} {parents : Parents n} (h : Cosets f.entry parents) (bs : List Nat) (tv : Nat) : Cosets (Frame.firstParent G tcLevel f bs tv).state parents

theorem Hex.GraphIso.Nauty.Sparse.Max.Cosets.other_prepare {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {f : Frame n} {parents : Parents n} (h : Cosets f.entry parents) (bs : List Nat) (tv : Nat) : Cosets (Frame.otherParent G tcLevel f bs tv).state parents

theorem Hex.GraphIso.Nauty.Sparse.Max.Cosets.child {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {p : Parent n} {parents : Parents n} (h : Cosets p.state parents) (hs : Scope G tcLevel p.node p.bs p.state parents) (hfirst : p.first = true → p.state.gcaFirst = 0 ∨ p.state.gcaFirst = p.node.level) (hother : p.first = false → p.state.gcaFirst < p.node.level) : Cosets (Parent.child G.graph tcLevel p).entry (parents.push p)

First sweeps overwrite the selected index for their new child; ordinary sweeps retain the older first ancestor's index. Before the first leaf, counter zero names no suspended parent.

theorem Hex.GraphIso.Nauty.Sparse.Max.Cosets.node {n : Nat} {g : Graph n} {inf tcLevel fuel level numcells : Nat} {st : State n} {parents : Parents n} (h : Cosets st parents) : Cosets (Generic.node false g inf tcLevel fuel level numcells st).snd parents

theorem Hex.GraphIso.Nauty.Sparse.Max.Cosets.back {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel : Nat} {p : Parent n} {parents : Parents n} (h : Cosets (Parent.child G.graph tcLevel p).entry (parents.push p)) (hs : Scope G tcLevel p.node p.bs p.state parents) : Cosets (Parent.back G.graph tcLevel fuel p) parents

Returning an off-path child and recovering its parent retains all older coset associations. The just-completed child is removed from the suspended-parent map.

theorem Hex.GraphIso.Nauty.Sparse.Max.Cosets.first_back {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel last : Nat} {p : Parent n} {parents : Parents n} {leaf : State n} (hs : Scope G tcLevel p.node p.bs p.state parents) (path : have ch := Parent.child G.graph tcLevel p; Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel ch.level ch.numcells ch.entry last leaf) : Cosets (Parent.firstBack G.graph tcLevel fuel p) parents

First-child recovery names the receiving parent, so none of its strictly older suspended parents can be mistaken for that first ancestor.