theorem
Hex.GraphIso.Nauty.Generation.initial_stab
{n k : Nat}
{G : Colored n k}
{p : Perm n}
(hp : IsIso G G p)
(hn : 0 < n)
:
CellStab (initPtn n (n + 2) (initialPartition G).snd) 1 (initialPartition G).fst (renamingArray (renamingOf p))
Every graph automorphism stabilizes the initial ordered colour cells. The raw representation is the same one used by the pruning checker.
theorem
Hex.GraphIso.Nauty.Generation.path_stab
{n k : Nat}
{G : Colored n k}
{st : SearchSt n}
{level : Nat}
(hn : 0 < n)
(hpath : PathStab { g := rowsOf G } (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
{p : Perm n}
(hp : IsIso G G p)
(hfix : ∀ (v : Fin n), st.fixedpts.mem ↑v = true → p.get v = v)
:
CellStab st.ptn level st.lab (renamingArray (renamingOf p))
A true automorphism fixing the individualized path stabilizes the current cells in the raw representation used by search pruning.
theorem
Hex.GraphIso.Nauty.Generation.window_stable
{n k : Nat}
{G : Colored n k}
{st : SearchSt n}
{level tc len : Nat}
(hpath : PathStab { g := rowsOf G } (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
(hlab : LabOk st.lab n)
(hcell : IsCell st.ptn level tc len)
(hrange : tc + len ≤ st.lab.size)
{p : Perm n}
(hp : IsIso G G p)
(hfix : ∀ (v : Fin n), st.fixedpts.mem ↑v = true → p.get v = v)
(v : Fin n)
(hv : (windowSet n st.lab tc len).mem ↑v = true)
:
Every target cell is invariant under the true point stabilizer of the current individualized path.
theorem
Hex.GraphIso.Nauty.Generation.discrete_fixes
{n : Nat}
{ptn lab γ : Array Nat}
{level : Nat}
(hstab : CellStab ptn level lab γ)
(hsize : lab.size = n)
(hperm : lab.toList.Perm (List.range n))
(hptn : ptn.size = n)
(hend : ptn[ptn.size - 1]! ≤ level)
(hdisc : discreteAt ptn level n = true)
(v : Nat)
:
At a discrete partition, a cell stabilizer fixes every vertex.
theorem
Hex.GraphIso.Nauty.Generation.terminal
{n k : Nat}
{G : Colored n k}
{st : SearchSt n}
{level : Nat}
(hpath : PathStab { g := rowsOf G } (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st)
(hsize : st.lab.size = n)
(hperm : st.lab.toList.Perm (List.range n))
(hptn : st.ptn.size = n)
(hend : st.ptn[st.ptn.size - 1]! ≤ level)
(hdisc : discreteAt st.ptn level n = true)
{p : Perm n}
(hp : IsIso G G p)
(hfix : ∀ (v : Fin n), st.fixedpts.mem ↑v = true → p.get v = v)
:
The pointwise stabilizer of an individualized path is trivial once refinement is discrete. This is the terminal case of the stabilizer chain.