def Hex.SparseGraph.toColored {n : Nat} (G : SparseGraph n) : GraphIso.Sparse.Colored n (min n 1)

The native uncoloured view has one colour on nonempty graphs and no colours on the empty graph. Both cases retain the original sparse graph.

Equations

• G.toColored = { graph := G, coloring := { cells := Hex.Vector.ofFn' fun (i : Fin n) => ⟨0, ⋯⟩, onto := ⋯ } }

theorem Hex.SparseGraph.isIso_toColored_iff {n : Nat} (G H : SparseGraph n) (p : Perm n) : GraphIso.Sparse.IsIso G.toColored H.toColored p ↔ G.IsIso H p

The zero-or-one-colour view has precisely the bare graph's forward isomorphisms, including the empty graph.

theorem Hex.SparseGraph.isomorphic_toColored_iff {n : Nat} (G H : SparseGraph n) : GraphIso.Sparse.Isomorphic G.toColored H.toColored ↔ G.Isomorphic H

structure Hex.SparseGraph.CanonResult (n : Nat) : Type

A bare sparse canonical form and its new-to-old labelling.

• form : SparseGraph n
• label : GraphIso.Label n

def Hex.SparseGraph.instDecidableEqCanonResult.decEq {n✝ : Nat} (x✝ x✝¹ : CanonResult n✝) : Decidable (x✝ = x✝¹)

Equations

• Hex.SparseGraph.instDecidableEqCanonResult.decEq { form := a, label := a_1 } { form := b, label := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.SparseGraph.instDecidableEqCanonResult {n✝ : Nat} : DecidableEq (CanonResult n✝)

Equations

• Hex.SparseGraph.instDecidableEqCanonResult = Hex.SparseGraph.instDecidableEqCanonResult.decEq

def Hex.SparseGraph.canonicalize {n : Nat} (G : SparseGraph n) : CanonResult n

Total native canonicalization of a bare sparse graph. The internal colouring represents its sole cell, including the zero-cell empty case.

Equations

• G.canonicalize = { form := (Hex.GraphIso.Sparse.canonicalize G.toColored).form.graph, label := (Hex.GraphIso.Sparse.canonicalize G.toColored).label }

def Hex.SparseGraph.canon {n : Nat} (G : SparseGraph n) : SparseGraph n

Equations

• G.canon = G.canonicalize.form

def Hex.SparseGraph.label {n : Nat} (G : SparseGraph n) : GraphIso.Label n

Equations

• G.label = G.canonicalize.label

def Hex.SparseGraph.findIso {n : Nat} (G H : SparseGraph n) : Option (Perm n)

Equations

• G.findIso H = Hex.GraphIso.Sparse.findIso G.toColored H.toColored

def Hex.SparseGraph.isIso {n : Nat} (G H : SparseGraph n) : Bool

Equations

• G.isIso H = (G.findIso H).isSome

theorem Hex.SparseGraph.canon_toColored {n : Nat} (G : SparseGraph n) : G.canon = (GraphIso.Sparse.canon G.toColored).graph

The bare result uses precisely the native coloured search's form.

theorem Hex.SparseGraph.label_toColored {n : Nat} (G : SparseGraph n) : G.label = GraphIso.Sparse.label G.toColored

theorem Hex.SparseGraph.relabel_label {n : Nat} (G : SparseGraph n) : G.relabel G.label.perm = G.canon

theorem Hex.SparseGraph.label_toArray {n : Nat} (G : SparseGraph n) : G.label.toArray = (GraphIso.Nauty.Sparse.runColored G.toColored).canonlab

The wrapper exposes the literal optimized search's canonical-label array.

theorem Hex.SparseGraph.canon_iso {n : Nat} (G : SparseGraph n) : G.Isomorphic G.canon

theorem Hex.SparseGraph.findIso_sound {n : Nat} {G H : SparseGraph n} {p : Perm n} (h : G.findIso H = some p) : G.IsIso H p

Every returned bare transporter preserves native adjacency.

theorem Hex.SparseGraph.isomorphic_of_isIso {n : Nat} {G H : SparseGraph n} (h : G.isIso H = true) : G.Isomorphic H

theorem Hex.SparseGraph.canon_invariant {n : Nat} {G H : SparseGraph n} (h : G.Isomorphic H) : G.canon = H.canon

Bare sparse canonical forms are invariant at every order, including the zero-colour empty case of the native wrapper.

theorem Hex.SparseGraph.iso_iff_canon_eq {n : Nat} (G H : SparseGraph n) : G.Isomorphic H ↔ G.canon = H.canon

theorem Hex.SparseGraph.canon_idempotent {n : Nat} (G : SparseGraph n) : G.canon.canon = G.canon

theorem Hex.SparseGraph.findIso_complete {n : Nat} {G H : SparseGraph n} (h : G.Isomorphic H) : ∃ (p : Perm n), G.findIso H = some p

theorem Hex.SparseGraph.findIso_isSome_iff {n : Nat} (G H : SparseGraph n) : (G.findIso H).isSome = true ↔ G.Isomorphic H

theorem Hex.SparseGraph.isIso_eq_true_iff {n : Nat} (G H : SparseGraph n) : G.isIso H = true ↔ G.Isomorphic H

theorem Hex.SparseGraph.isIso_eq_false_iff {n : Nat} (G H : SparseGraph n) : G.isIso H = false ↔ ¬G.Isomorphic H

theorem Hex.SparseGraph.findIso_eq_none_iff {n : Nat} (G H : SparseGraph n) : G.findIso H = none ↔ ¬G.Isomorphic H