theorem Hex.GraphIso.Nauty.Sparse.Max.FirstInput.witness {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel last : Nat} {f : Frame n} {leaf : State n} {parents : Parents n} (h : FirstInput G tcLevel f parents) (path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel f.level f.numcells f.entry last leaf) (hf : n + 1 ≤ f.level + fuel) : have out := (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel f.level f.numcells f.entry).snd; ∃ (targets : List Nat), ∃ (key : Key n), Generation.RefPath G.graph tcLevel out.allsamelevel f.level (State.refined (Graph.ofGraph G.graph) f.level f.numcells f.entry) targets key ∧ Generation.Matches G.graph f.level out targets key

The complete first call stores a selected native reference retaining uniformity at exactly its returned all-same boundary. The witness agrees with the literal saved codes, targets, sentinel and parsed first label.