Hypercubes

The n-dimensional hypercube is represented as Boolean coordinate functions Fin n → Bool. Two vertices are adjacent when they differ in exactly one coordinate.

@[reducible, inline]

abbrev PebblingLean.HypercubeVertex (n : ℕ) : Type

Vertices of the n-cube.

Equations

• PebblingLean.HypercubeVertex n = (Fin n → Bool)

theorem PebblingLean.Hypercube.card_vertex (n : ℕ) : Fintype.card (HypercubeVertex n) = 2 ^ n

def PebblingLean.Hypercube.dist {n : ℕ} (x y : HypercubeVertex n) : ℕ

Hamming distance on Boolean coordinate functions.

Equations

• PebblingLean.Hypercube.dist x y = {i : Fin n | x i ≠ y i}.card

def PebblingLean.Hypercube.diffSet {n : ℕ} (x y : HypercubeVertex n) : Finset (Fin n)

Coordinates on which two hypercube vertices differ.

Equations

• PebblingLean.Hypercube.diffSet x y = {i : Fin n | x i ≠ y i}

theorem PebblingLean.Hypercube.dist_eq_card_diffSet {n : ℕ} (x y : HypercubeVertex n) : dist x y = (diffSet x y).card

theorem PebblingLean.Hypercube.dist_le {n : ℕ} (x y : HypercubeVertex n) : dist x y ≤ n

Hamming distance in Q_n is at most n.

def PebblingLean.Hypercube.fromDiffSet {n : ℕ} (base : HypercubeVertex n) (s : Finset (Fin n)) : HypercubeVertex n

The vertex obtained from base by flipping exactly the coordinates in s.

Equations

• PebblingLean.Hypercube.fromDiffSet base s i = if i ∈ s then !base i else base i

@[simp]

theorem PebblingLean.Hypercube.diffSet_fromDiffSet {n : ℕ} (base : HypercubeVertex n) (s : Finset (Fin n)) : diffSet base (fromDiffSet base s) = s

@[simp]

theorem PebblingLean.Hypercube.fromDiffSet_diffSet {n : ℕ} (base v : HypercubeVertex n) : fromDiffSet base (diffSet base v) = v

def PebblingLean.Hypercube.diffSetEquiv {n : ℕ} (base : HypercubeVertex n) : HypercubeVertex n ≃ Finset (Fin n)

Vertices of Q_n are equivalent to subsets of coordinates, by recording where they differ from a fixed base vertex.

Equations

• PebblingLean.Hypercube.diffSetEquiv base = { toFun := PebblingLean.Hypercube.diffSet base, invFun := PebblingLean.Hypercube.fromDiffSet base, left_inv := ⋯, right_inv := ⋯ }

theorem PebblingLean.Hypercube.card_sphere {n : ℕ} (base : HypercubeVertex n) (k : ℕ) : Fintype.card { v : HypercubeVertex n // dist base v = k } = n.choose k

The Hamming sphere of radius k around any fixed hypercube vertex has cardinality n choose k.

@[simp]

theorem PebblingLean.Hypercube.dist_self {n : ℕ} (x : HypercubeVertex n) : dist x x = 0

theorem PebblingLean.Hypercube.dist_eq_zero_iff {n : ℕ} {x y : HypercubeVertex n} : dist x y = 0 ↔ x = y

theorem PebblingLean.Hypercube.dist_comm {n : ℕ} (x y : HypercubeVertex n) : dist x y = dist y x

theorem PebblingLean.Hypercube.dist_triangle {n : ℕ} (x y z : HypercubeVertex n) : dist x z ≤ dist x y + dist y z

Hamming distance satisfies the triangle inequality.

def PebblingLean.Hypercube.graph (n : ℕ) : Graph (HypercubeVertex n)

The n-dimensional hypercube graph.

Equations

• PebblingLean.Hypercube.graph n = { Adj := fun (x y : PebblingLean.HypercubeVertex n) => PebblingLean.Hypercube.dist x y = 1, symm := ⋯, loopless := ⋯ }

theorem PebblingLean.Hypercube.dist_adj_le_succ {n : ℕ} {x y t : HypercubeVertex n} (hxy : (graph n).Adj x y) : dist x t ≤ dist y t + 1

Adjacent hypercube vertices have distances to any third vertex that differ by at most one in this direction.