def Hex.GraphIso.Nauty.ColorStab {n k : Nat} (G : Colored n k) (perm : Array Nat) : Prop

A permutation stabilizes the ordered colour cells of the initial partition.

Equations

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

def Hex.GraphIso.Nauty.TraceStab {n k : Nat} (G : Colored n k) (st : Search n) : Prop

Every recorded generator stabilizes the initial colour partition.

Equations

• Hex.GraphIso.Nauty.TraceStab G st = ∀ (perm : Array Nat), perm ∈ st.genTrace → Hex.GraphIso.Nauty.ColorStab G perm

theorem Hex.GraphIso.Nauty.TraceStab.congr {n k : Nat} {G : Colored n k} {st out : Search n} (h : TraceStab G st) (ht : out.genTrace = st.genTrace) : TraceStab G out

Retaining the trace retains its colour stabilization.

theorem Hex.GraphIso.Nauty.scatter_color {n k : Nat} {G : Colored n k} {ref : Array Nat} {st : Search n} (hn0 : 0 < n) (href : ref.size = n) (hperm : ref.toList.Perm (List.range n)) (hr : CellsReach G ref) (hl : CellsReach G st.lab) (hw : st.workperm.size = n) : ColorStab G (scatter ref st).workperm

Scattering two reached labellings preserves the initial colour cells.

theorem Hex.GraphIso.Nauty.classify_canon_stab {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st out : Search n} (hauto : classify ctx level numcells st = (Generic.Leaf.autoCanon, out)) (hn0 : 0 < n) (hw : st.workperm.size = n) (href : st.canonlab.size = n) (hr : CellsReach G st.canonlab) (hl : CellsReach G st.lab) : ColorStab G out.workperm

Canonical admissions preserve colours even if a failed first scan filled the scratch array.

theorem Hex.GraphIso.Nauty.classify_stab {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st : Search n} (hn0 : 0 < n) (hw : st.workperm.size = n) (hf : st.firstlab.size = n) (hfr : CellsReach G st.firstlab) (hc : st.canonlab.size = n) (hcr : CellsReach G st.canonlab) (hl : CellsReach G st.lab) : have result := classify ctx level numcells st; result.fst = Generic.Leaf.autoFirst ∨ result.fst = Generic.Leaf.autoCanon → ColorStab G result.snd.workperm

Both automorphism classifications fill the scratch array with a colour-stabilizing scatter.

theorem Hex.GraphIso.Nauty.TraceStab.leaf {n k : Nat} {G : Colored n k} {st : Search n} (h : TraceStab G st) (leaf : Leaf) (level : Nat) (hc : leaf = Generic.Leaf.autoFirst ∨ leaf = Generic.Leaf.autoCanon → ColorStab G st.workperm) : TraceStab G (leafExit leaf level st).snd

Leaf actions preserve colour stabilization when both admission cases supply it.