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

Decode the complete native sparse generator list into Mathlib colour-preserving automorphisms, retaining its order and every entry.

Equations

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

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

The orbit count computed by the native sparse search.

Equations

• Hex.GraphIso.Mathlib.Sparse.autNumOrbits e G = Hex.GraphIso.Sparse.Aut.numOrbits (Hex.GraphIso.Mathlib.Sparse.encode e G)

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

The first-path index product computed by one native sparse search.

Equations

• Hex.GraphIso.Mathlib.Sparse.autOrder e G = Hex.GraphIso.Sparse.Aut.order (Hex.GraphIso.Mathlib.Sparse.encode e G)

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

Native sparse encoding identifies the full automorphism groups.

Equations

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

theorem Hex.GraphIso.Mathlib.Sparse.autos_complete {V : Type u} [Fintype V] {n k : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] (f : G.Iso G) : f ∈ Subgroup.closure {g : G.Iso G | g ∈ autos e G}

Every Mathlib colour-preserving automorphism is generated by the decoded output of the native sparse traversal.

theorem Hex.GraphIso.Mathlib.Sparse.autos_sameOrbit {V : Type u} [Fintype V] {n k : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] (v w : V) : (Sparse.Aut.orbits (encode e G))[↑(e v)]! = (Sparse.Aut.orbits (encode e G))[↑(e w)]! ↔ ∃ (f : G.Iso G), f.graphIso v = w

The actual sparse representative array classifies the full Mathlib automorphism orbits for any finite enumeration.

noncomputable def Hex.GraphIso.Mathlib.Sparse.autOrbitEquiv {V : Type u} [Fintype V] {n k : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] : MulAction.orbitRel.Quotient (G.Iso G) V ≃ MulAction.orbitRel.Quotient (↥(Sparse.Aut.group (encode e G))) (Fin n)

Equations

• Hex.GraphIso.Mathlib.Sparse.autOrbitEquiv e G = Quotient.congr e ⋯

theorem Hex.GraphIso.Mathlib.Sparse.autNumOrbits_card {V : Type u} [Fintype V] {n k : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] : autNumOrbits e G = Nat.card (MulAction.orbitRel.Quotient (G.Iso G) V)

The native sparse orbit count equals the number of full Mathlib automorphism orbits, including empty graphs and arbitrary enumerations.

theorem Hex.GraphIso.Mathlib.Sparse.autOrder_card {V : Type u} [Fintype V] {n k : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] : autOrder e G = Nat.card (G.Iso G)

The product accumulated by the native sparse traversal is the order of the full Mathlib automorphism group for any chosen enumeration.