def Hex.GraphIso.Nauty.canonVerdict {n : Nat} (ctx : Ctx n) (level : Nat) (st : Search n) : Leaf × Search n

Canonical comparison after first-reference admission has failed or is inapplicable.

Equations

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

theorem Hex.GraphIso.Nauty.classify_eq {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : Search n) : classify ctx 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 ctx sc.workperm) = true then (Generic.Leaf.autoFirst, sc) else canonVerdict ctx level sc else canonVerdict ctx level st

Separate first-reference admission from the canonical verdict.

def Hex.GraphIso.Nauty.VerdictInv {n : Nat} (ctx : Ctx n) (r : Leaf × Search n) : Prop

The current canonical store is valid, and a better verdict carries the row-prefix invariant needed to install the candidate.

Equations

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

theorem Hex.GraphIso.Nauty.classify_store {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : Search n} (hinv : CanongInv ctx st.canong st.canonlab st.samerows) : VerdictInv ctx (classify ctx level numcells st)

Classification preserves the canonical store and prepares any better candidate for installation, independently of the comparison-code invariant.

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

Code-one admission is precisely the first-reference scatter, accepted by the cheap boundary or by an explicit automorphism scan.

theorem Hex.GraphIso.Nauty.classify_first_checked {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st out : Search n} (hauto : classify ctx level numcells st = (Generic.Leaf.autoFirst, out)) (hwork : st.workperm.size = n) (hfirst : st.firstlab.size = n) (hfirstPerm : st.firstlab.toList.Perm (List.range n)) (hlab : st.lab.size = n) (hlabPerm : st.lab.toList.Perm (List.range n)) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hhistory : st.noncheaplevel ≤ st.gcaFirst → ∃ (root : RefineSt n), ∃ (current : RefineSt n), ∃ (href : FirstRef ctx tcLevel st.gcaFirst root st), Depth href.last st ∧ SubtreeOk ctx st.gcaFirst root ∧ FollowsPerm ctx st.firsttc st.gcaFirst root level current ∧ (∀ (i : Nat), i < n → current.ptn[i]! ≤ level) ∧ st.lab = current.lab) : checkAutom ctx.g out.workperm = true

The restored code-one admission is checked whenever the two histories at its cheap ancestor are available.

theorem Hex.GraphIso.Nauty.classify_canon_checked {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st out : Search n} (hauto : classify ctx level numcells st = (Generic.Leaf.autoCanon, out)) (hinv : CanongInv ctx st.canong st.canonlab st.samerows) (hwork : st.workperm.size = n) (href : st.canonlab.size = n) (hrefPerm : st.canonlab.toList.Perm (List.range n)) (hlab : st.lab.size = n) (hlabPerm : st.lab.toList.Perm (List.range n)) : checkAutom ctx.g out.workperm = true

Code-two admission is checked by equality with the installed canonical rows.

theorem Hex.GraphIso.Nauty.leafExit_store {n : Nat} {ctx : Ctx n} {leaf : Leaf} {level : Nat} {st : Search n} (h : VerdictInv ctx (leaf, st)) : have out := (leafExit leaf level st).snd; CanongInv ctx out.canong out.canonlab out.samerows

Acting on a justified verdict preserves the canonical row-store invariant.