def Hex.GraphIso.Sparse.Kernel.rows {n : Nat} (G : SparseGraph n) : List (List Nat)

Sorted neighbour literals, with one list per vertex.

Equations

• Hex.GraphIso.Sparse.Kernel.rows G = List.ofFn fun (i : Fin n) => List.map Fin.val (G.nbrs i).toList

theorem Hex.GraphIso.Sparse.Kernel.atD_rows {n : Nat} (G : SparseGraph n) (i : Fin n) : atD (rows G) ↑i [] = List.map Fin.val (G.nbrs i).toList

theorem Hex.GraphIso.Sparse.Kernel.atD_perm {n : Nat} (p : Perm n) (i : Fin n) : atD (List.map Fin.val p.vec.toList) (↑i) 0 = ↑(p.get i)

theorem Hex.GraphIso.Sparse.Kernel.atD_color {n k : Nat} (c : Coloring n k) (i : Fin n) : atD (List.map Fin.val c.cells.toList) (↑i) 0 = ↑c.cells[i]

def Hex.GraphIso.Sparse.Kernel.checkIso (n : Nat) (rowsA rowsB : List (List Nat)) (cellsA cellsB images : List Nat) : Bool

Validate a forward transporter on sparse literals. Sorting each mapped neighbour list checks exact row equality without scanning non-edges. The accompanying soundness theorem requires a checked permutation and equalities identifying all literals with their original graph data.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Sparse.Kernel.checkIso_of_isIso {n k : Nat} {G H : Colored n k} {p : Perm n} (h : IsIso G H p) : checkIso n (rows G.graph) (rows H.graph) (List.map Fin.val G.coloring.cells.toList) (List.map Fin.val H.coloring.cells.toList) (List.map Fin.val p.vec.toList) = true

Every genuine transporter passes the sparse literal checker.

theorem Hex.GraphIso.Sparse.Kernel.isIso_of_checkIso {n k : Nat} {G H : Colored n k} {p : Perm n} {RA RB : List (List Nat)} {CA CB PL : List Nat} (hA : rows G.graph = RA) (hB : rows H.graph = RB) (hcA : List.map Fin.val G.coloring.cells.toList = CA) (hcB : List.map Fin.val H.coloring.cells.toList = CB) (hp : List.map Fin.val p.vec.toList = PL) (hchk : checkIso n RA RB CA CB PL = true) : IsIso G H p

A kernel check on identified sparse literals proves the transporter.

theorem Hex.GraphIso.Sparse.Kernel.isomorphic_of_checkIso {n k : Nat} {G H : Colored n k} {p : Perm n} {RA RB : List (List Nat)} {CA CB PL : List Nat} (hA : rows G.graph = RA) (hB : rows H.graph = RB) (hcA : List.map Fin.val G.coloring.cells.toList = CA) (hcB : List.map Fin.val H.coloring.cells.toList = CB) (hp : List.map Fin.val p.vec.toList = PL) (hchk : checkIso n RA RB CA CB PL = true) : Isomorphic G H

theorem Hex.GraphIso.Sparse.Kernel.checkIso_eq {n k : Nat} (G H : Colored n k) (p : Perm n) : checkIso n (rows G.graph) (rows H.graph) (List.map Fin.val G.coloring.cells.toList) (List.map Fin.val H.coloring.cells.toList) (List.map Fin.val p.vec.toList) = Sparse.checkIso G H p

Literal and native checking agree on the same checked permutation.