LatticeTwo

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

Distance-two lattice paths: geometry and separated selection

ABK26's abstract percolation machinery (l.percolation.bound.general) steps along paths whose consecutive sites are at lattice distance at most one. The bad-cluster lemma l.percolation.bad.clusters however joins base cubes □, □' with dist(□,□') ≤ 1, i.e. lattice sup distance at most two in units of the cube side 3^{m-h}. A 2-adjacent chain is not a 1-adjacent lattice path, so the abstract layer as proved does not literally cover 2-clusters.

This module is the first half of that re-run: the purely combinatorial geometry of distance-two paths. It is a parallel layer under new names; no proved declaration is modified.

Where the step size enters

Exactly three places, and each costs only a dimension-only factor:

• Truncation. A distance-two path truncated at its first exit from z + □_n is confined to 2 · latDist z (x i) ≤ 3 ^ n + 3 (the distance-one layer has 3 ^ n + 1).
• Shell selection. The distance to the starting site now jumps by up to two per step, so a first passage of the level m * s proves in [m*s, m*s + 1] rather than exactly on m * s; consecutive selected sites are therefore s - 1-separated instead of s-separated. Taking the step s = 3 ^ (k+1) + 5 restores the separation 3 ^ (k+1) + 4 needed below.
• Range of independence. The wider localisation boxes need the wider site separation 3 ^ (k+1) + 4 (against 3 ^ (k+1) + 2) to keep the boxes at sup distance more than 3 ^ k; three_pow_lt_latDist_of_mem_locBox₂ supplies it.

The number 3 ^ (h - 3) of selected sites — the quantity that drives the whole induction — is unchanged, because the arithmetic 2 · 3 ^ (h-3) · (3 ^ (k+1) + 5) ≤ 3 ^ (k+h) still holds. This is why the gate constant of the distance-two layer is the same 16 d exp(40 (1-b)^{-1}) as the distance-one one.

Main definitions

• IsLatticePath₂: the distance-two path predicate.
• locBox₂: the localisation box of a truncated distance-two path.

Main results

• exists_truncated_path₂: truncation at the first exit from a cube.
• card_locBox₂_le: #(locBox₂ n z) ≤ 3 ^ (d * (n + 2)).
• three_pow_lt_latDist_of_mem_locBox₂: the independence range.
• exists_separated_subpaths₂: the separated-subpath extraction, with the same count 3 ^ (h - 3) as the distance-one layer.

References

• ABK26, l.percolation.bad.clusters, (the 2-connected component) and l.percolation.bound.general, (the abstract layer).

Distance-two paths

def Algsuperdiff.Section3.Provider.Percolation.IsLatticePath₂ {d : ℕ} (x : ℕ → Fin d → ℤ) (N : ℕ) : Prop

The distance-two path predicate: consecutive sites are at sup distance at most two.

Equations

• Algsuperdiff.Section3.Provider.Percolation.IsLatticePath₂ x N = ∀ i < N, Algsuperdiff.Section3.Provider.Percolation.latDist (x i) (x (i + 1)) ≤ 2

theorem Algsuperdiff.Section3.Provider.Percolation.IsLatticePath₂.mono {d : ℕ} {x : ℕ → Fin d → ℤ} {N M : ℕ} (h : IsLatticePath₂ x N) (hMN : M ≤ N) : IsLatticePath₂ x M

A distance-two path may be shortened.

theorem Algsuperdiff.Section3.Provider.Percolation.IsLatticePath₂.shift {d : ℕ} {x : ℕ → Fin d → ℤ} {N : ℕ} (h : IsLatticePath₂ x N) (a M : ℕ) (hle : a + M ≤ N) : IsLatticePath₂ (fun (t : ℕ) => x (a + t)) M

A distance-two path may be restarted at any of its sites.

theorem Algsuperdiff.Section3.Provider.Percolation.IsLatticePath₂.latDist_start_succ_le {d : ℕ} {x : ℕ → Fin d → ℤ} {N : ℕ} (h : IsLatticePath₂ x N) {i : ℕ} (hi : i < N) : latDist (x 0) (x (i + 1)) ≤ latDist (x 0) (x i) + 2

Along a distance-two path the sup distance to the starting site grows by at most two per step.

Truncation at the first exit from a cube

theorem Algsuperdiff.Section3.Provider.Percolation.exists_truncated_path₂ {d : ℕ} {x : ℕ → Fin d → ℤ} {N n : ℕ} {z : Fin d → ℤ} (h0 : x 0 = z) (hpath : IsLatticePath₂ x N) (hout : x N ∉ cubeAt n z) : ∃ M ≤ N, x M ∉ cubeAt n z ∧ ∀ i ≤ M, 2 * latDist z (x i) ≤ 3 ^ n + 3

Truncation of a distance-two path at its first exit from z + □_n: from a path started at z and ending outside z + □_n we extract an initial segment which still ends outside z + □_n and all of whose sites satisfy 2 * latDist z (x i) ≤ 3 ^ n + 3.

The distance-one layer confines the truncated path to 3 ^ n + 1; the extra 2 is the single place where the step size enters the localisation.

The localisation box of a distance-two path

def Algsuperdiff.Section3.Provider.Percolation.locRadius₂ (n : ℕ) : ℕ

Half-width, rounded up, of the distance-two localisation box at scale n.

Equations

• Algsuperdiff.Section3.Provider.Percolation.locRadius₂ n = (3 ^ n + 3) / 2

theorem Algsuperdiff.Section3.Provider.Percolation.two_mul_locRadius₂ (n : ℕ) : 2 * locRadius₂ n = 3 ^ n + 3

def Algsuperdiff.Section3.Provider.Percolation.locBox₂ {d : ℕ} (n : ℕ) (z : Fin d → ℤ) : Finset (Fin d → ℤ)

The finite set of lattice sites y with 2 * latDist z y ≤ 3 ^ n + 3: the region in which a distance-two path started at z and truncated at its first exit from z + □_n is confined.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Percolation.mem_locBox₂_iff {d n : ℕ} {z y : Fin d → ℤ} : y ∈ locBox₂ n z ↔ 2 * latDist z y ≤ 3 ^ n + 3

theorem Algsuperdiff.Section3.Provider.Percolation.mem_locBox₂_of_two_mul_latDist_le {d n : ℕ} {z y : Fin d → ℤ} (h : 2 * latDist z y ≤ 3 ^ n + 3) : y ∈ locBox₂ n z

theorem Algsuperdiff.Section3.Provider.Percolation.three_pow_lt_latDist_of_mem_locBox₂ {d k : ℕ} {a b u v : Fin d → ℤ} (hab : 3 ^ (k + 1) + 4 ≤ latDist a b) (hu : u ∈ locBox₂ k a) (hv : v ∈ locBox₂ k b) : 3 ^ k < latDist u v

Distance-two localisation boxes of two sites at sup distance at least 3 ^ (k + 1) + 4 are at sup distance strictly greater than 3 ^ k. This is the separation required by the finite-range independence hypothesis of ABK26; the distance-one layer needs only 3 ^ (k + 1) + 2.

theorem Algsuperdiff.Section3.Provider.Percolation.card_locBox₂_le {d : ℕ} (n : ℕ) (z : Fin d → ℤ) : (locBox₂ n z).card ≤ 3 ^ (d * (n + 2))

A crude count of the distance-two localisation box: one factor 3 ^ d more than the distance-one card_locBox_le.

Shell selection along a distance-two path

theorem Algsuperdiff.Section3.Provider.Percolation.exists_shell_indices₂ {d : ℕ} {x : ℕ → Fin d → ℤ} {N s M : ℕ} (hpath : IsLatticePath₂ x N) (hreach : M * s ≤ latDist (x 0) (x N)) : ∃ (i : ℕ → ℕ), i 0 = 0 ∧ (∀ m ≤ M, i m ≤ N) ∧ (∀ (m m' : ℕ), m ≤ m' → m' ≤ M → i m ≤ i m') ∧ ∀ m ≤ M, m * s ≤ latDist (x 0) (x (i m)) ∧ latDist (x 0) (x (i m)) ≤ m * s + 1

Shell selection for distance-two paths. Along a distance-two path whose final site is at sup distance at least M * s from the starting site there are indices i 0 ≤ ⋯ ≤ i M (bounded by the length of the path) with i 0 = 0 such that x (i m) lies in the shell [m * s, m * s + 1] around x 0.

theorem Algsuperdiff.Section3.Provider.Percolation.latDist_shell_separated₂ {d : ℕ} {x : ℕ → Fin d → ℤ} {i : ℕ → ℕ} {s M : ℕ} (hval : ∀ m ≤ M, m * s ≤ latDist (x 0) (x (i m)) ∧ latDist (x 0) (x (i m)) ≤ m * s + 1) {m m' : ℕ} (hm : m ≤ M) (hm' : m' ≤ M) (hmm' : m ≠ m') : s ≤ latDist (x (i m)) (x (i m')) + 1

Distinct shell-selected sites of a distance-two path are at sup distance at least s - 1, stated in the addition-free form s ≤ latDist + 1.

theorem Algsuperdiff.Section3.Provider.Percolation.exists_separated_subpaths₂ {d : ℕ} {x : ℕ → Fin d → ℤ} {N k h : ℕ} {z : Fin d → ℤ} {P : (Fin d → ℤ) → Prop} (hh : 3 ≤ h) (h0 : x 0 = z) (hpath : IsLatticePath₂ x N) (hout : x N ∉ cubeAt (k + h) z) (hP : ∀ i ≤ N, P (x i)) : ∃ (y : ℕ → Fin d → ℤ), (∀ m < 3 ^ (h - 3), y m ∈ locBox₂ (k + h) z) ∧ (∀ (m m' : ℕ), m < 3 ^ (h - 3) → m' < 3 ^ (h - 3) → m ≠ m' → 3 ^ (k + 1) + 4 ≤ latDist (y m) (y m')) ∧ ∀ m < 3 ^ (h - 3), ∃ (N' : ℕ) (x' : ℕ → Fin d → ℤ), x' 0 = y m ∧ IsLatticePath₂ x' N' ∧ x' N' ∉ cubeAt k (y m) ∧ ∀ t ≤ N', P (x' t)

The separated-subpath extraction for distance-two paths.

Let x be a distance-two path started at z which ends outside z + □_{k+h}, with h ≥ 3, and suppose a property P holds at every site of the path. Then there are 3 ^ (h - 3) sites of the path — the same count as in the distance-one layer — all lying in locBox₂ (k + h) z, pairwise at sup distance at least 3 ^ (k + 1) + 4, each of them the starting site of a distance-two subpath which leaves its own □_k-cube and along which P still holds.