def Hex.GraphIso.Nauty.Sparse.Store {n : Nat} (G : SparseGraph n) (st : State n) : Prop

The incumbent parses as a label and the allocated raw rows represent exactly its installed prefix. Unfilled capacity is not a complete graph.

Equations

• Hex.GraphIso.Nauty.Sparse.Store G st = ∃ (l : Hex.GraphIso.Label n), Hex.GraphIso.Label.ofArray? n st.canonlab = some l ∧ st.canong.Prefix (G.relabel l.perm) st.samerows

def Hex.GraphIso.Nauty.Sparse.Candidate {n : Nat} (G : SparseGraph n) (st : State n) (same : Nat) : Prop

A candidate prefix justified by the actual comparison, ready for the shared better-leaf installation.

Equations

• Hex.GraphIso.Nauty.Sparse.Candidate G st same = ∃ (l : Hex.GraphIso.Label n), Hex.GraphIso.Label.ofArray? n st.lab = some l ∧ st.canong.Prefix (G.relabel l.perm) same

theorem Hex.GraphIso.Nauty.Sparse.Store.congr {n : Nat} {G : SparseGraph n} {st out : State n} (h : Store G st) (hr : out.canong.toRows = st.canong.toRows) (hc : out.canonlab = st.canonlab) (hs : out.samerows = st.samerows) : Store G out

theorem Hex.GraphIso.Nauty.Sparse.Store.visit {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) (level numcells : Nat) : Store G (Sparse.visit (Graph.ofGraph G) level numcells st).snd.snd

theorem Hex.GraphIso.Nauty.Sparse.Store.record {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) (level code : Nat) : Store G (recordFirst level code st)

theorem Hex.GraphIso.Nauty.Sparse.Store.compare {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) (level code : Nat) : Store G (compareCodes level code st)

theorem Hex.GraphIso.Nauty.Sparse.Store.cheap {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) (first : Bool) (level : Nat) : Store G (cheapCheck first level st)

theorem Hex.GraphIso.Nauty.Sparse.Store.child {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) (first : Bool) (level tc tv : Nat) : Store G (Generic.Policy.child first level tc tv st)

theorem Hex.GraphIso.Nauty.Sparse.Store.afterChild {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) (level tv : Nat) : Store G (afterChildFirst level tv st)

theorem Hex.GraphIso.Nauty.Sparse.Store.leave {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) (tv : Nat) : Store G { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts.erase tv, 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, 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 }

theorem Hex.GraphIso.Nauty.Sparse.Store.afterSweep {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) (first : Bool) (level size index : Nat) : Store G (Generic.Policy.afterSweep first level size index st)

theorem Hex.GraphIso.Nauty.Sparse.Store.terminal {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) (level : Nat) (l : Label n) (hl : Label.ofArray? n st.lab = some l) : Store G (firstterminal level st)

theorem Hex.GraphIso.Nauty.Sparse.Store.finish {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) : Store G (Sparse.finish (Graph.ofGraph G) st)

theorem Hex.GraphIso.Nauty.Sparse.Store.classify {n : Nat} {G : SparseGraph n} {st : State n} (h : Store G st) (level numcells : Nat) (l : Label n) (hl : Label.ofArray? n st.lab = some l) : have r := Sparse.classify (Graph.ofGraph G) level numcells st; Store G r.snd ∧ ∀ (sr : Nat), r.fst = Generic.Leaf.better sr → Candidate G r.snd sr

Classification preserves the old incumbent and prepares a parsed, semantically valid candidate prefix for every better-leaf verdict.