Self-avoiding walks on the honeycomb lattice

StructureVertices of the honeycomb lattice#✓fully proved

A vertex of the honeycomb lattice is a triple \((x, y, s)\) with \(x, y \in \mathbb{Z}\) and \(s\) a boolean recording which of the two classes of the bipartition the vertex belongs to.

structure HoneycombVertex where
  x : ℤ
  y : ℤ
  side : Bool
deriving DecidableEq

Used by 9

Used byEndpoint of a direction word · Self-avoiding direction words · Origin of the honeycomb lattice · Steps in the honeycomb lattice · Distinct labels give distinct neighbors · Steps are involutions · Vertices along a direction word · Vertices visited by a direction word · Number of self-avoiding walks on the honeycomb lattice

DefinitionSteps in the honeycomb lattice#✓fully proved

For a vertex \(v = (x, y, s)\) and a direction label \(d \in \{0, 1, 2\}\), the step from \(v\) in direction \(d\) is a vertex on the other side of the bipartition. If \(s\) is true, it is \((x, y, \mathrm{false})\), \((x + 1, y, \mathrm{false})\) or \((x, y + 1, \mathrm{false})\) for \(d = 0, 1, 2\) respectively. If \(s\) is false, it is \((x, y, \mathrm{true})\), \((x - 1, y, \mathrm{true})\) or \((x, y - 1, \mathrm{true})\) for \(d = 0, 1, 2\) respectively.

def step (v : HoneycombVertex) (direction : Fin 3) : HoneycombVertex :=
  if v.side then
    match direction.1 with
    | 0 => ⟨v.x, v.y, false⟩
    | 1 => ⟨v.x + 1, v.y, false⟩
    | _ => ⟨v.x, v.y + 1, false⟩
  else
    match direction.1 with
    | 0 => ⟨v.x, v.y, true⟩
    | 1 => ⟨v.x - 1, v.y, true⟩
    | _ => ⟨v.x, v.y - 1, true⟩

Uses 1 · Used by 3

Statement usesVertices of the honeycomb lattice

Used byEndpoint of a direction word · Distinct labels give distinct neighbors · Steps are involutions

TheoremSteps are involutions#✓fully proved

For every vertex \(v\) of the honeycomb lattice and every direction label \(d \in \{0, 1, 2\}\), taking the step in direction \(d\) from \(v\) and then the step in direction \(d\) again returns to \(v\).

In particular, the coordinate model defines an undirected graph.

@[simp]
theorem step_step (v : HoneycombVertex) (direction : Fin 3) :
    step (step v direction) direction = v

Uses 2

Statement usesVertices of the honeycomb lattice · Steps in the honeycomb lattice

TheoremDistinct labels give distinct neighbors#✓fully proved

For every vertex \(v\) of the honeycomb lattice, the steps from \(v\) in the directions \(0\), \(1\) and \(2\) are three distinct vertices.

theorem step_injective (v : HoneycombVertex) : Function.Injective (step v)

Uses 2

Statement usesVertices of the honeycomb lattice · Steps in the honeycomb lattice

DefinitionOrigin of the honeycomb lattice#✓fully proved

The origin is the vertex \((0, 0, \mathrm{false})\).

The honeycomb lattice is vertex-transitive, so the choice of base vertex is arbitrary.

def origin : HoneycombVertex := ⟨0, 0, false⟩

Uses 1 · Used by 1

Statement usesVertices of the honeycomb lattice

Used byEndpoint of a direction word

DefinitionEndpoint of a direction word#✓fully proved

For a finite word \(d_1 d_2 \cdots d_k\) of direction labels in \(\{0, 1, 2\}\), its endpoint is the vertex reached from the origin by taking the step in direction \(d_1\), then the step in direction \(d_2\), and so on through \(d_k\). The endpoint of the empty word is the origin.

def endpoint (directions : List (Fin 3)) : HoneycombVertex :=
  directions.foldl step origin

Uses 3 · Used by 1

Statement usesVertices of the honeycomb lattice · Origin of the honeycomb lattice · Steps in the honeycomb lattice

Used byVertices along a direction word

DefinitionVertices along a direction word#✓fully proved

For a word \((d_1, \ldots, d_n)\) of direction labels in \(\{0, 1, 2\}\) and an integer \(0 \le i \le n\), the \(i\)-th vertex of the word is the endpoint of its prefix \((d_1, \ldots, d_i)\), the vertex reached from the origin after the first \(i\) steps.

def vertexAt {n : ℕ} (directions : Fin n → Fin 3) (i : Fin (n + 1)) :
    HoneycombVertex :=
  endpoint ((List.ofFn directions).take i.1)

Uses 2 · Used by 1

Statement usesVertices of the honeycomb lattice · Endpoint of a direction word

Used byVertices visited by a direction word

DefinitionVertices visited by a direction word#✓fully proved

For a word \((d_1, \ldots, d_n)\) of direction labels in \(\{0, 1, 2\}\), the set of visited vertices is the finite set of its \(i\)-th vertices for \(0 \le i \le n\); it contains the origin (for \(i = 0\)) and the endpoint of the word.

def visitedVertices {n : ℕ} (directions : Fin n → Fin 3) : Finset HoneycombVertex :=
  Finset.univ.image (vertexAt directions)

Uses 2 · Used by 2

Statement usesVertices of the honeycomb lattice · Vertices along a direction word

Used bySelf-avoiding direction words · Number of self-avoiding walks on the honeycomb lattice

DefinitionSelf-avoiding direction words#✓fully proved

A word \((d_1, \ldots, d_n)\) of direction labels in \(\{0, 1, 2\}\) is self-avoiding when its set of visited vertices has exactly \(n + 1\) elements, that is, when its \(n + 1\) vertices, the \(i\)-th vertices for \(0 \le i \le n\), are pairwise distinct.

def IsSelfAvoiding {n : ℕ} (directions : Fin n → Fin 3) : Prop :=
  (visitedVertices directions).card = n + 1

Uses 2 · Used by 1

Statement usesVertices of the honeycomb lattice · Vertices visited by a direction word

Used byNumber of self-avoiding walks on the honeycomb lattice

DefinitionNumber of self-avoiding walks on the honeycomb lattice#✓fully proved

For a natural number \(n\), this is the number of self-avoiding walks with \(n\) steps on the honeycomb lattice starting at the origin.

def walkCount (n : ℕ) : ℕ :=
  (Finset.univ.filter fun directions : Fin n → Fin 3 =>
    IsSelfAvoiding directions).card

Uses 3 · Used by 3

Statement usesVertices of the honeycomb lattice · Self-avoiding direction words · Vertices visited by a direction word

Used byThe connective constant of the honeycomb lattice · Six-step self-avoiding walks on the honeycomb lattice · Three-step self-avoiding walks on the honeycomb lattice

TheoremThree-step self-avoiding walks on the honeycomb lattice#✓fully proved

There are exactly \(12\) self-avoiding walks with \(3\) steps on the honeycomb lattice starting at a fixed vertex.

theorem walkCount_three : walkCount 3 = 12

Uses 1

Statement usesNumber of self-avoiding walks on the honeycomb lattice

TheoremSix-step self-avoiding walks on the honeycomb lattice#✓fully proved

There are exactly \(90\) self-avoiding walks with \(6\) steps on the honeycomb lattice starting at a fixed vertex.

Six is the first length at which a walk can close a hexagon.

theorem walkCount_six : walkCount 6 = 90

Uses 1

Statement usesNumber of self-avoiding walks on the honeycomb lattice

TheoremThe connective constant of the honeycomb lattice#●ready to prove

Let \(c_n\) be the number of \(n\)-step self-avoiding walks on the honeycomb lattice starting at the origin. Then \(c_n^{1/n} \to \sqrt{2 + \sqrt{2}}\) as \(n \to \infty\).

public theorem_wanted honeycomb_connective_constant :
    Tendsto
      (fun n ↦ (walkCount n : ℝ) ^ (1 / n : ℝ))
      atTop
      (nhds (Real.sqrt (2 + Real.sqrt 2)))

Sources

• H. Duminil-Copin and S. Smirnov, 'The connective constant of the honeycomb lattice equals sqrt(2 + sqrt 2)', Ann. of Math. 175 (2012), 1653-1665, https://doi.org/10.4007/annals.2012.175.3.14. Problem honeycomb_connective_constant of the lean-eval benchmark.

Uses 1

Statement usesNumber of self-avoiding walks on the honeycomb lattice

12 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.