Peierls argument for bond percolation

DefinitionSite on the positive horizontal axis#✓fully proved

The site (j, 0) on the positive horizontal axis.

def axisSite (j : ℕ) : Site 2 := ![(j : ℤ), 0]

Uses 1 · Used by 15

Statement usesSite of the hypercubic lattice

Used byCanonical contour of a finite origin cluster · Darts of the canonical contour · Canonical contour is longer than the exit index · Closed face walk of the canonical contour · Exit dart of a finite origin cluster · Exit dart on the positive horizontal axis · Exit index of a finite origin cluster · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · Axis site lies outside the origin cluster · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionAxis site lies outside the origin cluster#✓fully proved

The site (j + 1, 0) is not in the open cluster of the origin.

def exitPred (ω : ConfigSpace (Sym2 (Site 2))) (j : ℕ) : Prop :=
  axisSite (j + 1) ∉ cluster 2 ω (origin 2)

Uses 5 · Used by 13

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Site on the positive horizontal axis · Open cluster of a site · Origin of the hypercubic lattice

Used byCanonical contour of a finite origin cluster · Darts of the canonical contour · Canonical contour is longer than the exit index · Closed face walk of the canonical contour · Exit dart of a finite origin cluster · Exit index of a finite origin cluster · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionExit index of a finite origin cluster#✓fully proved

For a finite origin cluster, the least j such that (j + 1, 0) is not in the cluster.

noncomputable def exitIndex (hfin : (cluster 2 ω (origin 2)).Finite) : ℕ := by
  classical
  exact Nat.find (exitPred_exists (ω := ω) hfin)

Uses 8 · Used by 18

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path · Site of the hypercubic lattice · Site on the positive horizontal axis · Open cluster of a site · Axis site lies outside the origin cluster · Open subgraph of a bond configuration · Origin of the hypercubic lattice

Used byExistence of an anchored dual cycle around the origin cluster · Canonical contour of a finite origin cluster · Darts of the canonical contour · Canonical contour is longer than the exit index · Closed face walk of the canonical contour · Exit dart of a finite origin cluster · Exit dart on the positive horizontal axis · Face below the exit edge · Face above the exit edge · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · Anchored dual cycles give the anchored enclosure property · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionFace above the exit edge#✓fully proved

The unit face directly above the exit edge from (j, 0) to (j + 1, 0).

noncomputable def exitFaceUp (hfin : (cluster 2 ω (origin 2)).Finite) : Site 2 :=
  ![(exitIndex (ω := ω) hfin : ℤ), 0]

Uses 5 · Used by 14

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open cluster of a site · Exit index of a finite origin cluster · Origin of the hypercubic lattice

Used byExistence of an anchored dual cycle around the origin cluster · Closed face walk of the canonical contour · Canonical orbit cycle condition · Dual cycle reaching the left half-plane · Origin cluster's enclosing contour links the two axis exits · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · Anchored dual cycles give the anchored enclosure property · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionFace below the exit edge#✓fully proved

The unit face directly below the exit edge from (j, 0) to (j + 1, 0).

noncomputable def exitFaceDown (hfin : (cluster 2 ω (origin 2)).Finite) : Site 2 :=
  ![(exitIndex (ω := ω) hfin : ℤ), -1]

Uses 5 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open cluster of a site · Exit index of a finite origin cluster · Origin of the hypercubic lattice

Used byPlus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionExistence of an anchored dual cycle around the origin cluster#✓fully proved

Some cycle of the face-boundary graph of the origin cluster is based at the upper exit face and is longer than the exit index.

def AnchoredCycleExists (ω : ConfigSpace (Sym2 (Site 2)))
    (hfin : (cluster 2 ω (origin 2)).Finite) : Prop :=
  ∃ c : (faceBoundaryGraph (cluster 2 ω (origin 2))).Walk
      (exitFaceUp (ω := ω) hfin) (exitFaceUp (ω := ω) hfin),
    c.IsCycle ∧ exitIndex (ω := ω) hfin < c.length

Uses 7 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open cluster of a site · Face above the exit edge · Exit index of a finite origin cluster · Face-boundary graph of a set · Origin of the hypercubic lattice

Used byAnchored dual cycles give the anchored enclosure property · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · \(p_c(\mathbb{Z}^2) < 1\) via the canonical contour, assuming anchored cycles

TheoremAnchored dual cycles give the anchored enclosure property#✓fully proved

If every finite origin cluster has an anchored dual cycle (AnchoredCycleExists), then the anchored enclosure property StatMech.Percolation.PcAnchoredEnclosure holds. This reduces the Peierls bound to AnchoredCycleExists; it does not prove that hypothesis.

theorem pcAnchoredEnclosure_of_anchoredCycle
    (hwind : ∀ (ω : ConfigSpace (Sym2 (Site 2))) (hfin : (cluster 2 ω (origin 2)).Finite),
        AnchoredCycleExists ω hfin) :
    StatMech.Percolation.PcAnchoredEnclosure

Uses 10 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Existence of an anchored dual cycle around the origin cluster · Site of the hypercubic lattice · Open cluster of a site · Anchored dual-circuit enclosure property · Origin of the hypercubic lattice

Proof usesFace above the exit edge · Exit index of a finite origin cluster · Face-boundary graph of a set · Anchor sites for dual circuits

Used by\(p_c(\mathbb{Z}^2) < 1\) via the canonical contour, assuming anchored cycles

DefinitionDual cycle reaching the left half-plane#✓fully proved

Some cycle of the face-boundary graph of the origin cluster, based at the upper exit face, visits a face whose first coordinate is at most zero.

def CycleHasLeftFace (ω : ConfigSpace (Sym2 (Site 2)))
    (hfin : (cluster 2 ω (origin 2)).Finite) : Prop :=
  ∃ c : (faceBoundaryGraph (cluster 2 ω (origin 2))).Walk
      (exitFaceUp (ω := ω) hfin) (exitFaceUp (ω := ω) hfin),
    c.IsCycle ∧ ∃ w ∈ c.support, w 0 ≤ 0

Uses 6 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open cluster of a site · Face above the exit edge · Face-boundary graph of a set · Origin of the hypercubic lattice

Used by\(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits

DefinitionBoundary edges of a set of sites in \(\mathbb{Z}^2\), as unordered pairs#✓fully proved

The edges of ℤ² with exactly one endpoint in S, as unordered pairs.

noncomputable def bdEdgeSet2 (S : Set (Site 2)) : Set (Sym2 (Site 2)) := by
  classical
  exact {e | Sym2.lift ⟨fun x y => (x ∈ S ↔ y ∉ S), by
    intro x y
    simp only [eq_iff_iff]
    by_cases hx : x ∈ S <;> by_cases hy : y ∈ S <;> tauto⟩ e}

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byCut lattice of a set of sites

DefinitionCut lattice of a set of sites#✓fully proved

The square lattice with the boundary edges of S deleted.

noncomputable def cutLattice (S : Set (Site 2)) : SimpleGraph (Site 2) :=
  (hypercubicLattice 2).deleteEdges (bdEdgeSet2 S)

Uses 3 · Used by 1

Statement usesSite of the hypercubic lattice · Boundary edges of a set of sites in \(\mathbb{Z}^2\), as unordered pairs · Hypercubic lattice \(\mathbb{Z}^d\)

Used byInside region of an open cluster in the cut lattice

DefinitionInside region of an open cluster in the cut lattice#✓fully proved

The sites reachable from o in the cut lattice of the open cluster of o.

def insideRegion (ω : ConfigSpace (Sym2 (Site 2))) (o : Site 2) : Set (Site 2) :=
  {x | (cutLattice (cluster 2 ω o)).Reachable o x}

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open cluster of a site · Cut lattice of a set of sites

DefinitionOpen cluster maps into the lattice minus its boundary edges#✓fully proved

The open subgraph on the cluster of o maps into the lattice with the boundary edges of the cluster removed.

noncomputable def clusterOpenToBarrierHom (o : Site 2) :
    (openSubgraph 2 ω).induce (cluster 2 ω o) →g latticeMinusBarrier (cluster 2 ω o) where
  toFun v := (v : Site 2)
  map_rel' := by
    intro a b hab
    have hopen : IsOpenEdge 2 ω (a : Site 2) (b : Site 2) := hab
    exact latticeMinusBarrier_adj_of_both_mem _ hopen.1 a.2 b.2

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Open lattice edge of a bond configuration · Site of the hypercubic lattice · Boundary edge of a set · Open cluster of a site · Hypercubic lattice \(\mathbb{Z}^d\) · Square lattice with the boundary edges of a set removed · Open subgraph of a bond configuration

Used byDiscrete Jordan separation for finite open clusters

DefinitionBox exterior maps into the lattice minus boundary edges#✓fully proved

The lattice on the exterior of a box disjoint from K maps into the lattice with the boundary edges of K removed.

noncomputable def extToBarrierHom (K : Set (Site 2)) (R : ℕ) (hsub : exterior 2 R ⊆ Kᶜ) :
    (hypercubicLattice 2).induce (exterior 2 R) →g latticeMinusBarrier K where
  toFun v := (v : Site 2)
  map_rel' := by
    intro a b hab
    exact latticeMinusBarrier_adj_of_both_not_mem _ hab (hsub a.2) (hsub b.2)

Uses 5 · Used by 1

Statement usesSite of the hypercubic lattice · Boundary edge of a set · Exterior of a box in \(\mathbb{Z}^d\) · Hypercubic lattice \(\mathbb{Z}^d\) · Square lattice with the boundary edges of a set removed

Used byDiscrete Jordan separation for finite open clusters

TheoremDiscrete Jordan separation for finite open clusters#✓fully proved

A discrete Jordan separation for a finite open cluster: removing its boundary edges leaves the cluster connected, the far exterior connected, and no path between the cluster and its complement.

theorem discrete_jordan_separation (o : Site 2) (hfin : (cluster 2 ω o).Finite) :
    ∃ R : ℕ, cluster 2 ω o ⊆ box 2 R ∧
      (∀ ⦃x y : Site 2⦄, x ∈ cluster 2 ω o → y ∈ cluster 2 ω o →
        (latticeMinusBarrier (cluster 2 ω o)).Reachable x y) ∧
      (∀ ⦃x y : Site 2⦄, x ∈ exterior 2 R → y ∈ exterior 2 R →
        (latticeMinusBarrier (cluster 2 ω o)).Reachable x y) ∧
      (∀ ⦃x y : Site 2⦄, x ∈ cluster 2 ω o → y ∉ cluster 2 ω o →
        ¬ (latticeMinusBarrier (cluster 2 ω o)).Reachable x y)

Uses 15

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Open cluster of a site · Exterior of a box in \(\mathbb{Z}^d\) · Square lattice with the boundary edges of a set removed

Proof usesConnection by an open path · Boundary edge of a set · Base point of the exterior of a box · Open cluster maps into the lattice minus its boundary edges · Box exterior maps into the lattice minus boundary edges · Every finite set of sites lies in a box · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Setting a set of coordinates of a lattice site

DefinitionSite on the negative horizontal axis#✓fully proved

The site (-k, 0) on the negative horizontal axis.

def leftAxisSite (k : ℕ) : Site 2 := ![-(k : ℤ), 0]

Uses 1 · Used by 8

Statement usesSite of the hypercubic lattice

Used byExit dart on the negative horizontal axis · Left exit index of a finite cluster · Left exit condition at an axis site · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionLeft exit condition at an axis site#✓fully proved

The site (-(k + 1), 0) is not in the open cluster of the origin.

def leftExitPred (ω : ConfigSpace (Sym2 (Site 2))) (k : ℕ) : Prop :=
  leftAxisSite (k + 1) ∉ cluster 2 ω (origin 2)

Uses 5 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open cluster of a site · Site on the negative horizontal axis · Origin of the hypercubic lattice

Used byLeft exit index of a finite cluster · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionLeft exit index of a finite cluster#✓fully proved

For a finite origin cluster, the least k such that (-(k + 1), 0) is not in the cluster.

noncomputable def leftExitIndex (hfin : (cluster 2 ω (origin 2)).Finite) : ℕ := by
  classical
  exact Nat.find (leftExitPred_exists (ω := ω) hfin)

Uses 8 · Used by 9

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path · Site of the hypercubic lattice · Open cluster of a site · Site on the negative horizontal axis · Left exit condition at an axis site · Open subgraph of a bond configuration · Origin of the hypercubic lattice

Used byExit dart on the negative horizontal axis · Face below the left exit edge · Face above the left exit edge · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionFace above the left exit edge#✓fully proved

The unit face directly above the left exit edge.

noncomputable def leftExitFaceUp (hfin : (cluster 2 ω (origin 2)).Finite) : Site 2 :=
  ![-(leftExitIndex (ω := ω) hfin : ℤ) - 1, 0]

Uses 5 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open cluster of a site · Left exit index of a finite cluster · Origin of the hypercubic lattice

Used byOrigin cluster's enclosing contour links the two axis exits · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionFace below the left exit edge#✓fully proved

The unit face directly below the left exit edge.

noncomputable def leftExitFaceDown (hfin : (cluster 2 ω (origin 2)).Finite) : Site 2 :=
  ![-(leftExitIndex (ω := ω) hfin : ℤ) - 1, -1]

Uses 5 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open cluster of a site · Left exit index of a finite cluster · Origin of the hypercubic lattice

Used by\(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionOrigin cluster's enclosing contour links the two axis exits#✓fully proved

Some cycle of the face-boundary graph of the origin cluster, based at the upper exit face on the positive axis, passes through the upper exit face on the negative axis.

def EnclosingContourLinksExits (ω : ConfigSpace (Sym2 (Site 2)))
    (hfin : (cluster 2 ω (origin 2)).Finite) : Prop :=
  ∃ c : (faceBoundaryGraph (cluster 2 ω (origin 2))).Walk
      (exitFaceUp (ω := ω) hfin) (exitFaceUp (ω := ω) hfin),
    c.IsCycle ∧ leftExitFaceUp (ω := ω) hfin ∈ c.support

Uses 7 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open cluster of a site · Face above the exit edge · Face-boundary graph of a set · Face above the left exit edge · Origin of the hypercubic lattice

Used by\(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · \(p_c(\mathbb{Z}^2) < 1\) via exit dart orbits, assuming linked exits

Theorem\(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits#✓fully proved

p_c(ℤ²) < 1, under the hypothesis that EnclosingContourLinksExits holds for every configuration with a finite origin cluster.

theorem pc_lt_one_via_boundary
    (h : ∀ (ω : ConfigSpace (Sym2 (Site 2))) (hfin : (cluster 2 ω (origin 2)).Finite),
        EnclosingContourLinksExits ω hfin) :
    StatMech.Percolation.pc 2 < 1

Uses 20 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Origin cluster's enclosing contour links the two axis exits · Site of the hypercubic lattice · Open cluster of a site · Origin of the hypercubic lattice · Critical probability of bond percolation on the hypercubic lattice

Proof usesExistence of an anchored dual cycle around the origin cluster · Dual cycle reaching the left half-plane · Boundary edge of a set · Face above the exit edge · Exit index of a finite origin cluster · Face-boundary graph of a set · Hypercubic lattice \(\mathbb{Z}^d\) · \(\ell^1\) distance on \(\mathbb{Z}^d\) · Face above the left exit edge · Left exit index of a finite cluster · Primal edge shared by adjacent faces · Anchored dual-circuit enclosure property · Anchor sites for dual circuits · \(p_c(2) < 1\) from anchored dual-circuit enclosure

Used by\(p_c(\mathbb{Z}^2) < 1\) via exit dart orbits, assuming linked exits

DefinitionExit dart on the positive horizontal axis#✓fully proved

The boundary dart of the origin cluster across the exit edge on the positive horizontal axis.

noncomputable def exitDart (hfin : (cluster 2 ω (origin 2)).Finite) : Dart where
  tail := axisSite (exitIndex (ω := ω) hfin)
  head := axisSite (exitIndex (ω := ω) hfin + 1)
  adj := axisSite_exit_adj (ω := ω) hfin

Uses 8 · Used by 12

Statement usesConfiguration space of a statistical-mechanics model · Dart of the square lattice · Site of the hypercubic lattice · Site on the positive horizontal axis · Open cluster of a site · Exit index of a finite origin cluster · Hypercubic lattice \(\mathbb{Z}^d\) · Origin of the hypercubic lattice

Used by\(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Canonical contour of a finite origin cluster · Darts of the canonical contour · Canonical contour is longer than the exit index · Closed face walk of the canonical contour · Exit dart of a finite origin cluster · Left and right exit darts lie in the same boundary orbit · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · Simplicity of the exit orbit's face walk · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

DefinitionExit dart on the negative horizontal axis#✓fully proved

The boundary dart of the origin cluster across the exit edge on the negative horizontal axis.

noncomputable def leftExitDart (hfin : (cluster 2 ω (origin 2)).Finite) : Dart where
  tail := leftAxisSite (leftExitIndex (ω := ω) hfin)
  head := leftAxisSite (leftExitIndex (ω := ω) hfin + 1)
  adj := leftAxisSite_exit_adj (ω := ω) hfin

Uses 8 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Dart of the square lattice · Site of the hypercubic lattice · Open cluster of a site · Hypercubic lattice \(\mathbb{Z}^d\) · Site on the negative horizontal axis · Left exit index of a finite cluster · Origin of the hypercubic lattice

Used byLeft and right exit darts lie in the same boundary orbit · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

DefinitionNegative part of an integer#✓fully proved

The negative part min z 0 of an integer.

noncomputable def negPart (z : ℤ) : ℤ := if z < 0 then z else 0

Used by 9

Used by\(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Closed face walk of the canonical contour · Face walk along the first successors of a boundary dart · Unit face to the left of a dart · Face walk along a boundary orbit · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

DefinitionUnit face to the left of a dart#✓fully proved

The unit face to the left of the dart e, labelled by its lower left corner.

noncomputable def dartFace (e : Dart) : Site 2 :=
  ![ e.tail 0 + negPart (e.dir 0) + negPart (rot90Fun e.dir 0),
     e.tail 1 + negPart (e.dir 1) + negPart (rot90Fun e.dir 1) ]

Uses 5 · Used by 19

Statement usesDart of the square lattice · Direction of a lattice dart · Site of the hypercubic lattice · Negative part of an integer · Quarter-turn rotation of the square lattice

Used byFace loop around the domino · Face loop left of one period of a boundary orbit · Minimal-period orbit loop as a lattice walk · No diagonal touch along a boundary orbit · Boundary orbit face loop as a lattice walk · No-pinch condition for a boundary orbit · Face loop around the unit cell · Faces visited by a boundary orbit in one period · \(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Visit times of a boundary orbit to a face · Closed face walk of the canonical contour · Face walk along the first successors of a boundary dart · Face loop of a boundary orbit in the face-boundary graph · Face walk along a boundary orbit · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · Simplicity of the exit orbit's face walk · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

DefinitionLeft and right exit darts lie in the same boundary orbit#✓fully proved

The left exit dart lies in the boundary orbit of the right exit dart.

def ExitDartsSameOrbit (ω : ConfigSpace (Sym2 (Site 2)))
    (hfin : (cluster 2 ω (origin 2)).Finite) : Prop :=
  ∃ n : ℕ, (dartNext (cluster 2 ω (origin 2)))^[n] (exitDart (ω := ω) hfin)
    = leftExitDart (ω := ω) hfin

Uses 8 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Dart of the square lattice · Site of the hypercubic lattice · Open cluster of a site · Successor of a boundary dart · Exit dart on the positive horizontal axis · Exit dart on the negative horizontal axis · Origin of the hypercubic lattice

Used by\(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Canonical orbit cycle condition · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

Theorem\(p_c(\mathbb{Z}^2) < 1\) via exit dart orbits, assuming linked exits#✓fully proved

p_c(ℤ²) < 1, under the hypothesis that EnclosingContourLinksExits holds for every configuration with a finite origin cluster.

theorem pc_lt_one_via_dartOrbit
    (h : ∀ (ω : ConfigSpace (Sym2 (Site 2))) (hfin : (cluster 2 ω (origin 2)).Finite),
        EnclosingContourLinksExits ω hfin) :
    StatMech.Percolation.pc 2 < 1

Uses 7

Statement usesConfiguration space of a statistical-mechanics model · Origin cluster's enclosing contour links the two axis exits · Site of the hypercubic lattice · Open cluster of a site · Origin of the hypercubic lattice · Critical probability of bond percolation on the hypercubic lattice

Proof uses\(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits

DefinitionUndirected lattice edge of a dart#✓fully proved

The undirected lattice edge underlying a dart.

def dartPrimalEdge (e : Dart) : Sym2 (Site 2) := s(e.tail, e.head)

Uses 2 · Used by 2

Statement usesDart of the square lattice · Site of the hypercubic lattice

Used byPrimal edges of the canonical contour · Event that every edge of the canonical contour is closed

DefinitionCanonical contour of a finite origin cluster#✓fully proved

The canonical contour of a finite origin cluster: the closed walk around the boundary orbit of the exit dart on the positive axis.

noncomputable def canonicalContour (hfin : (cluster 2 ω (origin 2)).Finite) :
    (dartSuccGraph (cluster 2 ω (origin 2))).Walk
      ⟨exitDart (ω := ω) hfin, exitDart_isBoundaryDart (ω := ω) hfin⟩
      ⟨exitDart (ω := ω) hfin, exitDart_isBoundaryDart (ω := ω) hfin⟩ :=
  dartOrbitWalk (cluster 2 ω (origin 2))
    ⟨exitDart (ω := ω) hfin, exitDart_isBoundaryDart (ω := ω) hfin⟩

Uses 14

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path · Dart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Site on the positive horizontal axis · Open cluster of a site · Closed walk around a boundary dart orbit · Successor graph on boundary darts · Exit dart on the positive horizontal axis · Exit index of a finite origin cluster · Axis site lies outside the origin cluster · Open subgraph of a bond configuration · Origin of the hypercubic lattice

DefinitionDarts of the canonical contour#✓fully proved

The darts of one period of the boundary orbit of the exit dart.

noncomputable def canonicalContourDarts (hfin : (cluster 2 ω (origin 2)).Finite) : List Dart :=
  (List.range (dartOrbitPeriod (cluster 2 ω (origin 2))
      ⟨exitDart (ω := ω) hfin, exitDart_isBoundaryDart (ω := ω) hfin⟩)).map
    (fun k => (dartNext (cluster 2 ω (origin 2)))^[k + 1] (exitDart (ω := ω) hfin))

Uses 14 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path · Dart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Site on the positive horizontal axis · Open cluster of a site · Successor of a boundary dart · Minimal period of a boundary dart · Exit dart on the positive horizontal axis · Exit index of a finite origin cluster · Axis site lies outside the origin cluster · Open subgraph of a bond configuration · Origin of the hypercubic lattice

Used byPrimal edges of the canonical contour · Event that every edge of the canonical contour is closed

DefinitionPrimal edges of the canonical contour#✓fully proved

The primal edges of the canonical contour.

noncomputable def canonicalPrimalEdgeFinset (hfin : (cluster 2 ω (origin 2)).Finite) :
    Finset (Sym2 (Site 2)) :=
  ((canonicalContourDarts (ω := ω) hfin).map dartPrimalEdge).toFinset

Uses 7

Statement usesConfiguration space of a statistical-mechanics model · Dart of the square lattice · Site of the hypercubic lattice · Darts of the canonical contour · Open cluster of a site · Undirected lattice edge of a dart · Origin of the hypercubic lattice

DefinitionEvent that every edge of the canonical contour is closed#✓fully proved

The set of configurations in which every primal edge of the canonical contour of ω is closed.

def closedDartContourEvent (hfin : (cluster 2 ω (origin 2)).Finite) :
    Set (ConfigSpace (Sym2 (Site 2))) :=
  {η | ∀ D ∈ canonicalContourDarts (ω := ω) hfin, η (dartPrimalEdge D) = false}

Uses 7

Statement usesConfiguration space of a statistical-mechanics model · Dart of the square lattice · Site of the hypercubic lattice · Darts of the canonical contour · Open cluster of a site · Undirected lattice edge of a dart · Origin of the hypercubic lattice

DefinitionCanonical contour is longer than the exit index#✓fully proved

The period of the canonical contour exceeds the exit index, the length condition of an anchored enclosure.

def CanonicalContourWinds (ω : ConfigSpace (Sym2 (Site 2)))
    (hfin : (cluster 2 ω (origin 2)).Finite) : Prop :=
  exitIndex (ω := ω) hfin
    < dartOrbitPeriod (cluster 2 ω (origin 2))
        ⟨exitDart (ω := ω) hfin, exitDart_isBoundaryDart (ω := ω) hfin⟩

Uses 13

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path · Dart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Site on the positive horizontal axis · Open cluster of a site · Minimal period of a boundary dart · Exit dart on the positive horizontal axis · Exit index of a finite origin cluster · Axis site lies outside the origin cluster · Open subgraph of a bond configuration · Origin of the hypercubic lattice

DefinitionFace walk along the first successors of a boundary dart#✓fully proved

The walk of faces to the left of the first n successors of a boundary dart.

noncomputable def canonicalFaceWalkAux (K : Set (Site 2)) (e : Dart) (he : IsBoundaryDart K e) :
    (n : ℕ) → (faceBoundaryGraph K).Walk (dartFace e) (dartFace ((dartNext K)^[n] e))
  | 0 => SimpleGraph.Walk.nil
  | (n + 1) =>
      (canonicalFaceWalkAux K e he n).concat (by
        rw [Function.iterate_succ_apply']
        exact dartFace_step_adj K _ (iterate_isBoundaryDart K e he n))

Uses 17 · Used by 1

Statement usesDart of the square lattice · Direction of a lattice dart · Boundary dart of a set of sites · Site of the hypercubic lattice · Boundary edge of a set · Unit face to the left of a dart · Successor of a boundary dart · Face-boundary graph of a set · Lower left corner of the unit face at \((a, b)\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Hypercubic lattice \(\mathbb{Z}^d\) · Dart from a site in a unit direction · Negative part of an integer · Quarter-turn rotation of the square lattice · Primal edge shared by adjacent faces · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byClosed face walk of the canonical contour

DefinitionClosed face walk of the canonical contour#✓fully proved

The closed walk of faces to the left of the darts of the canonical contour, based at the upper exit face.

StatMech.Lattice.canonicalFaceWalk · 16 lines

noncomputable def canonicalFaceWalk (hfin : (cluster 2 ω (origin 2)).Finite) :
    (faceBoundaryGraph (cluster 2 ω (origin 2))).Walk
      (exitFaceUp (ω := ω) hfin) (exitFaceUp (ω := ω) hfin) := by
  refine (canonicalFaceWalkAux (cluster 2 ω (origin 2)) (exitDart (ω := ω) hfin)
    (exitDart_isBoundaryDart (ω := ω) hfin)
    (dartOrbitPeriod (cluster 2 ω (origin 2))
      ⟨exitDart (ω := ω) hfin, exitDart_isBoundaryDart (ω := ω) hfin⟩)).copy
    (dartFace_exitDart (ω := ω) hfin) ?_
  have hret : (dartNext (cluster 2 ω (origin 2)))^[dartOrbitPeriod (cluster 2 ω (origin 2))
        ⟨exitDart (ω := ω) hfin, exitDart_isBoundaryDart (ω := ω) hfin⟩]
        (exitDart (ω := ω) hfin) = exitDart (ω := ω) hfin := by
    have := dartOrbitPeriod_iterate (cluster 2 ω (origin 2))
      ⟨exitDart (ω := ω) hfin, exitDart_isBoundaryDart (ω := ω) hfin⟩
    have h2 := congrArg Subtype.val this
    rwa [dartNextSub_iterate_val] at h2
  rw [hret, dartFace_exitDart (ω := ω) hfin]

Uses 22

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path · Dart of the square lattice · Direction of a lattice dart · Boundary dart of a set of sites · Site of the hypercubic lattice · Site on the positive horizontal axis · Face walk along the first successors of a boundary dart · Open cluster of a site · Unit face to the left of a dart · Successor of a boundary dart · Successor map on boundary darts · Minimal period of a boundary dart · Exit dart on the positive horizontal axis · Face above the exit edge · Exit index of a finite origin cluster · Axis site lies outside the origin cluster · Face-boundary graph of a set · Negative part of an integer · Open subgraph of a bond configuration · Quarter-turn rotation of the square lattice · Origin of the hypercubic lattice

Theorem\(p_c(\mathbb{Z}^2) < 1\) via the canonical contour, assuming anchored cycles#✓fully proved

p_c(ℤ²) < 1, under the hypothesis that AnchoredCycleExists holds for every configuration with a finite origin cluster.

theorem pc_lt_one_via_canonicalContour
    (hres : ∀ (ω : ConfigSpace (Sym2 (Site 2))) (hfin : (cluster 2 ω (origin 2)).Finite),
        AnchoredCycleExists ω hfin) :
    StatMech.Percolation.pc 2 < 1

Uses 8

Statement usesConfiguration space of a statistical-mechanics model · Existence of an anchored dual cycle around the origin cluster · Site of the hypercubic lattice · Open cluster of a site · Origin of the hypercubic lattice · Critical probability of bond percolation on the hypercubic lattice

Proof usesAnchored dual cycles give the anchored enclosure property · \(p_c(2) < 1\) from anchored dual-circuit enclosure

DefinitionFace walk along a boundary orbit#✓fully proved

The walk in the face-boundary graph of K through the faces of e and its first n successors.

noncomputable def dartOrbitFaceWalk (K : Set (Site 2)) (e : Dart) (he : IsBoundaryDart K e) :
    (n : ℕ) → (faceBoundaryGraph K).Walk (dartFace e) (dartFace ((dartNext K)^[n] e))
  | 0 => SimpleGraph.Walk.nil
  | (n + 1) =>
      ((dartOrbitFaceWalk K e he n).concat
        (dartFace_step_adj K _ (iterate_isBoundaryDart K e he n))).copy rfl (by
          rw [Function.iterate_succ_apply'])

Uses 17 · Used by 7

Statement usesDart of the square lattice · Direction of a lattice dart · Boundary dart of a set of sites · Site of the hypercubic lattice · Boundary edge of a set · Unit face to the left of a dart · Successor of a boundary dart · Face-boundary graph of a set · Lower left corner of the unit face at \((a, b)\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Hypercubic lattice \(\mathbb{Z}^d\) · Dart from a site in a unit direction · Negative part of an integer · Quarter-turn rotation of the square lattice · Primal edge shared by adjacent faces · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byFace loop around the domino · Face loop left of one period of a boundary orbit · Face loop around the unit cell · Face loop of a boundary orbit in the face-boundary graph · Minimal-period face loop of the exit orbit · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

DefinitionFace loop of a boundary orbit in the face-boundary graph#✓fully proved

The closed walk of faces along one period of the boundary orbit of e, for finite K.

noncomputable def dartOrbitFaceLoop (K : Set (Site 2)) (hK : K.Finite) (e : Dart)
    (he : IsBoundaryDart K e) : (faceBoundaryGraph K).Walk (dartFace e) (dartFace e) :=
  (dartOrbitFaceWalk K e he (dartNext_periodic K hK e he).choose).copy rfl (by
    rw [(dartNext_periodic K hK e he).choose_spec.2])

Uses 15 · Used by 3

Statement usesDart of the square lattice · Direction of a lattice dart · Boundary dart of a set of sites · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Unit face to the left of a dart · Successor of a boundary dart · Successor map on boundary darts · Face walk along a boundary orbit · Face-boundary graph of a set · Hypercubic lattice \(\mathbb{Z}^d\) · Dart from a site in a unit direction · Quarter-turn rotation as a permutation · Quarter-turn rotation of the square lattice · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byBoundary orbit face loop as a lattice walk · Face loop of the exit orbit of a finite cluster · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

DefinitionFace loop of the exit orbit of a finite cluster#✓fully proved

The closed face walk of the exit orbit of a finite origin cluster, based at the upper exit face.

noncomputable def exitOrbitFaceLoop (hfin : (cluster 2 ω (origin 2)).Finite) :
    (faceBoundaryGraph (cluster 2 ω (origin 2))).Walk
      (exitFaceUp (ω := ω) hfin) (exitFaceUp (ω := ω) hfin) :=
  (dartOrbitFaceLoop (cluster 2 ω (origin 2)) hfin (exitDart (ω := ω) hfin)
    (exitDart_isBoundaryDart (ω := ω) hfin)).copy
      (dartFace_exitDart (ω := ω) hfin) (dartFace_exitDart (ω := ω) hfin)

Uses 19 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path · Dart of the square lattice · Direction of a lattice dart · Boundary dart of a set of sites · Site of the hypercubic lattice · Site on the positive horizontal axis · Open cluster of a site · Unit face to the left of a dart · Face loop of a boundary orbit in the face-boundary graph · Exit dart on the positive horizontal axis · Face above the exit edge · Exit index of a finite origin cluster · Axis site lies outside the origin cluster · Face-boundary graph of a set · Negative part of an integer · Open subgraph of a bond configuration · Quarter-turn rotation of the square lattice · Origin of the hypercubic lattice

Used byCanonical orbit cycle condition · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

DefinitionCanonical orbit cycle condition#✓fully proved

The face loop of the exit orbit is a cycle, and the left exit dart lies in the exit orbit.

def CanonicalOrbitCycle (ω : ConfigSpace (Sym2 (Site 2)))
    (hfin : (cluster 2 ω (origin 2)).Finite) : Prop :=
  (exitOrbitFaceLoop (ω := ω) hfin).IsCycle ∧ ExitDartsSameOrbit ω hfin

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Left and right exit darts lie in the same boundary orbit · Site of the hypercubic lattice · Open cluster of a site · Face above the exit edge · Face loop of the exit orbit of a finite cluster · Face-boundary graph of a set · Origin of the hypercubic lattice

Used by\(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

Theorem\(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle#✓fully proved

p_c(ℤ²) < 1, under the hypothesis that CanonicalOrbitCycle holds for every configuration with a finite origin cluster.

theorem pc_lt_one_orbit
    (h : ∀ (ω : ConfigSpace (Sym2 (Site 2))) (hfin : (cluster 2 ω (origin 2)).Finite),
        CanonicalOrbitCycle ω hfin) :
    (StatMech.Percolation.pc 2 : ℝ) < 1

Uses 46

Statement usesConfiguration space of a statistical-mechanics model · Canonical orbit cycle condition · Site of the hypercubic lattice · Open cluster of a site · Origin of the hypercubic lattice · Critical probability of bond percolation on the hypercubic lattice

Proof usesExistence of an anchored dual cycle around the origin cluster · Connection by an open path · Dual cycle reaching the left half-plane · Dart of the square lattice · Direction of a lattice dart · Left and right exit darts lie in the same boundary orbit · Boundary dart of a set of sites · Site on the positive horizontal axis · Boundary edge of a set · Box \((-n, n)^d\) in the hypercubic lattice · Unit face to the left of a dart · Successor of a boundary dart · Successor map on boundary darts · Face loop of a boundary orbit in the face-boundary graph · Face walk along a boundary orbit · Exit dart on the positive horizontal axis · Face above the exit edge · Exit index of a finite origin cluster · Face loop of the exit orbit of a finite cluster · Axis site lies outside the origin cluster · Face-boundary graph of a set · Lower left corner of the unit face at \((a, b)\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Hypercubic lattice \(\mathbb{Z}^d\) · \(\ell^1\) distance on \(\mathbb{Z}^d\) · Site on the negative horizontal axis · Exit dart on the negative horizontal axis · Face below the left exit edge · Left exit index of a finite cluster · Dart from a site in a unit direction · Negative part of an integer · Open subgraph of a bond configuration · Quarter-turn rotation as a permutation · Quarter-turn rotation of the square lattice · Primal edge shared by adjacent faces · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\) · Anchored dual-circuit enclosure property · Anchor sites for dual circuits · \(p_c(2) < 1\) from anchored dual-circuit enclosure

DefinitionExit dart of a finite origin cluster#✓fully proved

The exit dart of a finite origin cluster, as an element of the subtype of boundary darts.

noncomputable def exitBaseSub (hfin : (cluster 2 ω (origin 2)).Finite) :
    {d : Dart // IsBoundaryDart (cluster 2 ω (origin 2)) d} :=
  ⟨exitDart (ω := ω) hfin, exitDart_isBoundaryDart (ω := ω) hfin⟩

Uses 12 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path · Dart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Site on the positive horizontal axis · Open cluster of a site · Exit dart on the positive horizontal axis · Exit index of a finite origin cluster · Axis site lies outside the origin cluster · Open subgraph of a bond configuration · Origin of the hypercubic lattice

Used by\(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Minimal-period face loop of the exit orbit · Simplicity of the exit orbit's face walk · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits

DefinitionMinimal-period face loop of the exit orbit#✓fully proved

The closed walk of faces along one period of the exit orbit, based at the upper exit face.

noncomputable def exitMinFaceLoop (hfin : (cluster 2 ω (origin 2)).Finite) :
    (faceBoundaryGraph (cluster 2 ω (origin 2))).Walk
      (exitFaceUp (ω := ω) hfin) (exitFaceUp (ω := ω) hfin) :=
  ((dartOrbitFaceWalk (cluster 2 ω (origin 2)) (exitDart (ω := ω) hfin)
    (exitDart_isBoundaryDart (ω := ω) hfin)
    (dartOrbitPeriod (cluster 2 ω (origin 2)) (exitBaseSub (ω := ω) hfin))).copy
      rfl (by rw [exit_period_closure (ω := ω) hfin])).copy
      (dartFace_exitDart (ω := ω) hfin) (dartFace_exitDart (ω := ω) hfin)

Uses 23 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path · Dart of the square lattice · Direction of a lattice dart · Boundary dart of a set of sites · Site of the hypercubic lattice · Site on the positive horizontal axis · Open cluster of a site · Unit face to the left of a dart · Successor of a boundary dart · Successor map on boundary darts · Face walk along a boundary orbit · Minimal period of a boundary dart · Exit dart of a finite origin cluster · Exit dart on the positive horizontal axis · Face above the exit edge · Exit index of a finite origin cluster · Axis site lies outside the origin cluster · Face-boundary graph of a set · Negative part of an integer · Open subgraph of a bond configuration · Quarter-turn rotation of the square lattice · Origin of the hypercubic lattice

Used by\(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits

DefinitionSimplicity of the exit orbit's face walk#✓fully proved

The exit orbit has period at least three and visits distinct faces during one period.

def OrbitFaceSimple (ω : ConfigSpace (Sym2 (Site 2)))
    (hfin : (cluster 2 ω (origin 2)).Finite) : Prop :=
  3 ≤ dartOrbitPeriod (cluster 2 ω (origin 2)) (exitBaseSub (ω := ω) hfin) ∧
    Set.InjOn (fun k => dartFace ((dartNext (cluster 2 ω (origin 2)))^[k] (exitDart (ω := ω) hfin)))
      (Set.Iio (dartOrbitPeriod (cluster 2 ω (origin 2)) (exitBaseSub (ω := ω) hfin)))

Uses 10 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Dart of the square lattice · Site of the hypercubic lattice · Open cluster of a site · Unit face to the left of a dart · Successor of a boundary dart · Minimal period of a boundary dart · Exit dart of a finite origin cluster · Exit dart on the positive horizontal axis · Origin of the hypercubic lattice

Used by\(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits

Theorem\(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits#✓fully proved

p_c(ℤ²) < 1, under the hypothesis that for every configuration with a finite origin cluster the exit orbit is simple (OrbitFaceSimple) and contains the left exit dart.

theorem pc_lt_one_of_orbitFaceSimple
    (h : ∀ (ω : ConfigSpace (Sym2 (Site 2))) (hfin : (cluster 2 ω (origin 2)).Finite),
        OrbitFaceSimple ω hfin ∧ ExitDartsSameOrbit ω hfin) :
    (StatMech.Percolation.pc 2 : ℝ) < 1

Uses 47 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Left and right exit darts lie in the same boundary orbit · Simplicity of the exit orbit's face walk · Site of the hypercubic lattice · Open cluster of a site · Origin of the hypercubic lattice · Critical probability of bond percolation on the hypercubic lattice

Proof usesExistence of an anchored dual cycle around the origin cluster · Connection by an open path · Dual cycle reaching the left half-plane · Dart of the square lattice · Direction of a lattice dart · Boundary dart of a set of sites · Site on the positive horizontal axis · Boundary edge of a set · Box \((-n, n)^d\) in the hypercubic lattice · Unit face to the left of a dart · Successor of a boundary dart · Successor map on boundary darts · Face walk along a boundary orbit · Minimal period of a boundary dart · Exit dart of a finite origin cluster · Exit dart on the positive horizontal axis · Face above the exit edge · Exit index of a finite origin cluster · Minimal-period face loop of the exit orbit · Axis site lies outside the origin cluster · Face-boundary graph of a set · Lower left corner of the unit face at \((a, b)\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Hypercubic lattice \(\mathbb{Z}^d\) · \(\ell^1\) distance on \(\mathbb{Z}^d\) · Site on the negative horizontal axis · Exit dart on the negative horizontal axis · Face below the left exit edge · Left exit index of a finite cluster · Dart from a site in a unit direction · Negative part of an integer · Open subgraph of a bond configuration · Quarter-turn rotation as a permutation · Quarter-turn rotation of the square lattice · Primal edge shared by adjacent faces · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\) · Anchored dual-circuit enclosure property · Anchor sites for dual circuits · \(p_c(2) < 1\) from anchored dual-circuit enclosure

Used by\(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis

DefinitionSet and walk interior share boundary edges#✓fully proved

The set K and the inside jec_leftRegion Vc of the closed walk Vc have the same boundary edges.

def pww_BdEdgeMatch (K : Set (Site 2)) {a : Site 2} (Vc : (hypercubicLattice 2).Walk a a) : Prop :=
  ∀ e : Sym2 (Site 2), bdEdge K e ↔ bdEdge (jec_leftRegion Vc) e

Uses 4

Statement usesSite of the hypercubic lattice · Boundary edge of a set · Hypercubic lattice \(\mathbb{Z}^d\) · Inside of a closed walk by the even-odd rule

46 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.