theorem Hex.GraphIso.Nauty.Max.Frame.emit_step {n : Nat} {ctx : Ctx n} {tcLevel : Nat} {f : Frame n} (next : Generic.SweepFn (Search n) n) (h : (emit ctx tcLevel f).fst ≠ Generic.Exit.done) : Generic.nodeStep ctx tcLevel next false f.level f.numcells f.entry = emit ctx tcLevel f

A nonlocal emission is the actual node step, with no sweep invoked.

theorem Hex.GraphIso.Nauty.Max.better_discrete {n : Nat} {ctx : Ctx n} {level numcells sr : Nat} {st : Search n} (h : (classify ctx level numcells st).fst = Generic.Leaf.better sr) : numcells = n

A better classification occurs only at a discrete node.

theorem Hex.GraphIso.Nauty.Max.better_target {n level sr target : Nat} {short : Bool} {st : Search n} (he : (leafExit (Generic.Leaf.better sr) level st).fst = Generic.Exit.unwind target short) (ht : target < level) : target = st.noncheaplevel - 1

Installation sets the equal-code level to the leaf level, so every strict-ancestor return from a better leaf uses the cheap boundary.

theorem Hex.GraphIso.Nauty.Max.better_rule {n k : Nat} (G : Colored n k) (tcLevel sr : Nat) : NodeRule G tcLevel false fun (level numcells : Nat) (st : Search n) => verdict G tcLevel level numcells st = Generic.Leaf.better sr

The better-leaf rule discharges its complete local maximum obligation, including every nonlocal cheap return.