theorem Hex.GraphIso.Nauty.Sparse.runState_codes {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; ∃ (fs : List Nat), ∃ (bs : List Nat), ReturnCodes G.graph [] bs fs (runState (Graph.ofGraph G.graph) p.fst p.snd).snd

Every nonempty initialized native search returns settled comparisons. Its first reference and incumbent lower bound come from the actual first descent, with every structural and allocation premise derived at the root.

theorem Hex.GraphIso.Nauty.Sparse.ReturnCodes.store {n : Nat} {G : SparseGraph n} {cs bs fs : List Nat} {st : State n} (h : ReturnCodes G cs bs fs st) (storage : Storage n) (same : Nat) : ReturnCodes G cs bs fs { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := storage, samerows := same, compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, order := st.order, genTrace := st.genTrace, workperm := st.workperm }

Updating row storage does not change the two settled code machines or their parsed labels and native key bound.

theorem Hex.GraphIso.Nauty.Sparse.runColored_codes {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : ∃ (fs : List Nat), ∃ (bs : List Nat), ReturnCodes G.graph [] bs fs (runColored G)

Final native row installation retains the proved comparison result.

theorem Hex.GraphIso.Nauty.Sparse.runColored_incumbent {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : ∃ (key : Key n), State.best G.graph (runColored G) = some key

The completed nonempty sparse run has a readable incumbent whose label is parsed from the actual canonical-label array.