theorem Hex.GraphIso.Nauty.Max.NodeInput.leaf_best {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} (h : NodeInput G ctx tcLevel fuel false f bs fs parents) (hd : (prepareOther ctx tcLevel f.level f.numcells f.entry).fst = n) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) : have p := prepareOther ctx tcLevel f.level f.numcells f.entry; have c := classify ctx f.level p.fst p.snd.snd.snd.snd.snd; SearchState.best ctx (leafExit c.fst f.level c.snd).snd = some (incMax (SearchState.key ctx bs f.entry) (Frame.key ctx tcLevel f))

An actual discrete off-path emission installs the maximum of its incoming semantic incumbent and its full frozen node key.