theorem Hex.GraphIso.Nauty.Generic.Trivial.node_step {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level : Nat) (st : State n) : node false ctx inf tcLevel (fuel + 1) level st.frame.partition.numcells st = have ready := visit ctx level st.frame.partition.numcells st; if discreteAt ready.frame.partition.ptn level n = true then (Exit.unwind (level - 1) false, install ready) else have p := ready.frame.partition; have t := specMaketargetcell ctx p.lab p.ptn level tcLevel; have cell := positions t.snd.snd; have out := sweep false ctx inf tcLevel fuel (n + 1) level p.numcells t.fst ((cell.nextElem none).getD 0) (cell.nextElem none) cell 0 ready; match out.fst with | Exit.done => (Exit.unwind (level - 1) false, out.snd.snd) | exit => (exit, out.snd.snd)

One exhaustive node refines, installs a discrete leaf, or sweeps all positions of the specification target.

theorem Hex.GraphIso.Nauty.Generic.Trivial.sweep_fold {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level tc len : Nat} (st : State n) (key : Nat → Key n) (hlen : len ≤ n) (hnode : ∀ (o : Nat), o < len → ∀ (best : Option (Key n)), node false ctx inf tcLevel fuel (level + 1) (st.frame.partition.numcells + 1) (child level tc o { frame := st.frame, parents := st.parents, best := best }) = (Exit.unwind level false, have __src := visit ctx (level + 1) (st.frame.partition.numcells + 1) (child level tc o { frame := st.frame, parents := st.parents, best := best }); { frame := __src.frame, parents := __src.parents, best := some (incMax best (key o)) })) (cfuel o : Nat) : o ≤ len → len - o ≤ cfuel → ∀ (best : Option (Key n)) (tv1 index : Nat), sweep false ctx inf tcLevel fuel cfuel level st.frame.partition.numcells tc tv1 (if o < len then some o else none) (positions len) index { frame := st.frame, parents := st.parents, best := best } = (Exit.done, index, { frame := st.frame, parents := st.parents, best := List.foldl (fun (best : Option (Key n)) (o : Nat) => some (incMax best (key o))) best (List.range' o (len - o)) })

An exhaustive sweep folds its child maxima in increasing target-offset order. Child calls leave their saved parent available for recovery.

theorem Hex.GraphIso.Nauty.Generic.Trivial.node_eq {n : Nat} {ctx : Ctx n} {tcLevel fuel level : Nat} {p : RefineSt n} (h : Complete ctx tcLevel fuel level p) (st : State n) (hp : st.frame.partition = p) (inf : Nat) : node false ctx inf tcLevel fuel level p.numcells st = (Exit.unwind (level - 1) false, have __src := visit ctx level p.numcells st; { frame := __src.frame, parents := __src.parents, best := some (incMax st.best (prefixKey st.frame.codes (specNode ctx tcLevel fuel level p.lab p.ptn p.active p.numcells))) })

With enough depth for every leaf, the never-pruning policy computes the specification maximum and restores each node's refined frame.

theorem Hex.GraphIso.Nauty.Generic.Trivial.complete {n : Nat} {ctx : Ctx n} {tcLevel fuel level : Nat} {p : RefineSt n} (hok : NodeOk n level p.lab p.ptn p.active) (hbc : level ≤ bcount p.ptn level n) (hfuel : n + 1 ≤ level + fuel) : Complete ctx tcLevel fuel level p

A well-formed partition reaches every leaf within the usual level-versus-fuel bound. Each individualization adds a closed boundary.

theorem Hex.GraphIso.Nauty.Generic.Trivial.generic_trivial_eq_specNode {n : Nat} {ctx : Ctx n} {tcLevel fuel level : Nat} {p : RefineSt n} (hok : NodeOk n level p.lab p.ptn p.active) (hbc : level ≤ bcount p.ptn level n) (hfuel : n + 1 ≤ level + fuel) (inf : Nat) : (node false ctx inf tcLevel fuel level p.numcells { frame := { partition := p, codes := [], candidate := default }, parents := [], best := none }).snd.best = some (specNode ctx tcLevel fuel level p.lab p.ptn p.active p.numcells)

Starting with no incumbent and no path prefix, exhaustive generic search returns exactly the declarative subtree key with sufficient fuel.