theorem
Hex.GraphIso.Nauty.Max.Frame.emit_trace
{n : Nat}
(ctx : Ctx n)
(tcLevel : Nat)
(f : Frame n)
:
have p := prepareOther ctx tcLevel f.level f.numcells f.entry;
have leaf := (classify ctx f.level p.fst p.snd.snd.snd.snd.snd).fst;
(emit ctx tcLevel f).snd.genTrace = match leaf with
| Generic.Leaf.autoFirst => f.entry.genTrace.push (emit ctx tcLevel f).snd.workperm
| Generic.Leaf.autoCanon => f.entry.genTrace.push (emit ctx tcLevel f).snd.workperm
| x => f.entry.genTrace
A leaf action either retains the entry trace or appends precisely its checked scratch permutation.
theorem
Hex.GraphIso.Nauty.Max.canon_target
{n level target : Nat}
{short : Bool}
{st : Search n}
(he : (leafExit Generic.Leaf.autoCanon level st).fst = Generic.Exit.unwind target short)
:
Every code-two exit names either the first or canonical ancestor.
theorem
Hex.GraphIso.Nauty.Max.NodeInput.emit_keeps
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
(h : NodeInput G ctx tcLevel fuel false f bs fs parents)
(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)
:
Keeps parents (Frame.emit ctx tcLevel f).fst (Frame.emit ctx tcLevel f).snd
Every actual emission preserves the accumulated generator carriers at all surviving first ancestors, including the code-two coset exit.