Boundary conditions induced on a box by the outer annulus

22 fully proved

A. Gluing inner and outer configurations

DefinitionGluing a box configuration into an outer configuration#✓fully proved

Glue a configuration ω on Λ_n into an outer configuration ψ on Λ_(n+1): edges of Λ_n follow ω, the others follow ψ.

noncomputable def psiExt (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    (ω : ConfigSpace (Sym2 (boxVerts d n))) : ConfigSpace (Sym2 (boxVerts d (n + 1))) :=
  fun e => if h : e ∈ Set.range (innerEdge d n) then ω h.choose else ψ e

Uses 5 · Used by 22

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into the next box · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byDomain Markov property for the wired measure on nested boxes · Edge product of a glued configuration factorizes · Component decomposition of the wired glued graph · Component map into the wired glued graph · Glued and inner graphs have the same connections on the box · Inner open edges viewed in the larger box · Wired cluster count of a glued configuration splits additively · Wired glued open graph is the union of inner and outer graphs · Domain Markov property · Conditional free measure as an induced-wiring measure · Conditional free measure dominates the smaller free box for \(q \ge 1\) · Random-cluster weight of a glued configuration factorizes · Glued open edges at outer vertices are outer edges · Inner-graph connections are glued-graph connections · Conditional partition function in terms of the induced wiring · Glued connections between inner vertices are inner-graph connections · Cluster count of a glued configuration splits additively · Glued open graph is the union of inner and outer open edges · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Outer part of a configuration on \(\Lambda_{n+1}\) · Outer projection closes the edges of \(\Lambda_n\) · Outer projection keeps the edges outside \(\Lambda_n\)

B. The outer graph and the induced wiring

DefinitionOpen edges of an outer configuration outside the inner box#✓fully proved

The open edges of ψ on Λ_(n+1) that are not edges of Λ_n.

noncomputable def outsideOpenGraph (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    SimpleGraph (boxVerts d (n + 1)) where
  Adj x y := (boxGraph d (n + 1)).Adj x y ∧ ψ s(x, y) = true ∧ s(x, y) ∉ Set.range (innerEdge d n)
  symm := by
    refine ⟨?_⟩
    rintro x y ⟨hadj, hopen, hrange⟩
    refine ⟨hadj.symm, ?_, ?_⟩ <;> rw [Sym2.eq_swap] <;> assumption
  loopless := ⟨by rintro x ⟨hadj, _, _⟩; exact hadj.ne rfl⟩

Uses 4 · Used by 24

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into the next box

Used byInduced wiring lies below the inner boundary clique · Outer open graph plus the outer boundary clique · Wired glued open graph is the union of inner and outer graphs · Cluster map into the glued configuration · Injectivity of the free cluster map · Cluster map on avoiding outer clusters · Surjectivity of the free cluster map · Open graph of a glued configuration · Glued open edges at outer vertices are outer edges · Inner-graph connections are glued-graph connections · Wiring induced on a box by outer open edges · Adjacency criterion for the free induced wiring · Glued connections between inner vertices are inner-graph connections · Outer open connections give connections in the inner graph · Outer open cluster avoiding the inner box · 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 · Outer vertex whose outer open cluster avoids the inner box · Avoiding the inner box is constant on outer open clusters · A vertex whose outer cluster avoids the inner box lies outside it · Outer open graph lies in the glued open graph · Glued connections from an avoiding vertex are outer connections · Glued open graph is the union of inner and outer open edges

DefinitionOuter open graph plus the outer boundary clique#✓fully proved

The outer graph: open outer edges of ψ together with the clique on ∂Λ_(n+1).

noncomputable def outsideGraph (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    SimpleGraph (boxVerts d (n + 1)) :=
  outsideOpenGraph d n ψ ⊔ StatMech.Lattice.boundaryCliqueGraph (boxBoundary d (n + 1))

Uses 5 · Used by 11

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

Used byComponent decomposition of the wired glued graph · Component map into the wired glued graph · Wired open graph of a glued configuration · Glued and inner graphs have the same connections on the box · Wiring induced on a box through the outer graph · Induced wiring lies below the inner boundary clique · Outer component avoiding the inner box · Wired cluster count of a glued configuration splits additively · Outer vertex whose outer component avoids the inner box · Outer components avoiding the inner box · Wired glued open graph is the union of inner and outer graphs

DefinitionWiring induced on a box through the outer graph#✓fully proved

The wiring induced on Λ_n by ψ: distinct vertices of Λ_n connected in the outer graph.

noncomputable def inducedWiring (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    SimpleGraph (boxVerts d n) where
  Adj x y := x ≠ y ∧ (outsideGraph 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 9

Statement usesConfiguration space of a statistical-mechanics model · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Outer open graph plus the outer boundary clique

Used byWired box measure dominates the induced-wiring measure for \(q \ge 1\) · Domain Markov property for the wired measure on nested boxes · Component decomposition of the wired glued graph · Component map into the wired glued graph · Glued and inner graphs have the same connections on the box · Induced wiring lies below the inner boundary clique · Inner open graph with the induced wiring · Wired cluster count of a glued configuration splits additively · Conditional wired decrease on inner increasing events for \(q \ge 1\)

C. Decomposition of the glued graph

DefinitionInner open edges viewed in the larger box#✓fully proved

The open edges of ω, viewed as edges of Λ_(n+1).

noncomputable def innerImageGraph (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n))) :
    SimpleGraph (boxVerts d (n + 1)) where
  Adj x y := (boxGraph d (n + 1)).Adj x y ∧ psiExt d n (fun _ => false) ω s(x, y) = true
    ∧ s(x, y) ∈ Set.range (innerEdge d n)
  symm := by
    refine ⟨?_⟩
    rintro x y ⟨hadj, hopen, hrange⟩
    refine ⟨hadj.symm, ?_, ?_⟩ <;> rw [Sym2.eq_swap] <;> assumption
  loopless := ⟨by rintro x ⟨hadj, _, _⟩; exact hadj.ne rfl⟩

Uses 5 · Used by 14

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into the next box · Gluing a box configuration into an outer configuration

Used byComponent decomposition of the wired glued graph · Component map into the wired glued graph · Wired open graph of a glued configuration · Glued and inner graphs have the same connections on the box · Wired cluster count of a glued configuration splits additively · Wired glued open graph is the union of inner and outer graphs · Surjectivity of the free cluster map · Open graph of a glued configuration · 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 open graph is the union of inner and outer open edges

LemmaWired glued open graph is the union of inner and outer graphs#✓fully proved

The wired open graph of the glued configuration is the union of the inner open edges and the outer graph.

lemma psiWiredGraph_eq_sup (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    (ω : ConfigSpace (Sym2 (boxVerts d n))) :
    openSub (boxGraph d (n + 1)) (psiExt d n ψ ω)
        ⊔ StatMech.Lattice.boundaryCliqueGraph (boxBoundary d (n + 1))
      = innerImageGraph d n ω ⊔ outsideGraph d n ψ

Uses 14 · 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\) · Inner open edges viewed in the larger box · Open subgraph of an edge configuration · Outer open graph plus the outer boundary clique · Gluing a box configuration into an outer configuration · Complete graph on the boundary vertices

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

Used byWired cluster count of a glued configuration splits additively

AbbreviationWired open graph of a glued configuration#✓fully proved

The wired open graph of the glued configuration on Λ_(n+1).

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

Uses 4 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Inner open edges viewed in the larger box · Outer open graph plus the outer boundary clique

Used byComponent decomposition of the wired glued graph · Component map into the wired glued graph · Glued and inner graphs have the same connections on the box · Wired cluster count of a glued configuration splits additively

AbbreviationInner open graph with the induced wiring#✓fully proved

The open graph of ω on Λ_n with the induced wiring added.

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

Uses 5 · Used by 4

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 through the outer graph · Open subgraph of an edge configuration

Used byComponent decomposition of the wired glued graph · Component map into the wired glued graph · Glued and inner graphs have the same connections on the box · Wired cluster count of a glued configuration splits additively

LemmaGlued and inner graphs have the same connections on the box#✓fully proved

Two vertices of Λ_n are connected in the glued graph iff they are connected in innerGraph.

lemma fullGraph_reachable_boxVertIncl (d n : ℕ)
    (ω : ConfigSpace (Sym2 (boxVerts d n))) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    (x y : boxVerts d n) :
    (fullGraph d n ω ψ).Reachable (boxVertIncl d n x) (boxVertIncl d n y)
      ↔ (innerGraph d n ω ψ).Reachable x y

Uses 16

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

Proof usesVertex of the next box lying in the inner box · Nearest-neighbour graph on a box · Wiring induced on a box through the outer graph · Inclusion of box edges into the next box · Inner open edges viewed in the larger box · Open subgraph of an edge configuration · Outer open graph plus the outer boundary clique · 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\)

D. Counting clusters

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

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

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

Uses 4 · Used by 2

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\) · Outer open graph plus the outer boundary clique

Used byComponent decomposition of the wired glued graph · Outer component avoiding the inner box

DefinitionOuter component avoiding the inner box#✓fully proved

OutsideOnly as a predicate on components of the outer graph.

noncomputable def IsOutsideOnly (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    (outsideGraph d n ψ).ConnectedComponent → Prop :=
  ConnectedComponent.lift (OutsideOnly d n ψ)
    (fun _ _ p _ => propext ⟨fun h => outsideOnly_of_reachable d n ψ h p.reachable,
      fun h => outsideOnly_of_reachable d n ψ h p.reachable.symm⟩)

Uses 4 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Outer vertex whose outer component avoids the inner box · Vertices of the box \((-n, n)^d\) · Outer open graph plus the outer boundary clique

Used byComponent decomposition of the wired glued graph · Component map into the wired glued graph · Wired cluster count of a glued configuration splits additively · Outer components avoiding the inner box

DefinitionOuter components avoiding the inner box#✓fully proved

The components of the outer graph that avoid Λ_n.

def OutsideOnlyComp (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) : Type :=
  {c : (outsideGraph d n ψ).ConnectedComponent // IsOutsideOnly d n ψ c}

Uses 4 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Outer component avoiding the inner box · Vertices of the box \((-n, n)^d\) · Outer open graph plus the outer boundary clique

Used byComponent decomposition of the wired glued graph · Component map into the wired glued graph · Wired cluster count of a glued configuration splits additively · Number of outer components avoiding the inner box

DefinitionComponent map into the wired glued graph#✓fully proved

The map from components of innerGraph and outer components avoiding Λ_n to components of the glued graph.

noncomputable def fullComponentMap (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    (innerGraph d n ω ψ).ConnectedComponent ⊕ OutsideOnlyComp d n ψ →
      (fullGraph d n ω ψ).ConnectedComponent
  | Sum.inl c => c.lift (fun x => (fullGraph d n ω ψ).connectedComponentMk (boxVertIncl d n x))
      (fun _ _ p _ => ConnectedComponent.sound
        (fullGraph_reachable_of_innerGraph d n ω ψ p.reachable))
  | Sum.inr c => c.1.lift (fun v => (fullGraph d n ω ψ).connectedComponentMk v)
      (fun _ _ p _ => ConnectedComponent.sound
        (p.reachable.mono (outsideGraph_le_fullGraph d n ω ψ)))

Uses 17 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Outer component avoiding the inner box · Outer components avoiding the inner box · Nearest-neighbour graph on a box · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Wired open graph of a glued configuration · Wiring induced on a box through the outer graph · Inclusion of box edges into the next box · Inner open graph with the induced wiring · Inner open edges viewed in the larger box · Open subgraph of an edge configuration · Outer open graph plus the outer boundary clique · 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 byComponent decomposition of the wired glued graph

DefinitionComponent decomposition of the wired glued graph#✓fully proved

Components of the glued graph are components of innerGraph plus the outer components avoiding Λ_n.

noncomputable def fullComponentEquiv (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    (innerGraph d n ω ψ).ConnectedComponent ⊕ OutsideOnlyComp d n ψ ≃
      (fullGraph d n ω ψ).ConnectedComponent :=
  Equiv.ofBijective (fullComponentMap d n ω ψ)
    ⟨fullComponentMap_injective d n ω ψ, fullComponentMap_surjective d n ω ψ⟩

Uses 20 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertex of the next box lying in the inner box · Outer component avoiding the inner box · Outer vertex whose outer component avoids the inner box · Outer components avoiding the inner box · Nearest-neighbour graph on a box · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Component map into the wired glued graph · Wired open graph of a glued configuration · Wiring induced on a box through the outer graph · Inclusion of box edges into the next box · Inner open graph with the induced wiring · Inner open edges viewed in the larger box · Open subgraph of an edge configuration · Outer open graph plus the outer boundary clique · 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 byWired cluster count of a glued configuration splits additively

DefinitionNumber of outer components avoiding the inner box#✓fully proved

The number of outer components avoiding Λ_n.

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

Uses 3 · Used by 3

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

Used byDomain Markov property for the wired measure on nested boxes · Wired cluster count of a glued configuration splits additively · Outer weight factor of an outer configuration

LemmaWired cluster count of a glued configuration splits additively#✓fully proved

The wired cluster count of a glued configuration is the induced cluster count of ω plus outsideShift d n ψ.

lemma numClustersBC_psiExt (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    numClustersBC (boxGraph d (n + 1))
        (StatMech.Lattice.boundaryCliqueGraph (boxBoundary d (n + 1))) (psiExt d n ψ ω)
      = numClustersBC (boxGraph d n) (inducedWiring d n ψ) ω + outsideShift d n ψ

Uses 21 · 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\) · Wiring induced on a box through the outer graph · Number of clusters under a boundary wiring · Number of outer components avoiding the inner box · Gluing a box configuration into an outer configuration · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Boundary wiring relation

Proof usesOuter component avoiding the inner box · Outer components avoiding the inner box · Component decomposition of the wired glued graph · Wired open graph of a glued configuration · Inner open graph with the induced wiring · Inner open edges viewed in the larger box · Open subgraph of an edge configuration · Outer open graph plus the outer boundary clique · Wired glued open graph is the union of inner and outer graphs

Used byDomain Markov property for the wired measure on nested boxes

E. Factorization of the weights

DefinitionOuter Bernoulli edge factor of an outer configuration#✓fully proved

The Bernoulli edge product over the edges of Λ_(n+1) outside Λ_n, evaluated at ψ.

noncomputable def psiEdgeFactor (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    (p : ℝ) : ℝ :=
  ∏ e ∈ (boxGraph d (n + 1)).edgeFinset.filter (fun e => e ∉ Set.range (innerEdge d n)),
    (if ψ e then p else 1 - p)

Uses 6 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into the next box · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byDomain Markov property for the wired measure on nested boxes · Edge product of a glued configuration factorizes · Outer weight factor of an outer configuration · Random-cluster weight of a glued configuration factorizes · Outer factor of the weight of a glued configuration · Positivity of the outer weight factor

LemmaEdge product of a glued configuration factorizes#✓fully proved

The edge product of a glued configuration factorizes into the inner edge product and psiEdgeFactor.

lemma edgeProduct_psiExt (d n : ℕ) {p : ℝ} (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1))))
    (ω : ConfigSpace (Sym2 (boxVerts d n))) :
    edgeProduct (boxGraph d (n + 1)) p (psiExt d n ψ ω)
      = edgeProduct (boxGraph d n) p ω * psiEdgeFactor d n ψ p

Uses 11 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Bernoulli edge product · Outer Bernoulli edge factor of an outer configuration · Gluing a box configuration into an outer configuration · 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 the next box · Hypercubic lattice \(\mathbb{Z}^d\)

Used byDomain Markov property for the wired measure on nested boxes · Random-cluster weight of a glued configuration factorizes

DefinitionOuter weight factor of an outer configuration#✓fully proved

The factor depending only on ψ: psiEdgeFactor · q ^ outsideShift.

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

Uses 4 · Used by 1

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

Used byDomain Markov property for the wired measure on nested boxes

LemmaDomain Markov property for the wired measure on nested boxes#✓fully proved

Domain Markov property: the wired measure on Λ_(n+1), conditioned on the outer configuration ψ, is the random-cluster measure on Λ_n with the induced wiring.

lemma condBcProb_psiExt_eq_bcProb (d n : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) (ω : ConfigSpace (Sym2 (boxVerts d n))) :
    condBcProb (boxGraph d (n + 1))
        (StatMech.Lattice.boundaryCliqueGraph (boxBoundary d (n + 1))) p q
        (innerEdgeFinset d n) ψ (psiExt d n ψ ω)
      = bcProb (boxGraph d n) (inducedWiring d n ψ) p q ω

Uses 28 · 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 · Wiring induced on a box through the outer graph · Edges of the next box coming from the inner box · Gluing a box configuration into an outer configuration · 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 weight with a boundary wiring · Partition function with a boundary wiring · Inclusion of box vertices into the next box · Fibre of configurations agreeing off an edge set · Bernoulli edge product · Edge product of a glued configuration factorizes · Partition function of a conditioning fibre · Inclusion of box edges into the next box · Restriction of a next-box configuration to the inner edges · Number of clusters under a boundary wiring · Wired cluster count of a glued configuration splits additively · Number of outer components avoiding the inner box · Outer Bernoulli edge factor of an outer configuration · Outer weight factor of an outer configuration

Used byConditional wired decrease on inner increasing events for \(q \ge 1\)

F. The induced wiring lives on the boundary

LemmaInduced wiring lies below the inner boundary clique#✓fully proved

The induced wiring lies below the clique on ∂Λ_n.

lemma inducedWiring_le_wired (d n : ℕ) (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    inducedWiring d n ψ ≤ StatMech.Lattice.boundaryCliqueGraph (boxBoundary d n)

Uses 17 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Vertices of the box \((-n, n)^d\) · Wiring induced on a box through the outer graph · Complete graph on the boundary vertices

Proof usesVertex of the next box lying in the inner box · Nearest-neighbour graph on a box · Inclusion of box vertices into the next box · Inclusion of box edges into the next box · Outer open graph plus the outer boundary clique · Open edges of an outer configuration outside the inner box · Nearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Inner vertex boundary of a box · Boundary wiring relation

Used byWired box measure dominates the induced-wiring measure for \(q \ge 1\)

G. Domination by the wired measure

LemmaWired box measure dominates the induced-wiring measure for \(q \ge 1\)#✓fully proved

For q ≥ 1, the measure on Λ_n with the induced wiring is dominated by the wired measure on Λ_n.

lemma condBcProb_psiExt_dominated_wired (d n : ℕ)
    (ψ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) {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 : ℝ)) ω
        * bcProb (boxGraph d n) (inducedWiring d n ψ) p q ω)
      ≤ ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω
          * wiredFkProb (boxGraph d n) (boxBoundary d n) p q ω

Uses 15 · 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\) · Wiring induced on a box through the outer graph · Wired random-cluster probability of a configuration · Increasing event · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesBoundary clique gives the wired random-cluster measure · Random-cluster comparison of boundary conditions for \(q \ge 1\) · Induced wiring lies below the inner boundary clique · Complete graph on the boundary vertices · Boundary wiring relation

Used byConditional wired decrease on inner increasing events for \(q \ge 1\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.