theorem Hex.GraphIso.Nauty.Max.root_first {n k : Nat} (G : Colored n k) (hn0 : 0 < n) (hn : ∀ (f : Nat), f < n + 2 → (contract G 100).nodeValid f (Generic.nodeCall { g := rowsOf G } (n + 2) 100 f)) : have ctx := { g := rowsOf G }; have f := root G; have out := node true ctx (n + 2) 100 (n + 2) f.level f.numcells f.entry; out.fst = Generic.Exit.unwind 0 false ∧ ∃ (targets : List Nat), ∃ (key : Key n), Generation.RefPath ctx 100 out.snd.allsamelevel 1 (SearchState.refined ctx 1 f.numcells f.entry) targets key ∧ Generation.Matches ctx 1 out.snd targets key

The actual nonempty root initializes the complete first-path contract. Only strictly smaller maximum and trace calls remain premises. This entry point supports reasoning about first-path matches without importing generator completeness; the umbrella builds it alongside the complete key and generation interfaces.