PathCount

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Counting finite lattice paths

This file gives explicit finite enumerations of centered-cube starting sites, sup-neighbor offsets, and lattice paths of a prescribed vertex length. The enumeration deliberately includes an extra factor of 3^d, matching the dimension-only overcount used in the percolation union bound.

def Algsuperdiff.Section5.Percolation.cubeSiteOfIndex {d : ℕ} (k : ℕ) (j : Fin d → Fin (3 ^ k)) : Site d

The site encoded by one coordinate in Fin (3^k) in every direction, centered around the origin.

Equations

• Algsuperdiff.Section5.Percolation.cubeSiteOfIndex k j i = ↑↑(j i) - ↑(3 ^ k / 2)

def Algsuperdiff.Section5.Percolation.cubeSites (d k : ℕ) : Finset (Site d)

The finite set of lattice sites in the centered scale-k cube.

Equations

• Algsuperdiff.Section5.Percolation.cubeSites d k = Finset.image (Algsuperdiff.Section5.Percolation.cubeSiteOfIndex k) Finset.univ

theorem Algsuperdiff.Section5.Percolation.cubeSiteOfIndex_inCube {d k : ℕ} (j : Fin d → Fin (3 ^ k)) : inCube k (cubeSiteOfIndex k j)

Every explicitly encoded cube site satisfies the strict cube inequalities.

theorem Algsuperdiff.Section5.Percolation.mem_cubeSites_of_inCube {d k : ℕ} {x : Site d} (hx : inCube k x) : x ∈ cubeSites d k

The explicit cube-site enumeration contains every site in the cube.

theorem Algsuperdiff.Section5.Percolation.card_cubeSites (d k : ℕ) : (cubeSites d k).card = 3 ^ (d * k)

The scale-k cube contains exactly 3^(d*k) lattice sites.

def Algsuperdiff.Section5.Percolation.offsetOfIndex {d : ℕ} (j : Fin d → Fin 3) : Site d

The sup-neighbor offset encoded by one coordinate in Fin 3 in every direction.

Equations

• Algsuperdiff.Section5.Percolation.offsetOfIndex j i = ↑↑(j i) - 1

def Algsuperdiff.Section5.Percolation.neighborOffsets (d : ℕ) : Finset (Site d)

The finite palette of all 3^d sup-neighbor offsets, including zero.

Equations

• Algsuperdiff.Section5.Percolation.neighborOffsets d = Finset.image Algsuperdiff.Section5.Percolation.offsetOfIndex Finset.univ

theorem Algsuperdiff.Section5.Percolation.card_neighborOffsets (d : ℕ) : (neighborOffsets d).card = 3 ^ d

The neighbor-offset palette has cardinality 3^d.

theorem Algsuperdiff.Section5.Percolation.exists_neighborOffset_of_adj {d : ℕ} {x y : Site d} (hxy : Adj x y) : ∃ δ ∈ neighborOffsets d, y = x + δ

Every adjacent step is represented by the neighbor-offset palette.

def Algsuperdiff.Section5.Percolation.walksFrom {d : ℕ} (x : Site d) : ℕ → Finset (List (Site d))

All walks with n steps starting at x.

Equations

• One or more equations did not get rendered due to their size.
• Algsuperdiff.Section5.Percolation.walksFrom x 0 = {[x]}

theorem Algsuperdiff.Section5.Percolation.mem_walksFrom_of_isPath {d : ℕ} (x : Site d) (xs : List (Site d)) : IsPath (x :: xs) → x :: xs ∈ walksFrom x xs.length

A path belongs to the finite walk enumeration determined by its first vertex and number of remaining vertices.

theorem Algsuperdiff.Section5.Percolation.length_eq_succ_of_mem_walksFrom {d : ℕ} (x : Site d) {n : ℕ} {Γ : List (Site d)} : Γ ∈ walksFrom x n → Γ.length = n + 1

Every walk in the n-step enumeration has exactly n + 1 vertices.

theorem Algsuperdiff.Section5.Percolation.card_walksFrom_le {d : ℕ} (x : Site d) (n : ℕ) : (walksFrom x n).card ≤ (3 ^ d) ^ n

The number of n-step walks from a fixed site is at most (3^d)^n.

def Algsuperdiff.Section5.Percolation.pathsOfLength (d k : ℕ) : ℕ → Finset (List (Site d))

The finite set of lattice paths of vertex length n whose first vertex lies in the centered scale-k cube.

Equations

• One or more equations did not get rendered due to their size.
• Algsuperdiff.Section5.Percolation.pathsOfLength d k 0 = ∅

theorem Algsuperdiff.Section5.Percolation.IsPathFrom.mem_pathsOfLength {d k : ℕ} {Γ : List (Site d)} (hΓ : IsPathFrom k Γ) : Γ ∈ pathsOfLength d k Γ.length

Every crossing path occurs in the enumeration at its vertex length.

theorem Algsuperdiff.Section5.Percolation.length_eq_of_mem_pathsOfLength {d k n : ℕ} {Γ : List (Site d)} (hΓ : Γ ∈ pathsOfLength d k n) : Γ.length = n

Every path-list in the length-n enumeration has exactly n vertices.

theorem Algsuperdiff.Section5.Percolation.card_pathsOfLength_le (d k n : ℕ) : (pathsOfLength d k n).card ≤ 3 ^ (d * k) * (3 ^ d) ^ n

Path-count bound for the dimension-only union bound.