Boundary conditions for bond configurations

InductiveBoundary conditions for a bond model#✓fully proved

Boundary conditions for a bond model on a finite graph.

inductive BoundaryCondition
  | free
  | wired
  | periodic
  deriving DecidableEq, Repr

Used by 1

Used byNumber of open clusters under a boundary condition

DefinitionOpen edge in a bond configuration#✓fully proved

The edge {x, y} of G is open in the configuration ω.

def IsOpen (ω : Sym2 V → Bool) (x y : V) : Prop :=
  G.Adj x y ∧ ω s(x, y) = true

Used by 6

Used byOpen subgraph of a bond configuration · Wired and free FK weights within a factor \(q^{|\partial|}\), \(q \ge 1\) · Mixed supermodularity of free and wired cluster counts · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Boundary-preserving automorphisms preserve the wired FK probability · Boundary-matching isomorphisms preserve wired FK probabilities

DefinitionOpen subgraph of a bond configuration#✓fully proved

The spanning subgraph of G consisting of the open edges of ω.

def openGraph (ω : Sym2 V → Bool) : SimpleGraph V where
  Adj x y := IsOpen G ω x y
  symm := ⟨fun _ _ h => isOpen_symm G h⟩
  loopless := ⟨fun x h => isOpen_irrefl G x h⟩

Uses 1 · Used by 21

Statement usesOpen edge in a bond configuration

Used byNumber of open clusters with free boundary conditions · Wired open graph · Wired and free FK weights within a factor \(q^{|\partial|}\), \(q \ge 1\) · Monotonicity of the open subgraph · Monotonicity of the wired graph · Boundary clique gives the wired random-cluster measure · Mixed supermodularity of free and wired cluster counts · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Closed 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 · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Boundary-preserving automorphisms preserve the wired FK probability · Boundary-preserving automorphism as an isomorphism of wired graphs · Boundary-matching isomorphisms preserve wired FK probabilities · Wired-graph isomorphism for a pulled-back configuration

DefinitionNumber of open clusters with free boundary conditions#✓fully proved

The number of open clusters (connected components of the open graph) with free boundary conditions.

noncomputable def numClustersFree (ω : Sym2 V → Bool) : ℕ :=
  Nat.card (openGraph G ω).ConnectedComponent

Uses 1 · Used by 3

Statement usesOpen subgraph of a bond configuration

Used byNumber of open clusters under a boundary condition · Wired and free FK weights within a factor \(q^{|\partial|}\), \(q \ge 1\) · Mixed supermodularity of free and wired cluster counts

DefinitionBoundary wiring relation#✓fully proved

Both vertices lie on the boundary.

def wireRel (x y : V) : Prop := bdry x ∧ bdry y

Used by 61

Used byComplete graph on the boundary vertices · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Wired \(q = 2\) edge density is monotone in \(t\) · Wired and free FK weights within a factor \(q^{|\partial|}\), \(q \ge 1\) · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Edwards–Sokal one-point identity · Wired colorings as cluster colorings with a pinned boundary cluster · Wired random-cluster probability of connecting to the boundary · Boundary-supported wirings lie below the boundary clique · Boundary clique gives the wired random-cluster measure · Free–wired sandwich for boundary graphs inside the boundary clique · Boundary wirings lie between free and wired when \(q \ge 1\) · Mixed supermodularity of free and wired cluster counts · Wirings with the boundary clique dominate the wired measure, \(q \ge 1\) · Wired measure conditionally dominated by larger wirings, \(q \ge 1\) · Wired box measure dominates the induced-wiring measure for \(q \ge 1\) · Domain Markov property for the wired measure on nested boxes · Induced wiring lies below the inner boundary clique · Wired cluster count of a glued configuration splits additively · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Law of total probability over outside configurations · Factorization 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 · Factorization of the conditioned outer partition function · 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 · Outside-graph adjacency: open non-inner edge or boundary pair · Outer wired fibre masses sum to one · Inner wired domination of the restricted outer wired measure · FKG lattice condition for the wired measure when \(q \ge 1\) · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Secant bound gives free–wired density agreement off a countable set · 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 · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Masses of the conditioning fibres sum to one · 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 \(\Lambda_{n+1}\) measure decomposed over outer configurations · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Free off-centre lower bound by the recentred small-box marginal · Boundary-preserving automorphisms preserve the wired FK probability · Boundary-preserving automorphism as an isomorphism of wired graphs · Boundary-matching isomorphisms preserve wired FK probabilities · Wired-graph isomorphism for a pulled-back configuration · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure

DefinitionComplete graph on the boundary vertices#✓fully proved

The complete graph on the boundary vertices, used to wire the boundary together.

def boundaryCliqueGraph : SimpleGraph V := SimpleGraph.fromRel (wireRel bdry)

Uses 1 · Used by 71

Statement usesBoundary wiring relation

Used byWired open graph · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Wired \(q = 2\) edge density is monotone in \(t\) · Wired and free FK weights within a factor \(q^{|\partial|}\), \(q \ge 1\) · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Monotonicity of the wired graph · Open-edge graph with a boundary clique · Edwards–Sokal one-point identity · Wired colorings as cluster colorings with a pinned boundary cluster · Wired random-cluster probability of connecting to the boundary · Boundary-supported wirings lie below the boundary clique · Boundary clique gives the wired random-cluster measure · Free–wired sandwich for boundary graphs inside the boundary clique · Boundary wirings lie between free and wired when \(q \ge 1\) · Mixed supermodularity of free and wired cluster counts · Wirings with the boundary clique dominate the wired measure, \(q \ge 1\) · Wired measure conditionally dominated by larger wirings, \(q \ge 1\) · Wired box measure dominates the induced-wiring measure for \(q \ge 1\) · Domain Markov property for the wired measure on nested boxes · Induced wiring lies below the inner boundary clique · Wired cluster count of a glued configuration splits additively · Outer open graph plus the outer boundary clique · Wired glued open graph is the union of inner and outer graphs · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Law of total probability over outside configurations · Factorization 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 · Cluster graph of a glued configuration · Factorization of the conditioned outer partition function · 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 · Outside 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 · Outer wired fibre masses sum to one · Inner wired domination of the restricted outer wired measure · FKG lattice condition for the wired measure when \(q \ge 1\) · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Secant bound gives free–wired density agreement off a countable set · 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 · Inclusion of the wired inner graph into the extended wired graph · Inclusion of the wired inner graph into the extra-wired graph · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Masses of the conditioning fibres sum to one · 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 \(\Lambda_{n+1}\) measure decomposed over outer configurations · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Free off-centre lower bound by the recentred small-box marginal · Boundary-preserving automorphisms preserve the wired FK probability · Boundary-preserving automorphism as an isomorphism of wired graphs · Boundary-matching isomorphisms preserve wired FK probabilities · Wired-graph isomorphism for a pulled-back configuration · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure · Disjoint-box cap hypothesis for multi-open events · Conditional product cap for multi-open events in boxes

DefinitionWired open graph#✓fully proved

The wired open graph: the open edges of ω together with an edge between every two distinct boundary vertices.

def wiredGraph (ω : Sym2 V → Bool) : SimpleGraph V :=
  openGraph G ω ⊔ boundaryCliqueGraph bdry

Uses 2 · Used by 22

Statement usesComplete graph on the boundary vertices · Open subgraph of a bond configuration

Used byNumber of open clusters with wired boundary conditions · Wired and free FK weights within a factor \(q^{|\partial|}\), \(q \ge 1\) · Wired cluster count is antitone · Monotonicity of the wired graph · Boundary clique gives the wired random-cluster measure · Mixed supermodularity of free and wired cluster counts · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Closed 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 · 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 · Inclusion of the wired inner graph into the extra-wired graph · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Boundary-preserving automorphisms preserve the wired FK probability · Boundary-preserving automorphism as an isomorphism of wired graphs · Boundary-matching isomorphisms preserve wired FK probabilities · Wired-graph isomorphism for a pulled-back configuration

DefinitionNumber of open clusters with wired boundary conditions#✓fully proved

The number of open clusters with wired boundary conditions: all boundary vertices lie in a single cluster.

noncomputable def numClustersWired (ω : Sym2 V → Bool) : ℕ :=
  Nat.card (wiredGraph G bdry ω).ConnectedComponent

Uses 1 · Used by 38

Statement usesWired open graph

Used byNumber of open clusters under a boundary condition · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Continuity in \(t\) of wired \(q = 2\) edge marginals on a finite graph · Free-wired log-normalizer gap \(\le |\partial|\log q/|E|\) for \(q \ge 1\) · Convexity of the wired tilted log normalizer · Wired tilted log normalizer as a cumulant generating function · Wired tilted log normalizer has derivative the mean open fraction · Tilted mean of open edges equals the wired FK expectation · Wired and free FK weights within a factor \(q^{|\partial|}\), \(q \ge 1\) · Wired partition function at logistic \(p\) as a tilted sum · Wired cluster count is antitone · Wired box measure as a finite sum over box configurations · Holley cross inequality for wired and \(q = 1\) laws, \(q \ge 1\) · Wired law at most the \(q = 1\) law on increasing events, \(q \ge 1\) · Holley cross inequality for wired and Bernoulli weights, \(q \ge 1\) · Boundary clique gives the wired random-cluster measure · Free–wired domination on a finite graph for \(q \ge 1\) · Free box measure dominated by the wired one for \(q \ge 1\) · Holley's condition for free and wired probabilities when \(q \ge 1\) · Holley's condition for free and wired weights when \(q \ge 1\) · Mixed supermodularity of free and wired cluster counts · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Wired random-cluster measure as a probability mass function · Wired random-cluster weight · FKG inequality for the wired measure when \(q \ge 1\) · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Domain Markov property for the wired box measure · Wired random-cluster probabilities are positive · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\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 · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Wired FK edge marginals are at most one · Nonnegativity of wired FK edge marginals · Boundary-preserving automorphisms preserve the wired FK probability · Boundary-matching isomorphisms preserve wired FK probabilities

DefinitionNumber of open clusters under a boundary condition#✓fully proved

The number of open clusters under a boundary condition. The periodic case uses the free count: the periodic identification is built into the graph G.

noncomputable def numClusters (bc : BoundaryCondition) (ω : Sym2 V → Bool) : ℕ :=
  match bc with
  | BoundaryCondition.free => numClustersFree G ω
  | BoundaryCondition.wired => numClustersWired G bdry ω
  | BoundaryCondition.periodic => numClustersFree G ω

Uses 3

Statement usesBoundary conditions for a bond model · Number of open clusters with free boundary conditions · Number of open clusters with wired boundary conditions

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.