structure Hex.GraphIso.Nauty.Generation.TreeOk {n : Nat} (ctx : Ctx n) (level : Nat) (st : RefineSt n) : Prop

The refined search-tree invariant, including the depth bound needed to rule out a non-discrete node when the vertex budget is exhausted.

• it : IterOk ctx level st
• eqt : Equitable ctx level st.lab st.ptn
• acc : bcount st.ptn level n = st.numcells
• depth : level ≤ st.numcells

theorem Hex.GraphIso.Nauty.Generation.TreeOk.child {n : Nat} {ctx : Ctx n} {level tc e o : Nat} {st : RefineSt n} (h : TreeOk ctx level st) (hlvl : level < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (ho : o ≤ e - tc) : TreeOk ctx (level + 1) (childSt ctx level st tc st.lab[tc + o]!)

Every target child is a valid refined tree with strictly more cells.

theorem Hex.GraphIso.Nauty.Generation.TreeOk.nonempty {n : Nat} {ctx : Ctx n} {level tcLevel : Nat} {st : RefineSt n} (h : TreeOk ctx level st) (hlevel : 1 ≤ level) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) : ∃ (targets : List Nat), ∃ (key : Key n), HasLeaf ctx tcLevel level st targets key

Every valid refined tree has a leaf following the specification's target-cell rule. This prevents uniformity premises from being vacuous.