def
Hex.GraphIso.Nauty.Sparse.vertexKey
{n : Nat}
(G : SparseGraph n)
(tcLevel fuel level : Nat)
(lab ptn : Array Nat)
(tc numcells v : Nat)
:
Key n
The unpruned sparse child maximum indexed by its literal chosen vertex.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.Ready.window_target
{n k : Nat}
{G : Sparse.Colored n k}
{level numcells tc len : Nat}
{st : State n}
(_h : Ready G level numcells st)
(hc : IsCell st.ptn level tc len)
(hlen : 1 < len)
(hr : tc + len ≤ n)
:
Generic.Target State.frame level tc (windowSet n st.lab tc len) st
A full parent cell is a valid target for each of its native children.
theorem
Hex.GraphIso.Nauty.Sparse.Ready.vertex_key
{n k : Nat}
{G : Sparse.Colored n k}
{level numcells tc len v fuel : Nat}
{st : State n}
{gamma : Array Nat}
(h : Ready G level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(ha : checkAutom (Graph.context G.graph).g gamma = true)
(hstab : CellStab st.ptn level st.lab gamma)
(hc : IsCell st.ptn level tc len)
(hlen : 1 < len)
(hr : tc + len ≤ n)
(hv : (windowSet n st.lab tc len).mem v = true)
(hf : n < fuel + (numcells + 1))
(tcLevel : Nat)
:
A checked automorphism stabilizing the current cells identifies the entire native child maxima at the vertices it carries. The proof transports every unpruned leaf through the actual individualization and sparse dispatch.