theorem
Hex.GraphIso.Nauty.Sparse.PathInv.pairs
{n k : Nat}
{G : Sparse.Colored n k}
{level : Nat}
{st : State n}
(h : PathInv G level st)
(hp : PairsOk G st)
:
LocalAutos (Graph.context G.graph) level st.frame
The native path invariant transports the root workspace to precisely the pairs whose fixed sets cover the current individualized vertices.
theorem
Hex.GraphIso.Nauty.Sparse.PairsReady.long_drop
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel level numcells v : Nat}
{st : State n}
(h : PairsReady G tcLevel level numcells st)
{cell : VSet n}
(hv : v < n)
(hm : cell.mem v = true)
(hd : (Generic.Policy.longprune cell st).mem v = false)
:
Every member removed by the native long filter is moved to a smaller vertex by a checked automorphism stabilizing the current partition.
theorem
Hex.GraphIso.Nauty.Sparse.PairsReady.long_carried
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel level numcells tc len : Nat}
{st : State n}
(h : PairsReady G tcLevel level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(hc : IsCell st.ptn level tc len)
(hb : tc + len ≤ n)
(v : Fin n)
(hv : (windowSet n st.lab tc len).mem ↑v = true)
:
∃ (gamma : Array Nat), checkAutom (Graph.context G.graph).g gamma = true ∧ (∀ (u : Nat), u < n → st.fixedpts.mem u = true → gamma[u]! = u) ∧ CellStab st.ptn level st.lab gamma ∧ (windowSet n st.lab tc len).mem gamma[↑v]! = true ∧ (Generic.Policy.longprune (windowSet n st.lab tc len) st).mem gamma[↑v]! = true
Long filtering a whole current cell retains a representative reached by a checked automorphism fixing the current path. The proof concerns the literal native filter and does not assume complete generator discovery.