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

The full native colour-preserving automorphism orbit relation.

Equations

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

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

Decode the complete emitted trace of one native sparse traversal.

Equations

• Hex.GraphIso.Sparse.Aut.gens G = (Hex.GraphIso.Nauty.Sparse.runColored G).generators

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

The least representatives stored by the native traversal.

Equations

• Hex.GraphIso.Sparse.Aut.orbits G = (Hex.GraphIso.Nauty.Sparse.runColored G).orbits

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

The orbit count accumulated by the native joins.

Equations

• Hex.GraphIso.Sparse.Aut.numOrbits G = (Hex.GraphIso.Nauty.Sparse.runColored G).numorbits

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

The product of first-path indices accumulated by the native search. This projection performs one traversal and no individualized reruns.

Equations

• Hex.GraphIso.Sparse.Aut.order G = (Hex.GraphIso.Nauty.Sparse.runColored G).order

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

theorem Hex.GraphIso.Sparse.Aut.complete {n k : Nat} (G : Colored n k) {p : Perm n} (hp : IsIso G G p) : Perm.Generated (gens G) p

theorem Hex.GraphIso.Sparse.Aut.generated_iff {n k : Nat} (G : Colored n k) (p : Perm n) : Perm.Generated (gens G) p ↔ IsIso G G p

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

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

theorem Hex.GraphIso.Sparse.Aut.orbits_flat {n k : Nat} (G : Colored n k) : Nauty.Orbit.Flat (orbits G) n

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

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

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

theorem Hex.GraphIso.Sparse.Aut.numOrbits_eq_count {n k : Nat} (G : Colored n k) : numOrbits G = List.countP (fun (i : Nat) => (orbits G)[i]! == i) (List.range n)

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

The native generator list, orbit representatives, orbit count and first-path index product, extracted together from one sparse traversal.

Equations

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

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

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

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

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

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

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

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