Snake in the box

References:

• Wikipedia
• xkcd

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

A graph on the power set of Fin n, where two sets are adjacent if their intersection has size 1.

Equations

• SnakeInBox.Hypercube n = SimpleGraph.fromRel fun (a b : Finset (Fin n)) => (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 = ↑P.support.toFinset ∧ 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)

@[simp]

theorem SnakeInBox.Finset.univ_finset_of_isEmpty {α : Type u_1} [h : IsEmpty α] : Set.univ = {∅}

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]

theorem SnakeInBox.snake_dim_nine : LongestSnakeInTheBox 9 = sorry

theorem SnakeInBox.snake_dim_nine_lower_bound : 190 ≤ LongestSnakeInTheBox 9

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}. $$