def Hex.GraphIso.SameOrbit {n k : Nat} (G : Colored n k) (u v : Fin n) : Prop

Two vertices lie in one orbit of the automorphism group: some automorphism of G carries u to v.

Equations

• Hex.GraphIso.SameOrbit G u v = ∃ (p : Hex.Perm n), Hex.GraphIso.IsIso G G p ∧ p.get u = v

theorem Hex.GraphIso.SameOrbit.intro {n k : Nat} {G : Colored n k} {u v : Fin n} (p : Perm n) (hp : IsIso G G p) (h : p.get u = v) : SameOrbit G u v

theorem Hex.GraphIso.SameOrbit.elim {n k : Nat} {G : Colored n k} {u v : Fin n} (h : SameOrbit G u v) : ∃ (p : Perm n), IsIso G G p ∧ p.get u = v

theorem Hex.GraphIso.SameOrbit.refl {n k : Nat} (G : Colored n k) (u : Fin n) : SameOrbit G u u

theorem Hex.GraphIso.SameOrbit.symm {n k : Nat} {G : Colored n k} {u v : Fin n} (h : SameOrbit G u v) : SameOrbit G v u

theorem Hex.GraphIso.SameOrbit.trans {n k : Nat} {G : Colored n k} {u v w : Fin n} (h₁ : SameOrbit G u v) (h₂ : SameOrbit G v w) : SameOrbit G u w

def Hex.GraphIso.Aut.trace {n k : Nat} (G : Colored n k) : List (Array Nat)

The raw generator arrays the pinned traversal records, in discovery order.

Equations

• Hex.GraphIso.Aut.trace G = (Hex.GraphIso.Nauty.runColoredTraced G).autos.toList

def Hex.GraphIso.Aut.checked {n k : Nat} (G : Colored n k) : List (Array Nat × Perm n)

The recorded automorphisms that pass the check, each paired with the raw array it came from. One traversal, consulted once: the two projections below are the generator list and the arrays nauty's orbit bookkeeping is stated on.

Equations

• Hex.GraphIso.Aut.checked G = List.filterMap (fun (γ : Array Nat) => Option.map (fun (p : Hex.Perm n) => (γ, p)) (Hex.GraphIso.autom? G γ)) (Hex.GraphIso.Aut.trace G)

def Hex.GraphIso.Aut.gens {n k : Nat} (G : Colored n k) : List (Perm n)

The generators: the recorded traversal automorphisms that pass the check, in discovery order. Aut.trace_admitted in HexGraphIso.AutTrace proves that every recorded entry passes. Completeness uses the whole trace, including redundant code-2 entries; removing them would need a further generation proof.

Equations

• Hex.GraphIso.Aut.gens G = List.map (fun (x : Array Nat × Hex.Perm n) => x.snd) (Hex.GraphIso.Aut.checked G)

def Hex.GraphIso.Aut.raw {n k : Nat} (G : Colored n k) : List (Array Nat)

The raw arrays behind gens.

Equations

• Hex.GraphIso.Aut.raw G = List.map (fun (x : Array Nat × Hex.Perm n) => x.fst) (Hex.GraphIso.Aut.checked G)

theorem Hex.GraphIso.Aut.exists_perm_of_mem_raw {n k : Nat} {G : Colored n k} {γ : Array Nat} (h : γ ∈ raw G) : ∃ (p : Perm n), IsIso G G p ∧ ∀ (i : Fin n), ↑(p.get i) = γ[↑i]!

theorem Hex.GraphIso.Aut.lt_of_mem_raw {n k : Nat} {G : Colored n k} {γ : Array Nat} (h : γ ∈ raw G) (v : Nat) (hv : v < n) : γ[v]! < n

theorem Hex.GraphIso.Aut.inj_of_mem_raw {n k : Nat} {G : Colored n k} {γ : Array Nat} (h : γ ∈ raw G) (a b : Nat) : a < n → b < n → γ[a]! = γ[b]! → a = b

theorem Hex.GraphIso.Aut.gens_isIso {n k : Nat} {G : Colored n k} {p : Perm n} (h : p ∈ gens G) : IsIso G G p

Every checked generator is an automorphism. This is the membership guarantee stated on Aut.gens. autos_isIso is the same fact on the packaged AutResult.

def Hex.GraphIso.Aut.orbitsOf (n : Nat) (l : List (Array Nat)) : Array Nat

orbjoin folded over a generator list: the same computation the search performs on the generators it admits.

Equations

• Hex.GraphIso.Aut.orbitsOf n l = List.foldl (fun (o γ : Array Nat) => (Hex.GraphIso.Nauty.orbjoin o γ n).fst) (Array.ofFn fun (i : Fin n) => ↑i) l

def Hex.GraphIso.Aut.orbits {n k : Nat} (G : Colored n k) : Array Nat

nauty's vertex orbits. Every entry is the representative of its orbit.

Equations

• Hex.GraphIso.Aut.orbits G = Hex.GraphIso.Aut.orbitsOf n (Hex.GraphIso.Aut.raw G)

def Hex.GraphIso.Aut.countRoots (orb : Array Nat) (n : Nat) : Nat

The number of orbits recorded by an orbit array: the vertices that represent themselves.

Equations

• Hex.GraphIso.Aut.countRoots orb n = (List.filter (fun (v : Nat) => orb[v]! == v) (List.range n)).length

def Hex.GraphIso.Aut.sizeAt (orb : Array Nat) (n v : Nat) : Nat

The size of the orbit of v recorded by an orbit array.

Equations

• Hex.GraphIso.Aut.sizeAt orb n v = (List.filter (fun (u : Nat) => orb[u]! == orb[v]!) (List.range n)).length

def Hex.GraphIso.Aut.numOrbits {n k : Nat} (G : Colored n k) : Nat

The number of orbits.

Equations

• Hex.GraphIso.Aut.numOrbits G = Hex.GraphIso.Aut.countRoots (Hex.GraphIso.Aut.orbits G) n

def Hex.GraphIso.Aut.orbitSize {n k : Nat} (G : Colored n k) (v : Fin n) : Nat

The size of the orbit of v.

Equations

• Hex.GraphIso.Aut.orbitSize G v = Hex.GraphIso.Aut.sizeAt (Hex.GraphIso.Aut.orbits G) n ↑v

theorem Hex.GraphIso.Aut.orbSound {n k : Nat} (G : Colored n k) : Nauty.OrbSound (Nauty.OrbConn (raw G) n) (orbits G) n

theorem Hex.GraphIso.Aut.size_orbits {n k : Nat} (G : Colored n k) : (orbits G).size = n

theorem Hex.GraphIso.Aut.orbits_lt {n k : Nat} (G : Colored n k) {v : Nat} (hv : v < n) : (orbits G)[v]! < n

theorem Hex.GraphIso.Aut.sameOrbit_orbits {n k : Nat} (G : Colored n k) (v : Fin n) : SameOrbit G v ⟨(orbits G)[↑v]!, ⋯⟩

A vertex is carried onto its orbit representative by an automorphism.

theorem Hex.GraphIso.Aut.sameOrbit_of_orbits_eq {n k : Nat} (G : Colored n k) (u v : Fin n) (h : (orbits G)[↑u]! = (orbits G)[↑v]!) : SameOrbit G u v

Soundness of the orbit array: vertices sharing a representative really are in one orbit.

def Hex.GraphIso.Aut.indiv? {n k : Nat} (G : Colored n k) (v : Fin n) : Option (Colored n (k + 1))

Give v a colour of its own, at the end of the colour order. none when v is already alone in its cell, where the old colour would be left unused. Every colour-preserving automorphism of the result is an automorphism of G fixing v, so the search on it computes the stabilizer.

Equations

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

@[irreducible]

def Hex.GraphIso.Aut.orderAux (fuel : Nat) {n k : Nat} (G : Colored n k) (orb : Array Nat) : Nat

The orbit-stabilizer chain: multiply the length of one non-singleton orbit by the order of the stabilizer of a point in it, individualizing that point so that the search on the individualized colouring computes the stabilizer. orb is the orbit array of G, taken as an argument so that a caller holding it already does not pay for a second traversal.

fuel = n is enough: every successful individualization adds a colour, and a valid colouring has at most n colours. The theory companion proves this bound in orderAux_card with the invariant n ≤ k + fuel. At k = n, every automorphism fixes every vertex. indiv_of_orbitSize proves that the failure arm is unreachable when an orbit is non-singleton: colour-preserving automorphisms keep that orbit inside one colour cell.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Aut.orderAux 0 G orb = 1

def Hex.GraphIso.Aut.order {n k : Nat} (G : Colored n k) : Nat

The order of the full automorphism group, computed by the orbit-stabilizer chain. Aut.order_card in the theory companion proves its equality with the group's cardinality.

Equations

• Hex.GraphIso.Aut.order G = Hex.GraphIso.Aut.orderAux n G (Hex.GraphIso.Aut.orbits G)

structure Hex.GraphIso.AutResult (n : Nat) : Type

The automorphism data of a coloured graph: the generators the pinned traversal discovers, in discovery order, with the vertex orbits, the orbit count and the orbit-stabilizer product nauty derives from them.

• gens : List (Perm n)

  The generators, in the traversal's discovery order.

• orbits : Array Nat

  The orbit representative of each vertex.

• numOrbits : Nat

  The number of orbits.

• order : Nat

  The order of the full automorphism group.

def Hex.GraphIso.autos {n k : Nat} (G : Colored n k) : AutResult n

Generators of the automorphism group of a coloured graph, with the vertex orbits, the orbit count and the orbit-stabilizer product for the group order. Every returned permutation is an automorphism (autos_isIso). Vertices sharing an orbit representative are in one orbit (autos_sameOrbit_of_eq). HexGraphIso.AutComplete supplies the biconditional autos_sameOrbit and proves in autos_complete that the list generates the full group. The theory companion proves exact cardinality theorems for the orbit count and order. Computing the order runs one traversal per base point, so a caller who wants only the generators or the orbits should take Aut.gens or Aut.orbits.

Equations

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

theorem Hex.GraphIso.gens_autos {n k : Nat} (G : Colored n k) : (autos G).gens = Aut.gens G

The generator field is the generator list. The four projections are also available on their own, and a caller who wants only the generators should take Aut.gens: autos computes the group order too, and that runs one search per base point.

theorem Hex.GraphIso.orbits_autos {n k : Nat} (G : Colored n k) : (autos G).orbits = Aut.orbits G

The orbit field is the orbit array.

theorem Hex.GraphIso.numOrbits_autos {n k : Nat} (G : Colored n k) : (autos G).numOrbits = Aut.numOrbits G

The orbit-count field is the orbit count.

theorem Hex.GraphIso.order_autos {n k : Nat} (G : Colored n k) : (autos G).order = Aut.order G

The order field is the orbit-stabilizer product.

theorem Hex.GraphIso.autos_isIso {n k : Nat} {G : Colored n k} {p : Perm n} (h : p ∈ (autos G).gens) : IsIso G G p

Membership: every returned generator is an automorphism.

theorem Hex.GraphIso.size_autos_orbits {n k : Nat} (G : Colored n k) : (autos G).orbits.size = n

The orbit array has one entry per vertex.

theorem Hex.GraphIso.autos_orbits_lt {n k : Nat} (G : Colored n k) {v : Nat} (hv : v < n) : (autos G).orbits[v]! < n

Every orbit representative is a vertex.

theorem Hex.GraphIso.autos_sameOrbit_of_eq {n k : Nat} (G : Colored n k) (u v : Fin n) (h : (autos G).orbits[↑u]! = (autos G).orbits[↑v]!) : SameOrbit G u v

Soundness of the orbits: vertices sharing a representative are carried onto each other by an automorphism.