Paths in hypercubes

This file connects Hamming distance to the graph-walk API: vertices at Hamming distance d are joined by a walk of length d. This is the geometric input needed for direct delivery in the upper-bound proof.

@[simp]

theorem PebblingLean.Hypercube.fromDiffSet_empty {n : ℕ} (base : HypercubeVertex n) : fromDiffSet base ∅ = base

theorem PebblingLean.Hypercube.diffSet_fromDiffSet_insert {n : ℕ} (base : HypercubeVertex n) {s : Finset (Fin n)} {i : Fin n} (hi : i ∉ s) : diffSet (fromDiffSet base s) (fromDiffSet base (insert i s)) = {i}

theorem PebblingLean.Hypercube.adj_fromDiffSet_insert {n : ℕ} (base : HypercubeVertex n) {s : Finset (Fin n)} {i : Fin n} (hi : i ∉ s) : (graph n).Adj (fromDiffSet base s) (fromDiffSet base (insert i s))

Flipping one new coordinate gives an adjacent hypercube vertex.

theorem PebblingLean.Hypercube.exists_walk_fromDiffSet_to_base {n : ℕ} (base : HypercubeVertex n) (s : Finset (Fin n)) : ∃ (walk : (graph n).Walk (fromDiffSet base s) base), Graph.Walk.length (graph n) walk = s.card

Flipping the coordinates in s, one at a time, gives a walk back to the base vertex of length s.card.

theorem PebblingLean.Hypercube.exists_walk_length_dist {n : ℕ} (x y : HypercubeVertex n) : ∃ (walk : (graph n).Walk x y), Graph.Walk.length (graph n) walk = dist x y

Hypercube Hamming distance is realized by a graph walk of the same length.

theorem PebblingLean.Hypercube.canReachAtLeast_single_dist {n : ℕ} (center target : HypercubeVertex n) (T : ℕ) : Pebbling.CanReachAtLeast (graph n) (Pebbling.single center (T * 2 ^ dist center target)) target T

A single pile of T * 2^d pebbles can directly deliver T pebbles across Hamming distance d.