CrossingTrace

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

Crossing extensions of pre-exit cube traces

A uniformly sampled trace whose times are strictly before an exit need not itself contain a site outside the exited cube. This file supplies the two endpoint corrections that turn such a trace into a crossing of the annulus: at most one lattice site is prepended and at most one is appended, and neither is claimed to be visited. A lower bound on the good vertices of every crossing therefore transfers to the trace at a loss of at most 2 * d, which is the form the Section 5 argument consumes.

def Algsuperdiff.Section5.Trace.cubeSiteRadius (k : ℕ) : ℕ

The integer half-radius of a triadic cube in the lattice.

Equations

• Algsuperdiff.Section5.Trace.cubeSiteRadius k = 3 ^ k / 2

def Algsuperdiff.Section5.Trace.clampCoord (r : ℕ) (z : ℤ) : ℤ

Clamp an integer coordinate to the closed interval with the specified half-radius.

Equations

• Algsuperdiff.Section5.Trace.clampCoord r z = if z < -↑r then -↑r else if ↑r < z then ↑r else z

def Algsuperdiff.Section5.Trace.clampSite {d : ℕ} (k : ℕ) (z : Percolation.Site d) : Percolation.Site d

Clamp every site coordinate to the triadic lattice cube.

Equations

• Algsuperdiff.Section5.Trace.clampSite k z i = Algsuperdiff.Section5.Trace.clampCoord (Algsuperdiff.Section5.Trace.cubeSiteRadius k) (z i)

theorem Algsuperdiff.Section5.Trace.exists_inCube_siteDist_nearestTriadicSite_le_one {d : ℕ} (n : ℤ) (k : ℕ) (x : HCPolySupport.Vec d) (hx : x ∈ Metric.closedBall 0 (1 / 2 * 3 ^ (n + ↑k))) : ∃ (a : Percolation.Site d), Percolation.inCube k a ∧ Percolation.siteDist a (nearestTriadicSite n x) ≤ 1

A point of the closed centered cube at physical scale n + k has a nearest scale-n site at lattice distance at most one from inCube k.

def Algsuperdiff.Section5.Trace.outsideSite {d : ℕ} (k : ℕ) (z : Percolation.Site d) (i : Fin d) (positive : Bool) : Percolation.Site d

Move one site coordinate to the first lattice point outside the chosen cube face.

Equations

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

theorem Algsuperdiff.Section5.Trace.exists_not_inCube_siteDist_nearestTriadicSite_le_one_of_frontier {d : ℕ} (n : ℤ) (k : ℕ) {x y : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + ↑k))) (hy : y ∈ frontier (HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + ↑k)))) (hxy : dist x y < 3 ^ n) : ∃ (b : Percolation.Site d), ¬Percolation.inCube k b ∧ Percolation.siteDist (nearestTriadicSite n x) b ≤ 1

A point strictly inside the centered cube and less than one scale-n cell from a frontier point has a nearest site adjacent to an outside site.

theorem Algsuperdiff.Section5.Trace.exists_isPathFrom_extension {d k : ℕ} {Gamma : List (Percolation.Site d)} {a x y b : Percolation.Site d} (hGamma : Percolation.IsWeakPath Gamma) (hhead : Gamma.head? = some x) (hlast : Gamma.getLast? = some y) (ha : Percolation.siteDist a x ≤ 1) (hb : Percolation.siteDist y b ≤ 1) (hain : Percolation.inCube k a) (hbout : ¬Percolation.inCube (k + 1) b) : ∃ (Delta : List (Percolation.Site d)), Percolation.IsPathFrom k Delta ∧ Delta.toFinset = insert a (insert b Gamma.toFinset)

Adding one endpoint correction on each side of a weak trace produces a crossing path with the same vertices apart from those two corrections.

theorem Algsuperdiff.Section5.Trace.good_toFinset_card_lower_bound_of_isPathFrom_extension {d k L : ℕ} (hd : 0 < d) (Good : Percolation.Site d → Prop) [DecidablePred Good] {Gamma Delta : List (Percolation.Site d)} {a b : Percolation.Site d} (hDelta : Percolation.IsPathFrom k Delta) (hvertices : Delta.toFinset = insert a (insert b Gamma.toFinset)) (hcross : ∀ (Xi : List (Percolation.Site d)), Percolation.IsPathFrom k Xi → L ≤ (Finset.filter Good Xi.toFinset).card) : L - 2 * d ≤ (Finset.filter Good Gamma.toFinset).card

If every crossing path has at least L good distinct vertices, removing the two unclaimed endpoint corrections loses at most 2d good vertices.