Wired random-cluster measures decrease with the box

48 fully proved

A. Conditioning on the configuration outside the inner box

DefinitionOuter part of a configuration on \(\Lambda_{n+1}\)#✓fully proved

Project a configuration on Λ_(n+1) to its outer part: edges of Λ_n closed, the others unchanged.

noncomputable def outProj (d n : ℕ) (ρ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    ConfigSpace (Sym2 (boxVerts d (n + 1))) :=
  psiExt d n ρ (fun _ => false)

Uses 3 · Used by 11

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Gluing a box configuration into an outer configuration

Used byDecomposition of the free measure over the outer configuration · One-step box monotonicity of free measures for \(q \ge 1\) · Fibre masses of the free measure sum to one · Outer projection agrees with the configuration off \(\Lambda_n\) · Configurations with a given outer part form its conditioning fibre · Outer projection closes the edges of \(\Lambda_n\) · Outer projection keeps the edges outside \(\Lambda_n\) · Outer projection is idempotent · Masses of the conditioning fibres sum to one · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations · Wired box measures decrease on inner increasing events for \(q \ge 1\)

LemmaOuter projection closes the edges of \(\Lambda_n\)#✓fully proved

The projection closes edges of Λ_n.

lemma outProj_eq_false_of_range (n : ℕ) (ρ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    {e : Sym2 (boxVerts d (n + 1))} (he : e ∈ Set.range (innerEdge d n)) :
    outProj d n ρ e = false

Uses 8 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into the next box · Outer part of a configuration on \(\Lambda_{n+1}\)

Proof usesInclusion of box vertices into the next box · Gluing a box configuration into an outer configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byConfigurations with a given outer part form its conditioning fibre · Outer projection is idempotent

LemmaOuter projection keeps the edges outside \(\Lambda_n\)#✓fully proved

The projection keeps edges outside Λ_n.

lemma outProj_eq_of_not_range (n : ℕ) (ρ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    {e : Sym2 (boxVerts d (n + 1))} (he : e ∉ Set.range (innerEdge d n)) :
    outProj d n ρ e = ρ e

Uses 7 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into the next box · Outer part of a configuration on \(\Lambda_{n+1}\)

Proof usesGluing a box configuration into an outer configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byOuter projection agrees with the configuration off \(\Lambda_n\) · Configurations with a given outer part form its conditioning fibre · Outer projection is idempotent

LemmaOuter projection agrees with the configuration off \(\Lambda_n\)#✓fully proved

The projection agrees with the configuration off the edges of Λ_n.

lemma agreesOff_outProj (n : ℕ) (ρ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    AgreesOff (innerEdgeFinset d n) (outProj d n ρ) ρ

Uses 9

Statement usesConfiguration space of a statistical-mechanics model · Agreement of configurations off an edge set · Vertices of the box \((-n, n)^d\) · Edges of the next box coming from the inner box · Outer part of a configuration on \(\Lambda_{n+1}\)

Proof usesInclusion of box edges into the next box · Outer projection keeps the edges outside \(\Lambda_n\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

LemmaOuter projection is idempotent#✓fully proved

The projection is idempotent.

lemma outProj_idem (n : ℕ) (ρ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    outProj d n (outProj d n ρ) = outProj d n ρ

Uses 8 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Outer part of a configuration on \(\Lambda_{n+1}\)

Proof usesInclusion of box edges into the next box · Outer projection closes the edges of \(\Lambda_n\) · Outer projection keeps the edges outside \(\Lambda_n\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byDecomposition of the free measure over the outer configuration · Fibre masses of the free measure sum to one · Masses of the conditioning fibres sum to one · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations

LemmaConfigurations with a given outer part form its conditioning fibre#✓fully proved

The configurations with outer part ψ form the conditioning fibre of ψ.

lemma filter_outProj_eq_condFibre (n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    (hψ : outProj d n ψ = ψ) :
    Finset.univ.filter (fun ρ => outProj d n ρ = ψ)
      = condFibre (innerEdgeFinset d n) ψ

Uses 11 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Fibre of configurations agreeing off an edge set · Edges of the next box coming from the inner box · Outer part of a configuration on \(\Lambda_{n+1}\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesAgreement of configurations off an edge set · Inclusion of box edges into the next box · Outer projection closes the edges of \(\Lambda_n\) · Outer projection keeps the edges outside \(\Lambda_n\)

Used byDecomposition of the free measure over the outer configuration · Fibre masses of the free measure sum to one · Masses of the conditioning fibres sum to one · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations

LemmaConfigurations agreeing off \(F\) have the same conditioning fibre#✓fully proved

Configurations agreeing off F have the same conditioning fibre.

lemma condFibre_congr_dom {V : Type*} [Fintype V] [DecidableEq V]
    {F : Finset (Sym2 V)} {ψ ψ' : ConfigSpace (Sym2 V)} (h : AgreesOff F ψ ψ') :
    condFibre F ψ = condFibre F ψ'

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Agreement of configurations off an edge set · Fibre of configurations agreeing off an edge set

Used byConfigurations agreeing off \(F\) have equal conditional probabilities

LemmaConfigurations agreeing off \(F\) have equal conditional probabilities#✓fully proved

Configurations agreeing off F give the same conditional random-cluster probabilities.

lemma condBcProb_congr_dom {V : Type*} [Fintype V] [DecidableEq V] (G C : SimpleGraph V)
    [DecidableRel G.Adj] [DecidableRel C.Adj]
    (p q : ℝ) (F : Finset (Sym2 V)) (ψ ψ' ω : ConfigSpace (Sym2 V)) (h : AgreesOff F ψ ψ') :
    condBcProb G C p q F ψ ω = condBcProb G C p q F ψ' ω

Uses 7 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Agreement of configurations off an edge set · Conditional random-cluster measure with a boundary wiring

Proof usesRandom-cluster weight with a boundary wiring · Fibre of configurations agreeing off an edge set · Configurations agreeing off \(F\) have the same conditioning fibre · Partition function of a conditioning fibre

Used byLaw of total probability over outside configurations · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations

LemmaMasses of the conditioning fibres sum to one#✓fully proved

The masses of the conditioning fibres over all outer configurations sum to 1.

lemma sum_fibreMass_eq_one (n : ℕ) {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    ∑ ψ ∈ Finset.univ.filter (fun ψ => outProj d n ψ = ψ),
        (∑ σ ∈ condFibre (innerEdgeFinset d n) ψ,
          bcProb (boxGraph d (n + 1)) (boundaryCliqueGraph (boxBoundary d (n + 1))) p q σ) = 1

Uses 18 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Vertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Fibre of configurations agreeing off an edge set · Edges of the next box coming from the inner box · Outer part of a configuration on \(\Lambda_{n+1}\) · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Boundary wiring relation

Proof usesRandom-cluster weight with a boundary wiring · Partition function with a boundary wiring · Bernoulli edge product · Configurations with a given outer part form its conditioning fibre · Number of clusters under a boundary wiring · Outer projection is idempotent

Used byWired box measures decrease on inner increasing events for \(q \ge 1\)

LemmaWired \(\Lambda_{n+1}\) measure decomposed over outer configurations#✓fully proved

Decomposition of the wired measure on Λ_(n+1) over the configuration outside Λ_n.

lemma wiredSucc_bcProb_decompose (n : ℕ) {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (B : Set (ConfigSpace (Sym2 (boxVerts d (n + 1))))) :
    (∑ ρ, B.indicator (fun _ => (1 : ℝ)) ρ
        * bcProb (boxGraph d (n + 1)) (boundaryCliqueGraph (boxBoundary d (n + 1))) p q ρ)
      = ∑ ψ ∈ Finset.univ.filter (fun ψ => outProj d n ψ = ψ),
          (∑ σ ∈ condFibre (innerEdgeFinset d n) ψ,
            bcProb (boxGraph d (n + 1)) (boundaryCliqueGraph (boxBoundary d (n + 1))) p q σ)
          * (∑ ρ, B.indicator (fun _ => (1 : ℝ)) ρ
              * condBcProb (boxGraph d (n + 1)) (boundaryCliqueGraph (boxBoundary d (n + 1))) p q
                  (innerEdgeFinset d n) ψ ρ)

Uses 20 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Vertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Conditional random-cluster measure with a boundary wiring · Fibre of configurations agreeing off an edge set · Edges of the next box coming from the inner box · Outer part of a configuration on \(\Lambda_{n+1}\) · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Boundary wiring relation

Proof usesAgreement of configurations off an edge set · Disintegration of a boundary-wired measure over conditioning fibres · Random-cluster weight with a boundary wiring · Configurations agreeing off \(F\) have equal conditional probabilities · Configurations with a given outer part form its conditioning fibre · Partition function of a conditioning fibre · Outer projection is idempotent

Used byWired box measures decrease on inner increasing events for \(q \ge 1\)

B. Domination by the smaller wired box

LemmaConditional wired decrease on inner increasing events for \(q \ge 1\)#✓fully proved

For q ≥ 1, conditionally on any outer configuration, the wired measure on Λ_(n+1) gives an increasing event of Λ_n at most its wired Λ_n probability.

lemma condBcProb_innerRestrict_le (n : ℕ) {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    {A₀ : Set (ConfigSpace (Sym2 (boxVerts d n)))} (hA₀ : IsIncreasing A₀) :
    (∑ ρ, (innerRestrict d n ⁻¹' A₀).indicator (fun _ => (1 : ℝ)) ρ
        * condBcProb (boxGraph d (n + 1)) (boundaryCliqueGraph (boxBoundary d (n + 1))) p q
            (innerEdgeFinset d n) ψ ρ)
      ≤ ∑ ω, A₀.indicator (fun _ => (1 : ℝ)) ω
          * wiredFkProb (boxGraph d n) (boxBoundary d n) p q ω

Uses 24 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Conditional random-cluster measure with a boundary wiring · Edges of the next box coming from the inner box · Restriction of a next-box configuration to the inner edges · Wired random-cluster probability of a configuration · Increasing event · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Boundary wiring relation

Proof usesAgreement of configurations off an edge set · Random-cluster probability with a boundary wiring · Random-cluster weight with a boundary wiring · Inclusion of box vertices into the next box · Wired box measure dominates the induced-wiring measure for \(q \ge 1\) · Domain Markov property for the wired measure on nested boxes · Fibre of configurations agreeing off an edge set · Partition function of a conditioning fibre · Wiring induced on a box through the outer graph · Inclusion of box edges into the next box · Gluing a box configuration into an outer configuration

Used byWired box measures decrease on inner increasing events for \(q \ge 1\)

LemmaWired box measures decrease on inner increasing events for \(q \ge 1\)#✓fully proved

For q ≥ 1, the wired measure on Λ_(n+1) gives an increasing event of Λ_n at most its wired Λ_n probability.

lemma wiredSucc_bcProb_innerEvent_le (n : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    {A₀ : Set (ConfigSpace (Sym2 (boxVerts d n)))} (hA₀ : IsIncreasing A₀) :
    (∑ ρ, (innerRestrict d n ⁻¹' A₀).indicator (fun _ => (1 : ℝ)) ρ
        * bcProb (boxGraph d (n + 1)) (boundaryCliqueGraph (boxBoundary d (n + 1))) p q ρ)
      ≤ ∑ ω, A₀.indicator (fun _ => (1 : ℝ)) ω
          * wiredFkProb (boxGraph d n) (boxBoundary d n) p q ω

Uses 23 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Vertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Restriction of a next-box configuration to the inner edges · Wired random-cluster probability of a configuration · Increasing event · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Boundary wiring relation

Proof usesRandom-cluster weight with a boundary wiring · Partition function with a boundary wiring · Conditional random-cluster measure with a boundary wiring · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Fibre of configurations agreeing off an edge set · Bernoulli edge product · Edges of the next box coming from the inner box · Number of clusters under a boundary wiring · Outer part of a configuration on \(\Lambda_{n+1}\) · Masses of the conditioning fibres sum to one · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Wired box measures decrease on increasing cylinder events at \(q = 2\) · Per-box uniqueness of the random-cluster measures off a countable set

LemmaWired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum#✓fully proved

The wired Λ_(n+1) measure of a Λ_n cylinder event, as a finite sum.

lemma wiredFiniteMeasure_succ_real_innerRestrictEvent (n : ℕ) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1)
    (S : Set (ConfigSpace (Sym2 (boxVerts d n))))
    (hmeas : MeasurableSet (boxRestrict d n ⁻¹' S)) :
    (wiredFiniteMeasure d (n + 1) hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d n ⁻¹' S)
      = ∑ ρ : ConfigSpace (Sym2 (boxVerts d (n + 1))),
          (innerRestrict d n ⁻¹' S).indicator (fun _ => (1 : ℝ)) ρ
            * bcProb (boxGraph d (n + 1)) (boundaryCliqueGraph (boxBoundary d (n + 1))) p 2 ρ

Uses 23 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Restriction of a next-box configuration to the inner edges · Wired random-cluster measure on a box · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Boundary wiring relation

Proof usesBoundary clique gives the wired random-cluster measure · Inclusion of box vertices into the next box · Inclusion of box edges into \(\mathbb{Z}^d\) · Bernoulli edge product · Extension of a box configuration by closed edges · Inclusion of box edges into the next box · Wired random-cluster measure as a probability mass function · Wired random-cluster probability of a configuration · Wired random-cluster weight · Wired random-cluster partition function · Number of open clusters with wired boundary conditions

Used byWired box measures decrease on increasing cylinder events at \(q = 2\)

LemmaWired box measures decrease on increasing cylinder events at \(q = 2\)#✓fully proved

For q = 2, the wired Λ_(n+1) measure of an increasing Λ_n cylinder event is at most its wired Λ_n probability.

lemma wiredFiniteMeasure_succ_le_smallerBox (n : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    {S : Set (ConfigSpace (Sym2 (boxVerts d n)))} (hS : IsIncreasing S)
    (hmeas : MeasurableSet (boxRestrict d n ⁻¹' S)) :
    (wiredFiniteMeasure d (n + 1) hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d n ⁻¹' S)
      ≤ ∑ ω, S.indicator (fun _ => (1 : ℝ)) ω
          * wiredFkProb (boxGraph d n) (boxBoundary d n) p 2 ω

Uses 16 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Wired random-cluster measure on a box · Wired random-cluster probability of a configuration · Increasing event · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesRandom-cluster probability with a boundary wiring · Restriction of a next-box configuration to the inner edges · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Complete graph on the boundary vertices · Boundary wiring relation

Used byWired \(q = 2\) increasing-event probabilities do not grow with the box · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{m+1}\) at most in \(\Lambda_m\), \(m \ge n\)

C. Box-boundary connection events

LemmaOrigin-to-boundary connection is an increasing event#✓fully proved

The event that the origin is connected to the box boundary is increasing.

lemma isIncreasing_connToBdryEvent (n : ℕ) :
    IsIncreasing {ω : ConfigSpace (Sym2 (boxVerts d n)) |
      ConnToBdry (boxGraph d n) (boxBoundary d n) ω (IsingFK.boxOrigin d n)}

Uses 10 · Used by 8

Statement usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Increasing event · Open connection of a vertex to the boundary · Origin as a vertex of the box graph

Proof usesOpen connection between two vertices · Open subgraph of an edge configuration · Monotonicity of the open subgraph in the configuration

Used byMonotonicity in \(p\) of the Bernoulli percolation probability · Wired \(q = 2\) origin-to-boundary probability at most Bernoulli · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\)

LemmaWired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\)#✓fully proved

For q = 2, φ¹_{Λ_(n+1)}(0 ↔ ∂Λ_n) ≤ φ¹_{Λ_n}(0 ↔ ∂Λ_n).

lemma wiredFiniteMeasure_succ_le_boxBdryConnEvent (n : ℕ) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1) :
    (wiredFiniteMeasure d (n + 1) hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d n)
      ≤ (wiredFiniteMeasure d n hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d n)

Uses 25 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Wired random-cluster measure on a box · Site of the hypercubic lattice

Proof usesOpen connection between two vertices · Vertex boundary of a box · Event that two sites are joined by open edges inside a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Event that two vertices are joined by open edges · Inclusion of box edges into \(\mathbb{Z}^d\) · Bernoulli edge product · Extension of a box configuration by closed edges · Origin-to-boundary connection is an increasing event · Wired box measures decrease on increasing cylinder events at \(q = 2\) · Wired random-cluster measure as a probability mass function · Wired random-cluster probability of a configuration · Wired random-cluster weight · Wired random-cluster partition function · Increasing event · Open connection of a vertex to the boundary · Origin as a vertex of the box graph · Box \((-n, n)^d\) in the hypercubic lattice · Number of open clusters with wired boundary conditions

Used byWired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\) is nonincreasing in \(n\)

LemmaOpen edges of \(\Lambda_n\) are open edges of \(\Lambda_{n+1}\)#✓fully proved

An open edge of Λ_n is an open edge of Λ_(n+1).

lemma openSub_succ_adj_inner (n : ℕ) (ω : ConfigSpace (Sym2 (Site d))) (x y : boxVerts d n) :
    (openSub (boxGraph d (n + 1)) (boxRestrict d (n + 1) ω)).Adj
        (boxVertIncl d n x) (boxVertIncl d n y)
      ↔ (openSub (boxGraph d n) (boxRestrict d n ω)).Adj x y

Uses 11 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Open subgraph of an edge configuration · Site of the hypercubic lattice

Proof usesInclusion of box edges into \(\mathbb{Z}^d\) · Inclusion of box edges into the next box · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byPaths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\)

LemmaInner vertices next to the annulus lie on \(\partial\Lambda_n\)#✓fully proved

A vertex of Λ_n adjacent to a vertex of Λ_(n+1) \ Λ_n lies on ∂Λ_n.

lemma boxBoundary_of_openSub_succ_adj_outer (n : ℕ) (hn : 1 ≤ n)
    (ω : ConfigSpace (Sym2 (Site d)))
    {x : boxVerts d n} {z : boxVerts d (n + 1)} (hz : ¬ IsInnerVert d n z)
    (h : (openSub (boxGraph d (n + 1)) (boxRestrict d (n + 1) ω)).Adj (boxVertIncl d n x) z) :
    boxBoundary d n x

Uses 12 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertex of the next box lying in the inner box · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Open subgraph of an edge configuration · Site of the hypercubic lattice

Proof usesNearest neighbours in \(\mathbb{Z}^d\) · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byPaths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\)

LemmaBox inclusion maps the origin to the origin#✓fully proved

The inclusion Λ_n → Λ_(n+1) maps the origin to the origin.

lemma boxVertIncl_boxOrigin (n : ℕ) :
    boxVertIncl d n (IsingFK.boxOrigin d n) = IsingFK.boxOrigin d (n + 1)

Uses 5 · Used by 1

Statement usesInclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Origin as a vertex of the box graph

Proof usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byPaths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\)

LemmaPaths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\)#✓fully proved

A connection from the origin to ∂Λ_(n+1) inside Λ_(n+1) passes through ∂Λ_n.

lemma connToBdry_succ_of_connToBdry (n : ℕ) (hn : 1 ≤ n) (ω : ConfigSpace (Sym2 (Site d)))
    {v : boxVerts d (n + 1)} (hv : boxBoundary d (n + 1) v)
    (h : (openSub (boxGraph d (n + 1)) (boxRestrict d (n + 1) ω)).Reachable
        (IsingFK.boxOrigin d (n + 1)) v) :
    ConnToBdry (boxGraph d n) (boxBoundary d n) (boxRestrict d n ω) (IsingFK.boxOrigin d n)

Uses 17 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Open subgraph of an edge configuration · Open connection of a vertex to the boundary · Origin as a vertex of the box graph · Site of the hypercubic lattice

Proof usesOpen connection between two vertices · Vertex of the next box lying in the inner box · Inner vertices next to the annulus lie on \(\partial\Lambda_n\) · Inclusion of box vertices into the next box · Box inclusion maps the origin to the origin · Open edges of \(\Lambda_n\) are open edges of \(\Lambda_{n+1}\) · Box \((-n, n)^d\) in the hypercubic lattice · Inner vertex boundary of a box

Used byOne-step decrease of the events \(0 \leftrightarrow \partial\Lambda_n\)

LemmaOne-step decrease of the events \(0 \leftrightarrow \partial\Lambda_n\)#✓fully proved

The events 0 ↔ ∂Λ_n decrease in n.

lemma boxBdryConnEvent_succ_subset (n : ℕ) (hn : 1 ≤ n) :
    boxBdryConnEvent d (n + 1) ⊆ boxBdryConnEvent d n

Uses 10 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Site of the hypercubic lattice

Proof usesOpen connection between two vertices · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Paths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\) · Origin as a vertex of the box graph

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Events \(0 \leftrightarrow \partial\Lambda_n\) decrease in \(n \ge 1\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\) is nonincreasing in \(n\)

LemmaWired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\) is nonincreasing in \(n\)#✓fully proved

For q = 2, φ¹_{Λ_(n+1)}(0 ↔ ∂Λ_(n+1)) ≤ φ¹_{Λ_n}(0 ↔ ∂Λ_n).

lemma wiredFiniteMeasure_boxBdryConnEvent_antitone (n : ℕ) (hn : 1 ≤ n) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1) :
    (wiredFiniteMeasure d (n + 1) hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d (n + 1))
      ≤ (wiredFiniteMeasure d n hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d n)

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Wired random-cluster measure on a box · Site of the hypercubic lattice

Proof usesOne-step decrease of the events \(0 \leftrightarrow \partial\Lambda_n\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\)

Used byWired \(q = 2\) percolation probability as the limit of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\)

D. Restriction between nested boxes

DefinitionInclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\)#✓fully proved

The inclusion Λ_n → Λ_m for n ≤ m.

def boxVertInclLE (d : ℕ) {n m : ℕ} (h : n ≤ m) (x : boxVerts d n) : boxVerts d m :=
  ⟨(x : Site d), box_mono d h x.2⟩

Uses 3 · Used by 19

Statement usesVertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byEdge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free \(q = 2\) bulk sandwich from equal free edge densities · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Free off-centre lower bound by the recentred small-box marginal · Free off-centre sandwich from free rotation residues · Free unit-edge marginals converge to the free density · Wired unit-edge marginals converge to the wired density · Wired off-centre sandwich from wired rotation residues · Wired off-centre upper bound by the recentred small-box marginal · Box symmetries preserve the free \(q = 2\) density of box edges · Box symmetries preserve the wired \(q = 2\) density of box edges · Free \(q = 2\) box edge marginals are at most the free density · Wired \(q = 2\) box edge marginals are at least the wired density · Ergodicity of the wired random-cluster measure · Constant free density gives an upper bound on expected open edges · Constant wired density gives a lower bound on expected open edges

DefinitionInclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\)#✓fully proved

The inclusion of edges of Λ_n into edges of Λ_m for n ≤ m.

def innerEdgeLE (d : ℕ) {n m : ℕ} (h : n ≤ m) : Sym2 (boxVerts d n) → Sym2 (boxVerts d m) :=
  Sym2.map (boxVertInclLE d h)

Uses 2 · Used by 61

Statement usesInclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Vertices of the box \((-n, n)^d\)

Used byLeft-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Free translation invariance from free placements of every shift · Equal free probabilities from eventually equal translated masses · Free placement for a shift via eventually equal box masses · Difference of wired all-open masses of an edge set and its translate · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Wired placement for a shift via eventually equal box masses · Off-centre carrier vanishes by translation covariance · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Monotonicity of restriction between boxes · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Wired-marginal difference between a box and its translate · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free \(q = 2\) bulk sandwich from equal free edge densities · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Bulk edges of \(\Lambda_n\) · Lower bound on free bulk edge marginals · Free off-centre lower bound by the recentred small-box marginal · Free off-centre sandwich from free rotation residues · Free unit-edge marginals converge to the free density · Wired unit-edge marginals converge to the wired density · Wired bulk edges of \(\Lambda_n\) · Upper bound on wired bulk edge marginals · Wired off-centre sandwich from wired rotation residues · Wired off-centre upper bound by the recentred small-box marginal · Free \(q = 2\) edge density lies in \((0, 1)\) · Wired \(q = 2\) edge density lies in \((0, 1)\) · Box symmetries preserve the free \(q = 2\) density of box edges · Box symmetries preserve the wired \(q = 2\) density of box edges · Translation invariance of the free \(q = 2\) infinite-volume measure · Free \(q = 2\) box edge marginals are at most the free density · Wired \(q = 2\) box edge marginals are at least the wired density · Ergodicity of the wired random-cluster measure · Translation invariance of free and wired densities if marginals merge · Constant free density gives an upper bound on expected open edges · Free upper bound on expected open edges along a box-symmetry orbit · Equal free densities from merging free marginals · Translation invariance of the free density given merging marginals · Constant wired density gives a lower bound on expected open edges · Wired lower bound on expected open edges along a box-symmetry orbit · Equal wired densities from merging wired marginals · Translation invariance of the wired density given merging marginals · Box edge set included into \(\Lambda_m\) and translated by \(v\) · Translation invariance of the wired \(q = 2\) infinite-volume measure · Realized edge sets stay realized in larger boxes · Upper decorrelation of the wired measure from factorization · All-open Dirac mass satisfies the factorization bound · Free box integral of an edge indicator is the free edge marginal · Wired box integral of an edge indicator is the wired edge marginal · Wired all-open probability on a translated box · Translated wired box mass equals the centered box mass · Translated free box mass of an edge set · Translated free box mass equals the centred box probability

LemmaEdge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\)#✓fully proved

Including an edge into Λ_m and then into ℤ^d is including it into ℤ^d.

lemma edgeIncl_innerEdgeLE (d : ℕ) {n m : ℕ} (h : n ≤ m) (e : Sym2 (boxVerts d n)) :
    edgeIncl d m (innerEdgeLE d h e) = edgeIncl d n e

Uses 6 · Used by 15

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Site of the hypercubic lattice

Proof usesInclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Box \((-n, n)^d\) in the hypercubic lattice

Used byEqual free probabilities from eventually equal translated masses · Equal wired probabilities from eventually equal translated masses · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Per-box uniqueness of the random-cluster measures off a countable set · Free \(q = 2\) bulk sandwich from equal free edge densities · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Free off-centre sandwich from free rotation residues · Wired off-centre sandwich from wired rotation residues · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure · Translation invariance of the wired \(q = 2\) infinite-volume measure · Realized edge sets stay realized in larger boxes · All-open Dirac mass satisfies the factorization bound · Translated wired box mass equals the centered box mass · Translated free box mass equals the centred box probability

DefinitionRestriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\)#✓fully proved

Restrict a configuration on Λ_m to Λ_n for n ≤ m.

noncomputable def boxRestrictLE (d : ℕ) {n m : ℕ} (h : n ≤ m)
    (η : ConfigSpace (Sym2 (boxVerts d m))) : ConfigSpace (Sym2 (boxVerts d n)) :=
  fun eb => η (innerEdgeLE d h eb)

Uses 3 · Used by 37

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\)

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Left-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · Wired \(q = 2\) edge density is monotone in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · FKG inequality for free \(q = 2\) box measures on smaller-box events · FKG inequality for wired \(q = 2\) box measures on smaller-box events · One-step growth of free \(q = 2\) measures of increasing cylinders · Secant bound gives free–wired density agreement off a countable set · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Wired \(q = 2\) increasing-event probabilities do not grow with the box · Boundary connection of \(\Lambda_n\) is a \(\Lambda_m\) cylinder event · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Monotonicity of restriction between boxes · Boundary-connection event of \(\Lambda_n\) as an event on \(\Lambda_m\) · Boundary-connection event of \(\Lambda_n\) on \(\Lambda_m\) is increasing · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Free unit-edge marginals converge to the free density · Wired unit-edge marginals converge to the wired density · Free \(q = 2\) edge density lies in \((0, 1)\) · Wired \(q = 2\) edge density lies in \((0, 1)\) · Box symmetries preserve the free \(q = 2\) density of box edges · Box symmetries preserve the wired \(q = 2\) density of box edges · Free \(q = 2\) box edge marginals are at most the free density · Wired \(q = 2\) box edge marginals are at least the wired density · Constant free density gives an upper bound on expected open edges · Equal free densities from merging free marginals · Constant wired density gives a lower bound on expected open edges · Equal wired densities from merging wired marginals · Free box integral of an edge indicator is the free edge marginal · Wired box integral of an edge indicator is the wired edge marginal

LemmaRestriction to \(\Lambda_n\) factors through \(\Lambda_m\)#✓fully proved

Restricting to Λ_m and then to Λ_n is restricting to Λ_n.

lemma boxRestrictLE_boxRestrict (d : ℕ) {n m : ℕ} (h : n ≤ m)
    (ω : ConfigSpace (Sym2 (Site d))) :
    boxRestrictLE d h (boxRestrict d m ω) = boxRestrict d n ω

Uses 8 · Used by 33

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Vertices of the box \((-n, n)^d\) · Site of the hypercubic lattice

Proof usesInclusion of box edges into \(\mathbb{Z}^d\) · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\)

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Left-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · Wired \(q = 2\) edge density is monotone in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · FKG inequality for free \(q = 2\) box measures on smaller-box events · FKG inequality for wired \(q = 2\) box measures on smaller-box events · One-step growth of free \(q = 2\) measures of increasing cylinders · Secant bound gives free–wired density agreement off a countable set · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Wired \(q = 2\) increasing-event probabilities do not grow with the box · Boundary connection of \(\Lambda_n\) is a \(\Lambda_m\) cylinder event · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Free unit-edge marginals converge to the free density · Wired unit-edge marginals converge to the wired density · Free \(q = 2\) edge density lies in \((0, 1)\) · Wired \(q = 2\) edge density lies in \((0, 1)\) · Box symmetries preserve the free \(q = 2\) density of box edges · Box symmetries preserve the wired \(q = 2\) density of box edges · Free \(q = 2\) box edge marginals are at most the free density · Wired \(q = 2\) box edge marginals are at least the wired density · Constant free density gives an upper bound on expected open edges · Equal free densities from merging free marginals · Constant wired density gives a lower bound on expected open edges · Equal wired densities from merging wired marginals · Free box integral of an edge indicator is the free edge marginal · Wired box integral of an edge indicator is the wired edge marginal

LemmaMonotonicity of restriction between boxes#✓fully proved

Restriction between boxes is monotone.

lemma boxRestrictLE_monotone (d : ℕ) {n m : ℕ} (h : n ≤ m) :
    Monotone (boxRestrictLE d h)

Uses 4 · Used by 13

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Vertices of the box \((-n, n)^d\)

Proof usesInclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\)

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Wired \(q = 2\) edge density is monotone in \(t\) · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · FKG inequality for free \(q = 2\) box measures on smaller-box events · FKG inequality for wired \(q = 2\) box measures on smaller-box events · One-step growth of free \(q = 2\) measures of increasing cylinders · Secant bound gives free–wired density agreement off a countable set · Wired \(q = 2\) increasing-event probabilities do not grow with the box · Boundary-connection event of \(\Lambda_n\) on \(\Lambda_m\) is increasing · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\)

DefinitionBoundary-connection event of \(\Lambda_n\) as an event on \(\Lambda_m\)#✓fully proved

The event 0 ↔ ∂Λ_n inside Λ_n, as an event on Λ_m for n ≤ m.

noncomputable def connToBdryEventLE (d : ℕ) {n m : ℕ} (h : n ≤ m) :
    Set (ConfigSpace (Sym2 (boxVerts d m))) :=
  boxRestrictLE d h ⁻¹' {ω : ConfigSpace (Sym2 (boxVerts d n)) |
    ConnToBdry (boxGraph d n) (boxBoundary d n) ω (IsingFK.boxOrigin d n)}

Uses 7 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Vertices of the box \((-n, n)^d\) · Open connection of a vertex to the boundary · Origin as a vertex of the box graph

Used byBoundary connection of \(\Lambda_n\) is a \(\Lambda_m\) cylinder event · Boundary-connection event of \(\Lambda_n\) on \(\Lambda_m\) is increasing · Cylinder form of the \(\Lambda_n\) boundary connection is measurable · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{m+1}\) at most in \(\Lambda_m\), \(m \ge n\)

LemmaBoundary-connection event of \(\Lambda_n\) on \(\Lambda_m\) is increasing#✓fully proved

The event connToBdryEventLE is increasing.

lemma isIncreasing_connToBdryEventLE (d : ℕ) {n m : ℕ} (h : n ≤ m) :
    IsIncreasing (connToBdryEventLE d h)

Uses 13 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Boundary-connection event of \(\Lambda_n\) as an event on \(\Lambda_m\) · Increasing event

Proof usesConfiguration space of a statistical-mechanics model · Open connection between two vertices · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Monotonicity of restriction between boxes · Open subgraph of an edge configuration · Monotonicity of the open subgraph in the configuration · Open connection of a vertex to the boundary · Origin as a vertex of the box graph

Used byWired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{m+1}\) at most in \(\Lambda_m\), \(m \ge n\)

LemmaBoundary connection of \(\Lambda_n\) is a \(\Lambda_m\) cylinder event#✓fully proved

The event 0 ↔ ∂Λ_n is a Λ_m cylinder event for every m ≥ n.

lemma boxBdryConnEvent_eq_boxRestrict_preimage (d : ℕ) {n m : ℕ} (h : n ≤ m) :
    boxBdryConnEvent d n = boxRestrict d m ⁻¹' (connToBdryEventLE d h)

Uses 12 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Boundary-connection event of \(\Lambda_n\) as an event on \(\Lambda_m\) · Site of the hypercubic lattice

Proof usesVertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Open connection of a vertex to the boundary · Origin as a vertex of the box graph

Used byCylinder form of the \(\Lambda_n\) boundary connection is measurable · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{m+1}\) at most in \(\Lambda_m\), \(m \ge n\)

LemmaCylinder form of the \(\Lambda_n\) boundary connection is measurable#✓fully proved

The cylinder form of 0 ↔ ∂Λ_n is measurable.

lemma measurableSet_boxRestrict_connToBdryEventLE (d : ℕ) {n m : ℕ} (h : n ≤ m) :
    MeasurableSet (boxRestrict d m ⁻¹' (connToBdryEventLE d h))

Uses 15 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Boundary-connection event of \(\Lambda_n\) as an event on \(\Lambda_m\) · Site of the hypercubic lattice

Proof usesOpen connection between two vertices · Event that the box origin connects to the box boundary · Boundary connection of \(\Lambda_n\) is a \(\Lambda_m\) cylinder event · Vertex boundary of a box · Event that two sites are joined by open edges inside a box · Nearest-neighbour graph on a box · Event that two vertices are joined by open edges · Inclusion of box edges into \(\mathbb{Z}^d\) · Origin as a vertex of the box graph · Box \((-n, n)^d\) in the hypercubic lattice

Used byWired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{m+1}\) at most in \(\Lambda_m\), \(m \ge n\)

LemmaWired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum#✓fully proved

The wired Λ_m measure of a Λ_m cylinder event, as a finite sum.

lemma wiredFiniteMeasure_real_boxRestrictEvent (m : ℕ) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (S : Set (ConfigSpace (Sym2 (boxVerts d m))))
    (hmeas : MeasurableSet (boxRestrict d m ⁻¹' S)) :
    (wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d m ⁻¹' S)
      = ∑ ω : ConfigSpace (Sym2 (boxVerts d m)),
          S.indicator (fun _ =>
              (1 : ℝ)) ω * wiredFkProb (boxGraph d m) (boxBoundary d m) p 2 ω

Uses 16 · Used by 26

Statement usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Wired random-cluster measure on a box · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesInclusion of box edges into \(\mathbb{Z}^d\) · Bernoulli edge product · Extension of a box configuration by closed edges · Wired random-cluster measure as a probability mass function · Wired random-cluster weight · Wired random-cluster partition function · Number of open clusters with wired boundary conditions

Used byWired \(q = 2\) origin-to-boundary probability at most Bernoulli · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Wired \(q = 2\) edge density is monotone in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · FKG inequality for wired \(q = 2\) box measures on smaller-box events · Wired box measure of an all-open event equals its box mass · Secant bound gives free–wired density agreement off a countable set · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Wired \(q = 2\) increasing-event probabilities do not grow with the box · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{m+1}\) at most in \(\Lambda_m\), \(m \ge n\) · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Wired unit-edge marginals converge to the wired density · Wired \(q = 2\) edge density lies in \((0, 1)\) · Box symmetries preserve the wired \(q = 2\) density of box edges · Wired \(q = 2\) box edge marginals are at least the wired density · Ergodicity of the wired random-cluster measure · Constant wired density gives a lower bound on expected open edges · Equal wired densities from merging wired marginals · Wired box integral of an edge indicator is the wired edge marginal

LemmaWired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{m+1}\) at most in \(\Lambda_m\), \(m \ge n\)#✓fully proved

For q = 2 and n ≤ m, φ¹_{Λ_(m+1)}(0 ↔ ∂Λ_n) ≤ φ¹_{Λ_m}(0 ↔ ∂Λ_n).

lemma wiredFiniteMeasure_succ_le_boxBdryConnEvent_le (n m : ℕ) (h : n ≤ m) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1) :
    (wiredFiniteMeasure d (m + 1) hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d n)
      ≤ (wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d n)

Uses 16 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Wired random-cluster measure on a box · Site of the hypercubic lattice

Proof usesBoundary connection of \(\Lambda_n\) is a \(\Lambda_m\) cylinder event · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Boundary-connection event of \(\Lambda_n\) as an event on \(\Lambda_m\) · Boundary-connection event of \(\Lambda_n\) on \(\Lambda_m\) is increasing · Cylinder form of the \(\Lambda_n\) boundary connection is measurable · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired box measures decrease on increasing cylinder events at \(q = 2\) · Wired random-cluster probability of a configuration · Box \((-n, n)^d\) in the hypercubic lattice

Used byWired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) in \(\Lambda_{k+j}\) is nonincreasing in \(j\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+k+1}\) at most in \(\Lambda_{n+k}\)

LemmaWired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+k+1}\) at most in \(\Lambda_{n+k}\)#✓fully proved

For q = 2, φ¹_{Λ_(n+k+1)}(0 ↔ ∂Λ_n) ≤ φ¹_{Λ_(n+k)}(0 ↔ ∂Λ_n).

lemma wiredFiniteMeasure_boxBdryConnEvent_antitone_radius (n k : ℕ) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1) :
    (wiredFiniteMeasure d (n+k+1) hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d n)
      ≤ (wiredFiniteMeasure d (n+k) hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d n)

Uses 5

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Wired random-cluster measure on a box · Site of the hypercubic lattice

Proof usesWired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{m+1}\) at most in \(\Lambda_m\), \(m \ge n\)

E. Convergence of box-boundary connection probabilities

LemmaOpen edges of a box are open edges of \(\mathbb{Z}^d\)#✓fully proved

An open edge of the box is an open edge of ℤ^d.

lemma openSubgraph_adj_of_boxGraph (n : ℕ) (ω : ConfigSpace (Sym2 (Site d)))
    {x y : boxVerts d n} (h : (openSub (boxGraph d n) (boxRestrict d n ω)).Adj x y) :
    (openSubgraph d ω).Adj (x : Site d) (y : Site d)

Uses 10 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Open subgraph of an edge configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Open subgraph of a bond configuration

Proof usesInclusion of box edges into \(\mathbb{Z}^d\) · Hypercubic lattice \(\mathbb{Z}^d\)

Used byOpen connections in a box are open connections in \(\mathbb{Z}^d\)

LemmaOpen connections in a box are open connections in \(\mathbb{Z}^d\)#✓fully proved

An open connection inside the box is an open connection in ℤ^d.

lemma connected_of_boxConnected (n : ℕ) (ω : ConfigSpace (Sym2 (Site d)))
    {x y : boxVerts d n}
    (h : (openSub (boxGraph d n) (boxRestrict d n ω)).Reachable x y) :
    StatMech.Lattice.Connected d ω (x : Site d) (y : Site d)

Uses 10 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Open subgraph of an edge configuration · Connection by an open path · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesOpen edges of a box are open edges of \(\mathbb{Z}^d\) · Open subgraph of a bond configuration

Used byBoundary connection inside \(\Lambda_n\) reaches outside \(\Lambda_{n-1}\)

LemmaBoundary connection inside \(\Lambda_n\) reaches outside \(\Lambda_{n-1}\)#✓fully proved

A connection from the origin to ∂Λ_n inside Λ_n reaches the complement of Λ_(n-1).

lemma boxBdryConnEvent_subset_crossingEvent (n : ℕ) :
    boxBdryConnEvent d n ⊆ crossingEvent d n

Uses 15 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Site of the hypercubic lattice · One-arm event from the origin

Proof usesOpen connection between two vertices · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Open connections in a box are open connections in \(\mathbb{Z}^d\) · Origin as a vertex of the box graph · Connection by an open path · Box \((-n, n)^d\) in the hypercubic lattice · Inner vertex boundary of a box · Origin of the hypercubic lattice

Used byBox-boundary connection probability tends to percolation probability · Wired infinite-volume boundary connection tends to \(\theta^1(p, q)\)

LemmaOpen lattice edges between box vertices are open box edges#✓fully proved

An open edge of ℤ^d between box vertices is an open edge of the box.

lemma boxGraph_open_of_openSubgraph (n : ℕ) (ω : ConfigSpace (Sym2 (Site d)))
    {x y : boxVerts d n} (h : (openSubgraph d ω).Adj (x : Site d) (y : Site d)) :
    (openSub (boxGraph d n) (boxRestrict d n ω)).Adj x y

Uses 10 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Open subgraph of an edge configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Open subgraph of a bond configuration

Proof usesInclusion of box edges into \(\mathbb{Z}^d\) · Hypercubic lattice \(\mathbb{Z}^d\)

Used byOpen path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\)

LemmaOpen path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\)#✓fully proved

A connection from the origin to a site outside Λ_n gives a connection to ∂Λ_n inside Λ_n.

lemma boxBdryConn_of_crossing (n : ℕ) (hn : 1 ≤ n) (ω : ConfigSpace (Sym2 (Site d)))
    {v : Site d} (hv : v ∉ box d n)
    (h : (openSubgraph d ω).Reachable (origin d) v) :
    ConnToBdry (boxGraph d n) (boxBoundary d n) (boxRestrict d n ω) (IsingFK.boxOrigin d n)

Uses 16 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Open connection of a vertex to the boundary · Origin as a vertex of the box graph · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Open subgraph of a bond configuration · Origin of the hypercubic lattice

Proof usesOpen connection between two vertices · Open lattice edges between box vertices are open box edges · Open subgraph of an edge configuration · Nearest neighbours in \(\mathbb{Z}^d\) · Hypercubic lattice \(\mathbb{Z}^d\)

Used byA connection to outside the box passes through the box boundary · Leaving \(\Lambda_n\) implies connecting to \(\partial\Lambda_n\)

LemmaLeaving \(\Lambda_n\) implies connecting to \(\partial\Lambda_n\)#✓fully proved

Reaching the complement of Λ_n implies 0 ↔ ∂Λ_n.

lemma crossingEvent_succ_subset_boxBdryConnEvent (n : ℕ) (hn : 1 ≤ n) :
    crossingEvent d (n + 1) ⊆ boxBdryConnEvent d n

Uses 14 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Site of the hypercubic lattice · One-arm event from the origin

Proof usesOpen path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\) · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Open connection of a vertex to the boundary · Origin as a vertex of the box graph · Connection by an open path · Box \((-n, n)^d\) in the hypercubic lattice · Origin of the hypercubic lattice

Used byBox-boundary connection probability tends to percolation probability · Wired infinite-volume boundary connection tends to \(\theta^1(p, q)\)

LemmaWired infinite-volume boundary connection tends to \(\theta^1(p, q)\)#✓fully proved

Under the wired infinite-volume measure, P(0 ↔ ∂Λ_n) → θ¹(p, q).

lemma wiredIv_boxBdryConnEvent_tendsto {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    Tendsto (fun n => ((wiredInfiniteVolume d hp hp1 hq :
        ProbabilityMeasure (ConfigSpace (Sym2 (Site d)))) :
        Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d n))
      atTop (𝓝 (fkTheta d hp hp1 hq (q := q)))

Uses 9 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Wired random-cluster percolation probability \(\theta(p, q)\) · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesBoundary connection inside \(\Lambda_n\) reaches outside \(\Lambda_{n-1}\) · Leaving \(\Lambda_n\) implies connecting to \(\partial\Lambda_n\) · Wired crossing probabilities converge to the percolation probability · One-arm event from the origin

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Monotonicity of \(\theta^1(p, 2)\) in \(p\) · Wired \(q = 2\) percolation probability as the limit of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\)

LemmaEvents \(0 \leftrightarrow \partial\Lambda_n\) decrease in \(n \ge 1\)#✓fully proved

The events 0 ↔ ∂Λ_n decrease in n ≥ 1.

lemma boxBdryConnEvent_subset_le (k n : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n) :
    boxBdryConnEvent d n ⊆ boxBdryConnEvent d k

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Site of the hypercubic lattice

Proof usesOne-step decrease of the events \(0 \leftrightarrow \partial\Lambda_n\)

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Wired \(q = 2\) percolation probability as the limit of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\)

LemmaWired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) in \(\Lambda_{k+j}\) is nonincreasing in \(j\)#✓fully proved

For q = 2, j ↦ φ¹_{Λ_(k+j)}(0 ↔ ∂Λ_k) is antitone.

lemma radius_antitone (k : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    Antitone (fun j => (wiredFiniteMeasure d (k+j) hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d k))

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Wired random-cluster measure on a box · Site of the hypercubic lattice

Proof usesWired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{m+1}\) at most in \(\Lambda_m\), \(m \ge n\)

Used byWired \(q = 2\) percolation probability as the limit of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\) · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\)

LemmaAntitone bounded-below sequences converge to any subsequential limit#✓fully proved

A bounded-below antitone real sequence converges to the limit of any of its subsequences.

lemma tendsto_of_antitone_of_subseq {a : ℕ → ℝ} {L : ℝ} {φ : ℕ → ℕ} (hφ : StrictMono φ)
    (hanti : Antitone a) (hbdd : BddBelow (Set.range a))
    (hsub : Tendsto (fun m => a (φ m)) atTop (𝓝 L)) :
    Tendsto a atTop (𝓝 L)

Used by 1

Used byInfinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\)

LemmaInfinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\)#✓fully proved

For q = 2, φ¹_{Λ_(k+j)}(0 ↔ ∂Λ_k) converges as j → ∞ to the wired infinite-volume probability of 0 ↔ ∂Λ_k.

lemma wiredFiniteMeasure_radius_tendsto (k : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    Tendsto (fun j => (wiredFiniteMeasure d (k+j) hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d k))
      atTop (𝓝 (((wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2) :
          ProbabilityMeasure (ConfigSpace (Sym2 (Site d)))) :
          Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d k)))

Uses 20 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Wired random-cluster measure on a box · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesOpen connection between two vertices · Vertex boundary of a box · Event that two sites are joined by open edges inside a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Event that two vertices are joined by open edges · Inclusion of box edges into \(\mathbb{Z}^d\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) in \(\Lambda_{k+j}\) is nonincreasing in \(j\) · Antitone bounded-below sequences converge to any subsequential limit · Wired infinite-volume measure is a subsequential weak limit · Origin as a vertex of the box graph · Box \((-n, n)^d\) in the hypercubic lattice · Weak convergence of probability measures on configuration space · Portmanteau theorem for clopen events

Used byWired \(q = 2\) percolation probability as the limit of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\)

LemmaWired \(q = 2\) percolation probability as the limit of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\)#✓fully proved

For q = 2, φ¹_{Λ_n}(0 ↔ ∂Λ_n) → θ¹(p, 2).

lemma boxBdryConnEvent_diag_tendsto {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    Tendsto (fun n => (wiredFiniteMeasure d n hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d n))
      atTop (𝓝 (fkTheta d hp hp1 (by norm_num : (0 : ℝ) < 2) (q := 2)))

Uses 11 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Wired random-cluster percolation probability \(\theta(p, q)\) · Wired random-cluster measure on a box · Site of the hypercubic lattice

Proof usesEvents \(0 \leftrightarrow \partial\Lambda_n\) decrease in \(n \ge 1\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) in \(\Lambda_{k+j}\) is nonincreasing in \(j\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\) is nonincreasing in \(n\) · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) · Wired infinite-volume random-cluster measure · Wired infinite-volume boundary connection tends to \(\theta^1(p, q)\)

Used byWired \(q = 2\) percolation probability at most the Bernoulli one · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Ising FK box-boundary connection profile tends to \(\theta^1(p, 2)\)

LemmaIsing FK box-boundary connection profile tends to \(\theta^1(p, 2)\)#✓fully proved

The box-boundary connection profile of the Ising FK representation converges to θ¹(p, 2).

lemma boxBoundaryConnProfile_tendsto {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    Tendsto (fun n => IsingFK.boxBoundaryConnProfile d hp hp1 (by norm_num : (0 : ℝ) < 2) n)
      atTop (𝓝 (fkTheta d hp hp1 (by norm_num : (0 : ℝ) < 2) (q := 2)))

Uses 4 · Used by 5

Statement usesWired random-cluster percolation probability \(\theta(p, q)\) · Wired probability that the origin reaches the box boundary

Proof usesWired \(q = 2\) percolation probability as the limit of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\) · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do

Used byPositive planar percolation at some \(p < 1\) via the Ising model · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.