theorem Hex.GraphIso.Nauty.Sparse.Max.FirstEntry.upper {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel last : Nat} {f : Frame n} {leaf : State n} {parents : Parents n} (h : FirstEntry G f) (path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel f.level f.numcells f.entry last leaf) (hs : Scope G tcLevel f [] f.entry parents) (hf : n + 1 ≤ f.level + fuel) : Bounded (Frame.key G.graph tcLevel f) none (State.best G.graph (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel f.level f.numcells f.entry).snd)

The complete actual first-path call installs only keys below its full frozen subtree. The induction discharges every first-child bound; all later children use the proved native off-path recursion.