theorem
Hex.GraphIso.Nauty.Sparse.Max.FirstInput.maximum
{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)
:
The complete executed first descent satisfies its maximum contract. The induction supplies each first child's result, and the established off-path theorem handles every later sibling. All contexts are derived from the actual preparations, stored ancestors and child returns.