The wired box measure as a conditional measure on the next box

27 fully proved

A. Including Λ_n into Λ_{n+1}

DefinitionInclusion of box vertices into the next box#✓fully proved

The inclusion of the vertices of Λ_n into Λ_{n+1}. The case m = n + 1 of boxVertInclLE.

def boxVertIncl (d n : ℕ) (x : boxVerts d n) : boxVerts d (n + 1) :=
  ⟨(x : Site d), box_subset_succ d n x.2⟩

Uses 3 · Used by 43

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

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Domain 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 · Wiring induced on a box through the outer graph · Induced wiring lies below the inner boundary clique · Wired glued open graph is the union of inner and outer graphs · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Conditional free measure as an induced-wiring measure · Conditional free measure dominates the smaller free box for \(q \ge 1\) · Next-box free measure of a cylinder event as a finite sum · Cluster map into the glued configuration · Injectivity of the free cluster map · Cluster map on inner clusters · Surjectivity of the free cluster map · 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 · 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 · Glued open graph is the union of inner and outer open edges · Inclusion of the annulus wiring into the extra-wired graph · Box as an induced subgraph of the next box · Domain Markov property for the wired box measure · Extended-graph components as inner components plus annulus vertices · Extra-wired components as inner plus annulus-wiring components · Inclusion of box edges into the next box · Configurations closed off the inner edges as inner-box configurations · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph · Inner vertices next to the annulus lie on \(\partial\Lambda_n\) · Box inclusion maps the origin to the origin · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Paths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\) · Open edges of \(\Lambda_n\) are open edges of \(\Lambda_{n+1}\) · Outer projection closes the edges of \(\Lambda_n\) · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionBox as an induced subgraph of the next box#✓fully proved

Λ_n as an induced subgraph of Λ_{n+1}.

def boxGraphEmb (d n : ℕ) : boxGraph d n ↪g boxGraph d (n + 1) :=
  (boxGraph_eq_comap d n) ▸
    SimpleGraph.Embedding.comap ⟨boxVertIncl d n, boxVertIncl_injective d n⟩ (boxGraph d (n + 1))

Uses 6

Statement usesNearest-neighbour graph on a box · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

DefinitionInclusion of box edges into the next box#✓fully proved

The inclusion of edges (unordered pairs) of Λ_n into Λ_{n+1}.

def innerEdge (d n : ℕ) : Sym2 (boxVerts d n) → Sym2 (boxVerts d (n + 1)) :=
  Sym2.map (boxVertIncl d n)

Uses 2 · Used by 43

Statement usesInclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\)

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Domain 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 · Induced wiring lies below the inner boundary clique · Inner open edges viewed in the larger box · Open edges of an outer configuration outside the inner box · Outer Bernoulli edge factor of an outer configuration · Gluing a box configuration into an outer configuration · Wired glued open graph is the union of inner and outer graphs · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Conditional free measure as an induced-wiring measure · Conditional free measure dominates the smaller free box for \(q \ge 1\) · Next-box free measure of a cylinder event as a finite sum · 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 · Glued open graph is the union of inner and outer open edges · Positivity of the outer weight factor · Inclusion of the annulus wiring into the extra-wired graph · Domain Markov property for the wired box measure · Extended-graph components as inner components plus annulus vertices · Extra-wired components as inner plus annulus-wiring components · Extension of a configuration closing the annulus edges · Edges of the next box coming from the inner box · Configurations closed off the inner edges as inner-box configurations · Restriction of a next-box configuration to the inner edges · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph · Number of next-box edges not coming from the inner box · Outer projection agrees with the configuration off \(\Lambda_n\) · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Configurations with a given outer part form its conditioning fibre · Open edges of \(\Lambda_n\) are open edges of \(\Lambda_{n+1}\) · Outer projection closes the edges of \(\Lambda_n\) · Outer projection keeps the edges outside \(\Lambda_n\) · Outer projection is idempotent · Wired \(\Lambda_{n+1}\) measure of a \(\Lambda_n\) cylinder event as a sum · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionVertex of the next box lying in the inner box#✓fully proved

A vertex of Λ_{n+1} lies in Λ_n.

def IsInnerVert (d n : ℕ) (v : boxVerts d (n + 1)) : Prop := (v : Site d) ∈ box d n

Uses 3 · Used by 27

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

Used byComponent decomposition of the wired glued graph · Glued and inner graphs have the same connections on the box · Induced wiring lies below the inner boundary clique · Outer vertex whose outer component avoids the inner box · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Injectivity of the free cluster map · Surjectivity of the free cluster map · Glued open edges at outer vertices are outer edges · Glued connections between inner vertices are inner-graph connections · Outer vertex whose outer open cluster avoids the inner box · A vertex whose outer cluster avoids the inner box lies outside it · Glued connections from an avoiding vertex are outer connections · Number of annulus vertices between consecutive boxes · Inclusion of the annulus wiring into the extra-wired graph · Restriction of a wiring to the annulus vertices · Vertices of the annulus between consecutive boxes · Domain Markov property for the wired box measure · Extended-graph components as inner components plus annulus vertices · Extra-wired components as inner plus annulus-wiring components · Map from inner wired components and annulus vertices to components · Vertex on the boundary of the inner box · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph · Wiring with every edge inside the annulus · Inner vertices next to the annulus lie on \(\partial\Lambda_n\) · Paths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\)

B. Extension by closed annulus edges and wiring the inner boundary

DefinitionExtension of a configuration closing the annulus edges#✓fully proved

The extension of a configuration of Λ_n to Λ_{n+1} that closes every edge not coming from Λ_n.

noncomputable def crossExt (d n : ℕ) (ω : 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 false

Uses 5 · Used by 10

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 byClosed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Inclusion of the annulus wiring into the extra-wired graph · Domain Markov property for the wired box measure · Extended-graph components as inner components plus annulus vertices · Extra-wired components as inner plus annulus-wiring components · Extended open graph with the inner box boundary wired · Configurations closed off the inner edges as inner-box configurations · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph

DefinitionVertex on the boundary of the inner box#✓fully proved

A vertex of Λ_{n+1} on the vertex boundary of Λ_n.

def innerBdry (d n : ℕ) (v : boxVerts d (n + 1)) : Prop :=
  IsInnerVert d n v ∧ (v : Site d) ∈ vertexBoundary d n

Uses 5 · Used by 9

Statement usesVertex of the next box lying in the inner box · Vertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Inner vertex boundary of a box

Used byClosed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Inclusion of the annulus wiring into the extra-wired graph · Domain Markov property for the wired box measure · Extended-graph components as inner components plus annulus vertices · Extra-wired components as inner plus annulus-wiring components · Extended open graph with the inner box boundary wired · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph

DefinitionExtended open graph with the inner box boundary wired#✓fully proved

The open subgraph of crossExt ω in Λ_{n+1} with the boundary of Λ_n wired.

noncomputable def crossWiredGraph (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n))) :
    SimpleGraph (boxVerts d (n + 1)) :=
  wiredGraph (boxGraph d (n + 1)) (innerBdry d n) (crossExt d n ω)

Uses 8 · Used by 9

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Extension of a configuration closing the annulus edges · Vertex on the boundary of the inner box · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Wired open graph

Used byClosed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Inclusion of the annulus wiring into the extra-wired graph · Domain Markov property for the wired box measure · Extended-graph components as inner components plus annulus vertices · Extra-wired components as inner plus annulus-wiring components · Map from inner wired components and annulus vertices to components · Extended wired graph with an extra wiring added · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph

C. Clusters of the extended configuration

AbbreviationOpen graph of a box configuration with the box boundary wired#✓fully proved

The open subgraph of ω in Λ_n with the boundary of Λ_n wired.

noncomputable abbrev innerWiredGraph (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n))) :
    SimpleGraph (boxVerts d n) :=
  wiredGraph (boxGraph d n) (boxBoundary d n) ω

Uses 7 · 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\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Wired open graph

Used byClosed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Domain Markov property for the wired box measure · Extended-graph components as inner components plus annulus vertices · Extra-wired components as inner plus annulus-wiring components · Map from inner and annulus-wiring components to extra-wired ones · Map from inner wired components and annulus vertices to components · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph

DefinitionInclusion of the wired inner graph into the extended wired graph#✓fully proved

The inclusion of the wired open graph of Λ_n into crossWiredGraph.

def innerWiredHom (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n))) :
    (innerWiredGraph d n ω) →g (crossWiredGraph d n ω) where
  toFun := boxVertIncl d n
  map_rel' := fun {a b} hab => (crossWiredGraph_adj_boxVertIncl d n ω a b).mpr hab

Uses 19 · 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 · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Extension of a configuration closing the annulus edges · Extended open graph with the inner box boundary wired · Vertex on the boundary of the inner box · Inclusion of box edges into the next box · Open graph of a box configuration with the box boundary wired · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Inner vertex boundary of a box · Boundary wiring relation · Wired open graph

Used byMap from inner wired components and annulus vertices to components

DefinitionMap from inner wired components and annulus vertices to components#✓fully proved

Components of crossWiredGraph from wired components of ω in Λ_n and annulus vertices.

noncomputable def crossComponentEquivFun (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n))) :
    (innerWiredGraph d n ω).ConnectedComponent ⊕
      {v : boxVerts d (n + 1) // ¬ IsInnerVert d n v} →
      (crossWiredGraph d n ω).ConnectedComponent
  | Sum.inl c => c.map (innerWiredHom d n ω)
  | Sum.inr v => (crossWiredGraph d n ω).connectedComponentMk v.1

Uses 6 · 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\) · Extended open graph with the inner box boundary wired · Open graph of a box configuration with the box boundary wired · Inclusion of the wired inner graph into the extended wired graph

Used byExtended-graph components as inner components plus annulus vertices

DefinitionExtended-graph components as inner components plus annulus vertices#✓fully proved

Components of crossWiredGraph are the wired components of ω in Λ_n plus one singleton per annulus vertex.

noncomputable def crossComponentEquiv (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n))) :
    (innerWiredGraph d n ω).ConnectedComponent ⊕
      {v : boxVerts d (n + 1) // ¬ IsInnerVert d n v} ≃
      (crossWiredGraph d n ω).ConnectedComponent :=
  Equiv.ofBijective (crossComponentEquivFun d n ω)
    ⟨crossComponentEquivFun_injective d n ω, crossComponentEquivFun_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 · Vertex boundary of a box · Nearest-neighbour graph on a box · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Map from inner wired components and annulus vertices to components · Extension of a configuration closing the annulus edges · Extended open graph with the inner box boundary wired · Vertex on the boundary of the inner box · Inclusion of box edges into the next box · Open graph of a box configuration with the box boundary wired · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Inner vertex boundary of a box · Boundary wiring relation · Wired open graph

Used byDomain Markov property for the wired box measure

DefinitionNumber of annulus vertices between consecutive boxes#✓fully proved

The number of vertices of the annulus Λ_{n+1} \ Λ_n.

noncomputable def annulusCard (d n : ℕ) : ℕ :=
  Nat.card {v : boxVerts d (n + 1) // ¬ IsInnerVert d n v}

Uses 2 · Used by 2

Statement usesVertex of the next box lying in the inner box · Vertices of the box \((-n, n)^d\)

Used byDomain Markov property for the wired box measure · Annulus constant linking the extended and wired inner weights

D. Weights and the conditional measure

DefinitionNumber of next-box edges not coming from the inner box#✓fully proved

The number of edges of Λ_{n+1} not coming from Λ_n.

noncomputable def nonInnerEdgeCard (d n : ℕ) : ℕ :=
  ((boxGraph d (n + 1)).edgeFinset.filter (fun e => e ∉ Set.range (innerEdge d n))).card

Uses 5 · Used by 4

Statement usesNearest-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 byClosed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Domain Markov property for the wired box measure · Annulus constant linking the extended and wired inner weights · Annulus constant counting the components of an extra wiring

DefinitionAnnulus constant linking the extended and wired inner weights#✓fully proved

The constant (1 - p)^{#annulus edges} q^{#annulus vertices} relating the extended weight to the wired weight on Λ_n.

noncomputable def crossShift (d n : ℕ) (p q : ℝ) : ℝ :=
  (1 - p) ^ nonInnerEdgeCard d n * q ^ annulusCard d n

Uses 2 · Used by 1

Statement usesNumber of annulus vertices between consecutive boxes · Number of next-box edges not coming from the inner box

Used byDomain Markov property for the wired box measure

DefinitionEdges of the next box coming from the inner box#✓fully proved

The edges of Λ_{n+1} coming from Λ_n.

noncomputable def innerEdgeFinset (d n : ℕ) : Finset (Sym2 (boxVerts d (n + 1))) :=
  Finset.univ.image (innerEdge d n)

Uses 4 · Used by 20

Statement usesVertices 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 · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Conditional free probabilities depend only on the outer configuration · Domain Markov property · Conditional free measure as an induced-wiring measure · Fibre-mass factorization of random-cluster probabilities · Conditional free measure dominates the smaller free box for \(q \ge 1\) · Decomposition of the free measure over the outer configuration · One-step box monotonicity of free measures for \(q \ge 1\) · Conditional partition function in terms of the induced wiring · Fibre masses of the free measure sum to one · Domain Markov property for the wired box measure · Configurations closed off the inner edges as inner-box configurations · Outer projection agrees with the configuration off \(\Lambda_n\) · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Configurations with a given outer part form its conditioning fibre · 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\)

DefinitionRestriction of a next-box configuration to the inner edges#✓fully proved

The restriction of a configuration of Λ_{n+1} to the edges of Λ_n.

noncomputable def innerRestrict (d n : ℕ) (ρ : ConfigSpace (Sym2 (boxVerts d (n + 1)))) :
    ConfigSpace (Sym2 (boxVerts d n)) :=
  fun e => ρ (innerEdge d n e)

Uses 3 · Used by 18

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

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Domain Markov property for the wired measure on nested boxes · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Origin-to-\(\partial\Lambda_n\) event as an event on \(\Lambda_{n+1}\) · Conditional free measure as an induced-wiring measure · Conditional free measure dominates the smaller free box for \(q \ge 1\) · Increasing box events gain free \(q = 2\) probability in the next box · Next-box free measure of a cylinder event as a finite sum · One-step box monotonicity of free measures for \(q \ge 1\) · Conditional partition function in terms of the induced wiring · Domain Markov property for the wired box measure · Configurations closed off the inner edges as inner-box configurations · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Wired box measures decrease on increasing cylinder events at \(q = 2\) · 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\) · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionConfigurations closed off the inner edges as inner-box configurations#✓fully proved

Configurations of Λ_{n+1} closed off the inner edges correspond to configurations of Λ_n.

noncomputable def innerFibreEquiv (d n : ℕ) :
    {ρ : ConfigSpace (Sym2 (boxVerts d (n + 1))) //
        AgreesOff (innerEdgeFinset d n) (fun _ => false) ρ} ≃
      ConfigSpace (Sym2 (boxVerts d n)) where
  toFun ρ := innerRestrict d n ρ.1
  invFun ω := ⟨crossExt d n ω, agreesOff_crossExt d n ω⟩
  left_inv ρ := by
    apply Subtype.ext
    exact crossExt_innerRestrict_of_agreesOff d n ρ.2
  right_inv ω := innerRestrict_crossExt d n ω

Uses 10

Statement usesConfiguration space of a statistical-mechanics model · Agreement of configurations off an edge set · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Extension of a configuration closing the annulus edges · Inclusion of box edges into the next box · Edges of the next box coming from the inner box · Restriction of a next-box configuration to the inner edges · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

TheoremDomain Markov property for the wired box measure#✓fully proved

Conditioned on every edge outside Λ_n being closed, the random-cluster measure on Λ_{n+1} with the boundary of Λ_n wired is the wired random-cluster measure on Λ_n (Grimmett, The Random-Cluster Model, 2006, Lemma 4.13).

theorem condBcProb_crossExt_eq_wiredFkProb (d n : ℕ) {p q : ℝ}
    (_hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) (ω : ConfigSpace (Sym2 (boxVerts d n))) :
    condBcProb (boxGraph d (n + 1))
        (StatMech.Lattice.boundaryCliqueGraph (innerBdry d n)) p q
        (innerEdgeFinset d n) (fun _ => false) (crossExt d n ω)
      = wiredFkProb (boxGraph d n) (boxBoundary d n) p q ω

Uses 36

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 · Extension of a configuration closing the annulus edges · Vertex on the boundary of the inner box · Edges of the next box coming from the inner box · Wired random-cluster probability of a 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 · Vertex of the next box lying in the inner box · Number of annulus vertices between consecutive boxes · Random-cluster weight with a boundary wiring · Inclusion of box vertices into the next box · Fibre of configurations agreeing off an edge set · Extended-graph components as inner components plus annulus vertices · Annulus constant linking the extended and wired inner weights · Extended open graph with the inner box boundary wired · Bernoulli edge product · Partition function of a conditioning fibre · Inclusion of box edges into the next box · Restriction of a next-box configuration to the inner edges · Open graph of a box configuration with the box boundary wired · Number of next-box edges not coming from the inner box · Number of clusters under a boundary wiring · Open subgraph of an edge configuration · Wired random-cluster weight · Wired random-cluster partition function · Hypercubic lattice \(\mathbb{Z}^d\) · Number of open clusters with wired boundary conditions · Open subgraph of a bond configuration · Wired open graph

E. Additional wiring in the annulus

DefinitionWiring with every edge inside the annulus#✓fully proved

Every edge of D joins vertices of the annulus Λ_{n+1} \ Λ_n.

def IsAnnulusWiring (d n : ℕ) (D : SimpleGraph (boxVerts d (n + 1))) : Prop :=
  ∀ ⦃u v⦄, D.Adj u v → ¬ IsInnerVert d n u

Uses 2 · Used by 5

Statement usesVertex of the next box lying in the inner box · Vertices of the box \((-n, n)^d\)

Used byClosed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Extra-wired components as inner plus annulus-wiring components · Map from inner and annulus-wiring components to extra-wired ones · Inclusion of the wired inner graph into the extra-wired graph

DefinitionExtended wired graph with an extra wiring added#✓fully proved

crossWiredGraph with the extra wiring D added.

noncomputable def crossWiredGraphAdd (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (D : SimpleGraph (boxVerts d (n + 1))) : SimpleGraph (boxVerts d (n + 1)) :=
  crossWiredGraph d n ω ⊔ D

Uses 3 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Extended open graph with the inner box boundary wired

Used byClosed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Inclusion of the annulus wiring into the extra-wired graph · Extra-wired components as inner plus annulus-wiring components · Map from inner and annulus-wiring components to extra-wired ones · Inclusion of the wired inner graph into the extra-wired graph

AbbreviationVertices of the annulus between consecutive boxes#✓fully proved

The vertices of the annulus Λ_{n+1} \ Λ_n.

abbrev AnnulusVert (d n : ℕ) : Type := {v : boxVerts d (n + 1) // ¬ IsInnerVert d n v}

Uses 2 · Used by 6

Statement usesVertex of the next box lying in the inner box · Vertices of the box \((-n, n)^d\)

Used byClosed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Inclusion of the annulus wiring into the extra-wired graph · Restriction of a wiring to the annulus vertices · Extra-wired components as inner plus annulus-wiring components · Map from inner and annulus-wiring components to extra-wired ones · Annulus constant counting the components of an extra wiring

DefinitionRestriction of a wiring to the annulus vertices#✓fully proved

The restriction of D to the annulus vertices.

noncomputable def annulusSubgraph (d n : ℕ) (D : SimpleGraph (boxVerts d (n + 1))) :
    SimpleGraph (AnnulusVert d n) :=
  SimpleGraph.comap (Subtype.val) D

Uses 3 · Used by 5

Statement usesVertices of the annulus between consecutive boxes · Vertex of the next box lying in the inner box · Vertices of the box \((-n, n)^d\)

Used byClosed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Inclusion of the annulus wiring into the extra-wired graph · Extra-wired components as inner plus annulus-wiring components · Map from inner and annulus-wiring components to extra-wired ones · Annulus constant counting the components of an extra wiring

DefinitionInclusion of the wired inner graph into the extra-wired graph#✓fully proved

The inclusion of the wired open graph of Λ_n into crossWiredGraphAdd.

def innerWiredHomAdd (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    {D : SimpleGraph (boxVerts d (n + 1))} (hD : IsAnnulusWiring d n D) :
    (innerWiredGraph d n ω) →g (crossWiredGraphAdd d n ω D) where
  toFun := boxVertIncl d n
  map_rel' := fun {a b} hab => (crossWiredGraphAdd_adj_boxVertIncl d n ω hD a b).mpr hab

Uses 21 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Wiring with every edge inside the annulus · Vertex of the next box lying in the inner box · Vertex boundary of a box · Nearest-neighbour graph on a box · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Extension of a configuration closing the annulus edges · Extended open graph with the inner box boundary wired · Extended wired graph with an extra wiring added · Vertex on the boundary of the inner box · Inclusion of box edges into the next box · Open graph of a box configuration with the box boundary wired · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Inner vertex boundary of a box · Boundary wiring relation · Wired open graph

Used byMap from inner and annulus-wiring components to extra-wired ones

DefinitionInclusion of the annulus wiring into the extra-wired graph#✓fully proved

The inclusion of the annulus wiring into crossWiredGraphAdd.

def annulusHomAdd (d n : ℕ) (ω : ConfigSpace (Sym2 (boxVerts d n)))
    (D : SimpleGraph (boxVerts d (n + 1))) :
    (annulusSubgraph d n D) →g (crossWiredGraphAdd d n ω D) where
  toFun := Subtype.val
  map_rel' := fun {a b} hab => (crossWiredGraphAdd_adj_annulus d n ω D a b).mpr hab

Uses 19 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the annulus between consecutive boxes · Vertex of the next box lying in the inner box · Restriction of a wiring to the annulus vertices · Nearest-neighbour graph on a box · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Extension of a configuration closing the annulus edges · Extended open graph with the inner box boundary wired · Extended wired graph with an extra wiring added · Vertex on the boundary of the inner box · Inclusion of box edges into the next box · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Open subgraph of a bond configuration · Inner vertex boundary of a box · Boundary wiring relation · Wired open graph

Used byMap from inner and annulus-wiring components to extra-wired ones

DefinitionMap from inner and annulus-wiring components to extra-wired ones#✓fully proved

Components of crossWiredGraphAdd from wired components of ω in Λ_n and components of the annulus wiring.

noncomputable def crossComponentEquivAddFun (d n : ℕ)
    (ω : ConfigSpace (Sym2 (boxVerts d n))) {D : SimpleGraph (boxVerts d (n + 1))}
    (hD : IsAnnulusWiring d n D) :
    (innerWiredGraph d n ω).ConnectedComponent ⊕
      (annulusSubgraph d n D).ConnectedComponent →
      (crossWiredGraphAdd d n ω D).ConnectedComponent
  | Sum.inl c => c.map (innerWiredHomAdd d n ω hD)
  | Sum.inr a => a.map (annulusHomAdd d n ω D)

Uses 9 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the annulus between consecutive boxes · Wiring with every edge inside the annulus · Inclusion of the annulus wiring into the extra-wired graph · Restriction of a wiring to the annulus vertices · Vertices of the box \((-n, n)^d\) · Extended wired graph with an extra wiring added · Open graph of a box configuration with the box boundary wired · Inclusion of the wired inner graph into the extra-wired graph

Used byExtra-wired components as inner plus annulus-wiring components

DefinitionExtra-wired components as inner plus annulus-wiring components#✓fully proved

Components of crossWiredGraphAdd are the wired components of ω in Λ_n plus the components of the annulus wiring.

noncomputable def crossComponentEquivAdd (d n : ℕ)
    (ω : ConfigSpace (Sym2 (boxVerts d n))) {D : SimpleGraph (boxVerts d (n + 1))}
    (hD : IsAnnulusWiring d n D) :
    (innerWiredGraph d n ω).ConnectedComponent ⊕
      (annulusSubgraph d n D).ConnectedComponent ≃
      (crossWiredGraphAdd d n ω D).ConnectedComponent :=
  Equiv.ofBijective (crossComponentEquivAddFun d n ω hD)
    ⟨crossComponentEquivAddFun_injective d n ω hD,
     crossComponentEquivAddFun_surjective d n ω hD⟩

Uses 24 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the annulus between consecutive boxes · Wiring with every edge inside the annulus · Vertex of the next box lying in the inner box · Restriction of a wiring to the annulus vertices · Vertex boundary of a box · Nearest-neighbour graph on a box · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Map from inner and annulus-wiring components to extra-wired ones · Extension of a configuration closing the annulus edges · Extended open graph with the inner box boundary wired · Extended wired graph with an extra wiring added · Vertex on the boundary of the inner box · Inclusion of box edges into the next box · Open graph of a box configuration with the box boundary wired · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Inner vertex boundary of a box · Boundary wiring relation · Wired open graph

Used byClosed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law

DefinitionAnnulus constant counting the components of an extra wiring#✓fully proved

The constant (1 - p)^{#annulus edges} q^{#components of the annulus wiring}.

noncomputable def crossShiftAdd (d n : ℕ) (p q : ℝ)
    (D : SimpleGraph (boxVerts d (n + 1))) : ℝ :=
  (1 - p) ^ nonInnerEdgeCard d n * q ^ Nat.card (annulusSubgraph d n D).ConnectedComponent

Uses 4 · Used by 1

Statement usesVertices of the annulus between consecutive boxes · Restriction of a wiring to the annulus vertices · Vertices of the box \((-n, n)^d\) · Number of next-box edges not coming from the inner box

Used byClosed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.