theorem Hex.GraphIso.Aut.indiv_isIso_map {n k : ℕ} {G : Colored n k} {v w : Fin n} {Hv Hw : Colored n (k + 1)} (hv : indiv? G v = some Hv) (hw : indiv? G w = some Hw) {p : Perm n} (hp : IsIso G G p) (hpvw : p.get v = w) : IsIso Hv Hw p

An automorphism carrying v to w identifies the two colourings obtained by individualizing those vertices.

structure Hex.GraphIso.Aut.Kernel.KeyCert : Type

One checked canonical key.

• cert : Nauty.CertNode
• key : Kernel.Key

@[instance_reducible]

instance Hex.GraphIso.Aut.Kernel.instInhabitedKeyCert : Inhabited KeyCert

Equations

• Hex.GraphIso.Aut.Kernel.instInhabitedKeyCert = { default := { cert := Hex.GraphIso.Nauty.CertNode.leaf, key := { codes := [], rows := [] } } }

structure Hex.GraphIso.Aut.Kernel.Separation : Type

Evidence excluding one vertex as the image of a level's base point.

• vertex : ℕ
• witness : KeyCert

@[instance_reducible]

instance Hex.GraphIso.Aut.Kernel.instInhabitedSeparation : Inhabited Separation

Equations

• Hex.GraphIso.Aut.Kernel.instInhabitedSeparation = { default := { vertex := 0, witness := default } }

structure Hex.GraphIso.Aut.Kernel.Level : Type

One point-stabilizer level.

• base : ℕ
• orbit : List ℕ
• reference : KeyCert
• excluded : List Separation

@[instance_reducible]

instance Hex.GraphIso.Aut.Kernel.instInhabitedLevel : Inhabited Level

Equations

• Hex.GraphIso.Aut.Kernel.instInhabitedLevel = { default := { base := 0, orbit := [], reference := default, excluded := [] } }

inductive Hex.GraphIso.Aut.Kernel.Certificate : Type

A point-stabilizer certificate.

• done : Certificate
• step (level : Level) (rest : Certificate) : Certificate

@[instance_reducible]

instance Hex.GraphIso.Aut.Kernel.instInhabitedCertificate : Inhabited Certificate

Equations

• Hex.GraphIso.Aut.Kernel.instInhabitedCertificate = { default := Hex.GraphIso.Aut.Kernel.Certificate.done }

def Hex.GraphIso.Aut.Kernel.Certificate.bound : Certificate → ℕ

The product of the recorded orbit bounds.

Equations

• Hex.GraphIso.Aut.Kernel.Certificate.done.bound = 1
• (Hex.GraphIso.Aut.Kernel.Certificate.step L rest).bound = L.orbit.length * rest.bound

def Hex.GraphIso.Aut.Kernel.Level.find? (L : Level) (w : ℕ) : Option KeyCert

Find the exclusion evidence for a vertex.

Equations

• L.find? w = Option.map (fun (e : Hex.GraphIso.Aut.Kernel.Separation) => e.witness) (List.find? (fun (e : Hex.GraphIso.Aut.Kernel.Separation) => e.vertex == w) L.excluded)

def Hex.GraphIso.Aut.Kernel.Level.checkImage {n k : ℕ} (G : Colored n k) (rows : ℕ) (v : Fin n) (_Hv : Colored n (k + 1)) (L : Level) (w : ℕ) : Bool

Check the evidence for one possible image of the base point.

Equations

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

def Hex.GraphIso.Aut.Kernel.Level.check {n k : ℕ} (G : Colored n k) (rows : ℕ) (v : Fin n) (Hv : Colored n (k + 1)) (L : Level) : Bool

Check one level, including its reference key and every excluded image.

Equations

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

def Hex.GraphIso.Aut.Kernel.check {n k : ℕ} : Colored n k → ℕ → Certificate → Bool

Replay a point-stabilizer certificate. Every successful step adds one colour, so a terminal certificate is accepted only after the colouring has at least as many colours as vertices.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Aut.Kernel.check x✝¹ x✝ Hex.GraphIso.Aut.Kernel.Certificate.done = decide (n ≤ x✝²)

theorem Hex.GraphIso.Aut.Kernel.check_step {n k : ℕ} {G : Colored n k} {rows : ℕ} (L : Level) {rest : Certificate} (hv : L.base < n) {H : Colored n (k + 1)} (hH : indiv? G ⟨L.base, hv⟩ = some H) (hL : Level.check G rows ⟨L.base, hv⟩ H L = true) (hrest : check H rows rest = true) : check G rows (Certificate.step L rest) = true

Assemble an accepted step from separately replayed level and suffix certificates. The tactic uses this theorem to keep each kernel reduction small.

def Hex.GraphIso.Aut.Kernel.certify? {n k : ℕ} (budget : ℕ) (G : Colored n k) : Option Certificate

Run the untrusted automorphism and canonical-form searches and record a point-stabilizer certificate for kernel replay. budget bounds each canonical-form certificate search.

Equations

• Hex.GraphIso.Aut.Kernel.certify? budget G = Hex.GraphIso.Aut.Kernel.certifyAux✝ budget n G

theorem Hex.GraphIso.Aut.Kernel.Level.image_mem {n k : ℕ} {G : Colored n k} {rows : ℕ} {v : Fin n} {Hv : Colored n (k + 1)} {L : Level} (hrows : Kernel.packRows n G.graph.adjMatrix.data.toList = rows) (hHv : indiv? G v = some Hv) (hcheck : check G rows v Hv L = true) {p : Perm n} (hp : IsIso G G p) : ↑(p.get v) ∈ L.orbit

An accepted level contains the image of its base point under every automorphism of the current coloured graph.

theorem Hex.GraphIso.Aut.Kernel.Level.orbitSize_le {n k : ℕ} {G : Colored n k} {rows : ℕ} {v : Fin n} {Hv : Colored n (k + 1)} {L : Level} (hrows : Kernel.packRows n G.graph.adjMatrix.data.toList = rows) (hHv : indiv? G v = some Hv) (hcheck : check G rows v Hv L = true) : orbitSize G v ≤ L.orbit.length

The list at an accepted level bounds the actual orbit of its base point.

theorem Hex.GraphIso.Aut.Kernel.card_le_bound {n k : ℕ} {G : Colored n k} {rows : ℕ} {c : Certificate} (hrows : Kernel.packRows n G.graph.adjMatrix.data.toList = rows) (hcheck : check G rows c = true) : Nat.card ↥(group G) ≤ c.bound

Acceptance bounds the full automorphism-group order by the product of the recorded point-orbit bounds.

theorem Hex.GraphIso.Aut.Kernel.order_le_bound {n k : ℕ} {G : Colored n k} {rows : ℕ} {c : Certificate} (hrows : Kernel.packRows n G.graph.adjMatrix.data.toList = rows) (hcheck : check G rows c = true) : order G ≤ c.bound

Acceptance bounds the order reported by the executable automorphism search.

def Hex.GraphIso.Aut.equivGroup {n k : ℕ} (G : Colored n k) : Subgroup (Equiv.Perm (Fin n))

The full colour-preserving automorphism group as a Mathlib subgroup of Equiv.Perm (Fin n).

Equations

• Hex.GraphIso.Aut.equivGroup G = Subgroup.map Hex.Perm.equiv.toMonoidHom (Hex.GraphIso.Aut.group G)

@[simp]

theorem Hex.GraphIso.Aut.mem_equivGroup {n k : ℕ} (G : Colored n k) (p : Equiv.Perm (Fin n)) : p ∈ equivGroup G ↔ IsIso G G (Perm.ofEquiv p)

theorem Hex.GraphIso.Aut.equivGroup_eq_mapClosure {n k : ℕ} (G : Colored n k) : equivGroup G = Subgroup.map Perm.equiv.toMonoidHom (Subgroup.closure {p : Perm n | p ∈ gens G})

The existing completeness theorem, transported to the Mathlib-facing permutation representation.

theorem Hex.GraphIso.Aut.card_equivGroup {n k : ℕ} (G : Colored n k) : Nat.card ↥(equivGroup G) = Nat.card ↥(group G)

The executable and Mathlib-facing presentations of the full automorphism group have the same cardinality.

theorem Hex.GraphIso.Aut.isIso_nil {n k : ℕ} (G : Colored n k) (g : Equiv.Perm (Fin n)) : g ∈ [] → IsIso G G (Perm.ofEquiv g)

theorem Hex.GraphIso.Aut.isIso_cons {n k : ℕ} {G : Colored n k} {g : Equiv.Perm (Fin n)} {gs : List (Equiv.Perm (Fin n))} (hg : IsIso G G (Perm.ofEquiv g)) (hgs : ∀ p ∈ gs, IsIso G G (Perm.ofEquiv p)) (p : Equiv.Perm (Fin n)) : p ∈ g :: gs → IsIso G G (Perm.ofEquiv p)

theorem Hex.GraphIso.Aut.closure_eq_equivGroup {n k : ℕ} {G : Colored n k} {gs : List (Equiv.Perm (Fin n))} {gc : Kernel.Certificate} {rows N : ℕ} (hrows : Kernel.packRows n G.graph.adjMatrix.data.toList = rows) (hgraph : Kernel.check G rows gc = true) (hgens : ∀ g ∈ gs, IsIso G G (Perm.ofEquiv g)) (hcard : Nat.card ↥(Subgroup.closure {g : Equiv.Perm (Fin n) | g ∈ gs}) = N) (hbound : gc.bound = N) : Subgroup.closure {g : Equiv.Perm (Fin n) | g ∈ gs} = equivGroup G

A certified lower bound of the same size as the graph certificate's upper bound identifies a generator subgroup with the full automorphism group.

theorem Hex.GraphIso.Aut.card_equivGroup_eq {n k : ℕ} {G : Colored n k} {gs : List (Equiv.Perm (Fin n))} {gc : Kernel.Certificate} {rows N : ℕ} (hrows : Kernel.packRows n G.graph.adjMatrix.data.toList = rows) (hgraph : Kernel.check G rows gc = true) (hgens : ∀ g ∈ gs, IsIso G G (Perm.ofEquiv g)) (hcard : Nat.card ↥(Subgroup.closure {g : Equiv.Perm (Fin n) | g ∈ gs}) = N) (hbound : gc.bound = N) : Nat.card ↥(equivGroup G) = N

A generator subgroup certified to meet the graph certificate's upper bound determines the full automorphism-group order.

def Hex.GraphIso.Mathlib.graphAutEquiv {V : Type u} [Fintype V] (G : SimpleGraph V) (h : 0 < Fintype.card V) : G ≃g G ≃ (onecell G h).Iso (onecell G h)

A bare graph automorphism is the same thing as an automorphism of its one-cell coloured view.

Equations

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

theorem Hex.GraphIso.Mathlib.card_coloredIso {V : Type u} [Fintype V] {n k : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] : Nat.card (G.Iso G) = Nat.card ↥(Aut.equivGroup (encode e G))

Encoding identifies the cardinality of a Mathlib coloured graph's automorphism type with the executable graph's Equiv.Perm subgroup.

theorem Hex.GraphIso.Mathlib.card_graphIso {V : Type u} [Fintype V] {n : ℕ} (e : V ≃ Fin n) (G : SimpleGraph V) [DecidableRel G.Adj] (h : 0 < Fintype.card V) : Nat.card (G ≃g G) = Nat.card ↥(Aut.equivGroup (encode e (onecell G h)))

The corresponding cardinality identity for an uncoloured Mathlib graph.