The free q = 2 random-cluster measures increase with the box

49 fully proved

A. The wiring induced by an outer configuration

DefinitionWiring induced on a box by outer open edges#✓fully proved

The boundary wiring on Λ_n induced by an outer configuration ψ on Λ_(n+1): two distinct vertices of Λ_n are wired when ψ connects them by open edges outside Λ_n.

noncomputable def inducedWiringFree (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    SimpleGraph (boxVerts d n) where
  Adj x y := x ≠ y ∧ (outsideOpenGraph d n ψ).Reachable (boxVertIncl d n x) (boxVertIncl d n y)
  symm := by
    refine ⟨?_⟩
    rintro x y ⟨hne, hreach⟩
    exact ⟨hne.symm, hreach.symm⟩
  loopless := ⟨by rintro x ⟨hne, _⟩; exact hne rfl⟩

Uses 4 · Used by 12

Statement usesConfiguration space of a statistical-mechanics model · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Open edges of an outer configuration outside the inner box

Used byDomain Markov property · Conditional free measure as an induced-wiring measure · Conditional free measure dominates the smaller free box for \(q \ge 1\) · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Random-cluster weight of a glued configuration factorizes · Inner-graph connections are glued-graph connections · Conditional partition function in terms of the induced wiring · Adjacency criterion for the free induced wiring · Inner open graph with the free induced wiring · Glued connections between inner vertices are inner-graph connections · Outer open connections give connections in the inner graph · Cluster count of a glued configuration splits additively

LemmaAdjacency criterion for the free induced wiring#✓fully proved

Unfolding adjacency in the induced wiring.

lemma inducedWiringFree_adj (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    (x y : boxVerts d n) :
    (inducedWiringFree d n ψ).Adj x y
      ↔ x ≠ y ∧ (outsideOpenGraph d n ψ).Reachable (boxVertIncl d n x) (boxVertIncl d n y)

Uses 5

Statement usesConfiguration space of a statistical-mechanics model · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Wiring induced on a box by outer open edges · Open edges of an outer configuration outside the inner box

LemmaGlued open graph is the union of inner and outer open edges#✓fully proved

The open graph of a glued configuration is the union of the open edges of Λ_n and the outer open edges.

lemma psiFreeGraph_eq_sup (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    (ω : ConfigSpace (Sym2 (boxVerts d n))) :
    openSub (boxGraph d (n + 1)) (psiExt d n ψ ω)
      = innerImageGraph d n ω ⊔ outsideOpenGraph d n ψ

Uses 11 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inner open edges viewed in the larger box · Open subgraph of an edge configuration · Open edges of an outer configuration outside the inner box · Gluing a box configuration into an outer configuration

Proof usesInclusion of box vertices into the next box · Inclusion of box edges into the next box · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byCluster count of a glued configuration splits additively

AbbreviationOpen graph of a glued configuration#✓fully proved

The open graph on Λ_(n+1) of ω on Λ_n glued into ψ.

noncomputable abbrev fullGraphFree (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) : SimpleGraph (boxVerts d (n + 1)) :=
  innerImageGraph d n ω ⊔ outsideOpenGraph d n ψ

Uses 4 · Used by 12

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Inner open edges viewed in the larger box · Open edges of an outer configuration outside the inner box

Used byCluster decomposition of the glued configuration · Cluster map into the glued configuration · Injectivity of the free cluster map · Cluster map on inner clusters · Cluster map on avoiding outer clusters · Surjectivity of the free cluster map · Glued open edges at outer vertices are outer edges · Inner-graph connections are glued-graph connections · Glued connections between inner vertices are inner-graph connections · Cluster count of a glued configuration splits additively · Outer open graph lies in the glued open graph · Glued connections from an avoiding vertex are outer connections

AbbreviationInner open graph with the free induced wiring#✓fully proved

The open graph of ω on Λ_n together with the wiring induced by ψ.

noncomputable abbrev innerGraphFree (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) : SimpleGraph (boxVerts d n) :=
  openSub (boxGraph d n) ω ⊔ inducedWiringFree d n ψ

Uses 5 · Used by 10

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Wiring induced on a box by outer open edges · Open subgraph of an edge configuration

Used byCluster decomposition of the glued configuration · Cluster map into the glued configuration · Injectivity of the free cluster map · Cluster map on inner clusters · Cluster map on avoiding outer clusters · Surjectivity of the free cluster map · Inner-graph connections are glued-graph connections · Glued connections between inner vertices are inner-graph connections · Outer open connections give connections in the inner graph · Cluster count of a glued configuration splits additively

LemmaOuter open graph lies in the glued open graph#✓fully proved

The outer open graph is contained in the glued open graph.

lemma outsideOpenGraph_le_fullGraphFree (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    outsideOpenGraph d n ψ ≤ fullGraphFree d n ω ψ

Uses 5 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Open graph of a glued configuration · Open edges of an outer configuration outside the inner box

Proof usesInner open edges viewed in the larger box

Used byCluster map into the glued configuration · Surjectivity of the free cluster map · Inner-graph connections are glued-graph connections

LemmaOuter open connections give connections in the inner graph#✓fully proved

Vertices of Λ_n connected by outer open edges are connected in innerGraphFree.

lemma innerGraphFree_reachable_of_outsideReachable (d n : ℕ)
    (ω : ConfigSpace (Sym2 (boxVerts d n))) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    {x y : boxVerts d n}
    (h : (outsideOpenGraph d n ψ).Reachable (boxVertIncl d n x) (boxVertIncl d n y)) :
    (innerGraphFree d n ω ψ).Reachable x y

Uses 10 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Inner open graph with the free induced wiring · Open edges of an outer configuration outside the inner box

Proof usesNearest-neighbour graph on a box · Wiring induced on a box by outer open edges · Open subgraph of an edge configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byGlued connections between inner vertices are inner-graph connections

LemmaInner-graph connections are glued-graph connections#✓fully proved

Connections in innerGraphFree are connections in the glued open graph.

lemma fullGraphFree_reachable_of_innerGraphFree (d n : ℕ)
    (ω : ConfigSpace (Sym2 (boxVerts d n))) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    {x y : boxVerts d n} (h : (innerGraphFree d n ω ψ).Reachable x y) :
    (fullGraphFree d n ω ψ).Reachable (boxVertIncl d n x) (boxVertIncl d n y)

Uses 16 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Open graph of a glued configuration · Inner open graph with the free induced wiring

Proof usesNearest-neighbour graph on a box · Wiring induced on a box by outer open edges · Inclusion of box edges into the next box · Inner open edges viewed in the larger box · Open subgraph of an edge configuration · Open edges of an outer configuration outside the inner box · Outer open graph lies in the glued open graph · Gluing a box configuration into an outer configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byCluster map into the glued configuration

LemmaGlued connections between inner vertices are inner-graph connections#✓fully proved

Connections in the glued open graph between vertices of Λ_n are connections in innerGraphFree.

lemma innerGraphFree_reachable_of_fullGraphFree (d n : ℕ)
    (ω : ConfigSpace (Sym2 (boxVerts d n))) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    {x y : boxVerts d n}
    (h : (fullGraphFree d n ω ψ).Reachable (boxVertIncl d n x) (boxVertIncl d n y)) :
    (innerGraphFree d n ω ψ).Reachable x y

Uses 17 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Open graph of a glued configuration · Inner open graph with the free induced wiring

Proof usesVertex of the next box lying in the inner box · Nearest-neighbour graph on a box · Wiring induced on a box by outer open edges · Inclusion of box edges into the next box · Outer open connections give connections in the inner graph · Inner open edges viewed in the larger box · Open subgraph of an edge configuration · Open edges of an outer configuration outside the inner box · Gluing a box configuration into an outer configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byInjectivity of the free cluster map

LemmaGlued open edges at outer vertices are outer edges#✓fully proved

An edge of the glued open graph at a vertex outside Λ_n is an outer open edge.

lemma fullGraphFree_adj_of_outside (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) {u w : boxVerts d (n + 1)}
    (hu : ¬ IsInnerVert d n u) (h : (fullGraphFree d n ω ψ).Adj u w) :
    (outsideOpenGraph d n ψ).Adj u w

Uses 12 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertex of the next box lying in the inner box · Vertices of the box \((-n, n)^d\) · Open graph of a glued configuration · Open edges of an outer configuration outside the inner box

Proof usesNearest-neighbour graph on a box · Inclusion of box vertices into the next box · Inclusion of box edges into the next box · Inner open edges viewed in the larger box · Gluing a box configuration into an outer configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byGlued connections from an avoiding vertex are outer connections

B. Clusters of a glued configuration

DefinitionOuter vertex whose outer open cluster avoids the inner box#✓fully proved

A vertex of Λ_(n+1) whose outer open cluster contains no vertex of Λ_n.

def OutsideOnlyFree (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    (u : boxVerts d (n + 1)) : Prop :=
  ∀ v, (outsideOpenGraph d n ψ).Reachable u v → ¬ IsInnerVert d n v

Uses 4 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Vertex of the next box lying in the inner box · Vertices of the box \((-n, n)^d\) · Open edges of an outer configuration outside the inner box

Used byInjectivity of the free cluster map · Surjectivity of the free cluster map · Outer open cluster avoiding the inner box · An outer cluster avoids the inner box iff its representative does · Avoiding the inner box is constant on outer open clusters · A vertex whose outer cluster avoids the inner box lies outside it · Glued connections from an avoiding vertex are outer connections

LemmaA vertex whose outer cluster avoids the inner box lies outside it#✓fully proved

A vertex whose outer cluster avoids Λ_n is not in Λ_n.

lemma outsideOnlyFree_self_not_inner (d n : ℕ)
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) {u : boxVerts d (n + 1)}
    (hu : OutsideOnlyFree d n ψ u) : ¬ IsInnerVert d n u

Uses 5

Statement usesConfiguration space of a statistical-mechanics model · Vertex of the next box lying in the inner box · Outer vertex whose outer open cluster avoids the inner box · Vertices of the box \((-n, n)^d\)

Proof usesOpen edges of an outer configuration outside the inner box

LemmaAvoiding the inner box is constant on outer open clusters#✓fully proved

Avoiding Λ_n is constant on outer open clusters.

lemma outsideOnlyFree_of_reachable (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    {u v : boxVerts d (n + 1)} (hu : OutsideOnlyFree d n ψ u)
    (h : (outsideOpenGraph d n ψ).Reachable u v) : OutsideOnlyFree d n ψ v

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Outer vertex whose outer open cluster avoids the inner box · Vertices of the box \((-n, n)^d\) · Open edges of an outer configuration outside the inner box

Used byOuter open cluster avoiding the inner box

LemmaGlued connections from an avoiding vertex are outer connections#✓fully proved

From a vertex whose outer cluster avoids Λ_n, glued connections are outer connections.

lemma outsideOpenGraph_reachable_of_fullGraphFree_outsideOnly (d n : ℕ)
    (ω : ConfigSpace (Sym2 (boxVerts d n))) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    {u w : boxVerts d (n + 1)} (hu : OutsideOnlyFree d n ψ u)
    (h : (fullGraphFree d n ω ψ).Reachable u w) :
    (outsideOpenGraph d n ψ).Reachable u w

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Outer vertex whose outer open cluster avoids the inner box · Vertices of the box \((-n, n)^d\) · Open graph of a glued configuration · Open edges of an outer configuration outside the inner box

Proof usesVertex of the next box lying in the inner box · Glued open edges at outer vertices are outer edges

Used byInjectivity of the free cluster map

DefinitionOuter open cluster avoiding the inner box#✓fully proved

An outer open cluster that contains no vertex of Λ_n.

noncomputable def IsOutsideOnlyFree (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    (outsideOpenGraph d n ψ).ConnectedComponent → Prop :=
  ConnectedComponent.lift (OutsideOnlyFree d n ψ)
    (fun _ _ p _ => propext ⟨fun h => outsideOnlyFree_of_reachable d n ψ h p.reachable,
      fun h => outsideOnlyFree_of_reachable d n ψ h p.reachable.symm⟩)

Uses 5 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Outer vertex whose outer open cluster avoids the inner box · Vertices of the box \((-n, n)^d\) · Avoiding the inner box is constant on outer open clusters · Open edges of an outer configuration outside the inner box

Used byCluster map into the glued configuration · Injectivity of the free cluster map · Cluster map on avoiding outer clusters · Surjectivity of the free cluster map · An outer cluster avoids the inner box iff its representative does · Cluster count of a glued configuration splits additively · Outer open clusters avoiding the inner box

LemmaAn outer cluster avoids the inner box iff its representative does#✓fully proved

An outer cluster avoids Λ_n exactly when its representative vertex does.

@[simp] lemma isOutsideOnlyFree_mk (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    (v : boxVerts d (n + 1)) :
    IsOutsideOnlyFree d n ψ ((outsideOpenGraph d n ψ).connectedComponentMk v)
      ↔ OutsideOnlyFree d n ψ v

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Outer open cluster avoiding the inner box · Outer vertex whose outer open cluster avoids the inner box · Vertices of the box \((-n, n)^d\) · Open edges of an outer configuration outside the inner box

Used byInjectivity of the free cluster map · Surjectivity of the free cluster map

DefinitionOuter open clusters avoiding the inner box#✓fully proved

The outer open clusters that contain no vertex of Λ_n.

def OutsideOnlyCompFree (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) : Type :=
  {c : (outsideOpenGraph d n ψ).ConnectedComponent // IsOutsideOnlyFree d n ψ c}

Uses 4 · Used by 8

Statement usesConfiguration space of a statistical-mechanics model · Outer open cluster avoiding the inner box · Vertices of the box \((-n, n)^d\) · Open edges of an outer configuration outside the inner box

Used byCluster decomposition of the glued configuration · Cluster map into the glued configuration · Injectivity of the free cluster map · Cluster map on inner clusters · Cluster map on avoiding outer clusters · Surjectivity of the free cluster map · Cluster count of a glued configuration splits additively · Number of outer open clusters avoiding the inner box

DefinitionCluster map into the glued configuration#✓fully proved

The map from clusters of innerGraphFree and outer clusters avoiding Λ_n to clusters of the glued configuration.

noncomputable def fullComponentMapFree (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    (innerGraphFree d n ω ψ).ConnectedComponent ⊕ OutsideOnlyCompFree d n ψ →
      (fullGraphFree d n ω ψ).ConnectedComponent
  | Sum.inl c => c.lift (fun x => (fullGraphFree d n ω ψ).connectedComponentMk (boxVertIncl d n x))
      (fun _ _ p _ => ConnectedComponent.sound
        (fullGraphFree_reachable_of_innerGraphFree d n ω ψ p.reachable))
  | Sum.inr c => c.1.lift (fun v => (fullGraphFree d n ω ψ).connectedComponentMk v)
      (fun _ _ p _ => ConnectedComponent.sound
        (p.reachable.mono (outsideOpenGraph_le_fullGraphFree d n ω ψ)))

Uses 10 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Outer open cluster avoiding the inner box · Outer open clusters avoiding the inner box · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Open graph of a glued configuration · Inner-graph connections are glued-graph connections · Inner open graph with the free induced wiring · Open edges of an outer configuration outside the inner box · Outer open graph lies in the glued open graph

Used byCluster decomposition of the glued configuration · Injectivity of the free cluster map · Cluster map on inner clusters · Cluster map on avoiding outer clusters · Surjectivity of the free cluster map

LemmaCluster map on inner clusters#✓fully proved

The cluster map on an inner cluster.

lemma fullComponentMapFree_inl_mk (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) (x : boxVerts d n) :
    fullComponentMapFree d n ω ψ (Sum.inl ((innerGraphFree d n ω ψ).connectedComponentMk x))
      = (fullGraphFree d n ω ψ).connectedComponentMk (boxVertIncl d n x)

Uses 7 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Outer open clusters avoiding the inner box · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Cluster map into the glued configuration · Open graph of a glued configuration · Inner open graph with the free induced wiring

Used byInjectivity of the free cluster map · Surjectivity of the free cluster map

LemmaCluster map on avoiding outer clusters#✓fully proved

The cluster map on an outer cluster avoiding Λ_n.

lemma fullComponentMapFree_inr_mk (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) (v : boxVerts d (n + 1))
    (hv : IsOutsideOnlyFree d n ψ ((outsideOpenGraph d n ψ).connectedComponentMk v)) :
    fullComponentMapFree d n ω ψ
        (Sum.inr ⟨(outsideOpenGraph d n ψ).connectedComponentMk v, hv⟩)
      = (fullGraphFree d n ω ψ).connectedComponentMk v

Uses 8 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Outer open cluster avoiding the inner box · Outer open clusters avoiding the inner box · Vertices of the box \((-n, n)^d\) · Cluster map into the glued configuration · Open graph of a glued configuration · Inner open graph with the free induced wiring · Open edges of an outer configuration outside the inner box

Used byInjectivity of the free cluster map · Surjectivity of the free cluster map

LemmaInjectivity of the free cluster map#✓fully proved

The cluster map is injective.

lemma fullComponentMapFree_injective (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    Function.Injective (fullComponentMapFree d n ω ψ)

Uses 18 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Outer open clusters avoiding the inner box · Vertices of the box \((-n, n)^d\) · Cluster map into the glued configuration · Open graph of a glued configuration · Inner open graph with the free induced wiring

Proof usesVertex of the next box lying in the inner box · Outer open cluster avoiding the inner box · Outer vertex whose outer open cluster avoids the inner box · Inclusion of box vertices into the next box · Cluster map on inner clusters · Cluster map on avoiding outer clusters · Glued connections between inner vertices are inner-graph connections · An outer cluster avoids the inner box iff its representative does · Open edges of an outer configuration outside the inner box · Glued connections from an avoiding vertex are outer connections · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byCluster decomposition of the glued configuration

LemmaSurjectivity of the free cluster map#✓fully proved

The cluster map is surjective.

lemma fullComponentMapFree_surjective (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    Function.Surjective (fullComponentMapFree d n ω ψ)

Uses 18 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Outer open clusters avoiding the inner box · Vertices of the box \((-n, n)^d\) · Cluster map into the glued configuration · Open graph of a glued configuration · Inner open graph with the free induced wiring

Proof usesVertex of the next box lying in the inner box · Outer open cluster avoiding the inner box · Outer vertex whose outer open cluster avoids the inner box · Inclusion of box vertices into the next box · Cluster map on inner clusters · Cluster map on avoiding outer clusters · Inner open edges viewed in the larger box · An outer cluster avoids the inner box iff its representative does · Open edges of an outer configuration outside the inner box · Outer open graph lies in the glued open graph · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byCluster decomposition of the glued configuration

DefinitionCluster decomposition of the glued configuration#✓fully proved

Clusters of the glued configuration correspond to clusters of innerGraphFree plus outer clusters avoiding Λ_n.

noncomputable def fullComponentEquivFree (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    (innerGraphFree d n ω ψ).ConnectedComponent ⊕ OutsideOnlyCompFree d n ψ ≃
      (fullGraphFree d n ω ψ).ConnectedComponent :=
  Equiv.ofBijective (fullComponentMapFree d n ω ψ)
    ⟨fullComponentMapFree_injective d n ω ψ, fullComponentMapFree_surjective d n ω ψ⟩

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Outer open clusters avoiding the inner box · Vertices of the box \((-n, n)^d\) · Cluster map into the glued configuration · Injectivity of the free cluster map · Surjectivity of the free cluster map · Open graph of a glued configuration · Inner open graph with the free induced wiring

Used byCluster count of a glued configuration splits additively

DefinitionNumber of outer open clusters avoiding the inner box#✓fully proved

The number of outer open clusters avoiding Λ_n.

noncomputable def outsideShiftFree (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) : ℕ :=
  Nat.card (OutsideOnlyCompFree d n ψ)

Uses 3 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Outer open clusters avoiding the inner box · Vertices of the box \((-n, n)^d\)

Used byRandom-cluster weight of a glued configuration factorizes · Cluster count of a glued configuration splits additively · Outer factor of the weight of a glued configuration · Positivity of the outer weight factor

LemmaCluster count of a glued configuration splits additively#✓fully proved

The cluster count of a glued configuration is the cluster count of ω with the induced wiring plus the number of outer clusters avoiding Λ_n.

lemma numClusters_psiExt_free (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    numClusters (boxGraph d (n + 1)) (psiExt d n ψ ω)
      = numClustersBC (boxGraph d n) (inducedWiringFree d n ψ) ω + outsideShiftFree d n ψ

Uses 19 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Wiring induced on a box by outer open edges · Number of open clusters · Number of clusters under a boundary wiring · Number of outer open clusters avoiding the inner box · Gluing a box configuration into an outer configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesOuter open cluster avoiding the inner box · Outer open clusters avoiding the inner box · Cluster decomposition of the glued configuration · Open graph of a glued configuration · Inner open graph with the free induced wiring · Inner open edges viewed in the larger box · Open subgraph of an edge configuration · Open edges of an outer configuration outside the inner box · Glued open graph is the union of inner and outer open edges

Used byRandom-cluster weight of a glued configuration factorizes

C. Domain Markov property for the free measure

DefinitionOuter factor of the weight of a glued configuration#✓fully proved

The factor of the random-cluster weight of a glued configuration contributed by the outer configuration.

noncomputable def psiShiftFree (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    (p q : ℝ) : ℝ :=
  psiEdgeFactor d n ψ p * q ^ outsideShiftFree d n ψ

Uses 4 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Number of outer open clusters avoiding the inner box · Outer Bernoulli edge factor of an outer configuration

Used byDomain Markov property · Random-cluster weight of a glued configuration factorizes · Conditional partition function in terms of the induced wiring · Positivity of the outer weight factor

LemmaPositivity of the outer weight factor#✓fully proved

The outer weight factor is positive.

lemma psiShiftFree_pos {d n : ℕ} {ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))} {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) : 0 < psiShiftFree d n ψ p q

Uses 9 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Outer factor of the weight of a glued configuration

Proof usesNearest-neighbour graph on a box · Inclusion of box edges into the next box · Number of outer open clusters avoiding the inner box · Outer Bernoulli edge factor of an outer configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byDomain Markov property

LemmaRandom-cluster weight of a glued configuration factorizes#✓fully proved

The random-cluster weight of a glued configuration factors as the outer factor times the weight of ω with the induced wiring.

lemma fkWeight_psiExt_free (d n : ℕ) {p q : ℝ} (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    (ω : ConfigSpace (Sym2 (boxVerts d n))) :
    fkWeight (boxGraph d (n + 1)) p q (psiExt d n ψ ω)
      = bcWeight (boxGraph d n) (inducedWiringFree d n ψ) p q ω * psiShiftFree d n ψ p q

Uses 17 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster weight with a boundary wiring · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Unnormalized random-cluster weight · Wiring induced on a box by outer open edges · Gluing a box configuration into an outer configuration · Outer factor of the weight of a glued configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesBernoulli edge product · Edge product of a glued configuration factorizes · Number of open clusters · Number of clusters under a boundary wiring · Cluster count of a glued configuration splits additively · Number of outer open clusters avoiding the inner box · Outer Bernoulli edge factor of an outer configuration

Used byDomain Markov property · Conditional partition function in terms of the induced wiring

LemmaConditional partition function in terms of the induced wiring#✓fully proved

The conditional partition function given the outer configuration, in terms of the induced-wiring partition function.

lemma inducedFkZ_innerEdgeFinset_psi_free (d n : ℕ) {p q : ℝ}
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    inducedFkZ (boxGraph d (n + 1)) p q (innerEdgeFinset d n) ψ
      = bcZ (boxGraph d n) (inducedWiringFree d n ψ) p q * psiShiftFree d n ψ p q

Uses 19 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Partition function with a boundary wiring · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Total FK weight of a fibre · Wiring induced on a box by outer open edges · Edges of the next box coming from the inner box · Outer factor of the weight of a glued configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesAgreement of configurations off an edge set · Random-cluster weight with a boundary wiring · Inclusion of box vertices into the next box · Fibre of configurations agreeing off an edge set · Unnormalized random-cluster weight · Random-cluster weight of a glued configuration factorizes · Inclusion of box edges into the next box · Restriction of a next-box configuration to the inner edges · Gluing a box configuration into an outer configuration

Used byDomain Markov property

LemmaDomain Markov property#✓fully proved

Conditionally on the configuration ψ outside Λ_n, the free random-cluster measure on Λ_(n+1) restricted to Λ_n is the random-cluster measure on Λ_n with the wiring induced by ψ.

lemma condFkProb_psiExt_eq_bcProb_free (d n : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) (ω : ConfigSpace (Sym2 (boxVerts d n))) :
    condFkProb (boxGraph d (n + 1)) p q (innerEdgeFinset d n) ψ (psiExt d n ψ ω)
      = bcProb (boxGraph d n) (inducedWiringFree d n ψ) p q ω

Uses 20 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Random-cluster measure conditioned on the edges off a set · Wiring induced on a box by outer open edges · Edges of the next box coming from the inner box · Gluing a box configuration into an outer configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesRandom-cluster weight with a boundary wiring · Partition function with a boundary wiring · Domain Markov property (finite volume) · Unnormalized random-cluster weight · Random-cluster weight of a glued configuration factorizes · FK measure induced on a fibre · Total FK weight of a fibre · Conditional partition function in terms of the induced wiring · Outer factor of the weight of a glued configuration · Positivity of the outer weight factor

Used byConditional free measure as an induced-wiring measure

LemmaFibre masses of the free measure sum to one#✓fully proved

The masses of the conditioning fibres of the free measure on Λ_(n+1) sum to 1.

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

Uses 15 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Fibre of configurations agreeing off an edge set · Probability of an ambient FK configuration · 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 usesBernoulli edge product · Configurations with a given outer part form its conditioning fibre · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · Outer projection is idempotent

Used byOne-step box monotonicity of free measures for \(q \ge 1\)

LemmaFibre-mass factorization of random-cluster probabilities#✓fully proved

A random-cluster probability is its fibre mass times its conditional probability.

lemma fkProb_eq_fibreMass_mul_condFkProb (n : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (ω : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    fkProb (boxGraph d (n + 1)) p q ω
      = (∑ ρ ∈ condFibre (innerEdgeFinset d n) ω, fkProb (boxGraph d (n + 1)) p q ρ)
          * condFkProb (boxGraph d (n + 1)) p q (innerEdgeFinset d n) ω ω

Uses 14 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Fibre of configurations agreeing off an edge set · Random-cluster measure conditioned on the edges off a set · Probability of an ambient FK configuration · Edges of the next box coming from the inner box · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesAgreement of configurations off an edge set · Bernoulli edge product · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters

Used byDecomposition of the free measure over the outer configuration

LemmaConditional free probabilities depend only on the outer configuration#✓fully proved

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

lemma condFkProb_congr_dom_free (n : ℕ) {p q : ℝ}
    (ψ ψ' ω : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    (h : AgreesOff (innerEdgeFinset d n) ψ ψ') :
    condFkProb (boxGraph d (n + 1)) p q (innerEdgeFinset d n) ψ ω
      = condFkProb (boxGraph d (n + 1)) p q (innerEdgeFinset d n) ψ' ω

Uses 10 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Agreement of configurations off an edge set · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Random-cluster measure conditioned on the edges off a set · Edges of the next box coming from the inner box · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesFibre of configurations agreeing off an edge set · Probability of an ambient FK configuration

Used byDecomposition of the free measure over the outer configuration

D. The free measures increase with the box

LemmaDecomposition of the free measure over the outer configuration#✓fully proved

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

lemma freeSucc_fkProb_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 : ℝ)) ρ * fkProb (boxGraph d (n + 1)) p q ρ)
      = ∑ ψ ∈ Finset.univ.filter (fun ψ => outProj d n ψ = ψ),
          (∑ σ ∈ condFibre (innerEdgeFinset d n) ψ,
            fkProb (boxGraph d (n + 1)) p q σ)
          * (∑ ρ ∈ condFibre (innerEdgeFinset d n) ψ, B.indicator (fun _ => (1 : ℝ)) ρ
              * condFkProb (boxGraph d (n + 1)) p q (innerEdgeFinset d n) ψ ρ)

Uses 15 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Fibre of configurations agreeing off an edge set · Random-cluster measure conditioned on the edges off a set · Probability of an ambient FK configuration · 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 · Conditional free probabilities depend only on the outer configuration · Configurations with a given outer part form its conditioning fibre · Fibre-mass factorization of random-cluster probabilities · Outer projection is idempotent

Used byOne-step box monotonicity of free measures for \(q \ge 1\)

LemmaConditional free measure as an induced-wiring measure#✓fully proved

The conditional free measure of an event of Λ_n equals its probability under the induced-wiring measure.

lemma condFkProb_psiExt_sum_eq_inducedBox_free (d n : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    (B : Set (ConfigSpace (Sym2 (boxVerts d (n + 1))))) :
    (∑ ρ ∈ condFibre (innerEdgeFinset d n) ψ, B.indicator (fun _ => (1 : ℝ)) ρ *
        condFkProb (boxGraph d (n + 1)) p q (innerEdgeFinset d n) ψ ρ)
      = ∑ ω : ConfigSpace (Sym2 (boxVerts d n)),
          (psiExt d n ψ ⁻¹' B).indicator (fun _ => (1 : ℝ)) ω
            * bcProb (boxGraph d n) (inducedWiringFree d n ψ) p q ω

Uses 16 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Fibre of configurations agreeing off an edge set · Random-cluster measure conditioned on the edges off a set · Wiring induced on a box by outer open edges · Edges of the next box coming from the inner box · Gluing a box configuration into an outer configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesAgreement of configurations off an edge set · Inclusion of box vertices into the next box · Domain Markov property · Inclusion of box edges into the next box · Restriction of a next-box configuration to the inner edges

Used byConditional free measure dominates the smaller free box for \(q \ge 1\)

LemmaFree measure is dominated by induced-wiring measures for \(q \ge 1\)#✓fully proved

For q ≥ 1, the free measure on Λ_n gives an increasing event at most its probability under any induced wiring.

lemma fkProb_le_inducedFree (d 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₀) :
    (∑ ω, A₀.indicator (fun _ => (1 : ℝ)) ω * fkProb (boxGraph d n) p q ω)
      ≤ ∑ ω, A₀.indicator (fun _ => (1 : ℝ)) ω
          * bcProb (boxGraph d n) (inducedWiringFree d n ψ) p q ω

Uses 18 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Probability of an ambient FK configuration · Wiring induced on a box by outer open edges · Increasing event · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesRandom-cluster comparison of boundary conditions for \(q \ge 1\) · Random-cluster weight with a boundary wiring · Partition function with a boundary wiring · Bernoulli edge product · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · Number of clusters under a boundary wiring · Open subgraph of an edge configuration

Used byConditional free measure dominates the smaller free box for \(q \ge 1\)

LemmaConditional free measure dominates the smaller free box for \(q \ge 1\)#✓fully proved

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

lemma fkProb_le_condFkProb_innerRestrict_free (d 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₀) :
    (∑ ω, A₀.indicator (fun _ => (1 : ℝ)) ω * fkProb (boxGraph d n) p q ω)
      ≤ ∑ ρ ∈ condFibre (innerEdgeFinset d n) ψ,
          (innerRestrict d n ⁻¹' A₀).indicator (fun _ => (1 : ℝ)) ρ
            * condFkProb (boxGraph d (n + 1)) p q (innerEdgeFinset d n) ψ ρ

Uses 18 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Fibre of configurations agreeing off an edge set · Random-cluster measure conditioned on the edges off a set · Probability of an ambient FK configuration · Edges of the next box coming from the inner box · Restriction of a next-box configuration to the inner edges · Increasing event · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesRandom-cluster probability with a boundary wiring · Inclusion of box vertices into the next box · Conditional free measure as an induced-wiring measure · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Wiring induced on a box by outer open edges · Inclusion of box edges into the next box · Gluing a box configuration into an outer configuration

Used byOne-step box monotonicity of free measures for \(q \ge 1\)

LemmaOne-step box monotonicity of free measures for \(q \ge 1\)#✓fully proved

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

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

Uses 19 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Probability of an ambient FK configuration · Restriction of a next-box configuration to the inner edges · Increasing event · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesFibre of configurations agreeing off an edge set · Random-cluster measure conditioned on the edges off a set · Bernoulli edge product · Conditional free measure dominates the smaller free box for \(q \ge 1\) · Unnormalized random-cluster weight · Ambient FK normalizer · Decomposition of the free measure over the outer configuration · Edges of the next box coming from the inner box · Number of open clusters · Outer part of a configuration on \(\Lambda_{n+1}\) · Fibre masses of the free measure sum to one

Used byIncreasing box events gain free \(q = 2\) probability in the next box · Per-box uniqueness of the random-cluster measures off a countable set

LemmaFree box measure of a cylinder event as a finite sum#✓fully proved

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

lemma freeFiniteMeasure_real_boxRestrictEvent (m : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) (S : Set (ConfigSpace (Sym2 (boxVerts d m))))
    (hmeas : MeasurableSet (boxRestrict d m ⁻¹' S)) :
    (freeFiniteMeasure d m hp hp1 hq
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d m ⁻¹' S)
      = ∑ ω : ConfigSpace (Sym2 (boxVerts d m)),
          S.indicator (fun _ => (1 : ℝ)) ω * fkProb (boxGraph d m) p q ω

Uses 15 · Used by 14

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\) · Probability of an ambient FK configuration · Free random-cluster measure on a box · 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 · Ambient random-cluster law as a probability mass function · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters

Used byLeft-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · FKG inequality for free \(q = 2\) box measures on smaller-box events · Free box measure of an all-open event equals its box mass · One-step growth of free \(q = 2\) measures of increasing cylinders · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free unit-edge marginals converge to the free density · Free \(q = 2\) edge density lies in \((0, 1)\) · Box symmetries preserve the free \(q = 2\) density of box edges · Free \(q = 2\) box edge marginals are at most the free density · Constant free density gives an upper bound on expected open edges · Equal free densities from merging free marginals · Free box integral of an edge indicator is the free edge marginal

LemmaNext-box free measure of a cylinder event as a finite sum#✓fully proved

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

lemma freeFiniteMeasure_succ_real_innerRestrictEvent (n : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (S : Set (ConfigSpace (Sym2 (boxVerts d n))))
    (hmeas : MeasurableSet (boxRestrict d n ⁻¹' S)) :
    (freeFiniteMeasure d (n + 1) hp hp1 hq
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d n ⁻¹' S)
      = ∑ ρ : ConfigSpace (Sym2 (boxVerts d (n + 1))),
          (innerRestrict d n ⁻¹' S).indicator (fun _ => (1 : ℝ)) ρ
            * fkProb (boxGraph d (n + 1)) p q ρ

Uses 18 · Used by 2

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\) · Probability of an ambient FK configuration · Free random-cluster measure on a box · Restriction of a next-box configuration to the inner edges · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesInclusion 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 · Ambient random-cluster law as a probability mass function · Unnormalized random-cluster weight · Ambient FK normalizer · Inclusion of box edges into the next box · Number of open clusters

Used byIncreasing box events gain free \(q = 2\) probability in the next box · Per-box uniqueness of the random-cluster measures off a countable set

LemmaIncreasing box events gain free \(q = 2\) probability in the next box#✓fully proved

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

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

Uses 12 · 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\) · Probability of an ambient FK configuration · Free random-cluster measure on a box · Increasing event · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesNext-box free measure of a cylinder event as a finite sum · One-step box monotonicity of free measures for \(q \ge 1\) · Restriction of a next-box configuration to the inner edges

Used byOne-step growth of free \(q = 2\) measures of increasing cylinders

E. The free infinite-volume limit on increasing cylinder events

LemmaOne-step growth of free \(q = 2\) measures of increasing cylinders#✓fully proved

For q = 2 and N ≤ m, the free Λ_m measure of an increasing Λ_N cylinder event is at most its free Λ_(m+1) measure.

lemma fkFreeLimit_le_succ (N m : ℕ) (hNm : N ≤ m) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1)
    {S : Set (ConfigSpace (Sym2 (boxVerts d N)))} (hS : IsIncreasing S) :
    (freeFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)
      ≤ (freeFiniteMeasure d (m + 1) hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)

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\) · Free random-cluster measure on a box · Increasing event · Site of the hypercubic lattice

Proof usesNearest-neighbour graph on a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Monotonicity of restriction between boxes · Inclusion of box edges into \(\mathbb{Z}^d\) · Probability of an ambient FK configuration · Free box measure of a cylinder event as a finite sum · Increasing box events gain free \(q = 2\) probability in the next box · Box \((-n, n)^d\) in the hypercubic lattice

Used byFree \(q = 2\) box measures of increasing cylinders are monotone

LemmaFree \(q = 2\) box measures of increasing cylinders are monotone#✓fully proved

For q = 2, the free box measures of an increasing Λ_N cylinder event increase with the box.

lemma fkFreeLimit_monotone (N : ℕ) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1)
    {S : Set (ConfigSpace (Sym2 (boxVerts d N)))} (hS : IsIncreasing S) :
    Monotone (fun k => (freeFiniteMeasure d (N+k) hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S))

Uses 7 · 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\) · Free random-cluster measure on a box · Increasing event · Site of the hypercubic lattice

Proof usesOne-step growth of free \(q = 2\) measures of increasing cylinders

Used byFree \(q = 2\) box measures of increasing cylinders converge

DefinitionLimit of free \(q = 2\) box measures of a cylinder event#✓fully proved

The limit sup_k φ⁰_{Λ_(N+k)}(S) of the free q = 2 box measures of a Λ_N cylinder event S.

noncomputable def fkFreeLimitValue (N : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (S : Set (ConfigSpace (Sym2 (boxVerts d N)))) : ℝ :=
  ⨆ k, (freeFiniteMeasure d (N+k) hp hp1 (by norm_num : (0 : ℝ) < 2)
      : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)

Uses 5 · Used by 7

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\) · Free random-cluster measure on a box · Site of the hypercubic lattice

Used byLeft-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Free \(q = 2\) box measures are bounded by the limit value · Free \(q = 2\) box measures of increasing cylinders converge · Free \(q = 2\) infinite-volume mass of increasing cylinders as a box limit · Free \(q = 2\) box edge marginals are at most the free density · Constant free density gives an upper bound on expected open edges

LemmaFree box measures are at most one#✓fully proved

Free box measures are at most 1.

lemma freeFiniteMeasure_real_le_one (m : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (A : Set (ConfigSpace (Sym2 (Site d)))) :
    (freeFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real A ≤ 1

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Free random-cluster measure on a box · Site of the hypercubic lattice

Used byFree \(q = 2\) box measures are bounded by the limit value · Free \(q = 2\) box measures of increasing cylinders converge

LemmaFree \(q = 2\) box measures of increasing cylinders converge#✓fully proved

For q = 2, the free box measures of an increasing Λ_N cylinder event converge to fkFreeLimitValue.

lemma fk_free_limit_exists (N : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    {S : Set (ConfigSpace (Sym2 (boxVerts d N)))} (hS : IsIncreasing S) :
    Tendsto (fun m => (freeFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)) atTop
      (𝓝 (fkFreeLimitValue N hp hp1 S))

Uses 9 · Used by 2

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\) · Limit of free \(q = 2\) box measures of a cylinder event · Free random-cluster measure on a box · Increasing event · Site of the hypercubic lattice

Proof usesFree \(q = 2\) box measures of increasing cylinders are monotone · Free box measures are at most one

Used byFree \(q=2\) box masses of increasing cylinders tend to infinite volume · Free \(q = 2\) infinite-volume mass of increasing cylinders as a box limit

LemmaFree \(q = 2\) box measures are bounded by the limit value#✓fully proved

For q = 2, every free box measure of a Λ_N cylinder event with N ≤ m is at most fkFreeLimitValue.

lemma fk_free_le_limit (N m : ℕ) (hNm : N ≤ m) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (S : Set (ConfigSpace (Sym2 (boxVerts d N)))) :
    (freeFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)
      ≤ fkFreeLimitValue N hp hp1 S

Uses 7 · Used by 3

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\) · Limit of free \(q = 2\) box measures of a cylinder event · Free random-cluster measure on a box · Site of the hypercubic lattice

Proof usesFree box measures are at most one

Used byLeft-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) box edge marginals are at most the free density · Constant free density gives an upper bound on expected open edges

LemmaFree \(q = 2\) infinite-volume mass of increasing cylinders as a box limit#✓fully proved

For q = 2, the free infinite-volume measure of an increasing cylinder event equals fkFreeLimitValue.

lemma fkFreeLimit_freeInfiniteVolume_eq (N : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    {S : Set (ConfigSpace (Sym2 (boxVerts d N)))} (hS : IsIncreasing S) :
    (freeInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)
      = fkFreeLimitValue N hp hp1 S

Uses 13 · Used by 4

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\) · Limit of free \(q = 2\) box measures of a cylinder event · Free infinite-volume random-cluster measure · Increasing event · Site of the hypercubic lattice

Proof usesFree \(q = 2\) box measures of increasing cylinders converge · Free random-cluster measure on a box · Free infinite-volume measure is a subsequential weak limit · Cylinder events of a box are clopen · Weak convergence of probability measures on configuration space · Portmanteau theorem for clopen events

Used byLeft-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Free \(q = 2\) box edge marginals are at most the free density · Constant free density gives an upper bound on expected open edges

LemmaFree \(q=2\) box masses of increasing cylinders tend to infinite volume#✓fully proved

For q = 2, the free box measures of an increasing cylinder event converge, along the whole sequence of boxes, to its free infinite-volume measure.

lemma fk_free_infinite_measure (N : ℕ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    {S : Set (ConfigSpace (Sym2 (boxVerts d N)))} (hS : IsIncreasing S) :
    Tendsto (fun m => (freeFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)) atTop
      (𝓝 ((freeInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)))

Uses 10 · Used by 19

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\) · Free random-cluster measure on a box · Free infinite-volume random-cluster measure · Increasing event · Site of the hypercubic lattice

Proof usesLimit of free \(q = 2\) box measures of a cylinder event · Free \(q = 2\) infinite-volume mass of increasing cylinders as a box limit · Free \(q = 2\) box measures of increasing cylinders converge

Used byLeft-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · FKG inequality for the free \(q = 2\) infinite-volume measure · Wired \(q = 2\) measure dominates the free one on increasing cylinders · Convergence and ordering of free and wired limits at \(q = 2\) · Convergence and ordering at \(q = 2\) in subsequence form · Free all-open probabilities converge to the infinite-volume value · Free translation invariance from free placements of every shift · Secant bound gives free–wired density agreement off a countable set · Free density is at most each translated wired marginal · Per-box \(q = 2\) uniqueness off a countable set of tilts · 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\) · Free unit-edge marginals converge to the free density · Free \(q = 2\) edge density lies in \((0, 1)\) · Box symmetries preserve the free \(q = 2\) density of box edges · Equal free densities from merging free marginals · Free translation invariance from the placement hypothesis

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.