ClusterTwo

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

2-connected components of a lattice site set, and their diameter

A 2-connected component (or 2-cluster) of B*_{m-h} is a maximal subset A ⊆ B*_{m-h} such that any two cubes in A can be connected by a chain of successive cubes □, □' ∈ A with dist(□,□') ≤ 1. For z ∈ 3^{m-h}ℤ^d ∩ □_m we denote by B*_{m-h}(z;2) the 2-connected component containing z + □_{m-h} if B*(z + □_{m-h}) occurs, and the empty set otherwise.

In lattice coordinates that is exactly the predicate IsLatticePath₂ of LatticeTwo.lean, so a 2-cluster is a connected component of the site set for distance-two chains.

Faithfulness of the transcription

• The chain condition of the source ranges over cubes □, □' ∈ A, i.e. the intermediate cubes must themselves be bad; Connected₂ S u v accordingly asks the whole chain to lie inside the site set S. The printed form is nominally stronger — the chain inside the cluster A itself — and one direction is recorded here: connected₂_of_mem_cluster₂ joins any two sites of a 2-cluster by a chain inside S.
• "Maximal subset" is implemented by cluster₂, whose membership criterion mem_cluster₂_iff reads v ∈ cluster₂ S u ↔ u ∈ S ∧ Connected₂ S u v: the cluster collects every site of S joined to u, and connected₂_of_mem_cluster₂ is its 2-connectedness.
• The "empty set otherwise" clause is cluster₂_nonempty_iff: the 2-cluster is nonempty exactly when the base site lies in the site set.
• latDiam is the sup-metric diameter of the centres of the cubes of a cluster, in units of the cube side; closedLatDiam = latDiam + 1 on a nonempty cluster is the sup-metric diameter of the union of the corresponding closed cubes, again in units of the cube side (a nonempty cluster of n cubes whose centres span latDiam reaches from one cube's near face to the other's far face). The bad-cluster node uses closedLatDiam, the larger and hence the faithful reading of the printed diam.

Main definitions

• Connected₂, cluster₂: the 2-connected relation and the 2-cluster.
• latDiam, closedLatDiam: the lattice diameters.

Main results

• Connected₂.refl, .symm, .trans: Connected₂ is an equivalence on S.
• mem_cluster₂_iff, cluster₂_subset, self_mem_cluster₂, cluster₂_nonempty_iff, connected₂_of_mem_cluster₂: the characterizations of the 2-cluster.
• exists_crossingEvent₂At_of_le_latDiam: the deterministic step "a 2-cluster of lattice diameter ≥ 3^{k+1}/2 contains a distance-two crossing of the annulus □_{k+1} \ □_k based at one of its own sites".

References

• ABK26, l.percolation.bad.clusters, (e.bad.cluster.def) (e.diameter.bound.bad.clusters).

The 2-connected relation

def Algsuperdiff.Section3.Provider.Percolation.Connected₂ {d : ℕ} (S : Finset (Fin d → ℤ)) (u v : Fin d → ℤ) : Prop

The whole chain is required to lie in S, as in the source ("a chain of successive cubes □, □' ∈ A").

Equations

• Algsuperdiff.Section3.Provider.Percolation.Connected₂ S u v = ∃ (N : ℕ) (x : ℕ → Fin d → ℤ), x 0 = u ∧ x N = v ∧ Algsuperdiff.Section3.Provider.Percolation.IsLatticePath₂ x N ∧ ∀ i ≤ N, x i ∈ S

theorem Algsuperdiff.Section3.Provider.Percolation.Connected₂.refl {d : ℕ} {S : Finset (Fin d → ℤ)} {u : Fin d → ℤ} (hu : u ∈ S) : Connected₂ S u u

theorem Algsuperdiff.Section3.Provider.Percolation.Connected₂.mem_right {d : ℕ} {S : Finset (Fin d → ℤ)} {u v : Fin d → ℤ} (h : Connected₂ S u v) : v ∈ S

theorem Algsuperdiff.Section3.Provider.Percolation.Connected₂.symm {d : ℕ} {S : Finset (Fin d → ℤ)} {u v : Fin d → ℤ} (h : Connected₂ S u v) : Connected₂ S v u

theorem Algsuperdiff.Section3.Provider.Percolation.Connected₂.trans {d : ℕ} {S : Finset (Fin d → ℤ)} {u v w : Fin d → ℤ} (h₁ : Connected₂ S u v) (h₂ : Connected₂ S v w) : Connected₂ S u w

The 2-cluster

noncomputable def Algsuperdiff.Section3.Provider.Percolation.cluster₂ {d : ℕ} (S : Finset (Fin d → ℤ)) (u : Fin d → ℤ) : Finset (Fin d → ℤ)

ABK26 e.bad.cluster.def: the 2-connected component of the site set S containing u if u ∈ S, and the empty set otherwise.

Equations

• Algsuperdiff.Section3.Provider.Percolation.cluster₂ S u = if u ∈ S then {v ∈ S | Algsuperdiff.Section3.Provider.Percolation.Connected₂ S u v} else ∅

theorem Algsuperdiff.Section3.Provider.Percolation.mem_cluster₂_iff {d : ℕ} {S : Finset (Fin d → ℤ)} {u v : Fin d → ℤ} : v ∈ cluster₂ S u ↔ u ∈ S ∧ Connected₂ S u v

theorem Algsuperdiff.Section3.Provider.Percolation.cluster₂_subset {d : ℕ} (S : Finset (Fin d → ℤ)) (u : Fin d → ℤ) : cluster₂ S u ⊆ S

The 2-cluster is a subset of the site set: the source's A ⊆ B*_{m-h}.

theorem Algsuperdiff.Section3.Provider.Percolation.self_mem_cluster₂ {d : ℕ} {S : Finset (Fin d → ℤ)} {u : Fin d → ℤ} (hu : u ∈ S) : u ∈ cluster₂ S u

The 2-cluster of a site of S contains that site.

theorem Algsuperdiff.Section3.Provider.Percolation.cluster₂_nonempty_iff {d : ℕ} {S : Finset (Fin d → ℤ)} {u : Fin d → ℤ} : (cluster₂ S u).Nonempty ↔ u ∈ S

theorem Algsuperdiff.Section3.Provider.Percolation.connected₂_of_mem_cluster₂ {d : ℕ} {S : Finset (Fin d → ℤ)} {u v w : Fin d → ℤ} (hv : v ∈ cluster₂ S u) (hw : w ∈ cluster₂ S u) : Connected₂ S v w

First half of maximality. Any two sites of a 2-cluster are joined by a chain of successive sites of S at lattice sup distance at most two.

Lattice diameters

def Algsuperdiff.Section3.Provider.Percolation.latDiam {d : ℕ} (A : Finset (Fin d → ℤ)) : ℕ

The sup-metric diameter of a finite set of lattice sites, in units of the lattice spacing: the largest sup distance between two of its sites.

Equations

• Algsuperdiff.Section3.Provider.Percolation.latDiam A = A.sup fun (u : Fin d → ℤ) => A.sup fun (v : Fin d → ℤ) => Algsuperdiff.Section3.Provider.Percolation.latDist u v

theorem Algsuperdiff.Section3.Provider.Percolation.latDist_le_latDiam {d : ℕ} {A : Finset (Fin d → ℤ)} {u v : Fin d → ℤ} (hu : u ∈ A) (hv : v ∈ A) : latDist u v ≤ latDiam A

theorem Algsuperdiff.Section3.Provider.Percolation.exists_le_latDist_of_le_latDiam {d : ℕ} {A : Finset (Fin d → ℤ)} {D : ℕ} (hD : 0 < D) (h : D ≤ latDiam A) : ∃ u ∈ A, ∃ v ∈ A, D ≤ latDist u v

A positive lower bound on the lattice diameter is attained by a pair of sites.

def Algsuperdiff.Section3.Provider.Percolation.closedLatDiam {d : ℕ} (A : Finset (Fin d → ℤ)) : ℕ

The sup-metric diameter, in units of the cube side, of the union of the closed unit cubes centred at the sites of A. On a nonempty A this is latDiam A + 1; the empty set has diameter 0.

This is the reading of the printed diam(B*_{m-h}(z;2)) used by the bad-cluster node: it is the larger of the two candidate readings (the other being the centre-to-centre latDiam), so bounding the probability that it is large is the stronger statement.

Equations

• Algsuperdiff.Section3.Provider.Percolation.closedLatDiam A = if A.Nonempty then Algsuperdiff.Section3.Provider.Percolation.latDiam A + 1 else 0

theorem Algsuperdiff.Section3.Provider.Percolation.closedLatDiam_eq_of_nonempty {d : ℕ} {A : Finset (Fin d → ℤ)} (hA : A.Nonempty) : closedLatDiam A = latDiam A + 1

From a large 2-cluster to a distance-two crossing

theorem Algsuperdiff.Section3.Provider.Percolation.exists_crossingEvent₂At_of_le_latDiam {d : ℕ} {Ω : Type u_1} {B : ℕ → (Fin d → ℤ) → Set Ω} {ω : Ω} {S : Finset (Fin d → ℤ)} {u : Fin d → ℤ} {k : ℕ} (hbad : ∀ y ∈ S, ω ∈ ⋃ (L : ℕ), B L y) (hdiam : 3 ^ (k + 1) ≤ 2 * latDiam (cluster₂ S u)) : ∃ w ∈ cluster₂ S u, ω ∈ crossingEvent₂At B k w

The deterministic step of e.diameter.bound.bad.clusters.

If the 2-cluster of u has lattice diameter D with 3 ^ (k+1) ≤ 2 D, and every site of the site set carries the bad event ⋃_L B_L, then one of the sites of that 2-cluster is the base of a distance-two crossing of its own annulus □_{k+1} \ □_k, i.e. of the event crossingEvent₂At B k.

This is the "follows from e.diameter.bound (rescaled)" of the source proof, made explicit at the ruled adjacency: the chain joining the two extreme sites of the cluster is a distance-two path, which the distance-two abstract layer of DiameterTwo.lean — and not the proved distance-one layer — covers.