theorem
Hex.GraphIso.Nauty.Sparse.Generation.path_stab
{n k : Nat}
{G : Sparse.Colored n k}
{level : Nat}
{st : State n}
(h : PathInv G level st)
(hn : 0 < n)
{p : Perm n}
(hp : Sparse.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 sparse automorphism fixing the individualized vertices stabilizes the executed current partition. The raw array is interpreted by the existing path invariant; no graph search is performed here.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.window_stable
{n k : Nat}
{G : Sparse.Colored n k}
{level tc len : Nat}
{st : State n}
(h : PathInv G level st)
(hlab : LabOk st.lab n)
(hc : IsCell st.ptn level tc len)
(hr : tc + len ≤ st.lab.size)
{p : Perm n}
(hp : Sparse.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)
:
The true point stabilizer preserves every current target cell.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.terminal
{n k : Nat}
{G : Sparse.Colored n k}
{level : Nat}
{st : State n}
(h : PathInv G level st)
(hr : Ready G level n st)
(hn : 0 < n)
(hl : 1 ≤ level)
{p : Perm n}
(hp : Sparse.IsIso G G p)
(hfix : ∀ (v : Fin n), st.fixedpts.mem ↑v = true → p.get v = v)
:
A discrete reached partition has trivial point stabilizer. This provides the terminal case for generation along the actual first path.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.first_terminal
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{f : Max.Frame n}
{parents : Max.Parents n}
(h : Max.FirstInput G tcLevel f parents)
(hd : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).fst = n)
{base : List (Fin n)}
(hbase : ∀ (b : Fin n), f.entry.fixedpts.mem ↑b = true ↔ b ∈ base)
{gs : List (Perm n)}
{p : Perm n}
(hp : Sparse.IsIso G G p)
(hfix : Perm.Fixes base p)
:
Perm.Generated gs p
An actual first discrete visit generates the whole remaining point stabilizer with the empty word, since every such automorphism is identity.