theorem Hex.GraphIso.Nauty.Max.NodeInput.first_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 true f bs fs parents) (hd : (Generic.prepareFirst ctx tcLevel f.level f.numcells f.entry).fst = n) : SearchState.best ctx (firstterminal f.level (Generic.prepareFirst ctx tcLevel f.level f.numcells f.entry).snd.snd.snd.snd) = some (Frame.key ctx tcLevel f)

Installing the first discrete leaf records precisely its frozen specification key, including the incoming refinement-code prefix.

theorem Hex.GraphIso.Nauty.Max.first_leaf {n k : Nat} (G : Colored n k) (tcLevel : Nat) : NodeRule G tcLevel true fun (level numcells : Nat) (st : Search n) => (Generic.prepareFirst { g := rowsOf G } tcLevel level numcells st).fst = n

The first discrete branch completes the node without invoking its sweep continuation.