def Hex.GraphIso.Nauty.TraceOk {n : Nat} (ctx : Ctx n) (st : Search n) : Prop

Every permutation in the unbounded generator trace is a checked automorphism.

Equations

• Hex.GraphIso.Nauty.TraceOk ctx st = ∀ (γ : Array Nat), γ ∈ st.genTrace → Hex.GraphIso.Nauty.checkAutom ctx.g γ = true

theorem Hex.GraphIso.Nauty.classify_trace {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : Search n) : (classify ctx level numcells st).snd.genTrace = st.genTrace

Classification builds scratch data without adding it to the generator trace.

theorem Hex.GraphIso.Nauty.classify_internal_state {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : Search n} (h : (classify ctx level numcells st).fst = Generic.Leaf.internal) : classify ctx level numcells st = (Generic.Leaf.internal, st)

An internal classification returns the input state unchanged.

theorem Hex.GraphIso.Nauty.leafExit_trace {n : Nat} {κ : Type} (leaf : Leaf) (level : Nat) (st : SearchState n κ) : (leafExit leaf level st).snd.genTrace = match leaf with | Generic.Leaf.autoFirst => st.genTrace.push st.workperm | Generic.Leaf.autoCanon => st.genTrace.push st.workperm | x => st.genTrace

The two automorphism verdicts append exactly the scratch permutation.

theorem Hex.GraphIso.Nauty.leafExit_checked {n : Nat} {ctx : Ctx n} {level : Nat} {st : Search n} (h : TraceOk ctx st) (leaf : Leaf) (hcheck : leaf = Generic.Leaf.autoFirst ∨ leaf = Generic.Leaf.autoCanon → checkAutom ctx.g st.workperm = true) : TraceOk ctx (leafExit leaf level st).snd

Only the two automorphism verdicts append a permutation. Both require a checked scratch value.

theorem Hex.GraphIso.Nauty.Aligned.first_checked {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {root : RefineSt n} {st out : Search n} (h : Aligned ctx st.gcaFirst root level level numcells st) (href : FirstRef ctx tcLevel st.gcaFirst root st) (hdepth : Depth href.last st) (hsmall : SubtreeOk ctx st.gcaFirst root) (hok : SearchOk G level numcells st) (hauto : Nauty.classify ctx level numcells st = (Generic.Leaf.autoFirst, out)) (hwork : st.workperm.size = 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) : checkAutom ctx.g out.workperm = true

At a discrete node, alignment supplies the two histories required by cheap admission.

theorem Hex.GraphIso.Nauty.classify_first_scanned {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st out : Search n} (hauto : classify ctx level numcells st = (Generic.Leaf.autoFirst, out)) (hnoncheap : st.gcaFirst < st.noncheaplevel) (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)) (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) : checkAutom ctx.g out.workperm = true

A code-one admission outside a cheap ancestor is justified by its explicit scan.