theorem Hex.GraphIso.Nauty.Sparse.firstPath_exists {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells : Nat} {st : State n} (hn : 0 < n) (hl : 1 ≤ level) (h : NodeInv G level numcells st) (horbit : ∀ (v : Nat), v < n → st.orbits[v]! = v) (hf : n + 1 ≤ level + fuel) : ∃ (last : Nat), ∃ (leaf : State n), Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel level numcells st last leaf ∧ 1 ≤ last ∧ Ready G last n leaf

Every valid native first-path entry with identity orbits reaches a discrete leaf within the executable's depth bound. The returned leaf has the production partition and cache invariants.

theorem Hex.GraphIso.Nauty.Sparse.initial_path {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; ∃ (last : Nat), ∃ (leaf : State n), Generic.FirstPath (Graph.ofGraph G.graph) 100 (n + 2) 1 p.snd.length (initial (Graph.ofGraph G.graph) p.fst p.snd) last leaf ∧ 1 ≤ last ∧ Ready G last n leaf

Stable colour buckets and the initialized identity orbit array give a successful actual first descent for every nonempty sparse coloured graph.