def Hex.GraphIso.Nauty.Sparse.prepareOther {n : Nat} (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : Nat × Nat × Int × VSet n × Nat × State n

The exact visit, comparison and target dispatch at an off-path node.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.Comparison.prepare {n : Nat} {G : SparseGraph n} {cs bs fs : List Nat} {st : State n} (h : Comparison G cs bs fs st) (tcLevel numcells : Nat) (hlen : cs.length ≤ n) : have p := prepareOther (Graph.ofGraph G) tcLevel (cs.length + 1) numcells st; Comparison G (cs ++ [p.snd.fst]) bs fs p.snd.snd.snd.snd.snd ∧ State.key G bs p.snd.snd.snd.snd.snd = State.key G bs st

Off-path preparation extends both histories by its executed code and retains the incoming semantic native incumbent.

theorem Hex.GraphIso.Nauty.Sparse.recover_labels {n : Nat} (inf level : Nat) (st : State n) : have out := Generic.Policy.recover inf level st; out.firstlab = st.firstlab ∧ out.canonlab = st.canonlab

Native recovery invalidates scratch while retaining both saved labels.

theorem Hex.GraphIso.Nauty.Sparse.Comparison.recover {n : Nat} {G : SparseGraph n} {cs bs fs : List Nat} {st : State n} (h : Comparison G cs bs fs st) (hnonpos : st.compCanon ≤ 0) {level : Nat} (hlen : level ≤ cs.length) (inf : Nat) : Comparison G (List.take level cs) bs fs (Generic.Policy.recover inf level st)

Restoring a settled code verdict truncates its current path at the receiving ancestor and retains both reference comparisons and key bound.

theorem Hex.GraphIso.Nauty.Sparse.recover_key {n : Nat} (G : SparseGraph n) (bs : List Nat) (inf level : Nat) (st : State n) : State.key G bs (Generic.Policy.recover inf level st) = State.key G bs st

theorem Hex.GraphIso.Nauty.Sparse.Comparison.recover_rows {n : Nat} {G : SparseGraph n} {cs bs fs : List Nat} {st : State n} (h : Comparison 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 := st.canong, samerows := st.samerows, 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 }) (hnegative : st.compCanon < 0) {level : Nat} (hlen : level ≤ cs.length) (inf : Nat) : Comparison G (List.take level cs) bs fs (Generic.Policy.recover inf level st)

A negative row verdict repurposes compCanon after code equality. Recovery restores the code machine from that equality and retains the same native key bound and saved first comparison.