Domination of an inner wired FK measure by an outer one

77 fully proved

A.1. Inner edges

DefinitionInner vertex of the outer graph#✓fully proved

A vertex of G_out is inner if it lies in the image of ι.

def ocd_IsInnerVert (v : Vout) : Prop := ∃ x : Vin, ιV x = v

Used by 8

Used byInjectivity of the cluster map · Surjectivity of the cluster map · Full-graph edges at non-inner vertices are outside-graph edges · Full-graph reachability of images gives inner cluster reachability · Endpoints of inner image edges are inner vertices · Full-graph reachability from an outside-only vertex stays outside · Outside-only vertex · Outside-only vertices are not inner

DefinitionImage of an inner-graph edge in the outer graph#✓fully proved

The image in G_out of an edge of G_in under ι.

def ocd_innerEdge (e : Sym2 Vin) : Sym2 Vout := Sym2.map ιV e

Used by 37

Used byGlued configuration agrees with the outer one off the inner edge set · Inner vertex with an outside-graph edge lies on the inner boundary · Factorization of the edge weight of a glued configuration · Projection fibres are conditioning fibres · Finite set of inner edges · Edges of the inner graph map onto the inner edges of the outer graph · Injectivity of the edge map · Edge map sends \(\{x, y\}\) to \(\{\iota x, \iota y\}\) · Image of the inner open subgraph in the outer graph · Endpoints of inner image edges are inner vertices · Inner image graph on embedded vertices is the open subgraph · Restriction of an outer configuration to inner edges · Restriction pulls back all-open events to their images · Restricting a glued configuration recovers the inner one · Outer wired all-open probability at most the inner wired one · Inner edge set is the range of the edge map · Projected configuration is closed on inner edges · Projection keeps non-inner edges · Idempotence of the inner-edge projection · Outside-graph adjacency: open non-inner edge or boundary pair · Outside graph is a subgraph of the full cluster graph · Graph of open non-inner edges · Outer Bernoulli edge weight of a configuration · Positivity of the outer edge weight · Gluing of inner and outer configurations · Glued configuration on inner edges ignores the outer configuration · Glued configuration equals the outer one at each non-inner edge · Glued configuration takes the inner value on inner edges · Glued value on \(\{\iota x, \iota y\}\) is the inner value on \(\{x, y\}\) · Agreeing configuration is the gluing of its own restriction · Full cluster graph as the union of inner image and outside graphs · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Wired off-centre upper bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure · Translation invariance of the wired \(q = 2\) infinite-volume measure

LemmaInjectivity of the edge map#✓fully proved

The edge map Sym2.map ι is injective when ι is.

lemma ocd_innerEdge_injective (hι : Function.Injective ιV) :
    Function.Injective (ocd_innerEdge ιV)

Uses 1 · Used by 2

Statement usesImage of an inner-graph edge in the outer graph

Used byFactorization of the edge weight of a glued configuration · Glued configuration takes the inner value on inner edges

LemmaEdge map sends \(\{x, y\}\) to \(\{\iota x, \iota y\}\)#✓fully proved

The image of the edge {x, y} is {ι x, ι y}.

lemma ocd_innerEdge_mk (x y : Vin) :
    ocd_innerEdge ιV s(x, y) = s(ιV x, ιV y)

Uses 1 · Used by 5

Statement usesImage of an inner-graph edge in the outer graph

Used byInner vertex with an outside-graph edge lies on the inner boundary · Edges of the inner graph map onto the inner edges of the outer graph · Endpoints of inner image edges are inner vertices · Inner image graph on embedded vertices is the open subgraph · Glued value on \(\{\iota x, \iota y\}\) is the inner value on \(\{x, y\}\)

DefinitionAdjacency matching of the inner embedding#✓fully proved

The map ι matches adjacency: x ~ y in G_in iff ι x ~ ι y in G_out.

def ocd_AdjMatch : Prop := ∀ x y, Gin.Adj x y ↔ Gout.Adj (ιV x) (ιV y)

Used by 28

Used byFactorization of the wired FK weight of a glued configuration · Conditional outer wired probability at most the inner wired one, \(q \ge 1\) · Domination by the inner wired measure under a coarser induced wiring · Conditional outer measure is the induced-wiring FK measure · Conditional outer probability as an induced-wiring probability · Factorization of the edge weight of a glued configuration · Free inner measure is dominated by the conditional outer measure · Free inner measure is dominated by every induced-wiring measure · Cluster bijection for a glued configuration · Cluster map into the clusters of a glued configuration · Injectivity of the cluster map · Cluster map sends the inner cluster of \(x\) to that of \(\iota x\) · Cluster map sends an outside-only cluster of \(v\) to that of \(v\) · Surjectivity of the cluster map · Inner cluster reachability gives full-graph reachability of images · Full-graph and inner cluster reachability agree on embedded vertices · Factorization of the conditioned outer partition function · Edges of the inner graph map onto the inner edges of the outer graph · Full-graph reachability of images gives inner cluster reachability · Inner image graph on embedded vertices is the open subgraph · Lattice inclusion matches induced adjacency · Inner wired domination for vertex sets of \(\mathbb{Z}^d\) · Glued cluster count is induced-wiring count plus outside-only clusters · Inner wired domination of the restricted outer wired measure · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure

A.2. Gluing configurations

DefinitionGluing of inner and outer configurations#✓fully proved

The configuration on G_out that equals the inner configuration ω on inner edges and the outer configuration ψ elsewhere.

noncomputable def ocd_psiExt (ψ : ConfigSpace (Sym2 Vout)) (ω : ConfigSpace (Sym2 Vin)) :
    ConfigSpace (Sym2 Vout) :=
  fun e => if h : e ∈ Set.range (ocd_innerEdge ιV) then ω h.choose else ψ e

Uses 2 · Used by 28

Statement usesConfiguration space of a statistical-mechanics model · Image of an inner-graph edge in the outer graph

Used byGlued configuration agrees with the outer one off the inner edge set · Factorization of the wired FK weight of a glued configuration · Conditional outer wired probability at most the inner wired one, \(q \ge 1\) · Conditional outer measure is the induced-wiring FK measure · Conditional outer probability as an induced-wiring probability · Conditioning fibre is the set of gluings · Factorization of the edge weight of a glued configuration · Free inner measure is dominated by the conditional outer measure · Cluster graph of a glued configuration · Factorization of the conditioned outer partition function · Image of the inner open subgraph in the outer graph · Endpoints of inner image edges are inner vertices · Inner image graph on embedded vertices is the open subgraph · Restricting a glued configuration recovers the inner one · Glued cluster count is induced-wiring count plus outside-only clusters · Projection closing every inner edge · Projected configuration is closed on inner edges · Projection keeps non-inner edges · Outside graph is a subgraph of the full cluster graph · Glued configuration on inner edges ignores the outer configuration · Glued configuration equals the outer one at each non-inner edge · Glued configuration takes the inner value on inner edges · Glued value on \(\{\iota x, \iota y\}\) is the inner value on \(\{x, y\}\) · Agreeing configuration is the gluing of its own restriction · Full cluster graph as the union of inner image and outside graphs · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure

DefinitionRestriction of an outer configuration to inner edges#✓fully proved

The restriction of a configuration on G_out to the edges of G_in, read through ι.

noncomputable def ocd_innerRestrict (ρ : ConfigSpace (Sym2 Vout)) : ConfigSpace (Sym2 Vin) :=
  fun e => ρ (ocd_innerEdge ιV e)

Uses 2 · Used by 15

Statement usesConfiguration space of a statistical-mechanics model · Image of an inner-graph edge in the outer graph

Used byConditional outer wired probability at most the inner wired one, \(q \ge 1\) · Conditional outer probability as an induced-wiring probability · Conditioning fibre is the set of gluings · Free inner measure is dominated by the conditional outer measure · Factorization of the conditioned outer partition function · Restriction pulls back all-open events to their images · Restricting a glued configuration recovers the inner one · Inner wired domination for vertex sets of \(\mathbb{Z}^d\) · Outer wired all-open probability at most the inner wired one · Agreeing configuration is the gluing of its own restriction · Inner wired domination of the restricted outer wired measure · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure

DefinitionFinite set of inner edges#✓fully proved

The finite set of inner edges of G_out.

noncomputable def ocd_innerEdgeFinset : Finset (Sym2 Vout) :=
  Finset.univ.image (ocd_innerEdge ιV)

Uses 1 · Used by 17

Statement usesImage of an inner-graph edge in the outer graph

Used byGlued configuration agrees with the outer one off the inner edge set · Law of total probability over outside configurations · Conditional outer wired probability at most the inner wired one, \(q \ge 1\) · Conditional outer measure is the induced-wiring FK measure · Conditional outer probability as an induced-wiring probability · Conditioning fibre is the set of gluings · Projection fibres are conditioning fibres · Free inner measure is dominated by the conditional outer measure · Factorization of the conditioned outer partition function · Inner edge set is the range of the edge map · Agreeing configuration is the gluing of its own restriction · Outer wired fibre masses sum to one · Inner wired domination of the restricted outer wired measure · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure

LemmaInner edge set is the range of the edge map#✓fully proved

Membership in the inner edge set is membership in the image of the edge map.

lemma ocd_mem_innerEdgeFinset {e : Sym2 Vout} :
    e ∈ ocd_innerEdgeFinset (Vin := Vin) ιV ↔ e ∈ Set.range (ocd_innerEdge ιV)

Uses 2 · Used by 4

Statement usesImage of an inner-graph edge in the outer graph · Finite set of inner edges

Used byGlued configuration agrees with the outer one off the inner edge set · Projection fibres are conditioning fibres · Agreeing configuration is the gluing of its own restriction · Ergodicity of the wired random-cluster measure

LemmaGlued configuration takes the inner value on inner edges#✓fully proved

The glued configuration takes the inner value on inner edges.

lemma ocd_psiExt_innerEdge (hι : Function.Injective ιV) (ψ : ConfigSpace (Sym2 Vout))
    (ω : ConfigSpace (Sym2 Vin)) (e : Sym2 Vin) :
    ocd_psiExt ιV ψ ω (ocd_innerEdge ιV e) = ω e

Uses 4 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Image of an inner-graph edge in the outer graph · Gluing of inner and outer configurations

Proof usesInjectivity of the edge map

Used byFactorization of the edge weight of a glued configuration · Inner image graph on embedded vertices is the open subgraph · Restricting a glued configuration recovers the inner one · Projected configuration is closed on inner edges · Glued configuration on inner edges ignores the outer configuration · Glued value on \(\{\iota x, \iota y\}\) is the inner value on \(\{x, y\}\)

LemmaGlued configuration equals the outer one at each non-inner edge#✓fully proved

The glued configuration takes the outer value off the inner edges.

lemma ocd_psiExt_eq_psi_of_not_range (ψ : ConfigSpace (Sym2 Vout))
    (ω : ConfigSpace (Sym2 Vin)) {e : Sym2 Vout}
    (he : e ∉ Set.range (ocd_innerEdge ιV)) : ocd_psiExt ιV ψ ω e = ψ e

Uses 3 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Image of an inner-graph edge in the outer graph · Gluing of inner and outer configurations

Used byGlued configuration agrees with the outer one off the inner edge set · Factorization of the edge weight of a glued configuration · Projection keeps non-inner edges · Outside graph is a subgraph of the full cluster graph · Full cluster graph as the union of inner image and outside graphs

LemmaGlued value on \(\{\iota x, \iota y\}\) is the inner value on \(\{x, y\}\)#✓fully proved

The glued configuration on {ι x, ι y} is the inner value on {x, y}.

lemma ocd_psiExt_innerEdge_pair (hι : Function.Injective ιV) (ψ : ConfigSpace (Sym2 Vout))
    (ω : ConfigSpace (Sym2 Vin)) (x y : Vin) :
    ocd_psiExt ιV ψ ω s(ιV x, ιV y) = ω s(x, y)

Uses 5

Statement usesConfiguration space of a statistical-mechanics model · Gluing of inner and outer configurations

Proof usesImage of an inner-graph edge in the outer graph · Edge map sends \(\{x, y\}\) to \(\{\iota x, \iota y\}\) · Glued configuration takes the inner value on inner edges

LemmaRestricting a glued configuration recovers the inner one#✓fully proved

Restricting a glued configuration recovers the inner configuration.

@[simp] lemma ocd_innerRestrict_psiExt (hι : Function.Injective ιV) (ψ : ConfigSpace (Sym2 Vout))
    (ω : ConfigSpace (Sym2 Vin)) : ocd_innerRestrict ιV (ocd_psiExt ιV ψ ω) = ω

Uses 5 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Restriction of an outer configuration to inner edges · Gluing of inner and outer configurations

Proof usesImage of an inner-graph edge in the outer graph · Glued configuration takes the inner value on inner edges

Used byConditional outer wired probability at most the inner wired one, \(q \ge 1\) · Conditional outer probability as an induced-wiring probability · Free inner measure is dominated by the conditional outer measure · Factorization of the conditioned outer partition function · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure

LemmaGlued configuration agrees with the outer one off the inner edge set#✓fully proved

A glued configuration agrees with the outer configuration off the inner edges.

lemma ocd_agreesOff_psiExt (ψ : ConfigSpace (Sym2 Vout)) (ω : ConfigSpace (Sym2 Vin)) :
    AgreesOff (ocd_innerEdgeFinset (Vin := Vin) ιV) ψ (ocd_psiExt ιV ψ ω)

Uses 7 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Agreement of configurations off an edge set · Finite set of inner edges · Gluing of inner and outer configurations

Proof usesImage of an inner-graph edge in the outer graph · Inner edge set is the range of the edge map · Glued configuration equals the outer one at each non-inner edge

Used byConditional outer measure is the induced-wiring FK measure · Conditioning fibre is the set of gluings

LemmaAgreeing configuration is the gluing of its own restriction#✓fully proved

A configuration that agrees with ψ off the inner edges is the gluing of ψ with its own restriction.

lemma ocd_psiExt_innerRestrict_of_agreesOff (hι : Function.Injective ιV)
    {ψ ρ : ConfigSpace (Sym2 Vout)}
    (hρ : AgreesOff (ocd_innerEdgeFinset (Vin := Vin) ιV) ψ ρ) :
    ocd_psiExt ιV ψ (ocd_innerRestrict ιV ρ) = ρ

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Agreement of configurations off an edge set · Finite set of inner edges · Restriction of an outer configuration to inner edges · Gluing of inner and outer configurations

Proof usesImage of an inner-graph edge in the outer graph · Inner edge set is the range of the edge map

Used byConditioning fibre is the set of gluings

LemmaConditioning fibre is the set of gluings#✓fully proved

The configurations agreeing with ψ off the inner edges are exactly the gluings of ψ with inner configurations.

lemma ocd_condFibre_eq_image_psiExt (hι : Function.Injective ιV) (ψ : ConfigSpace (Sym2 Vout)) :
    condFibre (ocd_innerEdgeFinset (Vin := Vin) ιV) ψ
      = Finset.univ.image (ocd_psiExt ιV ψ)

Uses 8 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Fibre of configurations agreeing off an edge set · Finite set of inner edges · Gluing of inner and outer configurations

Proof usesAgreement of configurations off an edge set · Glued configuration agrees with the outer one off the inner edge set · Restriction of an outer configuration to inner edges · Agreeing configuration is the gluing of its own restriction

Used byConditional outer probability as an induced-wiring probability · Factorization of the conditioned outer partition function

B.1. Definitions

DefinitionGraph of open non-inner edges#✓fully proved

The graph of ψ-open edges of G_out that are not inner edges.

noncomputable def ocd_outsideOpenGraph (ψ : ConfigSpace (Sym2 Vout)) : SimpleGraph Vout where
  Adj x y := Gout.Adj x y ∧ ψ s(x, y) = true ∧ s(x, y) ∉ Set.range (ocd_innerEdge ιV)
  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 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Image of an inner-graph edge in the outer graph

Used byOutside graph with the wired boundary clique · Outside-graph adjacency: open non-inner edge or boundary pair · Outside graph is a subgraph of the full cluster graph · Full cluster graph as the union of inner image and outside graphs

DefinitionOutside graph with the wired boundary clique#✓fully proved

The outside graph: ψ-open non-inner edges together with the clique on the wired boundary ∂_out.

noncomputable def ocd_outsideGraph (ψ : ConfigSpace (Sym2 Vout)) : SimpleGraph Vout :=
  ocd_outsideOpenGraph Gout ιV ψ ⊔ StatMech.Lattice.boundaryCliqueGraph bdryOut

Uses 3 · Used by 23

Statement usesConfiguration space of a statistical-mechanics model · Graph of open non-inner edges · Complete graph on the boundary vertices

Used byInner vertex with an outside-graph edge lies on the inner boundary · Cluster map into the clusters of a glued configuration · Injectivity of the cluster map · Cluster map sends an outside-only cluster of \(v\) to that of \(v\) · Surjectivity of the cluster map · Full-graph edges at non-inner vertices are outside-graph edges · Inner cluster reachability gives full-graph reachability of images · Wiring induced on the inner graph · Induced-wiring adjacency: distinct and joined in the outside graph · Full-graph reachability of images gives inner cluster reachability · Outside reachability gives inner cluster reachability · Outside-only property of an outside cluster · Cluster of a vertex is outside-only iff the vertex is · Lattice induced wirings are coarser than the inner boundary clique · Glued cluster count is induced-wiring count plus outside-only clusters · Outside-graph adjacency: open non-inner edge or boundary pair · Outside graph is a subgraph of the full cluster graph · Full-graph reachability from an outside-only vertex stays outside · Outside-only vertex · Outside-only clusters · Outside-only property is constant on outside clusters · Outside-only vertices are not inner · Full cluster graph as the union of inner image and outside graphs

LemmaOutside-graph adjacency: open non-inner edge or boundary pair#✓fully proved

Adjacency in the outside graph.

lemma ocd_outsideGraph_adj (ψ : ConfigSpace (Sym2 Vout)) (x y : Vout) :
    (ocd_outsideGraph Gout ιV bdryOut ψ).Adj x y
      ↔ (Gout.Adj x y ∧ ψ s(x, y) = true ∧ s(x, y) ∉ Set.range (ocd_innerEdge ιV))
        ∨ (x ≠ y ∧ bdryOut x ∧ bdryOut y)

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Image of an inner-graph edge in the outer graph · Outside graph with the wired boundary clique

Proof usesGraph of open non-inner edges · Complete graph on the boundary vertices · Boundary wiring relation

Used byInner vertex with an outside-graph edge lies on the inner boundary

DefinitionWiring induced on the inner graph#✓fully proved

The wiring induced on G_in by ψ: distinct inner vertices are adjacent when their images are joined in the outside graph.

noncomputable def ocd_inducedWiring (ψ : ConfigSpace (Sym2 Vout)) : SimpleGraph Vin where
  Adj x y := x ≠ y ∧ (ocd_outsideGraph Gout ιV bdryOut ψ).Reachable (ιV x) (ιV y)
  symm := by
    refine ⟨?_⟩
    rintro x y ⟨hne, hreach⟩
    exact ⟨hne.symm, hreach.symm⟩
  loopless := ⟨by rintro x ⟨hne, _⟩; exact hne rfl⟩

Uses 2 · Used by 21

Statement usesConfiguration space of a statistical-mechanics model · Outside graph with the wired boundary clique

Used byFactorization of the wired FK weight of a glued configuration · Conditional outer wired probability at most the inner wired one, \(q \ge 1\) · Domination by the inner wired measure under a coarser induced wiring · Conditional outer measure is the induced-wiring FK measure · Conditional outer probability as an induced-wiring probability · Free inner measure is dominated by the conditional outer measure · Free inner measure is dominated by every induced-wiring measure · Inner cluster reachability gives full-graph reachability of images · Factorization of the conditioned outer partition function · Induced-wiring adjacency: distinct and joined in the outside graph · Inner cluster graph with the induced wiring · Full-graph reachability of images gives inner cluster reachability · Outside reachability gives inner cluster reachability · Lattice induced wirings are coarser than the inner boundary clique · Inner wired domination for vertex sets of \(\mathbb{Z}^d\) · Glued cluster count is induced-wiring count plus outside-only clusters · Inner wired domination of the restricted outer wired measure · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure

LemmaInduced-wiring adjacency: distinct and joined in the outside graph#✓fully proved

Adjacency in the induced wiring.

lemma ocd_inducedWiring_adj (ψ : ConfigSpace (Sym2 Vout)) (x y : Vin) :
    (ocd_inducedWiring Gout ιV bdryOut ψ).Adj x y
      ↔ x ≠ y ∧ (ocd_outsideGraph Gout ιV bdryOut ψ).Reachable (ιV x) (ιV y)

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · Wiring induced on the inner graph · Outside graph with the wired boundary clique

DefinitionImage of the inner open subgraph in the outer graph#✓fully proved

The image in G_out of the open subgraph of an inner configuration ω.

noncomputable def ocd_innerImageGraph (ω : ConfigSpace (Sym2 Vin)) : SimpleGraph Vout where
  Adj x y := Gout.Adj x y ∧ ocd_psiExt ιV (fun _ => false) ω s(x, y) = true
    ∧ s(x, y) ∈ Set.range (ocd_innerEdge ιV)
  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 3 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Image of an inner-graph edge in the outer graph · Gluing of inner and outer configurations

Used byFull-graph edges at non-inner vertices are outside-graph edges · Inner cluster reachability gives full-graph reachability of images · Full-graph reachability of images gives inner cluster reachability · Endpoints of inner image edges are inner vertices · Inner image graph on embedded vertices is the open subgraph · Full cluster graph as the union of inner image and outside graphs

DefinitionInner cluster graph with the induced wiring#✓fully proved

The inner cluster graph: open edges of ω together with the induced wiring.

noncomputable def ocd_innerGraph (ω : ConfigSpace (Sym2 Vin)) (ψ : ConfigSpace (Sym2 Vout)) :
    SimpleGraph Vin :=
  openSub Gin ω ⊔ ocd_inducedWiring Gout ιV bdryOut ψ

Uses 3 · Used by 11

Statement usesConfiguration space of a statistical-mechanics model · Wiring induced on the inner graph · Open subgraph of an edge configuration

Used byCluster bijection for a glued configuration · Cluster map into the clusters of a glued configuration · Injectivity of the cluster map · Cluster map sends the inner cluster of \(x\) to that of \(\iota x\) · Cluster map sends an outside-only cluster of \(v\) to that of \(v\) · Surjectivity of the cluster map · Inner cluster reachability gives full-graph reachability of images · Full-graph and inner cluster reachability agree on embedded vertices · Full-graph reachability of images gives inner cluster reachability · Outside reachability gives inner cluster reachability · Glued cluster count is induced-wiring count plus outside-only clusters

DefinitionCluster graph of a glued configuration#✓fully proved

The cluster graph of the glued configuration on G_out with the wired boundary clique.

noncomputable def ocd_fullGraph (ω : ConfigSpace (Sym2 Vin)) (ψ : ConfigSpace (Sym2 Vout)) :
    SimpleGraph Vout :=
  openSub Gout (ocd_psiExt ιV ψ ω) ⊔ StatMech.Lattice.boundaryCliqueGraph bdryOut

Uses 4 · Used by 14

Statement usesConfiguration space of a statistical-mechanics model · Gluing of inner and outer configurations · Open subgraph of an edge configuration · Complete graph on the boundary vertices

Used byCluster bijection for a glued configuration · Cluster map into the clusters of a glued configuration · Injectivity of the cluster map · Cluster map sends the inner cluster of \(x\) to that of \(\iota x\) · Cluster map sends an outside-only cluster of \(v\) to that of \(v\) · Surjectivity of the cluster map · Full-graph edges at non-inner vertices are outside-graph edges · Inner cluster reachability gives full-graph reachability of images · Full-graph and inner cluster reachability agree on embedded vertices · Full-graph reachability of images gives inner cluster reachability · Glued cluster count is induced-wiring count plus outside-only clusters · Outside graph is a subgraph of the full cluster graph · Full-graph reachability from an outside-only vertex stays outside · Full cluster graph as the union of inner image and outside graphs

B.2. Reachability

LemmaOutside graph is a subgraph of the full cluster graph#✓fully proved

The outside graph is a subgraph of the full cluster graph.

lemma ocd_outsideGraph_le_fullGraph (ω : ConfigSpace (Sym2 Vin)) (ψ : ConfigSpace (Sym2 Vout)) :
    ocd_outsideGraph Gout ιV bdryOut ψ ≤ ocd_fullGraph Gout ιV bdryOut ω ψ

Uses 9 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Cluster graph of a glued configuration · Outside graph with the wired boundary clique

Proof usesImage of an inner-graph edge in the outer graph · Graph of open non-inner edges · Gluing of inner and outer configurations · Glued configuration equals the outer one at each non-inner edge · Open subgraph of an edge configuration · Complete graph on the boundary vertices

Used byCluster map into the clusters of a glued configuration · Surjectivity of the cluster map

LemmaGlued configuration on inner edges ignores the outer configuration#✓fully proved

On inner edges the glued configuration does not depend on the outer configuration.

lemma ocd_psiExt_eq_false_of_range (hι : Function.Injective ιV) (ψ : ConfigSpace (Sym2 Vout))
    (ω : ConfigSpace (Sym2 Vin)) {e : Sym2 Vout} (he : e ∈ Set.range (ocd_innerEdge ιV)) :
    ocd_psiExt ιV ψ ω e = ocd_psiExt ιV (fun _ => false) ω e

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Image of an inner-graph edge in the outer graph · Gluing of inner and outer configurations

Proof usesGlued configuration takes the inner value on inner edges

Used byFull cluster graph as the union of inner image and outside graphs

LemmaFull cluster graph as the union of inner image and outside graphs#✓fully proved

The full cluster graph is the union of the inner image graph and the outside graph.

lemma ocd_psiWiredGraph_eq_sup (hι : Function.Injective ιV) (ψ : ConfigSpace (Sym2 Vout))
    (ω : ConfigSpace (Sym2 Vin)) :
    ocd_fullGraph Gout ιV bdryOut ω ψ
      = ocd_innerImageGraph Gout ιV ω ⊔ ocd_outsideGraph Gout ιV bdryOut ψ

Uses 11 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Cluster graph of a glued configuration · Image of the inner open subgraph in the outer graph · Outside graph with the wired boundary clique

Proof usesImage of an inner-graph edge in the outer graph · Graph of open non-inner edges · Gluing of inner and outer configurations · Glued configuration on inner edges ignores the outer configuration · Glued configuration equals the outer one at each non-inner edge · Open subgraph of an edge configuration · Complete graph on the boundary vertices

Used byFull-graph edges at non-inner vertices are outside-graph edges · Inner cluster reachability gives full-graph reachability of images · Full-graph reachability of images gives inner cluster reachability

LemmaEndpoints of inner image edges are inner vertices#✓fully proved

Both endpoints of an inner image edge are inner vertices.

lemma ocd_innerImageGraph_adj_inner (hι : Function.Injective ιV) (ω : ConfigSpace (Sym2 Vin))
    {u v : Vout} (h : (ocd_innerImageGraph Gout ιV ω).Adj u v) :
    ocd_IsInnerVert ιV u ∧ ocd_IsInnerVert ιV v

Uses 6 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Inner vertex of the outer graph · Image of the inner open subgraph in the outer graph

Proof usesImage of an inner-graph edge in the outer graph · Edge map sends \(\{x, y\}\) to \(\{\iota x, \iota y\}\) · Gluing of inner and outer configurations

Used byFull-graph edges at non-inner vertices are outside-graph edges · Full-graph reachability of images gives inner cluster reachability

LemmaInner image graph on embedded vertices is the open subgraph#✓fully proved

The inner image graph on images of ι is the open subgraph of ω.

lemma ocd_innerImageGraph_adj_ιV (hι : Function.Injective ιV)
    (hadjm : ocd_AdjMatch Gin Gout ιV) (ω : ConfigSpace (Sym2 Vin)) (x y : Vin) :
    (ocd_innerImageGraph Gout ιV ω).Adj (ιV x) (ιV y) ↔ (openSub Gin ω).Adj x y

Uses 8 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Adjacency matching of the inner embedding · Image of the inner open subgraph in the outer graph · Open subgraph of an edge configuration

Proof usesImage of an inner-graph edge in the outer graph · Edge map sends \(\{x, y\}\) to \(\{\iota x, \iota y\}\) · Gluing of inner and outer configurations · Glued configuration takes the inner value on inner edges

Used byInner cluster reachability gives full-graph reachability of images · Full-graph reachability of images gives inner cluster reachability

LemmaOutside reachability gives inner cluster reachability#✓fully proved

Inner vertices whose images are joined in the outside graph are joined in the inner cluster graph.

lemma ocd_innerGraph_reachable_of_outsideReachable (ω : ConfigSpace (Sym2 Vin))
    (ψ : ConfigSpace (Sym2 Vout)) {x y : Vin}
    (h : (ocd_outsideGraph Gout ιV bdryOut ψ).Reachable (ιV x) (ιV y)) :
    (ocd_innerGraph Gin Gout ιV bdryOut ω ψ).Reachable x y

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Inner cluster graph with the induced wiring · Outside graph with the wired boundary clique

Proof usesWiring induced on the inner graph · Open subgraph of an edge configuration

Used byFull-graph reachability of images gives inner cluster reachability

LemmaInner cluster reachability gives full-graph reachability of images#✓fully proved

Reachability in the inner cluster graph gives reachability of the images in the full cluster graph.

lemma ocd_fullGraph_reachable_of_innerGraph (hι : Function.Injective ιV)
    (hadjm : ocd_AdjMatch Gin Gout ιV) (ω : ConfigSpace (Sym2 Vin))
    (ψ : ConfigSpace (Sym2 Vout)) {x y : Vin}
    (h : (ocd_innerGraph Gin Gout ιV bdryOut ω ψ).Reachable x y) :
    (ocd_fullGraph Gout ιV bdryOut ω ψ).Reachable (ιV x) (ιV y)

Uses 10 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Adjacency matching of the inner embedding · Cluster graph of a glued configuration · Inner cluster graph with the induced wiring

Proof usesWiring induced on the inner graph · Image of the inner open subgraph in the outer graph · Inner image graph on embedded vertices is the open subgraph · Outside graph with the wired boundary clique · Full cluster graph as the union of inner image and outside graphs · Open subgraph of an edge configuration

Used byCluster map into the clusters of a glued configuration · Full-graph and inner cluster reachability agree on embedded vertices

LemmaFull-graph reachability of images gives inner cluster reachability#✓fully proved

Reachability of images in the full cluster graph gives reachability in the inner cluster graph.

lemma ocd_innerGraph_reachable_of_fullGraph (hι : Function.Injective ιV)
    (hadjm : ocd_AdjMatch Gin Gout ιV) (ω : ConfigSpace (Sym2 Vin))
    (ψ : ConfigSpace (Sym2 Vout)) {x y : Vin}
    (h : (ocd_fullGraph Gout ιV bdryOut ω ψ).Reachable (ιV x) (ιV y)) :
    (ocd_innerGraph Gin Gout ιV bdryOut ω ψ).Reachable x y

Uses 13 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Adjacency matching of the inner embedding · Cluster graph of a glued configuration · Inner cluster graph with the induced wiring

Proof usesInner vertex of the outer graph · Wiring induced on the inner graph · Outside reachability gives inner cluster reachability · Image of the inner open subgraph in the outer graph · Endpoints of inner image edges are inner vertices · Inner image graph on embedded vertices is the open subgraph · Outside graph with the wired boundary clique · Full cluster graph as the union of inner image and outside graphs · Open subgraph of an edge configuration

Used byInjectivity of the cluster map · Full-graph and inner cluster reachability agree on embedded vertices

LemmaFull-graph and inner cluster reachability agree on embedded vertices#✓fully proved

Images of inner vertices are joined in the full cluster graph iff the vertices are joined in the inner cluster graph.

lemma ocd_fullGraph_reachable_ιV (hι : Function.Injective ιV)
    (hadjm : ocd_AdjMatch Gin Gout ιV) (ω : ConfigSpace (Sym2 Vin))
    (ψ : ConfigSpace (Sym2 Vout)) (x y : Vin) :
    (ocd_fullGraph Gout ιV bdryOut ω ψ).Reachable (ιV x) (ιV y)
      ↔ (ocd_innerGraph Gin Gout ιV bdryOut ω ψ).Reachable x y

Uses 6

Statement usesConfiguration space of a statistical-mechanics model · Adjacency matching of the inner embedding · Cluster graph of a glued configuration · Inner cluster graph with the induced wiring

Proof usesInner cluster reachability gives full-graph reachability of images · Full-graph reachability of images gives inner cluster reachability

LemmaFull-graph edges at non-inner vertices are outside-graph edges#✓fully proved

A full cluster graph edge at a non-inner vertex is an outside graph edge.

lemma ocd_fullGraph_adj_of_outside (hι : Function.Injective ιV) (ω : ConfigSpace (Sym2 Vin))
    (ψ : ConfigSpace (Sym2 Vout)) {u w : Vout}
    (hu : ¬ ocd_IsInnerVert ιV u) (h : (ocd_fullGraph Gout ιV bdryOut ω ψ).Adj u w) :
    (ocd_outsideGraph Gout ιV bdryOut ψ).Adj u w

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Inner vertex of the outer graph · Cluster graph of a glued configuration · Outside graph with the wired boundary clique

Proof usesImage of the inner open subgraph in the outer graph · Endpoints of inner image edges are inner vertices · Full cluster graph as the union of inner image and outside graphs

Used byFull-graph reachability from an outside-only vertex stays outside

B.3. Clusters of a glued configuration

DefinitionOutside-only vertex#✓fully proved

A vertex is outside-only if its outside cluster contains no inner vertex.

def ocd_OutsideOnly (ψ : ConfigSpace (Sym2 Vout)) (u : Vout) : Prop :=
  ∀ v, (ocd_outsideGraph Gout ιV bdryOut ψ).Reachable u v → ¬ ocd_IsInnerVert ιV v

Uses 3 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Inner vertex of the outer graph · Outside graph with the wired boundary clique

Used byInjectivity of the cluster map · Surjectivity of the cluster map · Outside-only property of an outside cluster · Cluster of a vertex is outside-only iff the vertex is · Full-graph reachability from an outside-only vertex stays outside · Outside-only property is constant on outside clusters · Outside-only vertices are not inner

LemmaOutside-only vertices are not inner#✓fully proved

An outside-only vertex is not inner.

lemma ocd_outsideOnly_self_not_inner (ψ : ConfigSpace (Sym2 Vout)) {u : Vout}
    (hu : ocd_OutsideOnly Gout ιV bdryOut ψ u) : ¬ ocd_IsInnerVert ιV u

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Inner vertex of the outer graph · Outside-only vertex

Proof usesOutside graph with the wired boundary clique

LemmaOutside-only property is constant on outside clusters#✓fully proved

Being outside-only is constant on outside clusters.

lemma ocd_outsideOnly_of_reachable (ψ : ConfigSpace (Sym2 Vout)) {u v : Vout}
    (hu : ocd_OutsideOnly Gout ιV bdryOut ψ u)
    (h : (ocd_outsideGraph Gout ιV bdryOut ψ).Reachable u v) :
    ocd_OutsideOnly Gout ιV bdryOut ψ v

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Outside-only vertex · Outside graph with the wired boundary clique

Used byOutside-only property of an outside cluster

LemmaFull-graph reachability from an outside-only vertex stays outside#✓fully proved

From an outside-only vertex, reachability in the full cluster graph stays in the outside graph.

lemma ocd_outsideGraph_reachable_of_fullGraph_outsideOnly (hι : Function.Injective ιV)
    (ω : ConfigSpace (Sym2 Vin)) (ψ : ConfigSpace (Sym2 Vout)) {u w : Vout}
    (hu : ocd_OutsideOnly Gout ιV bdryOut ψ u)
    (h : (ocd_fullGraph Gout ιV bdryOut ω ψ).Reachable u w) :
    (ocd_outsideGraph Gout ιV bdryOut ψ).Reachable u w

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Outside-only vertex · Cluster graph of a glued configuration · Outside graph with the wired boundary clique

Proof usesInner vertex of the outer graph · Full-graph edges at non-inner vertices are outside-graph edges

Used byInjectivity of the cluster map

DefinitionOutside-only property of an outside cluster#✓fully proved

The outside-only property of a cluster of the outside graph.

noncomputable def ocd_IsOutsideOnly (ψ : ConfigSpace (Sym2 Vout)) :
    (ocd_outsideGraph Gout ιV bdryOut ψ).ConnectedComponent → Prop :=
  ConnectedComponent.lift (ocd_OutsideOnly Gout ιV bdryOut ψ)
    (fun _ _ p _ => propext ⟨fun h => ocd_outsideOnly_of_reachable ψ h p.reachable,
      fun h => ocd_outsideOnly_of_reachable ψ h p.reachable.symm⟩)

Uses 4 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Outside-only vertex · Outside graph with the wired boundary clique · Outside-only property is constant on outside clusters

Used byCluster map into the clusters of a glued configuration · Injectivity of the cluster map · Cluster map sends an outside-only cluster of \(v\) to that of \(v\) · Surjectivity of the cluster map · Cluster of a vertex is outside-only iff the vertex is · Glued cluster count is induced-wiring count plus outside-only clusters · Outside-only clusters

LemmaCluster of a vertex is outside-only iff the vertex is#✓fully proved

The cluster of v is outside-only iff v is.

@[simp] lemma ocd_isOutsideOnly_mk (ψ : ConfigSpace (Sym2 Vout)) (v : Vout) :
    ocd_IsOutsideOnly Gout ιV bdryOut ψ
        ((ocd_outsideGraph Gout ιV bdryOut ψ).connectedComponentMk v)
      ↔ ocd_OutsideOnly Gout ιV bdryOut ψ v

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Outside-only property of an outside cluster · Outside-only vertex · Outside graph with the wired boundary clique

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

DefinitionOutside-only clusters#✓fully proved

The outside clusters that contain no inner vertex.

def ocd_OutsideOnlyComp (ψ : ConfigSpace (Sym2 Vout)) : Type _ :=
  {c : (ocd_outsideGraph Gout ιV bdryOut ψ).ConnectedComponent //
    ocd_IsOutsideOnly Gout ιV bdryOut ψ c}

Uses 3 · Used by 8

Statement usesConfiguration space of a statistical-mechanics model · Outside-only property of an outside cluster · Outside graph with the wired boundary clique

Used byCluster bijection for a glued configuration · Cluster map into the clusters of a glued configuration · Injectivity of the cluster map · Cluster map sends the inner cluster of \(x\) to that of \(\iota x\) · Cluster map sends an outside-only cluster of \(v\) to that of \(v\) · Surjectivity of the cluster map · Glued cluster count is induced-wiring count plus outside-only clusters · Number of outside-only clusters

DefinitionCluster map into the clusters of a glued configuration#✓fully proved

The map from inner clusters and outside-only clusters to the clusters of the glued configuration.

noncomputable def ocd_fullComponentMap (hι : Function.Injective ιV)
    (hadjm : ocd_AdjMatch Gin Gout ιV) (ω : ConfigSpace (Sym2 Vin)) (ψ : ConfigSpace (Sym2 Vout)) :
    (ocd_innerGraph Gin Gout ιV bdryOut ω ψ).ConnectedComponent ⊕
        ocd_OutsideOnlyComp Gout ιV bdryOut ψ →
      (ocd_fullGraph Gout ιV bdryOut ω ψ).ConnectedComponent
  | Sum.inl c => c.lift (fun x => (ocd_fullGraph Gout ιV bdryOut ω ψ).connectedComponentMk (ιV x))
      (fun _ _ p _ => ConnectedComponent.sound
        (ocd_fullGraph_reachable_of_innerGraph hι hadjm ω ψ p.reachable))
  | Sum.inr c => c.1.lift (fun v => (ocd_fullGraph Gout ιV bdryOut ω ψ).connectedComponentMk v)
      (fun _ _ p _ => ConnectedComponent.sound
        (p.reachable.mono (ocd_outsideGraph_le_fullGraph ω ψ)))

Uses 9 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Adjacency matching of the inner embedding · Outside-only property of an outside cluster · Outside-only clusters · Cluster graph of a glued configuration · Inner cluster reachability gives full-graph reachability of images · Inner cluster graph with the induced wiring · Outside graph with the wired boundary clique · Outside graph is a subgraph of the full cluster graph

Used byCluster bijection for a glued configuration · Injectivity of the cluster map · Cluster map sends the inner cluster of \(x\) to that of \(\iota x\) · Cluster map sends an outside-only cluster of \(v\) to that of \(v\) · Surjectivity of the cluster map

LemmaCluster map sends the inner cluster of \(x\) to that of \(\iota x\)#✓fully proved

The cluster map sends the inner cluster of x to the full cluster of ι x.

lemma ocd_fullComponentMap_inl_mk (hι : Function.Injective ιV) (hadjm : ocd_AdjMatch Gin Gout ιV)
    (ω : ConfigSpace (Sym2 Vin)) (ψ : ConfigSpace (Sym2 Vout)) (x : Vin) :
    ocd_fullComponentMap Gin Gout ιV bdryOut hι hadjm ω ψ
        (Sum.inl ((ocd_innerGraph Gin Gout ιV bdryOut ω ψ).connectedComponentMk x))
      = (ocd_fullGraph Gout ιV bdryOut ω ψ).connectedComponentMk (ιV x)

Uses 6 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Adjacency matching of the inner embedding · Outside-only clusters · Cluster map into the clusters of a glued configuration · Cluster graph of a glued configuration · Inner cluster graph with the induced wiring

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

LemmaCluster map sends an outside-only cluster of \(v\) to that of \(v\)#✓fully proved

The cluster map sends an outside-only cluster of v to the full cluster of v.

lemma ocd_fullComponentMap_inr_mk (hι : Function.Injective ιV) (hadjm : ocd_AdjMatch Gin Gout ιV)
    (ω : ConfigSpace (Sym2 Vin)) (ψ : ConfigSpace (Sym2 Vout)) (v : Vout)
    (hv : ocd_IsOutsideOnly Gout ιV bdryOut ψ
        ((ocd_outsideGraph Gout ιV bdryOut ψ).connectedComponentMk v)) :
    ocd_fullComponentMap Gin Gout ιV bdryOut hι hadjm ω ψ
        (Sum.inr ⟨(ocd_outsideGraph Gout ιV bdryOut ψ).connectedComponentMk v, hv⟩)
      = (ocd_fullGraph Gout ιV bdryOut ω ψ).connectedComponentMk v

Uses 8 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Adjacency matching of the inner embedding · Outside-only property of an outside cluster · Outside-only clusters · Cluster map into the clusters of a glued configuration · Cluster graph of a glued configuration · Inner cluster graph with the induced wiring · Outside graph with the wired boundary clique

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

LemmaInjectivity of the cluster map#✓fully proved

The cluster map is injective.

lemma ocd_fullComponentMap_injective (hι : Function.Injective ιV)
    (hadjm : ocd_AdjMatch Gin Gout ιV) (ω : ConfigSpace (Sym2 Vin)) (ψ : ConfigSpace (Sym2 Vout)) :
    Function.Injective (ocd_fullComponentMap Gin Gout ιV bdryOut hι hadjm ω ψ)

Uses 15 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Adjacency matching of the inner embedding · Outside-only clusters · Cluster map into the clusters of a glued configuration · Cluster graph of a glued configuration · Inner cluster graph with the induced wiring

Proof usesInner vertex of the outer graph · Outside-only property of an outside cluster · Outside-only vertex · Cluster map sends the inner cluster of \(x\) to that of \(\iota x\) · Cluster map sends an outside-only cluster of \(v\) to that of \(v\) · Full-graph reachability of images gives inner cluster reachability · Cluster of a vertex is outside-only iff the vertex is · Outside graph with the wired boundary clique · Full-graph reachability from an outside-only vertex stays outside

Used byCluster bijection for a glued configuration

LemmaSurjectivity of the cluster map#✓fully proved

The cluster map is surjective.

lemma ocd_fullComponentMap_surjective (hι : Function.Injective ιV)
    (hadjm : ocd_AdjMatch Gin Gout ιV) (ω : ConfigSpace (Sym2 Vin)) (ψ : ConfigSpace (Sym2 Vout)) :
    Function.Surjective (ocd_fullComponentMap Gin Gout ιV bdryOut hι hadjm ω ψ)

Uses 14 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Adjacency matching of the inner embedding · Outside-only clusters · Cluster map into the clusters of a glued configuration · Cluster graph of a glued configuration · Inner cluster graph with the induced wiring

Proof usesInner vertex of the outer graph · Outside-only property of an outside cluster · Outside-only vertex · Cluster map sends the inner cluster of \(x\) to that of \(\iota x\) · Cluster map sends an outside-only cluster of \(v\) to that of \(v\) · Cluster of a vertex is outside-only iff the vertex is · Outside graph with the wired boundary clique · Outside graph is a subgraph of the full cluster graph

Used byCluster bijection for a glued configuration

DefinitionCluster bijection for a glued configuration#✓fully proved

The clusters of the glued configuration are in bijection with the inner clusters plus the outside-only clusters.

noncomputable def ocd_fullComponentEquiv (hι : Function.Injective ιV)
    (hadjm : ocd_AdjMatch Gin Gout ιV) (ω : ConfigSpace (Sym2 Vin)) (ψ : ConfigSpace (Sym2 Vout)) :
    (ocd_innerGraph Gin Gout ιV bdryOut ω ψ).ConnectedComponent ⊕
        ocd_OutsideOnlyComp Gout ιV bdryOut ψ ≃
      (ocd_fullGraph Gout ιV bdryOut ω ψ).ConnectedComponent :=
  Equiv.ofBijective (ocd_fullComponentMap Gin Gout ιV bdryOut hι hadjm ω ψ)
    ⟨ocd_fullComponentMap_injective hι hadjm ω ψ, ocd_fullComponentMap_surjective hι hadjm ω ψ⟩

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Adjacency matching of the inner embedding · Outside-only clusters · Cluster map into the clusters of a glued configuration · Injectivity of the cluster map · Surjectivity of the cluster map · Cluster graph of a glued configuration · Inner cluster graph with the induced wiring

Used byGlued cluster count is induced-wiring count plus outside-only clusters

DefinitionNumber of outside-only clusters#✓fully proved

The number of outside-only clusters of ψ.

noncomputable def ocd_outsideShift (Gout : SimpleGraph Vout) [DecidableRel Gout.Adj]
    (ιV : Vin → Vout) (bdryOut : Vout → Prop) [DecidablePred bdryOut]
    (ψ : ConfigSpace (Sym2 Vout)) : ℕ :=
  Nat.card (ocd_OutsideOnlyComp Gout ιV bdryOut ψ)

Uses 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Outside-only clusters

Used byFactorization of the wired FK weight of a glued configuration · Glued cluster count is induced-wiring count plus outside-only clusters · Outer factor of the FK weight of a glued configuration · Positivity of the outer factor

LemmaGlued cluster count is induced-wiring count plus outside-only clusters#✓fully proved

The wired cluster count of a glued configuration is the induced-wiring cluster count of the inner configuration plus the number of outside-only clusters.

lemma ocd_numClustersBC_psiExt (hι : Function.Injective ιV) (hadjm : ocd_AdjMatch Gin Gout ιV)
    (ω : ConfigSpace (Sym2 Vin)) (ψ : ConfigSpace (Sym2 Vout)) :
    numClustersBC Gout (StatMech.Lattice.boundaryCliqueGraph bdryOut) (ocd_psiExt ιV ψ ω)
      = numClustersBC Gin (ocd_inducedWiring Gout ιV bdryOut ψ) ω
          + ocd_outsideShift Gout ιV bdryOut ψ

Uses 15 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Number of clusters under a boundary wiring · Adjacency matching of the inner embedding · Wiring induced on the inner graph · Number of outside-only clusters · Gluing of inner and outer configurations · Complete graph on the boundary vertices · Boundary wiring relation

Proof usesOutside-only property of an outside cluster · Outside-only clusters · Cluster bijection for a glued configuration · Cluster graph of a glued configuration · Inner cluster graph with the induced wiring · Outside graph with the wired boundary clique · Open subgraph of an edge configuration

Used byFactorization of the wired FK weight of a glued configuration

C. Weights of glued configurations

LemmaEdges of the inner graph map onto the inner edges of the outer graph#✓fully proved

The image of the edges of G_in is the set of inner edges of G_out.

lemma ocd_innerEdge_image_edgeFinset (hι : Function.Injective ιV)
    (hadjm : ocd_AdjMatch Gin Gout ιV) :
    Gin.edgeFinset.image (ocd_innerEdge ιV)
      = Gout.edgeFinset.filter (· ∈ Set.range (ocd_innerEdge ιV))

Uses 3 · Used by 1

Statement usesAdjacency matching of the inner embedding · Image of an inner-graph edge in the outer graph

Proof usesEdge map sends \(\{x, y\}\) to \(\{\iota x, \iota y\}\)

Used byFactorization of the edge weight of a glued configuration

DefinitionOuter Bernoulli edge weight of a configuration#✓fully proved

The Bernoulli edge weight of ψ on the non-inner edges of G_out.

noncomputable def ocd_psiEdgeFactor (Gout : SimpleGraph Vout) [DecidableRel Gout.Adj]
    (ιV : Vin → Vout) (ψ : ConfigSpace (Sym2 Vout)) (p : ℝ) : ℝ :=
  ∏ e ∈ Gout.edgeFinset.filter (fun e => e ∉ Set.range (ocd_innerEdge ιV)),
    (if ψ e then p else 1 - p)

Uses 2 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Image of an inner-graph edge in the outer graph

Used byFactorization of the wired FK weight of a glued configuration · Factorization of the edge weight of a glued configuration · Positivity of the outer edge weight · Outer factor of the FK weight of a glued configuration · Positivity of the outer factor

LemmaPositivity of the outer edge weight#✓fully proved

The outer edge weight is positive for p ∈ (0, 1).

lemma ocd_psiEdgeFactor_pos {ψ : ConfigSpace (Sym2 Vout)} {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    0 < ocd_psiEdgeFactor Gout ιV ψ p

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Outer Bernoulli edge weight of a configuration

Proof usesImage of an inner-graph edge in the outer graph

Used byPositivity of the outer factor

LemmaFactorization of the edge weight of a glued configuration#✓fully proved

The edge weight of a glued configuration factors into the inner edge weight and the outer edge weight.

lemma ocd_edgeProduct_psiExt (hι : Function.Injective ιV) (hadjm : ocd_AdjMatch Gin Gout ιV)
    {p : ℝ} (ψ : ConfigSpace (Sym2 Vout)) (ω : ConfigSpace (Sym2 Vin)) :
    edgeProduct Gout p (ocd_psiExt ιV ψ ω)
      = edgeProduct Gin p ω * ocd_psiEdgeFactor Gout ιV ψ p

Uses 10 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Adjacency matching of the inner embedding · Outer Bernoulli edge weight of a configuration · Gluing of inner and outer configurations

Proof usesImage of an inner-graph edge in the outer graph · Edges of the inner graph map onto the inner edges of the outer graph · Injectivity of the edge map · Glued configuration equals the outer one at each non-inner edge · Glued configuration takes the inner value on inner edges

Used byFactorization of the wired FK weight of a glued configuration

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

The factor ψ contributes to the FK weight of a glued configuration: its outer edge weight times q to the number of outside-only clusters.

noncomputable def ocd_psiShift (Gout : SimpleGraph Vout) [DecidableRel Gout.Adj]
    (ιV : Vin → Vout) (bdryOut : Vout → Prop) [DecidablePred bdryOut]
    (ψ : ConfigSpace (Sym2 Vout)) (p q : ℝ) : ℝ :=
  ocd_psiEdgeFactor Gout ιV ψ p * q ^ ocd_outsideShift Gout ιV bdryOut ψ

Uses 3 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Number of outside-only clusters · Outer Bernoulli edge weight of a configuration

Used byFactorization of the wired FK weight of a glued configuration · Conditional outer measure is the induced-wiring FK measure · Factorization of the conditioned outer partition function · Positivity of the outer factor

LemmaPositivity of the outer factor#✓fully proved

The outer factor is positive for p ∈ (0, 1) and q > 0.

lemma ocd_psiShift_pos {ψ : ConfigSpace (Sym2 Vout)} {q : ℝ} {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hq : 0 < q) :
    0 < ocd_psiShift Gout ιV bdryOut ψ p q

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Outer factor of the FK weight of a glued configuration

Proof usesNumber of outside-only clusters · Outer Bernoulli edge weight of a configuration · Positivity of the outer edge weight

Used byConditional outer measure is the induced-wiring FK measure

LemmaFactorization of the wired FK weight of a glued configuration#✓fully proved

The wired FK weight of a glued configuration is the induced-wiring FK weight of the inner configuration times the outer factor.

lemma ocd_bcWeight_psiExt (hι : Function.Injective ιV) (hadjm : ocd_AdjMatch Gin Gout ιV)
    {p q : ℝ} (ψ : ConfigSpace (Sym2 Vout)) (ω : ConfigSpace (Sym2 Vin)) :
    bcWeight Gout (StatMech.Lattice.boundaryCliqueGraph bdryOut) p q (ocd_psiExt ιV ψ ω)
      = bcWeight Gin (ocd_inducedWiring Gout ιV bdryOut ψ) p q ω
          * ocd_psiShift Gout ιV bdryOut ψ p q

Uses 14 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster weight with a boundary wiring · Adjacency matching of the inner embedding · Wiring induced on the inner graph · Gluing of inner and outer configurations · Outer factor of the FK weight of a glued configuration · Complete graph on the boundary vertices · Boundary wiring relation

Proof usesBernoulli edge product · Number of clusters under a boundary wiring · Factorization of the edge weight of a glued configuration · Glued cluster count is induced-wiring count plus outside-only clusters · Number of outside-only clusters · Outer Bernoulli edge weight of a configuration

Used byConditional outer measure is the induced-wiring FK measure · Factorization of the conditioned outer partition function

D. The conditional measure on the inner graph

LemmaFactorization of the conditioned outer partition function#✓fully proved

The partition function of the outer measure conditioned on ψ is the induced-wiring partition function times the outer factor.

lemma ocd_inducedBcZ_psi (hι : Function.Injective ιV) (hadjm : ocd_AdjMatch Gin Gout ιV)
    {p q : ℝ} (ψ : ConfigSpace (Sym2 Vout)) :
    inducedBcZ Gout (StatMech.Lattice.boundaryCliqueGraph bdryOut) p q
        (ocd_innerEdgeFinset (Vin := Vin) ιV) ψ
      = bcZ Gin (ocd_inducedWiring Gout ιV bdryOut ψ) p q
          * ocd_psiShift Gout ιV bdryOut ψ p q

Uses 16 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Partition function with a boundary wiring · Partition function of a conditioning fibre · Adjacency matching of the inner embedding · Wiring induced on the inner graph · Finite set of inner edges · Outer factor of the FK weight of a glued configuration · Complete graph on the boundary vertices · Boundary wiring relation

Proof usesRandom-cluster weight with a boundary wiring · Fibre of configurations agreeing off an edge set · Factorization of the wired FK weight of a glued configuration · Conditioning fibre is the set of gluings · Restriction of an outer configuration to inner edges · Restricting a glued configuration recovers the inner one · Gluing of inner and outer configurations

Used byConditional outer measure is the induced-wiring FK measure

LemmaConditional outer measure is the induced-wiring FK measure#✓fully proved

Conditioned on ψ off the inner edges, the outer wired measure of a glued configuration is the induced-wiring FK measure of the inner configuration.

lemma ocd_condBcProb_psiExt_eq_bcProb (hι : Function.Injective ιV)
    (hadjm : ocd_AdjMatch Gin Gout ιV)
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (ψ : ConfigSpace (Sym2 Vout)) (ω : ConfigSpace (Sym2 Vin)) :
    condBcProb Gout (StatMech.Lattice.boundaryCliqueGraph bdryOut) p q
        (ocd_innerEdgeFinset (Vin := Vin) ιV) ψ (ocd_psiExt ιV ψ ω)
      = bcProb Gin (ocd_inducedWiring Gout ιV bdryOut ψ) p q ω

Uses 18 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Conditional random-cluster measure with a boundary wiring · Adjacency matching of the inner embedding · Wiring induced on the inner graph · Finite set of inner edges · Gluing of inner and outer configurations · Complete graph on the boundary vertices · Boundary wiring relation

Proof usesAgreement of configurations off an edge set · Random-cluster weight with a boundary wiring · Partition function with a boundary wiring · Partition function of a conditioning fibre · Glued configuration agrees with the outer one off the inner edge set · Factorization of the wired FK weight of a glued configuration · Factorization of the conditioned outer partition function · Outer factor of the FK weight of a glued configuration · Positivity of the outer factor

Used byConditional outer probability as an induced-wiring probability

LemmaConditional outer probability as an induced-wiring probability#✓fully proved

The conditional outer probability of an event is the induced-wiring probability of its pullback under gluing.

lemma ocd_condBcProb_psiExt_sum_eq_inducedBox (hι : Function.Injective ιV)
    (hadjm : ocd_AdjMatch Gin Gout ιV) {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (ψ : ConfigSpace (Sym2 Vout)) (B : Set (ConfigSpace (Sym2 Vout))) :
    (∑ ρ, B.indicator (fun _ => (1:ℝ)) ρ *
        condBcProb Gout (StatMech.Lattice.boundaryCliqueGraph bdryOut) p q
          (ocd_innerEdgeFinset (Vin := Vin) ιV) ψ ρ)
      = ∑ ω : ConfigSpace (Sym2 Vin),
          (ocd_psiExt ιV ψ ⁻¹' B).indicator (fun _ => (1:ℝ)) ω
            * bcProb Gin (ocd_inducedWiring Gout ιV bdryOut ψ) p q ω

Uses 17 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Conditional random-cluster measure with a boundary wiring · Adjacency matching of the inner embedding · Wiring induced on the inner graph · Finite set of inner edges · Gluing of inner and outer configurations · Complete graph on the boundary vertices · Boundary wiring relation

Proof usesAgreement of configurations off an edge set · Random-cluster weight with a boundary wiring · Fibre of configurations agreeing off an edge set · Partition function of a conditioning fibre · Conditional outer measure is the induced-wiring FK measure · Conditioning fibre is the set of gluings · Restriction of an outer configuration to inner edges · Restricting a glued configuration recovers the inner one

Used byConditional outer wired probability at most the inner wired one, \(q \ge 1\) · Free inner measure is dominated by the conditional outer measure · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure

LemmaDomination by the inner wired measure under a coarser induced wiring#✓fully proved

If the induced wiring is coarser than the clique on ∂_in, the induced-wiring measure is dominated by the wired measure on G_in (for q ≥ 1).

lemma ocd_condBcProb_psiExt_dominated (hι : Function.Injective ιV)
    (hadjm : ocd_AdjMatch Gin Gout ιV) (bdryIn : Vin → Prop) [DecidablePred bdryIn]
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (ψ : ConfigSpace (Sym2 Vout))
    (hwire : ocd_inducedWiring Gout ιV bdryOut ψ ≤ StatMech.Lattice.boundaryCliqueGraph bdryIn)
    {A : Set (ConfigSpace (Sym2 Vin))} (hA : IsIncreasing A) :
    (∑ ω, A.indicator (fun _ => (1:ℝ)) ω
        * bcProb Gin (ocd_inducedWiring Gout ιV bdryOut ψ) p q ω)
      ≤ ∑ ω, A.indicator (fun _ => (1:ℝ)) ω
          * wiredFkProb Gin bdryIn p q ω

Uses 10 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Adjacency matching of the inner embedding · Wiring induced on the inner graph · Wired random-cluster probability of a configuration · Increasing event · Complete graph on the boundary vertices

Proof usesBoundary clique gives the wired random-cluster measure · Random-cluster comparison of boundary conditions for \(q \ge 1\) · Boundary wiring relation

Used byConditional outer wired probability at most the inner wired one, \(q \ge 1\)

LemmaFree inner measure is dominated by every induced-wiring measure#✓fully proved

The free FK measure on G_in is dominated by every induced-wiring measure (for q ≥ 1).

lemma ocd_free_le_inducedBcProb (hι : Function.Injective ιV)
    (hadjm : ocd_AdjMatch Gin Gout ιV)
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (ψ : ConfigSpace (Sym2 Vout))
    {A : Set (ConfigSpace (Sym2 Vin))} (hA : IsIncreasing A) :
    (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * fkProb Gin p q ω) ≤
      ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω *
        bcProb Gin (ocd_inducedWiring Gout ιV bdryOut ψ) p q ω

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Probability of an ambient FK configuration · Adjacency matching of the inner embedding · Wiring induced on the inner graph · Increasing event

Proof usesEmpty wiring gives the free random-cluster measure · Random-cluster comparison of boundary conditions for \(q \ge 1\)

Used byFree inner measure is dominated by the conditional outer measure

LemmaFree inner measure is dominated by the conditional outer measure#✓fully proved

The free FK measure on G_in is dominated by the restricted conditional outer measure (for q ≥ 1).

lemma ocd_free_le_condBcProb_innerRestrict
    (hι : Function.Injective ιV)
    (hadjm : ocd_AdjMatch Gin Gout ιV)
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (ψ : ConfigSpace (Sym2 Vout))
    {A : Set (ConfigSpace (Sym2 Vin))} (hA : IsIncreasing A) :
    (∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * fkProb Gin p q ω) ≤
      ∑ ρ, (ocd_innerRestrict ιV ⁻¹' A).indicator
          (fun _ => (1 : ℝ)) ρ *
        condBcProb Gout
          (StatMech.Lattice.boundaryCliqueGraph bdryOut) p q
          (ocd_innerEdgeFinset (Vin := Vin) ιV) ψ ρ

Uses 15

Statement usesConfiguration space of a statistical-mechanics model · Conditional random-cluster measure with a boundary wiring · Probability of an ambient FK configuration · Adjacency matching of the inner embedding · Finite set of inner edges · Restriction of an outer configuration to inner edges · Increasing event · Complete graph on the boundary vertices · Boundary wiring relation

Proof usesRandom-cluster probability with a boundary wiring · Conditional outer probability as an induced-wiring probability · Free inner measure is dominated by every induced-wiring measure · Wiring induced on the inner graph · Restricting a glued configuration recovers the inner one · Gluing of inner and outer configurations

E. Averaging over outside configurations

DefinitionProjection closing every inner edge#✓fully proved

The projection of a configuration on G_out that closes every inner edge.

noncomputable def ocd_outProj (ιV : Vin → Vout) (ρ : ConfigSpace (Sym2 Vout)) :
    ConfigSpace (Sym2 Vout) :=
  ocd_psiExt ιV ρ (fun _ => false)

Uses 2 · Used by 10

Statement usesConfiguration space of a statistical-mechanics model · Gluing of inner and outer configurations

Used byLaw of total probability over outside configurations · Projection fibres are conditioning fibres · Projected configuration is closed on inner edges · Projection keeps non-inner edges · Idempotence of the inner-edge projection · Outer wired fibre masses sum to one · Inner wired domination of the restricted outer wired measure · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure

LemmaProjected configuration is closed on inner edges#✓fully proved

The projection closes inner edges.

lemma ocd_outProj_eq_false_of_range (hι : Function.Injective ιV) (ρ : ConfigSpace (Sym2 Vout))
    {e : Sym2 Vout} (he : e ∈ Set.range (ocd_innerEdge ιV)) :
    ocd_outProj ιV ρ e = false

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Image of an inner-graph edge in the outer graph · Projection closing every inner edge

Proof usesGluing of inner and outer configurations · Glued configuration takes the inner value on inner edges

Used byProjection fibres are conditioning fibres · Idempotence of the inner-edge projection

LemmaProjection keeps non-inner edges#✓fully proved

The projection keeps non-inner edges.

lemma ocd_outProj_eq_of_not_range (ρ : ConfigSpace (Sym2 Vout))
    {e : Sym2 Vout} (he : e ∉ Set.range (ocd_innerEdge ιV)) :
    ocd_outProj ιV ρ e = ρ e

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Image of an inner-graph edge in the outer graph · Projection closing every inner edge

Proof usesGluing of inner and outer configurations · Glued configuration equals the outer one at each non-inner edge

Used byProjection fibres are conditioning fibres · Idempotence of the inner-edge projection

LemmaIdempotence of the inner-edge projection#✓fully proved

The projection is idempotent.

lemma ocd_outProj_idem (hι : Function.Injective ιV) (ρ : ConfigSpace (Sym2 Vout)) :
    ocd_outProj ιV (ocd_outProj ιV ρ) = ocd_outProj ιV ρ

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Projection closing every inner edge

Proof usesImage of an inner-graph edge in the outer graph · Projected configuration is closed on inner edges · Projection keeps non-inner edges

Used byLaw of total probability over outside configurations · Outer wired fibre masses sum to one

LemmaProjection fibres are conditioning fibres#✓fully proved

The fibre of the projection over a projected configuration is its conditioning fibre.

lemma ocd_filter_outProj_eq_condFibre (hι : Function.Injective ιV) (ψ : ConfigSpace (Sym2 Vout))
    (hψ : ocd_outProj ιV ψ = ψ) :
    Finset.univ.filter (fun ρ => ocd_outProj ιV ρ = ψ)
      = condFibre (ocd_innerEdgeFinset (Vin := Vin) ιV) ψ

Uses 9 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Fibre of configurations agreeing off an edge set · Finite set of inner edges · Projection closing every inner edge

Proof usesAgreement of configurations off an edge set · Image of an inner-graph edge in the outer graph · Inner edge set is the range of the edge map · Projected configuration is closed on inner edges · Projection keeps non-inner edges

Used byLaw of total probability over outside configurations · Outer wired fibre masses sum to one

LemmaOuter wired fibre masses sum to one#✓fully proved

The outer wired masses of the fibres over projected configurations sum to one.

lemma ocd_sum_fibreMass_eq_one (hι : Function.Injective ιV) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    ∑ ψ ∈ Finset.univ.filter (fun ψ => ocd_outProj ιV ψ = ψ),
        (∑ σ ∈ condFibre (ocd_innerEdgeFinset (Vin := Vin) ιV) ψ,
          bcProb Gout (StatMech.Lattice.boundaryCliqueGraph bdryOut) p q σ) = 1

Uses 13 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Fibre of configurations agreeing off an edge set · Finite set of inner edges · Projection closing every inner edge · Complete graph on the boundary vertices · Boundary wiring relation

Proof usesRandom-cluster weight with a boundary wiring · Partition function with a boundary wiring · Bernoulli edge product · Number of clusters under a boundary wiring · Projection fibres are conditioning fibres · Idempotence of the inner-edge projection

Used byInner wired domination of the restricted outer wired measure · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure

LemmaLaw of total probability over outside configurations#✓fully proved

Law of total probability for the outer wired measure over the configuration off the inner edges. See also bcProb_fibre_decompose in FKDisjointBoxDomainMarkov for a general conditioned edge set.

lemma ocd_bcProb_decompose (hι : Function.Injective ιV) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) (B : Set (ConfigSpace (Sym2 Vout))) :
    (∑ ρ, B.indicator (fun _ => (1:ℝ)) ρ
        * bcProb Gout (StatMech.Lattice.boundaryCliqueGraph bdryOut) p q ρ)
      = ∑ ψ ∈ Finset.univ.filter (fun ψ => ocd_outProj ιV ψ = ψ),
          (∑ σ ∈ condFibre (ocd_innerEdgeFinset (Vin := Vin) ιV) ψ,
            bcProb Gout (StatMech.Lattice.boundaryCliqueGraph bdryOut) p q σ)
          * (∑ ρ, B.indicator (fun _ => (1:ℝ)) ρ
              * condBcProb Gout (StatMech.Lattice.boundaryCliqueGraph bdryOut) p q
                  (ocd_innerEdgeFinset (Vin := Vin) ιV) ψ ρ)

Uses 15 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Conditional random-cluster measure with a boundary wiring · Fibre of configurations agreeing off an edge set · Finite set of inner edges · Projection closing every inner edge · Complete graph on the boundary vertices · Boundary wiring relation

Proof usesAgreement of configurations off an edge set · Disintegration of a boundary-wired measure over conditioning fibres · Random-cluster weight with a boundary wiring · Configurations agreeing off \(F\) have equal conditional probabilities · Partition function of a conditioning fibre · Projection fibres are conditioning fibres · Idempotence of the inner-edge projection

Used byInner wired domination of the restricted outer wired measure · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure

LemmaConditional outer wired probability at most the inner wired one, \(q \ge 1\)#✓fully proved

Conditioned on ψ, the restricted outer wired probability of an increasing event is at most its wired probability on G_in, if the induced wiring is coarser than the clique on ∂_in.

lemma ocd_condBcProb_innerRestrict_le (hι : Function.Injective ιV)
    (hadjm : ocd_AdjMatch Gin Gout ιV) (bdryIn : Vin → Prop) [DecidablePred bdryIn]
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (ψ : ConfigSpace (Sym2 Vout))
    (hwire : ocd_inducedWiring Gout ιV bdryOut ψ ≤ StatMech.Lattice.boundaryCliqueGraph bdryIn)
    {A : Set (ConfigSpace (Sym2 Vin))} (hA : IsIncreasing A) :
    (∑ ρ, (ocd_innerRestrict ιV ⁻¹' A).indicator (fun _ => (1:ℝ)) ρ
        * condBcProb Gout (StatMech.Lattice.boundaryCliqueGraph bdryOut) p q
            (ocd_innerEdgeFinset (Vin := Vin) ιV) ψ ρ)
      ≤ ∑ ω, A.indicator (fun _ => (1:ℝ)) ω * wiredFkProb Gin bdryIn p q ω

Uses 15 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Conditional random-cluster measure with a boundary wiring · Adjacency matching of the inner embedding · Wiring induced on the inner graph · Finite set of inner edges · Restriction of an outer configuration to inner edges · Wired random-cluster probability of a configuration · Increasing event · Complete graph on the boundary vertices · Boundary wiring relation

Proof usesRandom-cluster probability with a boundary wiring · Domination by the inner wired measure under a coarser induced wiring · Conditional outer probability as an induced-wiring probability · Restricting a glued configuration recovers the inner one · Gluing of inner and outer configurations

Used byInner wired domination of the restricted outer wired measure · Ergodicity of the wired random-cluster measure

LemmaInner wired domination of the restricted outer wired measure#✓fully proved

Domination of the restricted outer wired measure by the inner wired measure on increasing events, when every induced wiring is coarser than the clique on ∂_in (for q ≥ 1).

lemma ocd_wired_inner_dominated_bcProb (hι : Function.Injective ιV)
    (hadjm : ocd_AdjMatch Gin Gout ιV) (bdryIn : Vin → Prop) [DecidablePred bdryIn]
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (hwire : ∀ ψ : ConfigSpace (Sym2 Vout),
      ocd_inducedWiring Gout ιV bdryOut ψ ≤ StatMech.Lattice.boundaryCliqueGraph bdryIn)
    {A : Set (ConfigSpace (Sym2 Vin))} (hA : IsIncreasing A) :
    (∑ ρ, (ocd_innerRestrict ιV ⁻¹' A).indicator (fun _ => (1:ℝ)) ρ
        * bcProb Gout (StatMech.Lattice.boundaryCliqueGraph bdryOut) p q ρ)
      ≤ ∑ ω, A.indicator (fun _ => (1:ℝ)) ω * wiredFkProb Gin bdryIn p q ω

Uses 20 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Adjacency matching of the inner embedding · Wiring induced on the inner graph · Restriction of an outer configuration to inner edges · Wired random-cluster probability of a configuration · Increasing event · Complete graph on the boundary vertices · Boundary wiring relation

Proof usesRandom-cluster weight with a boundary wiring · Partition function with a boundary wiring · Conditional random-cluster measure with a boundary wiring · Fibre of configurations agreeing off an edge set · Bernoulli edge product · Number of clusters under a boundary wiring · Law of total probability over outside configurations · Conditional outer wired probability at most the inner wired one, \(q \ge 1\) · Finite set of inner edges · Projection closing every inner edge · Outer wired fibre masses sum to one

Used byInner wired domination for vertex sets of \(\mathbb{Z}^d\)

F. Sub-boxes of the hypercubic lattice

LemmaLattice inclusion matches induced adjacency#✓fully proved

The inclusion of a vertex set of ℤ^d into a larger one matches the induced hypercubic adjacency.

lemma ocd_latticeAdjMatch {Sin Sout : Set (Site d)} [Fintype Sin] [Fintype Sout]
    (ιV : {y : Site d // y ∈ Sin} → {y : Site d // y ∈ Sout})
    (hιval : ∀ x, (ιV x : Site d) = (x : Site d)) :
    ocd_AdjMatch (SimpleGraph.comap Subtype.val (hypercubicLattice d))
      (SimpleGraph.comap Subtype.val (hypercubicLattice d)) ιV

Uses 3 · Used by 5

Statement usesAdjacency matching of the inner embedding · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byInner wired domination for vertex sets of \(\mathbb{Z}^d\) · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure

LemmaInner vertex with an outside-graph edge lies on the inner boundary#✓fully proved

An inner vertex joined to a non-inner vertex in the outside graph lies on the inner boundary.

lemma ocd_bdryIn_of_outsideGraph_adj [Fintype Sin] [Fintype Sout]
    (ιV : {y : Site d // y ∈ Sin} → {y : Site d // y ∈ Sout})
    (hιval : ∀ x, (ιV x : Site d) = (x : Site d))
    (bdryOut : {y : Site d // y ∈ Sout} → Prop) [DecidablePred bdryOut]
    (bdryIn : {y : Site d // y ∈ Sin} → Prop) [DecidablePred bdryIn]
    (hmargin : ∀ x : {y : Site d // y ∈ Sin}, ¬ bdryOut (ιV x))
    (hbdryIn : ∀ (x : {y : Site d // y ∈ Sin}) (z : Site d),
      NearestNeighbour d (x : Site d) z → z ∉ Sin → bdryIn x)
    (ψ : ConfigSpace (Sym2 {y : Site d // y ∈ Sout}))
    {x : {y : Site d // y ∈ Sin}} {z : {y : Site d // y ∈ Sout}}
    (h : (ocd_outsideGraph (SimpleGraph.comap Subtype.val (hypercubicLattice d)) ιV bdryOut ψ).Adj
        (ιV x) z) :
    bdryIn x

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Outside graph with the wired boundary clique · Nearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Proof usesImage of an inner-graph edge in the outer graph · Edge map sends \(\{x, y\}\) to \(\{\iota x, \iota y\}\) · Outside-graph adjacency: open non-inner edge or boundary pair

Used byLattice induced wirings are coarser than the inner boundary clique

LemmaLattice induced wirings are coarser than the inner boundary clique#✓fully proved

For sub-boxes of ℤ^d avoiding the outer boundary, every induced wiring is coarser than the clique on the inner boundary.

lemma ocd_latticeInducedWiring_le [Fintype Sin] [Fintype Sout]
    (ιV : {y : Site d // y ∈ Sin} → {y : Site d // y ∈ Sout})
    (hιval : ∀ x, (ιV x : Site d) = (x : Site d)) (hιinj : Function.Injective ιV)
    (bdryOut : {y : Site d // y ∈ Sout} → Prop) [DecidablePred bdryOut]
    (bdryIn : {y : Site d // y ∈ Sin} → Prop) [DecidablePred bdryIn]
    (hmargin : ∀ x : {y : Site d // y ∈ Sin}, ¬ bdryOut (ιV x))
    (hbdryIn : ∀ (x : {y : Site d // y ∈ Sin}) (z : Site d),
      NearestNeighbour d (x : Site d) z → z ∉ Sin → bdryIn x)
    (ψ : ConfigSpace (Sym2 {y : Site d // y ∈ Sout})) :
    ocd_inducedWiring (SimpleGraph.comap Subtype.val (hypercubicLattice d)) ιV bdryOut ψ
      ≤ StatMech.Lattice.boundaryCliqueGraph bdryIn

Uses 9 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Wiring induced on the inner graph · Nearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Complete graph on the boundary vertices · Hypercubic lattice \(\mathbb{Z}^d\)

Proof usesInner vertex with an outside-graph edge lies on the inner boundary · Outside graph with the wired boundary clique · Boundary wiring relation

Used byInner wired domination for vertex sets of \(\mathbb{Z}^d\) · Ergodicity of the wired random-cluster measure

LemmaInner wired domination for vertex sets of \(\mathbb{Z}^d\)#✓fully proved

For a vertex set of ℤ^d inside a larger one and avoiding its wired boundary, the restricted outer wired FK measure is dominated by the inner wired FK measure on increasing events (for q ≥ 1).

lemma ocd_latticeWired_inner_dominated [Fintype Sin] [Fintype Sout]
    (ιV : {y : Site d // y ∈ Sin} → {y : Site d // y ∈ Sout})
    (hιval : ∀ x, (ιV x : Site d) = (x : Site d)) (hιinj : Function.Injective ιV)
    (bdryOut : {y : Site d // y ∈ Sout} → Prop) [DecidablePred bdryOut]
    (bdryIn : {y : Site d // y ∈ Sin} → Prop) [DecidablePred bdryIn]
    (hmargin : ∀ x : {y : Site d // y ∈ Sin}, ¬ bdryOut (ιV x))
    (hbdryIn : ∀ (x : {y : Site d // y ∈ Sin}) (z : Site d),
      NearestNeighbour d (x : Site d) z → z ∉ Sin → bdryIn x)
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    {A : Set (ConfigSpace (Sym2 {y : Site d // y ∈ Sin}))} (hA : IsIncreasing A) :
    (∑ ρ, (ocd_innerRestrict ιV ⁻¹' A).indicator (fun _ => (1:ℝ)) ρ
        * wiredFkProb (SimpleGraph.comap Subtype.val (hypercubicLattice d)) bdryOut p q ρ)
      ≤ ∑ ω, A.indicator (fun _ => (1:ℝ)) ω
          * wiredFkProb (SimpleGraph.comap Subtype.val (hypercubicLattice d)) bdryIn p q ω

Uses 16 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Restriction of an outer configuration to inner edges · Wired random-cluster probability of a configuration · Increasing event · Nearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Proof usesRandom-cluster probability with a boundary wiring · Boundary clique gives the wired random-cluster measure · Adjacency matching of the inner embedding · Wiring induced on the inner graph · Lattice inclusion matches induced adjacency · Lattice induced wirings are coarser than the inner boundary clique · Inner wired domination of the restricted outer wired measure · Complete graph on the boundary vertices · Boundary wiring relation

Used byOuter wired all-open probability at most the inner wired one

LemmaRestriction pulls back all-open events to their images#✓fully proved

The pullback of "all edges of t are open" under restriction is "all edges of ι(t) are open".

lemma ocd_innerRestrict_preimage_multiOpenEvent (hι : Function.Injective ιV)
    (t : Finset (Sym2 Vin)) :
    ocd_innerRestrict ιV ⁻¹' (med_genericMultiOpenEvent t)
      = med_genericMultiOpenEvent (t.image (ocd_innerEdge ιV))

Uses 4 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Event that all edges of a finite set are open · Image of an inner-graph edge in the outer graph · Restriction of an outer configuration to inner edges

Used byOuter wired all-open probability at most the inner wired one · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure

LemmaOuter wired all-open probability at most the inner wired one#✓fully proved

For a vertex set of ℤ^d inside a larger one and avoiding its wired boundary, the outer wired probability that all edges of ι(t) are open is at most the inner wired probability that all edges of t are open (for q ≥ 1).

StatMech.FK.ocd_latticeWired_multiMass_dominated · 15 lines

lemma ocd_latticeWired_multiMass_dominated [Fintype Sin] [Fintype Sout]
    (ιV : {y : Site d // y ∈ Sin} → {y : Site d // y ∈ Sout})
    (hιval : ∀ x, (ιV x : Site d) = (x : Site d)) (hιinj : Function.Injective ιV)
    (bdryOut : {y : Site d // y ∈ Sout} → Prop) [DecidablePred bdryOut]
    (bdryIn : {y : Site d // y ∈ Sin} → Prop) [DecidablePred bdryIn]
    (hmargin : ∀ x : {y : Site d // y ∈ Sin}, ¬ bdryOut (ιV x))
    (hbdryIn : ∀ (x : {y : Site d // y ∈ Sin}) (z : Site d),
      NearestNeighbour d (x : Site d) z → z ∉ Sin → bdryIn x)
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (t : Finset (Sym2 {y : Site d // y ∈ Sin})) :
    med_multiMassProb
        (wiredFkProb (SimpleGraph.comap Subtype.val (hypercubicLattice d)) bdryOut p q)
        (t.image (ocd_innerEdge ιV))
      ≤ med_multiMassProb
          (wiredFkProb (SimpleGraph.comap Subtype.val (hypercubicLattice d)) bdryIn p q) t

Uses 12 · Used by 4

Statement usesMass of the all-open event under a weight function · Image of an inner-graph edge in the outer graph · Wired random-cluster probability of a configuration · Nearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Proof usesConfiguration space of a statistical-mechanics model · Event that all edges of a finite set are open · Restriction of an outer configuration to inner edges · Restriction pulls back all-open events to their images · Inner wired domination for vertex sets of \(\mathbb{Z}^d\) · Increasing event

Used byPer-box uniqueness of the random-cluster measures off a countable set · Wired off-centre upper bound by the recentred small-box marginal · Ergodicity of the wired random-cluster measure · Translation invariance of the wired \(q = 2\) infinite-volume measure

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.