structure Hex.GraphIso.Nauty.Sparse.Max.Scope {n k : Nat} (G : Sparse.Colored n k) (tcLevel : Nat) (f : Frame n) (bs : List Nat) (st : State n) (parents : Parents n) : Prop

A native call or sweep retains its frozen ancestor chain, recorded code prefixes, incumbent growth and the actual cheap-boundary counters.

• codes : CodeScope G f.codes parents.frames
• complete (t : Nat) : 1 ≤ t → t < f.level → ∃ (p : Parent n), parents t = some p
• valid (t : Nat) (p : Parent n) : parents t = some p → 1 ≤ t ∧ t < f.level ∧ p.node.level = t ∧ Parent.Valid G tcLevel p
• parent : 1 < f.level → ∃ (p : Parent n), parents (f.level - 1) = some p ∧ Parent.child G.graph tcLevel p = f
• chain (t : Nat) (p : Parent n) : parents t = some p → 1 < t → ∃ (prev : Parent n), parents (t - 1) = some prev ∧ Parent.child G.graph tcLevel prev = p.node
• grows (t : Nat) (p : Parent n) : parents t = some p → Grows (State.key G.graph p.bs p.state) (State.key G.graph bs st)
• boundary (t : Nat) (p : Parent n) : parents t = some p → st.noncheaplevel = p.state.noncheaplevel ∨ t + 1 ≤ st.noncheaplevel

theorem Hex.GraphIso.Nauty.Sparse.Max.Scope.root {n k : Nat} (G : Sparse.Colored n k) (tcLevel numcells : Nat) (entry st : State n) (bs : List Nat) : Scope G tcLevel { level := 1, numcells := numcells, codes := [], entry := entry } bs st fun (x : Nat) => none

theorem Hex.GraphIso.Nauty.Sparse.Max.Scope.change {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {bs ds : List Nat} {st out : State n} {parents : Parents n} (h : Scope G tcLevel f bs st parents) (hg : Grows (State.key G.graph bs st) (State.key G.graph ds out)) (hb : out.noncheaplevel = st.noncheaplevel ∨ f.level ≤ out.noncheaplevel) : Scope G tcLevel f ds out parents

Native local work or a returned child can update the current state without changing any suspended entry. The proved counter alternative and incumbent growth suffice to retain all ancestor obligations.

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

Suspending the current parent and individualizing its selected vertex constructs the next node's entire ancestor scope.