Snake in the box

References:

• Wikipedia
• Hypercube
• xkcd

def SnakeInBox.Hypercube (n : ℕ) : SimpleGraph (Finset (Fin n))

A graph on the power set of Fin n, where two sets are adjacent if they differ by a single element.

Equations

• SnakeInBox.Hypercube n = SimpleGraph.fromRel fun (a b : Finset (Fin n)) => (symmDiff a b).card = 1

def SnakeInBox.IsSnakeInGraphOfLength {V : Type u} [DecidableEq V] (G : SimpleGraph V) (G' : G.Subgraph) (k : ℕ) : Prop

A subgraph G' is a 'snake' of length k in graph G if it is an induced path of length k.

Equations

• SnakeInBox.IsSnakeInGraphOfLength G G' k = (G'.IsInduced ∧ ∃ (u : V) (v : V) (P : G.Walk u v), P.IsPath ∧ G'.verts = {v_1 : V | v_1 ∈ P.support} ∧ P.length = k)

noncomputable def SnakeInBox.LongestSnakeInGraph {V : Type u} [DecidableEq V] (G : SimpleGraph V) : ℕ

The length of the longest induced path (or 'snake') in a graph G.

Equations

• SnakeInBox.LongestSnakeInGraph G = sSup {k : ℕ | ∃ (S : G.Subgraph), SnakeInBox.IsSnakeInGraphOfLength G S k}

noncomputable def SnakeInBox.LongestSnakeInTheBox (n : ℕ) : ℕ

The length of the longest snake for the Hypercube n graph.

Equations

• SnakeInBox.LongestSnakeInTheBox n = SnakeInBox.LongestSnakeInGraph (SnakeInBox.Hypercube n)

theorem SnakeInBox.snake_zero_zero : LongestSnakeInTheBox 0 = 0

The longest snake in the $0$-dimensional cube, i.e. the cube consisting of one point, is zero, since there only is one induced path and it is of length zero.

theorem SnakeInBox.snake_small_dimensions : List.map LongestSnakeInTheBox (List.range 9) = [0, 1, 2, 4, 7, 13, 26, 50, 98]

The maximum length for the snake-in-the-box problem is known for dimensions zero through eight; it is $0, 1, 2, 4, 7, 13, 26, 50, 98$.

theorem SnakeInBox.snake_dim_nine : LongestSnakeInTheBox 9 = sorry

For dimension $9$, the length of the longest snake in the box is not known. This is currently the smallest dimension where this question is open.

theorem SnakeInBox.snake_dim_nine_lower_bound : 190 ≤ LongestSnakeInTheBox 9

The best length found so far for dimension nine is 190.

theorem SnakeInBox.snake_upper_bound (n : ℕ) : ↑(LongestSnakeInTheBox n) ≤ 1 + 2 ^ (n - 1) * (6 * ↑n) / (6 * ↑n + 1 / (6 * √6) * √↑n)

An upper bound of the maximal length of the longest snake in a box is given by $$ 1 + 2^{n-1}\frac{6n}{6n + \frac{1}{6\sqrt{6}}n^{\frac 1 2} - 7}. $$