def Hex.GraphIso.Mathlib.Sparse.encode {V : Type u} [Fintype V] {n k : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] : Sparse.Colored n k

Encode a Mathlib graph directly into sorted sparse rows. A general adjacency oracle requires testing vertex pairs, but no dense matrix is allocated. Each ordered colour is retained without renumbering.

Equations

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

theorem Hex.GraphIso.Mathlib.Sparse.encode_adj {V : Type u} [Fintype V] {n k : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] (i j : Fin n) : (encode e G).graph.adj i j = true ↔ G.graph.Adj (e.symm i) (e.symm j)

theorem Hex.GraphIso.Mathlib.Sparse.encode_color {V : Type u} [Fintype V] {n k : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] (i : Fin n) : (encode e G).coloring.cells[i] = G.color (e.symm i)

@[simp]

theorem Hex.GraphIso.Mathlib.Sparse.toDense_encode {V : Type u} [Fintype V] {n k : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] : (encode e G).toDense = Mathlib.encode e G

The two encodings have identical adjacency and ordered colours. This theorem is a proof bridge; sparse execution does not use toDense.

def Hex.GraphIso.Mathlib.Sparse.isoOfIsIso {V : Type u} {W : Type v} [Fintype V] [Fintype W] {n k : ℕ} {G : Colored V k} {H : Colored W k} [DecidableRel G.graph.Adj] [DecidableRel H.graph.Adj] (eV : V ≃ Fin n) (eW : W ≃ Fin n) {p : Perm n} (h : Sparse.IsIso (encode eV G) (encode eW H) p) : G.Iso H

Decode a verified native sparse transporter as a Mathlib isomorphism.

Equations

• Hex.GraphIso.Mathlib.Sparse.isoOfIsIso eV eW h = Hex.GraphIso.Mathlib.isoOfIsIso eV eW ⋯

theorem Hex.GraphIso.Mathlib.Sparse.isIso_of_iso {V : Type u} {W : Type v} [Fintype V] [Fintype W] {n k : ℕ} {G : Colored V k} {H : Colored W k} [DecidableRel G.graph.Adj] [DecidableRel H.graph.Adj] (eV : V ≃ Fin n) (eW : W ≃ Fin n) (h : G.Iso H) : Sparse.IsIso (encode eV G) (encode eW H) (Perm.ofEquiv (eV.symm.trans (h.graphIso.trans eW)))

theorem Hex.GraphIso.Mathlib.Sparse.encode_iso_iff {V : Type u} {W : Type v} [Fintype V] [Fintype W] {n k : ℕ} {G : Colored V k} {H : Colored W k} [DecidableRel G.graph.Adj] [DecidableRel H.graph.Adj] (eV : V ≃ Fin n) (eW : W ≃ Fin n) : G.Isomorphic H ↔ Sparse.Isomorphic (encode eV G) (encode eW H)

Isomorphism is independent of the chosen finite enumerations.