theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.emit_bound {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {bs fs : List Nat} (h : Valid G f) (hi : CodeEntry G tcLevel f.level f.numcells f.entry) (hc : Comparison G.graph f.codes bs fs f.entry) (he : (emit G.graph tcLevel f).fst ≠ Generic.Exit.done) : Bounded (key G.graph tcLevel f) (State.key G.graph bs f.entry) (State.best G.graph (emit G.graph tcLevel f).snd)

Every actual terminal dispatch respects the full node upper bound, whether it compares discrete rows or rejects a nondiscrete code prefix.

theorem Hex.GraphIso.Nauty.Sparse.Max.afterSweep_best {n : Nat} (G : SparseGraph n) (first : Bool) (level size index : Nat) (st : State n) : State.best G (Generic.Policy.afterSweep first level size index st) = State.best G st

theorem Hex.GraphIso.Nauty.Sparse.Max.node_upper {n k : Nat} (G : Sparse.Colored n k) (tcLevel fuel : Nat) : NodeUpper G tcLevel fuel

The executed native off-path node and sibling recursion never install a key above the incoming incumbent and complete frozen subtree. This is the unconditional upper half of the production maximum induction.