theorem Hex.GraphIso.Nauty.Sparse.Max.node_max {n k : Nat} (G : Sparse.Colored n k) (tcLevel fuel : Nat) : NodeMax G tcLevel fuel

The actual off-path search satisfies its complete maximum contract. The induction assembles local native state invariants at preparation, child entry and recovery; its only recursive premise is the smaller executed call. No production-maximum theorem is assumed.