def Hex.GraphIso.Families.path (n : Nat) : Graph n

The path 0 - 1 - ⋯ - (n-1).

Equations

• Hex.GraphIso.Families.path n = Hex.Graph.ofRel fun (i j : Fin n) => ↑j == ↑i + 1

def Hex.GraphIso.Families.cycle (n : Nat) : Graph n

The cycle on n vertices in their natural order. For n ≤ 2 this degenerates to the path.

Equations

• Hex.GraphIso.Families.cycle n = Hex.Graph.ofRel fun (i j : Fin n) => ↑j == (↑i + 1) % n

def Hex.GraphIso.Families.circulant (n : Nat) (s : List Nat) : Graph n

The circulant graph: i and j are adjacent when their difference modulo n lies in the connection set (in either direction).

Equations

• Hex.GraphIso.Families.circulant n s = Hex.Graph.ofRel fun (i j : Fin n) => s.contains ((n + ↑j - ↑i) % n)

def Hex.GraphIso.Families.gpetersen (p q : Nat) : Graph (2 * p)

The generalized Petersen graph G(p, q) on 2p vertices: outer vertices 0..p-1 form a p-cycle, inner vertex p+i is adjacent to p+((i+q) mod p), and the spoke edges join i to p+i. G(5, 2) is the Petersen graph and G(5, 1) the pentagonal prism.

Equations

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

def Hex.GraphIso.Families.completeMultipartite (parts : List Nat) : Graph parts.sum

The complete multipartite graph over the given part sizes: vertices are numbered part by part in the given order, and two vertices are adjacent exactly when they lie in different parts.

Equations

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

def Hex.GraphIso.Families.completeMultipartite.partOf : List Nat → Nat → Nat

The index of the part containing flat vertex v.

Equations

• Hex.GraphIso.Families.completeMultipartite.partOf [] a✝ = 0
• Hex.GraphIso.Families.completeMultipartite.partOf (p :: rest) a✝ = if a✝ < p then 0 else 1 + Hex.GraphIso.Families.completeMultipartite.partOf rest (a✝ - p)

def Hex.GraphIso.Families.completeBipartite (a b : Nat) : Graph (a + b)

The complete bipartite graph K_{a,b}: vertices 0..a-1 on the left, a..a+b-1 on the right.

Equations

• Hex.GraphIso.Families.completeBipartite a b = Hex.Graph.ofRel fun (i j : Fin (a + b)) => decide (↑i < a) && decide (a ≤ ↑j)

def Hex.GraphIso.Families.copies (t : Nat) {m : Nat} (G : Graph m) : Graph (t * m)

t disjoint copies of a graph on m vertices: copy c occupies vertices c*m..(c+1)*m-1 in the original order.

Equations

• Hex.GraphIso.Families.copies t G = Hex.Graph.ofRel fun (i j : Fin (t * m)) => ↑i / m == ↑j / m && if h : m = 0 then false else G.adj ⟨↑i % m, ⋯⟩ ⟨↑j % m, ⋯⟩

def Hex.GraphIso.Families.grid (a b : Nat) : Graph (a * b)

The a × b grid: vertex (r, c) is numbered r*b + c, and vertices are adjacent when they differ by one in exactly one coordinate.

Equations

• Hex.GraphIso.Families.grid a b = Hex.Graph.ofRel fun (i j : Fin (a * b)) => ↑i / b == ↑j / b && ↑j % b == ↑i % b + 1 || ↑i % b == ↑j % b && ↑j / b == ↑i / b + 1

def Hex.GraphIso.Families.hypercube (d : Nat) : Graph (2 ^ d)

The hypercube of dimension d: vertices are the 2^d bitstrings, numbered by their value, adjacent when they differ in one bit.

Equations

• Hex.GraphIso.Families.hypercube d = Hex.Graph.ofRel fun (i j : Fin (2 ^ d)) => (List.range d).any fun (b : Nat) => ↑j == ↑i ^^^ 1 <<< b

def Hex.GraphIso.Families.choose (n r : Nat) : Nat

The binomial coefficient, by the multiplicative formula: the running product after i steps is choose n i, and multiplying it by n - i before dividing by i + 1 keeps every division exact. choose lives in Mathlib and this library is Mathlib-free.

Equations

• Hex.GraphIso.Families.choose n r = if n < r then 0 else List.foldl (fun (acc i : Nat) => acc * (n - i) / (i + 1)) 1 (List.range r)

def Hex.GraphIso.Families.unrankColex (m r v : Nat) : List Nat

The r-element subset of Fin m with colexicographic rank v: the standard combinatorial number system, choosing the largest possible top element greedily. Elements are returned in descending order.

Equations

• Hex.GraphIso.Families.unrankColex m r v = Hex.GraphIso.Families.unrankColex.go r v (m - 1) m

def Hex.GraphIso.Families.unrankColex.go : Nat → Nat → Nat → Nat → List Nat

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Families.unrankColex.go 0 a✝² a✝¹ a✝ = []
• Hex.GraphIso.Families.unrankColex.go n.succ a✝¹ a✝ 0 = []

def Hex.GraphIso.Families.johnson (m r : Nat) : Graph (choose m r)

The Johnson graph J(m, r) on the choose m r subsets of size r in colexicographic order, adjacent when the subsets share r - 1 elements.

Equations

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

def Hex.GraphIso.Families.kneser (m r : Nat) : Graph (choose m r)

The Kneser graph K(m, r) on the choose m r subsets of size r in colexicographic order, adjacent when the subsets are disjoint.

Equations

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

def Hex.GraphIso.Families.triangular (m : Nat) : Graph (choose m 2)

The triangular graph T(m) = J(m, 2).

Equations

• Hex.GraphIso.Families.triangular m = Hex.GraphIso.Families.johnson m 2

def Hex.GraphIso.Families.latinSquare (m : Nat) : Graph (m * m)

The Latin-square graph L₃(m) of the cyclic Latin square (r, c) ↦ (r + c) mod m: vertices are the m² cells numbered r * m + c, adjacent when they share a row, a column, or a symbol. For m ≥ 2 this is strongly regular with parameters (m², 3(m−1), m, 6). At m = 5 its parameters (25, 12, 5, 6) are those of the Paley graph on 25 vertices, but the two graphs are not isomorphic. That is the standard example of two non-isomorphic strongly regular graphs with the same parameters.

Equations

• Hex.GraphIso.Families.latinSquare m = Hex.Graph.ofRel fun (i j : Fin (m * m)) => ↑i != ↑j && (↑i / m == ↑j / m || ↑i % m == ↑j % m || (↑i / m + ↑i % m) % m == (↑j / m + ↑j % m) % m)

def Hex.GraphIso.Families.paley (q : Nat) : Graph q

The Paley graph on q vertices: i and j are adjacent when their difference is a nonzero quadratic residue modulo q, symmetrized. The intended domain is a prime q ≡ 1 (mod 4), where the residue relation is already symmetric.

Equations

• Hex.GraphIso.Families.paley q = Hex.Graph.ofRel fun (i j : Fin q) => (List.range q).any fun (x : Nat) => x != 0 && x * x % q == (q + ↑j - ↑i) % q