def
Hex.GraphIso.Nauty.Sparse.Replay.checkAutom
{n : Nat}
(G : SparseGraph n)
(level : Nat)
(lab out ptn raw : Array Nat)
:
Check a raw automorphism and its transport of the current ordered cells to another sibling. Parsing checks the entire permutation; graph checking uses sparse generation marks. The cell test operates only on label segments.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.Replay.checkAutom_sound
{n : Nat}
{G : SparseGraph n}
{level : Nat}
{lab out ptn raw : Array Nat}
(hp : lab.size = n)
(hq : out.size = n)
(hs : ptn.size = n)
(hend : ptn[ptn.size - 1]! ≤ level)
(h : checkAutom G level lab out ptn raw = true)
:
Every accepted witness is an actual graph automorphism transporting the complete ordered partition, not just the individualized vertex.
theorem
Hex.GraphIso.Nauty.Sparse.Replay.Valid.map
{n : Nat}
{G : SparseGraph n}
{B : Key n}
{a : Bool}
{tcLevel fuel level numcells : Nat}
{lab out ptn : Array Nat}
{active : VSet n}
(hg : SpecNode G level lab ptn active numcells)
(hh : SpecNode G level out ptn active numcells)
(p : Perm n)
(hiso : ∀ (i j : Fin n), G.adj (p.get i) (p.get j) = G.adj i j)
(hc : cellsPerm ptn level out (Array.map (renamingOf p).toFun lab))
(h : Valid G B (specLeaves G tcLevel fuel level lab ptn active numcells) a)
:
Valid G B (specLeaves G tcLevel fuel level out ptn active numcells) a
A checked earlier sibling's bound and attainment transfer through a genuine automorphism. Both directions use actual sparse leaf transport.