def Hex.GraphIso.Nauty.Sparse.canonVerdict {n : Nat} (g : Graph n) (level : Nat) (st : State n) : Leaf × State n

The canonical-comparison part of the native classifier, after the first-reference admission is inapplicable or has failed.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.canonVerdict_ne {n : Nat} (g : Graph n) (level : Nat) (st : State n) : (canonVerdict g level st).fst ≠ Generic.Leaf.autoFirst

theorem Hex.GraphIso.Nauty.Sparse.classify_eq {n : Nat} (g : Graph n) (level numcells : Nat) (st : State n) : classify g level numcells st = if (st.eqlevFirst != level && decide (st.compCanon < 0)) = true then (Generic.Leaf.bad, st) else if (numcells != n) = true then (Generic.Leaf.internal, st) else if (st.eqlevFirst == level) = true then have sc := scatter st.firstlab st; if (decide (sc.gcaFirst ≥ sc.noncheaplevel) || isautom g sc.workperm) = true then (Generic.Leaf.autoFirst, sc) else canonVerdict g level sc else canonVerdict g level st

This decomposition is definitionally the executed sparse classifier.

theorem Hex.GraphIso.Nauty.Sparse.classify_first {n : Nat} {g : Graph n} {level numcells : Nat} {st out : State n} (hauto : classify g level numcells st = (Generic.Leaf.autoFirst, out)) : numcells = n ∧ st.eqlevFirst = level ∧ out = scatter st.firstlab st ∧ (st.noncheaplevel ≤ st.gcaFirst ∨ isautom g out.workperm = true)

First-reference admission scatters the saved first label and takes exactly one of the cheap-boundary and explicit-scan guards.