Random-cluster measures on finite graphs

DefinitionOpen subgraph of an edge configuration#✓fully proved

The open subgraph of G under the edge configuration ω: the edges of G that ω declares open.

def openSub (ω : ConfigSpace (Sym2 V)) : SimpleGraph V where
  Adj x y := G.Adj x y ∧ ω s(x, y) = true
  symm := by
    refine ⟨fun x y h => ?_⟩
    refine ⟨h.1.symm, ?_⟩
    rw [Sym2.eq_swap]; exact h.2
  loopless := ⟨fun x h => h.1.ne rfl⟩

Uses 1 · Used by 92

Statement usesConfiguration space of a statistical-mechanics model

Used byConnection to the boundary depends only on graph edges · Wired and free FK weights within a factor \(q^{|\partial|}\), \(q \ge 1\) · Vertex coloring induced by a coloring of open clusters · Random-cluster connection probability · Open connection between two vertices · Correspondence for cluster-constant colorings equal at two vertices · Ising two-point function equals the \(q = 2\) connection probability · Edwards–Sokal correlation identity · Potts two-point agreement at least \(1/q\) for \(q \ge 2\), \(\beta J > 0\) · Open-edge graph with a boundary clique · There are \(q^{k(\omega)}\) colorings constant on the open clusters · Spin configuration constant on open clusters · Cluster-constant colorings as colorings of clusters · Edwards–Sokal weight summed over spins is the random-cluster weight · 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-graph comparison \(\varphi^{C'}(A) \le q^N \varphi^C(A)\) · Empty wiring gives the free random-cluster measure · Boundary clique gives the wired random-cluster measure · Comparison inequalities · Kernel of the Laplacian of the open subgraph · Mixed supermodularity of free and wired cluster counts · Mixed supermodularity of cluster counts for nested wirings · Cluster count plus open-edge count is monotone · Number of clusters under a boundary wiring · Number of open clusters equals the dimension of the Laplacian kernel · Supermodularity of the random-cluster cluster count · Random-cluster weight is at most \(q^{|V|}\) for \(q \ge 1\) · Isomorphism invariance of the ambient FK normalizer · Ambient FK normalizer is supermultiplicative under disjoint union · Graph isomorphism restricted to open subgraphs · FK partition function of a graph with no vertices is one · Peeling bound for \(-\log Z\) of a tagged graph · Component decomposition of the wired glued graph · Component map into the wired glued graph · Glued and inner graphs have the same connections on the box · Inner open graph with the induced wiring · Wired cluster count of a glued configuration splits additively · Wired glued open graph is the union of inner and outer graphs · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Cluster graph of a glued configuration · Inner cluster reachability gives full-graph reachability of images · Inner cluster graph with the induced wiring · Full-graph reachability of images gives inner cluster reachability · Outside reachability gives inner cluster reachability · Inner image graph on embedded vertices is the open subgraph · Glued cluster count is induced-wiring count plus outside-only clusters · Outside graph is a subgraph of the full cluster graph · Full cluster graph as the union of inner image and outside graphs · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Inner-graph connections are glued-graph connections · Inner open graph with the free induced wiring · Glued connections between inner vertices are inner-graph connections · Outer open connections give connections in the inner graph · Cluster count of a glued configuration splits additively · Glued open graph is the union of inner and outer open edges · Domain Markov property for the wired box measure · Convergence to the free two-point function under stochastic increase · Convergence to the wired two-point function under stochastic decrease · Open path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\) · Inner vertices next to the annulus lie on \(\partial\Lambda_n\) · Open lattice edges between box vertices are open box edges · Paths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\) · Open connections in a box are open connections in \(\mathbb{Z}^d\) · Origin-to-boundary connection is an increasing event · Boundary-connection event of \(\Lambda_n\) on \(\Lambda_m\) is increasing · Open edges of \(\Lambda_n\) are open edges of \(\Lambda_{n+1}\) · Open edges of a box are open edges of \(\mathbb{Z}^d\) · Each non-edge contributes a factor 2 to the partition function · Per-box \(q = 2\) uniqueness off a countable set of tilts · Interface subadditivity of \(-\log\) of the edge partition function · Per-edge free energy of boxes converges for \(d \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free off-centre lower bound by the recentred small-box marginal · Event that two vertices are joined by open edges · Finite-energy property · Graph automorphisms preserve the free FK probability · Automorphism as an isomorphism of open subgraphs · Isomorphic graphs have equal free FK probabilities after relabelling · Open-subgraph isomorphism for a pulled-back configuration · Number of open clusters · Opening an edge lowers the cluster count by at most one · Opening an edge does not increase the cluster count · Open subgraph as the meet of \(G\) with the open-edge graph · Monotonicity of the open subgraph in the configuration · Toggling a non-edge leaves the open subgraph unchanged · FKG inequality for connection events for \(q \ge 1\) · Translation invariance of the free \(q = 2\) infinite-volume measure

LemmaOpen subgraph as the meet of \(G\) with the open-edge graph#✓fully proved

The open subgraph is G ⊓ fromEdgeSet {e | ω e = true} in Mathlib's terms.

lemma openSub_eq_inf_fromEdgeSet (ω : ConfigSpace (Sym2 V)) :
    openSub G ω = G ⊓ SimpleGraph.fromEdgeSet {e | ω e = true}

Uses 2

Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of an edge configuration

DefinitionNumber of open clusters#✓fully proved

The number k(ω) of open clusters: connected components of the open subgraph, isolated vertices included.

def numClusters (ω : ConfigSpace (Sym2 V)) : ℕ :=
  Fintype.card (openSub G ω).ConnectedComponent

Uses 2 · Used by 81

Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of an edge configuration

Used byFK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Convexity of the ambient tilted log normalizer · Monotonicity in \(p\) of free \(q = 2\) edge marginals on a finite graph · Continuity in \(t\) of free \(q = 2\) edge marginals on a finite graph · Free-wired log-normalizer gap \(\le |\partial|\log q/|E|\) for \(q \ge 1\) · Wired and free FK weights within a factor \(q^{|\partial|}\), \(q \ge 1\) · Bernoulli probability that edges \(F\) are all open is \(p^{|F|}\) · Bernoulli bound \(p^m\) for a fixed self-avoiding walk in the box · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\) · 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\) · Ising two-point function equals the \(q = 2\) connection probability · Edwards–Sokal correlation identity · Potts two-point agreement at least \(1/q\) for \(q \ge 2\), \(\beta J > 0\) · There are \(q^{k(\omega)}\) colorings constant on the open clusters · Edwards–Sokal weight summed over spins is the random-cluster weight · Empty wiring gives the free random-cluster measure · Edge density lies between \(p/(p+q(1-p))\) and \(p\) for \(q \ge 1\) · Comparison inequalities · Random-cluster measure increases stochastically in \(p\) when \(q \ge 1\) · Holley's cross inequality for FK measures, \(p_1 \le p_2\), \(q \ge 1\) · FKG lattice condition for the random-cluster measure · Free–wired domination on a finite graph for \(q \ge 1\) · FKG inequality for the random-cluster model · FKG inequality for increasing random-cluster events · Monotonicity of the random-cluster measure in p · 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 · Cluster count plus open-edge count is monotone · Number of open clusters equals the dimension of the Laplacian kernel · Supermodularity of the random-cluster cluster count · Doubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Per-edge free energy converges along \(K_j\) for \(d, q \ge 1\) · Random-cluster weight is at most \(q^{|V|}\) for \(q \ge 1\) · Uniform upper bound on the box free energy for \(d, n, q \ge 1\) · Isomorphism invariance of the ambient FK normalizer · Ambient FK normalizer is supermultiplicative under disjoint union · Subadditivity of \(-\log Z\) along a juxtaposition sequence · FK partition function of a graph with no vertices is one · FK partition function at least the all-closed weight for \(q \ge 1\) · Bound \(-\log Z \le |E|\,(-\log(1-p))\) for \(q \ge 1\) · Peeling bound for \(-\log Z\) of a tagged graph · Fibre-mass factorization of random-cluster probabilities · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Random-cluster weight of a glued configuration factorizes · Free box measure of a cylinder event as a finite sum · Next-box free measure of a cylinder event as a finite sum · One-step box monotonicity of free measures for \(q \ge 1\) · Cluster count of a glued configuration splits additively · Fibre masses of the free measure sum to one · Free box measure of a box connection event is the two-point function · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Each non-edge contributes a factor 2 to the partition function · Per-box \(q = 2\) uniqueness off a countable set of tilts · Interface subadditivity of \(-\log\) of the edge partition function · Per-edge free energy of boxes converges for \(d \ge 1\) · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free off-centre lower bound by the recentred small-box marginal · Free \(q = 2\) edge density lies in \((0, 1)\) · Domain Markov property (finite volume) · Finite-energy property · Ambient random-cluster law as a probability mass function · Graph automorphisms preserve the free FK probability · Unnormalized random-cluster weight · At \(q = 1\) the random-cluster weight is the Bernoulli product · Inhomogeneous random-cluster weight · Isomorphic graphs have equal free FK probabilities after relabelling · Differential formula · Differential formula in β · Opening an edge lowers the cluster count by at most one · Opening an edge does not increase the cluster count · Translation invariance of the free \(q = 2\) infinite-volume measure

DefinitionBernoulli edge product#✓fully proved

The Bernoulli edge product ∏_{e ∈ E(G)} (p if e open, 1 - p if e closed).

def edgeProduct (p : ℝ) (ω : ConfigSpace (Sym2 V)) : ℝ :=
  ∏ e ∈ G.edgeFinset, (if ω e then p else 1 - p)

Uses 1 · Used by 113

Statement usesConfiguration space of a statistical-mechanics model

Used by\(q = 1\) probability of an edge pattern is its Bernoulli weight · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Convexity of the ambient tilted log normalizer · Continuity in \(p\) of the Bernoulli edge weight · Monotonicity in \(p\) of free \(q = 2\) edge marginals on a finite graph · Continuity in \(t\) of free \(q = 2\) edge marginals on a finite graph · 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\) · 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 · Bernoulli probability that edges \(F\) are all open is \(p^{|F|}\) · Bernoulli bound \(p^m\) for a fixed self-avoiding walk in the box · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\) · 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\) · Ising two-point function equals the \(q = 2\) connection probability · Edwards–Sokal correlation identity · Potts two-point agreement at least \(1/q\) for \(q \ge 2\), \(\beta J > 0\) · Edwards–Sokal weight summed over spins is the random-cluster weight · Edwards–Sokal one-point identity · Boundary-graph comparison \(\varphi^{C'}(A) \le q^N \varphi^C(A)\) · Empty wiring gives the free random-cluster measure · Boundary clique gives the wired random-cluster measure · Holley's condition for probabilities with nested wirings, \(q \ge 1\) · Disintegration of a boundary-wired measure over conditioning fibres · Random-cluster comparison of boundary conditions for \(q \ge 1\) · Boundary-graph FK measure increases in \(p\) for \(q \ge 1\) · FKG inequality for the random-cluster measure, \(q \ge 1\) · Random-cluster weight with a boundary wiring · Holley's condition for weights with nested wirings, \(q \ge 1\) · Holley's condition for nested-wiring conditional measures, \(q \ge 1\) · Conditional measures increase with the wiring for \(q \ge 1\) · Edge density lies between \(p/(p+q(1-p))\) and \(p\) for \(q \ge 1\) · Comparison inequalities · Random-cluster measure increases stochastically in \(p\) when \(q \ge 1\) · Holley's cross inequality for FK measures, \(p_1 \le p_2\), \(q \ge 1\) · FKG lattice condition for the random-cluster measure · Free–wired domination on a finite graph for \(q \ge 1\) · FKG inequality for the random-cluster model · FKG inequality for increasing random-cluster events · Monotonicity of the random-cluster measure in p · 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\) · Doubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Per-edge free energy converges along \(K_j\) for \(d, q \ge 1\) · Random-cluster weight is at most \(q^{|V|}\) for \(q \ge 1\) · Uniform upper bound on the box free energy for \(d, n, q \ge 1\) · Isomorphism invariance of the ambient FK normalizer · Ambient FK normalizer is supermultiplicative under disjoint union · Subadditivity of \(-\log Z\) along a juxtaposition sequence · FK partition function of a graph with no vertices is one · FK partition function at least the all-closed weight for \(q \ge 1\) · Bound \(-\log Z \le |E|\,(-\log(1-p))\) for \(q \ge 1\) · Peeling bound for \(-\log Z\) of a tagged graph · Domain Markov property for the wired measure on nested boxes · Edge product of a glued configuration factorizes · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Factorization of the wired FK weight of a glued configuration · Factorization of the edge weight of a glued configuration · Outer wired fibre masses sum to one · Inner wired domination of the restricted outer wired measure · 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\) · Fibre-mass factorization of random-cluster probabilities · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Random-cluster weight of a glued configuration factorizes · Free box measure of a cylinder event as a finite sum · Next-box free measure of a cylinder event as a finite sum · One-step box monotonicity of free measures for \(q \ge 1\) · Fibre masses of the free measure sum to one · Domain Markov property for the wired box measure · Free box measure of a box connection event is the two-point function · Wired random-cluster probabilities are positive · Masses of the conditioning fibres sum to one · 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 · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Each non-edge contributes a factor 2 to the partition function · Per-box \(q = 2\) uniqueness off a countable set of tilts · Interface subadditivity of \(-\log\) of the edge partition function · Per-edge free energy of boxes converges for \(d \ge 1\) · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free off-centre lower bound by the recentred small-box marginal · Wired FK edge marginals are at most one · Nonnegativity of wired FK edge marginals · Free \(q = 2\) edge density lies in \((0, 1)\) · Domain Markov property (finite volume) · Finite-energy property · Ambient random-cluster law as a probability mass function · Graph automorphisms preserve the free FK probability · Boundary-preserving automorphisms preserve the wired FK probability · Unnormalized random-cluster weight · At \(q = 1\) the random-cluster weight is the Bernoulli product · Isomorphic graphs have equal free FK probabilities after relabelling · Boundary-matching isomorphisms preserve wired FK probabilities · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure

DefinitionUnnormalized random-cluster weight#✓fully proved

The unnormalized random-cluster weight p ^ o(ω) (1 - p) ^ c(ω) q ^ k(ω).

def fkWeight (p q : ℝ) (ω : ConfigSpace (Sym2 V)) : ℝ :=
  edgeProduct G p ω * q ^ numClusters G ω

Uses 3 · Used by 80

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Number of open clusters

Used by\(q = 1\) probability of an edge pattern is its Bernoulli weight · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Convexity of the ambient tilted log normalizer · Monotonicity in \(p\) of free \(q = 2\) edge marginals on a finite graph · Continuity in \(t\) of free \(q = 2\) edge marginals on a finite graph · Free-wired log-normalizer gap \(\le |\partial|\log q/|E|\) for \(q \ge 1\) · Wired and free FK weights within a factor \(q^{|\partial|}\), \(q \ge 1\) · Sandwich \(Z^w \le Z \le q^{|\partial|} Z^w\) for \(q \ge 1\) · Bernoulli probability that edges \(F\) are all open is \(p^{|F|}\) · Bernoulli bound \(p^m\) for a fixed self-avoiding walk in the box · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\) · 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\) · Ising two-point function equals the \(q = 2\) connection probability · Edwards–Sokal correlation identity · Potts two-point agreement at least \(1/q\) for \(q \ge 2\), \(\beta J > 0\) · Edwards–Sokal bond marginal is the random-cluster measure · Edwards–Sokal weight summed over spins is the random-cluster weight · Empty wiring gives the free random-cluster measure · Edge density lies between \(p/(p+q(1-p))\) and \(p\) for \(q \ge 1\) · Comparison inequalities · Random-cluster measure increases stochastically in \(p\) when \(q \ge 1\) · Holley's cross inequality for FK measures, \(p_1 \le p_2\), \(q \ge 1\) · FKG lattice condition for the random-cluster measure · Free–wired domination on a finite graph for \(q \ge 1\) · FKG inequality for the random-cluster model · FKG inequality for increasing random-cluster events · Monotonicity of the random-cluster measure in p · 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\) · Doubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Per-edge free energy converges along \(K_j\) for \(d, q \ge 1\) · Random-cluster weight is at most \(q^{|V|}\) for \(q \ge 1\) · Edge partition function is at most \(2^{|E|} q^{|V|}\) for \(q \ge 1\) · Uniform upper bound on the box free energy for \(d, n, q \ge 1\) · Isomorphism invariance of the ambient FK normalizer · Ambient FK normalizer is supermultiplicative under disjoint union · Subadditivity of \(-\log Z\) along a juxtaposition sequence · FK partition function of a graph with no vertices is one · FK partition function at least the all-closed weight for \(q \ge 1\) · Bound \(-\log Z \le |E|\,(-\log(1-p))\) for \(q \ge 1\) · Peeling bound for \(-\log Z\) of a tagged graph · Domain Markov property · Fibre-mass factorization of random-cluster probabilities · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Random-cluster weight of a glued configuration factorizes · Free box measure of a cylinder event as a finite sum · Next-box free measure of a cylinder event as a finite sum · One-step box monotonicity of free measures for \(q \ge 1\) · Conditional partition function in terms of the induced wiring · Fibre masses of the free measure sum to one · Free box measure of a box connection event is the two-point function · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Each non-edge contributes a factor 2 to the partition function · Per-box \(q = 2\) uniqueness off a countable set of tilts · Edge partition function of the random-cluster model · Interface subadditivity of \(-\log\) of the edge partition function · Per-edge free energy of boxes converges for \(d \ge 1\) · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free off-centre lower bound by the recentred small-box marginal · Free \(q = 2\) edge density lies in \((0, 1)\) · Domain Markov property (finite volume) · Finite-energy property · Ambient random-cluster law as a probability mass function · Probability of an ambient FK configuration · Graph automorphisms preserve the free FK probability · At \(q = 1\) the random-cluster weight is the Bernoulli product · Ambient FK normalizer · Isomorphic graphs have equal free FK probabilities after relabelling · FK measure induced on a fibre · Total FK weight of a fibre · Translation invariance of the free \(q = 2\) infinite-volume measure

DefinitionAmbient FK normalizer#✓fully proved

The ambient FK normalizer, summing over every bit assignment on Sym2 V. Each loop or nonedge contributes a factor of two relative to the edge partition function ecz_fkZEdge defined in EdgePartitionFunction.

def fkZ (p q : ℝ) : ℝ :=
  ∑ ω : ConfigSpace (Sym2 V), fkWeight G p q ω

Uses 2 · Used by 74

Statement usesConfiguration space of a statistical-mechanics model · Unnormalized random-cluster weight

Used by\(q = 1\) probability of an edge pattern is its Bernoulli weight · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Ambient tilted log normalizer of a finite graph · Convexity of the ambient tilted log normalizer · Monotonicity in \(p\) of free \(q = 2\) edge marginals on a finite graph · Continuity in \(t\) of free \(q = 2\) edge marginals on a finite graph · Free-wired log-normalizer gap \(\le |\partial|\log q/|E|\) for \(q \ge 1\) · Sandwich \(Z^w \le Z \le q^{|\partial|} Z^w\) for \(q \ge 1\) · Bernoulli probability that edges \(F\) are all open is \(p^{|F|}\) · Bernoulli bound \(p^m\) for a fixed self-avoiding walk in the box · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\) · 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\) · Ising two-point function equals the \(q = 2\) connection probability · Edwards–Sokal correlation identity · Potts two-point agreement at least \(1/q\) for \(q \ge 2\), \(\beta J > 0\) · Edwards–Sokal bond marginal is the random-cluster measure · Empty wiring gives the free random-cluster measure · Edge density lies between \(p/(p+q(1-p))\) and \(p\) for \(q \ge 1\) · Comparison inequalities · Random-cluster measure increases stochastically in \(p\) when \(q \ge 1\) · Holley's cross inequality for FK measures, \(p_1 \le p_2\), \(q \ge 1\) · FKG lattice condition for the random-cluster measure · Free–wired domination on a finite graph for \(q \ge 1\) · FKG inequality for the random-cluster model · FKG inequality for increasing random-cluster events · Monotonicity of the random-cluster measure in p · Free box measure dominated by the wired one for \(q \ge 1\) · Holley's condition for free and wired probabilities when \(q \ge 1\) · Negative log ambient normalizer of a box · Negative log ambient normalizer of the box \(\Lambda_n\) · Doubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Isomorphism invariance of the ambient FK normalizer · Ambient FK normalizer is supermultiplicative under disjoint union · Subadditivity of \(-\log Z\) along a juxtaposition sequence · Negative log of the ambient FK normalizer · Orthant blocks have the FK partition function of \(\Lambda_K\) · Doubling inequality for \(-\log Z\) of the free \(q = 2\) FK model · Iterated and single induced graphs share the FK partition function · Induced graphs with equal range have equal FK partition functions · FK partition function of a graph with no vertices is one · FK partition function at least the all-closed weight for \(q \ge 1\) · Left part of a tag split has the block partition function · Bound \(-\log Z \le |E|\,(-\log(1-p))\) for \(q \ge 1\) · Peeling bound for \(-\log Z\) of a tagged graph · The all-tag restriction has the partition function of \(\Lambda_{2K+1}\) · Right part of a tag split has the restricted partition function · Fibre-mass factorization of random-cluster probabilities · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Free box measure of a cylinder event as a finite sum · Next-box free measure of a cylinder event as a finite sum · One-step box monotonicity of free measures for \(q \ge 1\) · Fibre masses of the free measure sum to one · Free box measure of a box connection event is the two-point function · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Each non-edge contributes a factor 2 to the partition function · Per-box \(q = 2\) uniqueness off a countable set of tilts · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free off-centre lower bound by the recentred small-box marginal · Free \(q = 2\) edge density lies in \((0, 1)\) · Domain Markov property (finite volume) · Finite-energy property · Ambient random-cluster law as a probability mass function · Probability of an ambient FK configuration · Graph automorphisms preserve the free FK probability · Isomorphic graphs have equal free FK probabilities after relabelling · Translation invariance of the free \(q = 2\) infinite-volume measure

DefinitionProbability of an ambient FK configuration#✓fully proved

The probability of an ambient configuration: fkWeight G p q ω / fkZ G p q. For 0 < p < 1 and q > 0, its graph-edge marginal is the random-cluster law and unused coordinates are uniform.

noncomputable def fkProb (p q : ℝ) (ω : ConfigSpace (Sym2 V)) : ℝ :=
  fkWeight G p q ω / fkZ G p q

Uses 3 · Used by 97

Statement usesConfiguration space of a statistical-mechanics model · Unnormalized random-cluster weight · Ambient FK normalizer

Used by\(q = 1\) measure equals Bernoulli percolation on graph-edge events · \(q = 1\) probability of an edge pattern is its Bernoulli weight · Wired \(q = 2\) origin-to-boundary probability at most Bernoulli · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Monotonicity in \(p\) of free \(q = 2\) edge marginals on a finite graph · Continuity in \(t\) of free \(q = 2\) edge marginals on a finite graph · Left-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · Bernoulli probability that edges \(F\) are all open is \(p^{|F|}\) · Bernoulli bound \(p^m\) for a fixed self-avoiding walk in the box · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\) · 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\) · Random-cluster connection probability · Ising two-point function equals the \(q = 2\) connection probability · Edwards–Sokal correlation identity · Potts two-point agreement at least \(1/q\) for \(q \ge 2\), \(\beta J > 0\) · Edwards–Sokal bond marginal is the random-cluster measure · Empty wiring gives the free random-cluster measure · Edge density lies between \(p/(p+q(1-p))\) and \(p\) for \(q \ge 1\) · Probability that an edge is open under the random-cluster measure · Comparison inequalities · Random-cluster measure increases stochastically in \(p\) when \(q \ge 1\) · Holley's cross inequality for FK measures, \(p_1 \le p_2\), \(q \ge 1\) · FKG lattice condition for the random-cluster measure · Boundary wirings lie between free and wired when \(q \ge 1\) · Free–wired domination on a finite graph for \(q \ge 1\) · FKG inequality for the random-cluster model · FKG inequality for increasing random-cluster events · Monotonicity of the random-cluster measure in p · Free box measure dominated by the wired one for \(q \ge 1\) · Holley's condition for free and wired probabilities when \(q \ge 1\) · Free inner measure is dominated by the conditional outer measure · Free inner measure is dominated by every induced-wiring measure · FKG inequality for free \(q = 2\) box measures on smaller-box events · Translation covariance of free box masses · Free box measure of an all-open event equals its box mass · Free translation invariance from free placements of every shift · Equal free probabilities from eventually equal translated masses · Free placement for a shift via eventually equal box masses · Conditional free probabilities depend only on the outer configuration · One-step growth of free \(q = 2\) measures of increasing cylinders · Fibre-mass factorization of random-cluster probabilities · Conditional free measure dominates the smaller free box for \(q \ge 1\) · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Free box measure of a cylinder event as a finite sum · Increasing box events gain free \(q = 2\) probability in the next box · Next-box free measure of a cylinder event as a finite sum · Decomposition of the free measure over the outer configuration · One-step box monotonicity of free measures for \(q \ge 1\) · Fibre masses of the free measure sum to one · Off-centre carrier vanishes by translation covariance · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Free box measure of a box connection event is the two-point function · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set · Free unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Two-sided free \(q = 2\) bulk bounds from the free sandwich · Free \(q = 2\) bulk sandwich from equal free edge densities · Lower bound on free bulk edge marginals · Free off-centre lower bound by the recentred small-box marginal · Free off-centre sandwich from free rotation residues · Free unit-edge marginals converge to the free density · Free unit-edge marginal in the square-root box · Wired off-centre upper bound by the recentred small-box marginal · Free \(q = 2\) edge density lies in \((0, 1)\) · Free uniform bulk deviation at \(q = 2\) · Random-cluster measure conditioned on the edges off a set · Domain Markov property (finite volume) · Conditional probability that an edge is open given the rest · Finite-energy property · Random-cluster expectation of an observable · Ambient random-cluster law as a probability mass function · Graph automorphisms preserve free FK edge marginals · Graph automorphisms preserve the free FK probability · Box symmetries preserve the free \(q = 2\) density of box edges · Translation covariance of FK edge marginals on boxes · Boundary-matching isomorphisms transport FK edge marginals · Isomorphic graphs have equal free FK probabilities after relabelling · Two-point function of the free random-cluster measure · FKG inequality for connection events for \(q \ge 1\) · Translation invariance of the free \(q = 2\) infinite-volume measure · Free off-centre sandwich hypothesis · Free \(q = 2\) box edge marginals are at most the free density · Translation invariance of free and wired densities if marginals merge · Constant free density gives an upper bound on expected open edges · Free upper bound on expected open edges along a box-symmetry orbit · Equal free densities from merging free marginals · Translation invariance of the free density given merging marginals · Free box integral of an edge indicator is the free edge marginal · Translated free box mass of an edge set · Translated free box mass equals the centred box probability

DefinitionAmbient random-cluster law as a probability mass function#✓fully proved

The ambient extension of the random-cluster edge law as a PMF on all Sym2 V configurations, with independent uniform bits on loops and nonedges.

noncomputable def fkPMF {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    PMF (ConfigSpace (Sym2 V)) :=
  PMF.ofFintype (fun ω => ENNReal.ofReal (fkProb G p q ω)) <| by
    rw [← ENNReal.ofReal_sum_of_nonneg fun ω _ => fkProb_nonneg G hp hp1 hq ω,
      fkProb_sum_eq_one G hp hp1 hq]
    simp

Uses 6 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Probability of an ambient FK configuration · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters

Used byFree box measure dominated by the wired one for \(q \ge 1\) · Free random-cluster measure on a box · Free box measure of a cylinder event as a finite sum · Next-box free measure of a cylinder event as a finite sum · Free box measure of a box connection event is the two-point function

LemmaAt \(q = 1\) the random-cluster weight is the Bernoulli product#✓fully proved

At q = 1 the random-cluster weight is the Bernoulli product weight.

lemma fkWeight_one (p : ℝ) (ω : ConfigSpace (Sym2 V)) :
    fkWeight G p 1 ω = edgeProduct G p ω

Uses 4 · Used by 8

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Unnormalized random-cluster weight

Proof usesNumber of open clusters

Used by\(q = 1\) probability of an edge pattern is its Bernoulli weight · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Bernoulli probability that edges \(F\) are all open is \(p^{|F|}\) · Holley cross inequality for wired and \(q = 1\) laws, \(q \ge 1\) · Comparison inequalities

DefinitionAgreement of configurations off an edge set#✓fully proved

ω agrees with ψ on every edge outside F.

def AgreesOff (F : Finset (Sym2 V)) (ψ : ConfigSpace (Sym2 V)) :
    ConfigSpace (Sym2 V) → Prop :=
  fun ω => ∀ e, e ∉ F → ω e = ψ e

Uses 1 · Used by 29

Statement usesConfiguration space of a statistical-mechanics model

Used byDisintegration of a boundary-wired measure over conditioning fibres · Conditional random-cluster measure with a boundary wiring · Holley's condition for nested-wiring conditional measures, \(q \ge 1\) · Conditional measures increase with the wiring for \(q \ge 1\) · Domain Markov property for the wired measure on nested boxes · Glued configuration agrees with the outer one off the inner edge set · Law of total probability over outside configurations · 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 · Agreeing configuration is the gluing of its own restriction · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Conditional free probabilities depend only on the outer configuration · Conditional free measure as an induced-wiring measure · Fibre-mass factorization of random-cluster probabilities · Decomposition of the free measure over the outer configuration · Conditional partition function in terms of the induced wiring · Domain Markov property for the wired box measure · Configurations closed off the inner edges as inner-box configurations · Outer projection agrees with the configuration off \(\Lambda_n\) · Configurations agreeing off \(F\) have equal conditional probabilities · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Configurations agreeing off \(F\) have the same conditioning fibre · Configurations with a given outer part form its conditioning fibre · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations · Fibre of configurations agreeing off an edge set · Event depending only on edges outside a set · Ergodicity of the wired random-cluster measure

DefinitionFibre of configurations agreeing off an edge set#✓fully proved

The fibre of configurations agreeing with ψ off F.

noncomputable def condFibre (F : Finset (Sym2 V)) (ψ : ConfigSpace (Sym2 V)) :
    Finset (ConfigSpace (Sym2 V)) :=
  Finset.univ.filter (AgreesOff F ψ)

Uses 2 · Used by 36

Statement usesConfiguration space of a statistical-mechanics model · Agreement of configurations off an edge set

Used byDisintegration of a boundary-wired measure over conditioning fibres · Holley's condition for nested-wiring conditional measures, \(q \ge 1\) · Conditional measures increase with the wiring for \(q \ge 1\) · Partition function of a conditioning fibre · Domain Markov property for the wired measure on nested boxes · Law of total probability over outside configurations · Conditional outer probability as an induced-wiring probability · Conditioning fibre is the set of gluings · Projection fibres are conditioning fibres · Factorization of the conditioned outer partition function · Outer wired fibre masses sum to one · Inner wired domination of the restricted outer wired measure · Closed annulus plus inner-boundary wiring gives wired \(\Lambda_n\) law · Conditional free probabilities depend only on the outer configuration · Conditional free measure as an induced-wiring measure · Fibre-mass factorization of random-cluster probabilities · Conditional free measure dominates the smaller free box for \(q \ge 1\) · Decomposition of the free measure over the outer configuration · One-step box monotonicity of free measures for \(q \ge 1\) · Conditional partition function in terms of the induced wiring · Fibre masses of the free measure sum to one · Domain Markov property for the wired box measure · Configurations agreeing off \(F\) have equal conditional probabilities · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Configurations agreeing off \(F\) have the same conditioning fibre · Configurations with a given outer part form its conditioning fibre · Masses of the conditioning fibres sum to one · Wired \(\Lambda_{n+1}\) measure decomposed over outer configurations · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Random-cluster measure conditioned on the edges off a set · Domain Markov property (finite volume) · Total FK weight of a fibre · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure

DefinitionTotal FK weight of a fibre#✓fully proved

The total FK weight of the fibre condFibre F ψ.

noncomputable def inducedFkZ (p q : ℝ) (F : Finset (Sym2 V))
    (ψ : ConfigSpace (Sym2 V)) : ℝ :=
  ∑ ρ ∈ condFibre F ψ, fkWeight G p q ρ

Uses 3 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Fibre of configurations agreeing off an edge set · Unnormalized random-cluster weight

Used byDomain Markov property · Conditional partition function in terms of the induced wiring · Domain Markov property (finite volume) · FK measure induced on a fibre

DefinitionFK measure induced on a fibre#✓fully proved

The FK measure induced on the fibre condFibre F ψ: FK weight divided by the fibre's total weight.

noncomputable def inducedFkProb (p q : ℝ) (F : Finset (Sym2 V))
    (ψ ω : ConfigSpace (Sym2 V)) : ℝ :=
  fkWeight G p q ω / inducedFkZ G p q F ψ

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Unnormalized random-cluster weight · Total FK weight of a fibre

Used byDomain Markov property · Domain Markov property (finite volume)

DefinitionRandom-cluster measure conditioned on the edges off a set#✓fully proved

The random-cluster measure conditioned on agreeing with ψ off F.

noncomputable def condFkProb (p q : ℝ) (F : Finset (Sym2 V))
    (ψ ω : ConfigSpace (Sym2 V)) : ℝ :=
  fkProb G p q ω / ∑ ρ ∈ condFibre F ψ, fkProb G p q ρ

Uses 3 · Used by 8

Statement usesConfiguration space of a statistical-mechanics model · Fibre of configurations agreeing off an edge set · Probability of an ambient FK configuration

Used byConditional free probabilities depend only on the outer configuration · Domain Markov property · Conditional free measure as an induced-wiring measure · Fibre-mass factorization of random-cluster probabilities · Conditional free measure dominates the smaller free box for \(q \ge 1\) · Decomposition of the free measure over the outer configuration · One-step box monotonicity of free measures for \(q \ge 1\) · Domain Markov property (finite volume)

TheoremDomain Markov property (finite volume)#✓fully proved

Conditioned on the states of the edges outside F, the random-cluster measure is the FK weight renormalized on the fibre (Grimmett, The Random-Cluster Model, 2006, Lemma 4.13).

theorem condFkProb_eq_inducedFkProb {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (F : Finset (Sym2 V)) (ψ ω : ConfigSpace (Sym2 V)) :
    condFkProb G p q F ψ ω = inducedFkProb G p q F ψ ω

Uses 10 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster measure conditioned on the edges off a set · FK measure induced on a fibre

Proof usesFibre of configurations agreeing off an edge set · Bernoulli edge product · Probability of an ambient FK configuration · Unnormalized random-cluster weight · Ambient FK normalizer · Total FK weight of a fibre · Number of open clusters

Used byDomain Markov property

DefinitionClosing the edges of a set in a configuration#✓fully proved

The configuration that closes every edge of F and agrees with ψ elsewhere.

noncomputable def projOff (F : Finset (Sym2 V)) (ψ : ConfigSpace (Sym2 V)) :
    ConfigSpace (Sym2 V) :=
  fun e => if e ∈ F then false else ψ e

Uses 1 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model

Used byFibre representatives with every edge of a set closed · Ergodicity of the wired random-cluster measure

DefinitionFibre representatives with every edge of a set closed#✓fully proved

Representatives of the fibres of F: configurations with every edge of F closed.

noncomputable def fibreReps (F : Finset (Sym2 V)) : Finset (ConfigSpace (Sym2 V)) :=
  Finset.univ.filter (fun ψ => projOff F ψ = ψ)

Uses 2 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Closing the edges of a set in a configuration

Used byErgodicity of the wired random-cluster measure · Disjoint-box cap hypothesis for multi-open events · Conditional product cap for multi-open events in boxes

DefinitionEvent depending only on edges outside a set#✓fully proved

Membership in B depends only on the states of edges outside F.

def DependsOnOutside (F : Finset (Sym2 V)) (B : Set (ConfigSpace (Sym2 V))) : Prop :=
  ∀ ψ ρ, AgreesOff F ψ ρ → (ψ ∈ B ↔ ρ ∈ B)

Uses 2 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Agreement of configurations off an edge set

Used byErgodicity of the wired random-cluster measure · Conditional product cap for multi-open events in boxes

LemmaToggling a non-edge leaves the open subgraph unchanged#✓fully proved

Off the edges of G, flipping e does not change the open subgraph.

lemma openSub_setOpen_eq_setClosed_of_notMem {e : Sym2 V} (he : e ∉ G.edgeFinset)
    (ω : ConfigSpace (Sym2 V)) :
    openSub G (setOpen e ω) = openSub G (setClosed e ω)

Uses 4 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of an edge configuration · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byPer-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Finite-energy property · Opening an edge lowers the cluster count by at most one

LemmaOpening an edge does not increase the cluster count#✓fully proved

Opening an edge does not increase the number of clusters. This is a special case of Mathlib's SimpleGraph.ConnectedComponent.card_le_card_of_le, which proves it.

lemma numClusters_setOpen_le (e : Sym2 V) (ω : ConfigSpace (Sym2 V)) :
    numClusters G (setOpen e ω) ≤ numClusters G (setClosed e ω)

Uses 6 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Number of open clusters · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Proof usesOpen subgraph of an edge configuration · Closed configuration lies below the opened one

Used byEdge density lies between \(p/(p+q(1-p))\) and \(p\) for \(q \ge 1\) · Finite-energy property

LemmaOpening an edge lowers the cluster count by at most one#✓fully proved

Opening an edge lowers the number of clusters by at most one.

lemma numClusters_setClosed_le_setOpen_succ (e : Sym2 V) (ω : ConfigSpace (Sym2 V)) :
    numClusters G (setClosed e ω) ≤ numClusters G (setOpen e ω) + 1

Uses 9 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Number of open clusters · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Proof usesKernel of the Laplacian of the open subgraph · Number of open clusters equals the dimension of the Laplacian kernel · Open subgraph of an edge configuration · Toggling a non-edge leaves the open subgraph unchanged · Closed configuration lies below the opened one

Used byEdge density lies between \(p/(p+q(1-p))\) and \(p\) for \(q \ge 1\) · Cluster count plus open-edge count is monotone · Finite-energy property

DefinitionBernoulli product over the edges other than one edge#✓fully proved

The Bernoulli product over the edges of G other than e.

noncomputable def edgeRest (p : ℝ) (e : Sym2 V) (ω : ConfigSpace (Sym2 V)) : ℝ :=
  ∏ e' ∈ G.edgeFinset \ {e}, (if ω e' then p else 1 - p)

Uses 1 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model

Used byEdge density lies between \(p/(p+q(1-p))\) and \(p\) for \(q \ge 1\) · Finite-energy property

DefinitionConditional probability that an edge is open given the rest#✓fully proved

The conditional probability under φ_{G,p,q} that e is open given the states of all other edges: φ(setOpen e ω) / (φ(setOpen e ω) + φ(setClosed e ω)).

noncomputable def condOpen (p q : ℝ) (e : Sym2 V) (ω : ConfigSpace (Sym2 V)) : ℝ :=
  fkProb G p q (setOpen e ω) /
    (fkProb G p q (setOpen e ω) + fkProb G p q (setClosed e ω))

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byEdge density lies between \(p/(p+q(1-p))\) and \(p\) for \(q \ge 1\) · Finite-energy property

DefinitionFinite-energy constant of the random-cluster measure#✓fully proved

The finite-energy constant min (p / (p + q (1 - p))) (1 - p).

noncomputable def cFE (p q : ℝ) : ℝ := min (p / (p + q * (1 - p))) (1 - p)

Used by 1

Used byFinite-energy property

TheoremFinite-energy property#✓fully proved

Finite-energy property of the random-cluster measure. For p ∈ (0, 1) and q ≥ 1, the conditional probability that an edge is open given all other edges lies in [cFE p q, 1 - cFE p q]. For edges of G the sharper bounds p / (p + q (1 - p)) and p are proved along the way. See G. Grimmett, The Random-Cluster Model (2006), Chapter 3.

theorem finite_energy {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (e : Sym2 V) (ω : ConfigSpace (Sym2 V)) :
    cFE p q ≤ condOpen G p q e ω ∧ condOpen G p q e ω ≤ 1 - cFE p q

Uses 15

Statement usesConfiguration space of a statistical-mechanics model · Finite-energy constant of the random-cluster measure · Conditional probability that an edge is open given the rest

Proof usesBernoulli edge product · Bernoulli product over the edges other than one edge · Probability of an ambient FK configuration · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · Opening an edge lowers the cluster count by at most one · Opening an edge does not increase the cluster count · Open subgraph of an edge configuration · Toggling a non-edge leaves the open subgraph unchanged · Closing a coordinate of a configuration · Opening a coordinate of a configuration

DefinitionInhomogeneous Bernoulli edge product#✓fully proved

The inhomogeneous Bernoulli product ∏_{e ∈ E(G)} (pf e if e open, 1 - pf e if closed).

noncomputable def edgeProductW (pf : Sym2 V → ℝ) (ω : ConfigSpace (Sym2 V)) : ℝ :=
  ∏ e ∈ G.edgeFinset, (if ω e then pf e else 1 - pf e)

Uses 1 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model

Used byInhomogeneous random-cluster weight · Differential formula · Differential formula in β

DefinitionInhomogeneous random-cluster weight#✓fully proved

The inhomogeneous random-cluster weight edgeProductW G pf ω · q ^ k(ω).

noncomputable def fkWeightW (pf : Sym2 V → ℝ) (q : ℝ) (ω : ConfigSpace (Sym2 V)) : ℝ :=
  edgeProductW G pf ω * q ^ numClusters G ω

Uses 3 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Inhomogeneous Bernoulli edge product · Number of open clusters

Used byUnnormalized inhomogeneous random-cluster expectation · Inhomogeneous random-cluster probability · Partition function of the inhomogeneous random-cluster measure · Differential formula · Differential formula in β

DefinitionPartition function of the inhomogeneous random-cluster measure#✓fully proved

The partition function of the inhomogeneous random-cluster measure.

noncomputable def fkZW (pf : Sym2 V → ℝ) (q : ℝ) : ℝ :=
  ∑ ω : ConfigSpace (Sym2 V), fkWeightW G pf q ω

Uses 2 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Inhomogeneous random-cluster weight

Used byInhomogeneous random-cluster probability · Differential formula · Differential formula in β

DefinitionInhomogeneous random-cluster probability#✓fully proved

The inhomogeneous random-cluster probability fkWeightW / fkZW.

noncomputable def fkProbW (pf : Sym2 V → ℝ) (q : ℝ) (ω : ConfigSpace (Sym2 V)) : ℝ :=
  fkWeightW G pf q ω / fkZW G pf q

Uses 3 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Inhomogeneous random-cluster weight · Partition function of the inhomogeneous random-cluster measure

Used byExpectation under the inhomogeneous random-cluster measure · Differential formula · Differential formula in β

DefinitionExpectation under the inhomogeneous random-cluster measure#✓fully proved

The expectation of g under the inhomogeneous random-cluster measure.

noncomputable def fkMeanW (pf : Sym2 V → ℝ) (q : ℝ) (g : ConfigSpace (Sym2 V) → ℝ) : ℝ :=
  ∑ ω : ConfigSpace (Sym2 V), g ω * fkProbW G pf q ω

Uses 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Inhomogeneous random-cluster probability

Used byCovariance under the inhomogeneous random-cluster measure · Probability of an event under the inhomogeneous random-cluster measure · Differential formula · Differential formula in β

DefinitionCovariance under the inhomogeneous random-cluster measure#✓fully proved

The covariance E[f g] - E[f] E[g] under the inhomogeneous random-cluster measure (a finite form of Mathlib's ProbabilityTheory.covariance).

noncomputable def fkCovW (pf : Sym2 V → ℝ) (q : ℝ)
    (f g : ConfigSpace (Sym2 V) → ℝ) : ℝ :=
  fkMeanW G pf q (fun ω => f ω * g ω) - fkMeanW G pf q f * fkMeanW G pf q g

Uses 2 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Expectation under the inhomogeneous random-cluster measure

Used byDifferential formula · Differential formula in β

DefinitionReal-valued indicator that an edge is open#✓fully proved

The real-valued state 𝟙[e open] of the edge e.

noncomputable def coordR (e : Sym2 V) (ω : ConfigSpace (Sym2 V)) : ℝ :=
  if ω e then (1 : ℝ) else 0

Uses 1 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model

Used byLogarithmic \(\beta\)-derivative of the random-cluster weight · Differential formula · Differential formula in β

DefinitionInhomogeneous Bernoulli product over all edges but one#✓fully proved

The inhomogeneous Bernoulli product over the edges of G other than e₀.

noncomputable def edgeProductWOff (pf : Sym2 V → ℝ) (e₀ : Sym2 V)
    (ω : ConfigSpace (Sym2 V)) : ℝ :=
  ∏ j ∈ G.edgeFinset.erase e₀, (if ω j then pf j else 1 - pf j)

Uses 1 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model

Used byDifferential formula

DefinitionUnnormalized inhomogeneous random-cluster expectation#✓fully proved

The unnormalized expectation ∑_ω g(ω) fkWeightW G pf q ω.

noncomputable def fkNumerW (pf : Sym2 V → ℝ) (q : ℝ) (g : ConfigSpace (Sym2 V) → ℝ) : ℝ :=
  ∑ ω : ConfigSpace (Sym2 V), g ω * fkWeightW G pf q ω

Uses 2 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Inhomogeneous random-cluster weight

Used byDifferential formula · Differential formula in β

TheoremDifferential formula#✓fully proved

Differential formula for the random-cluster measure: the derivative of φ[g] in the parameter of the edge e₀ is Cov(g, 𝟙[e₀ open]) / (p (1 - p)) with p = pf e₀. See G. Grimmett, The Random-Cluster Model (2006), Chapter 3.

theorem hasDerivAt_fkMeanW {pf : Sym2 V → ℝ} (hpf : ∀ e, 0 < pf e) (hpf1 : ∀ e, pf e < 1)
    {q : ℝ} (hq : 0 < q) {e₀ : Sym2 V} (he : e₀ ∈ G.edgeFinset)
    (g : ConfigSpace (Sym2 V) → ℝ) :
    HasDerivAt (fun t => fkMeanW G (Function.update pf e₀ t) q g)
      (fkCovW G (Function.update pf e₀ (pf e₀)) q g (coordR e₀) / (pf e₀ * (1 - pf e₀)))
      (pf e₀)

Uses 11

Statement usesConfiguration space of a statistical-mechanics model · Real-valued indicator that an edge is open · Covariance under the inhomogeneous random-cluster measure · Expectation under the inhomogeneous random-cluster measure

Proof usesInhomogeneous Bernoulli edge product · Inhomogeneous Bernoulli product over all edges but one · Unnormalized inhomogeneous random-cluster expectation · Inhomogeneous random-cluster probability · Inhomogeneous random-cluster weight · Partition function of the inhomogeneous random-cluster measure · Number of open clusters

DefinitionProbability of an event under the inhomogeneous random-cluster measure#✓fully proved

The probability of the event A under the inhomogeneous random-cluster measure.

noncomputable def fkProbWOf (pf : Sym2 V → ℝ) (q : ℝ)
    (A : Set (ConfigSpace (Sym2 V))) : ℝ :=
  fkMeanW G pf q (A.indicator (fun _ => (1 : ℝ)))

Uses 2

Statement usesConfiguration space of a statistical-mechanics model · Expectation under the inhomogeneous random-cluster measure

LemmaDerivative in \(\beta\) of the edge parameter \(1 - e^{-\beta J}\)#✓fully proved

The derivative of the edge parameter p(β) = 1 - exp (-β J) is J exp (-β J).

lemma hasDerivAt_paramOfBeta (J β : ℝ) :
    HasDerivAt (fun b => 1 - Real.exp (-(b * J))) (J * Real.exp (-(β * J))) β

Used by 2

Used byMean-field differential inequality for inhomogeneous percolation · Differential formula in β

DefinitionEdge parameters \(p_e(\beta) = 1 - e^{-\beta J_e}\)#✓fully proved

The edge parameters p_e(β) = 1 - exp (-β J_e).

noncomputable def betaParams (J : Sym2 V → ℝ) (β : ℝ) : Sym2 V → ℝ :=
  fun e => 1 - Real.exp (-(β * J e))

Used by 3

Used byMean-field differential inequality for inhomogeneous percolation · Logarithmic \(\beta\)-derivative of the random-cluster weight · Differential formula in β

DefinitionLogarithmic \(\beta\)-derivative of the random-cluster weight#✓fully proved

The logarithmic β-derivative of the random-cluster weight under betaParams: ∑_{e ∈ E(G)} (J_e / p_e) (𝟙[e open] - p_e).

noncomputable def betaScore (G : SimpleGraph V) [DecidableRel G.Adj]
    (J : Sym2 V → ℝ) (β : ℝ)
    (ω : ConfigSpace (Sym2 V)) : ℝ :=
  ∑ e ∈ G.edgeFinset,
    (J e / betaParams J β e) * (coordR e ω - betaParams J β e)

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Edge parameters \(p_e(\beta) = 1 - e^{-\beta J_e}\) · Real-valued indicator that an edge is open

Used byDifferential formula in β

TheoremDifferential formula in β#✓fully proved

Differential formula in β for the random-cluster measure with edge parameters 1 - exp (-β J_e): d/dβ φ_β[g] = ∑_e (J_e / p_e) Cov(g, 𝟙[e open]). See G. Grimmett, The Random-Cluster Model (2006), Chapter 3.

theorem hasDerivAt_fkMeanW_beta_sum (G : SimpleGraph V) [DecidableRel G.Adj]
    {J : Sym2 V → ℝ}
    (hJ : ∀ e, 0 < J e) {β : ℝ} (hβ : 0 < β) {q : ℝ} (hq : 0 < q)
    (g : ConfigSpace (Sym2 V) → ℝ) :
    HasDerivAt (fun b => fkMeanW G (betaParams J b) q g)
      (∑ e ∈ G.edgeFinset,
        (J e / betaParams J β e) * fkCovW G (betaParams J β) q g (coordR e)) β

Uses 13

Statement usesConfiguration space of a statistical-mechanics model · Edge parameters \(p_e(\beta) = 1 - e^{-\beta J_e}\) · Real-valued indicator that an edge is open · Covariance under the inhomogeneous random-cluster measure · Expectation under the inhomogeneous random-cluster measure

Proof usesLogarithmic \(\beta\)-derivative of the random-cluster weight · Inhomogeneous Bernoulli edge product · Unnormalized inhomogeneous random-cluster expectation · Inhomogeneous random-cluster probability · Inhomogeneous random-cluster weight · Partition function of the inhomogeneous random-cluster measure · Derivative in \(\beta\) of the edge parameter \(1 - e^{-\beta J}\) · Number of open clusters

DefinitionNumber of open edges#✓fully proved

The number o(ω) of open edges of G in ω.

def openCount (ω : ConfigSpace (Sym2 V)) : ℕ :=
  (G.edgeFinset.filter (fun e => ω e = true)).card

Uses 1 · Used by 13

Statement usesConfiguration space of a statistical-mechanics model

Used byAverage edge density of the \(q = 2\) random-cluster measure · Convexity of the ambient tilted log normalizer · Average wired edge density · Average wired edge density as the mean of edge marginals · 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 · Expected wired open-edge count is the sum of edge marginals · Wired partition function at logistic \(p\) as a tilted sum · Per-box \(q = 2\) uniqueness off a countable set of tilts · Average edge density of a random-cluster measure · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionNumber of closed edges#✓fully proved

The number c(ω) of closed edges of G in ω.

def closedCount (ω : ConfigSpace (Sym2 V)) : ℕ :=
  (G.edgeFinset.filter (fun e => ω e = false)).card

Uses 1 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model

Used byConvexity of the ambient tilted log normalizer · Tilted mean of open edges equals the wired FK expectation · Wired partition function at logistic \(p\) as a tilted sum · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionTilt factor between two edge parameters#✓fully proved

The tilt factor λ = p₂ (1 - p₁) / ((1 - p₂) p₁), the ratio of the odds of an open edge at p₂ and at p₁.

noncomputable def tiltFactor (p1 p2 : ℝ) : ℝ := p2 * (1 - p1) / ((1 - p2) * p1)

Used by 2

Used byFinite-volume tilt data for a box edge at \(q = 2\) · Tilt data give wired density at \(p'\) at most free density at \(p > p'\)

DefinitionRandom-cluster expectation of an observable#✓fully proved

The expectation φ_{G,p,q}[X] = ∑_ω φ_{G,p,q}(ω) X(ω) of an observable X.

noncomputable def fkExpect (p q : ℝ) (X : ConfigSpace (Sym2 V) → ℝ) : ℝ :=
  ∑ ω : ConfigSpace (Sym2 V), fkProb G p q ω * X ω

Uses 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration

Used byAverage edge density of the \(q = 2\) random-cluster measure · Per-box \(q = 2\) uniqueness off a countable set of tilts · Average edge density of a random-cluster measure · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionRelabelling of an edge configuration by a vertex permutation#✓fully proved

The configuration ω ∘ σ on edges: the edge e is open in reCfg σ ω iff σ e is open in ω. See also reCfgIso, the same relabelling along an equivalence V ≃ W.

noncomputable def reCfg (σ : V ≃ V) (ω : ConfigSpace (Sym2 V)) : ConfigSpace (Sym2 V) :=
  fun e => ω (Sym2.map σ e)

Uses 1 · Used by 8

Statement usesConfiguration space of a statistical-mechanics model

Used byGraph automorphisms preserve free FK edge marginals · Boundary-preserving automorphisms preserve wired FK edge marginals · Graph automorphisms preserve the free FK probability · Automorphism as an isomorphism of open subgraphs · Boundary-preserving automorphisms preserve the wired FK probability · Boundary-preserving automorphism as an isomorphism of wired graphs · Pull-back along a permutation is relabelling · Relabelling as a permutation of the configuration space

DefinitionRelabelling as a permutation of the configuration space#✓fully proved

Relabelling by σ as a permutation of the configuration space, with inverse relabelling by σ⁻¹.

noncomputable def reCfgEquiv (σ : V ≃ V) :
    ConfigSpace (Sym2 V) ≃ ConfigSpace (Sym2 V) where
  toFun := reCfg σ
  invFun := reCfg σ.symm
  left_inv := fkTI_reCfg_reCfg σ
  right_inv := fkTI_reCfg_reCfg' σ

Uses 2 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Relabelling of an edge configuration by a vertex permutation

Used byGraph automorphisms preserve free FK edge marginals · Boundary-preserving automorphisms preserve wired FK edge marginals

DefinitionAutomorphism as an isomorphism of open subgraphs#✓fully proved

An automorphism σ of G is a graph isomorphism from the open subgraph of the relabelled configuration reCfg σ ω to the open subgraph of ω.

noncomputable def fkTI_openSubIso (σ : V ≃ V)
    (hσ : ∀ x y, G.Adj (σ x) (σ y) ↔ G.Adj x y) (ω : ConfigSpace (Sym2 V)) :
    openSub G (reCfg σ ω) ≃g openSub G ω where
  toEquiv := σ
  map_rel_iff' := by
    intro x y
    simp only [openSub_adj, reCfg]
    rw [Sym2.map_mk, hσ x y]

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of an edge configuration · Relabelling of an edge configuration by a vertex permutation

Used byGraph automorphisms preserve the free FK probability

LemmaGraph automorphisms preserve the free FK probability#✓fully proved

Graph automorphisms preserve the free FK probability. See also fvs_fkProb_reCfgIso for isomorphisms between two graphs.

lemma fkTI_fkProb_reCfg (σ : V ≃ V)
    (hσ : ∀ x y, G.Adj (σ x) (σ y) ↔ G.Adj x y) (p q : ℝ) (ω : ConfigSpace (Sym2 V)) :
    fkProb G p q (reCfg σ ω) = fkProb G p q ω

Uses 9 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration · Relabelling of an edge configuration by a vertex permutation

Proof usesBernoulli edge product · Automorphism as an isomorphism of open subgraphs · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · Open subgraph of an edge configuration

Used byGraph automorphisms preserve free FK edge marginals

DefinitionBoundary-preserving automorphism as an isomorphism of wired graphs#✓fully proved

An automorphism σ of G preserving the boundary set is a graph isomorphism between the wired graphs (open edges plus all boundary pairs) of reCfg σ ω and ω.

StatMech.FK.fkTI_wiredGraphIso · 16 lines

noncomputable def fkTI_wiredGraphIso (σ : V ≃ V)
    (hσ : ∀ x y, G.Adj (σ x) (σ y) ↔ G.Adj x y) (hbdry : ∀ x, bdry (σ x) ↔ bdry x)
    (ω : ConfigSpace (Sym2 V)) :
    StatMech.Lattice.wiredGraph G bdry (reCfg σ ω) ≃g StatMech.Lattice.wiredGraph G bdry ω where
  toEquiv := σ
  map_rel_iff' := by
    intro x y
    simp only [StatMech.Lattice.wiredGraph_adj, reCfg]
    rw [Sym2.map_mk, hσ x y, hbdry x, hbdry y]
    constructor
    · rintro (h | ⟨hne, hx, hy⟩)
      · exact Or.inl h
      · exact Or.inr ⟨fun h => hne (by rw [h]), hx, hy⟩
    · rintro (h | ⟨hne, hx, hy⟩)
      · exact Or.inl h
      · exact Or.inr ⟨fun h => hne (σ.injective h), hx, hy⟩

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Relabelling of an edge configuration by a vertex permutation · Complete graph on the boundary vertices · Open subgraph of a bond configuration · Boundary wiring relation · Wired open graph

Used byBoundary-preserving automorphisms preserve the wired FK probability

LemmaBoundary-preserving automorphisms preserve the wired FK probability#✓fully proved

Graph automorphisms preserving the boundary preserve the wired FK probability.

lemma fkTI_wiredFkProb_reCfg (σ : V ≃ V)
    (hσ : ∀ x y, G.Adj (σ x) (σ y) ↔ G.Adj x y) (hbdry : ∀ x, bdry (σ x) ↔ bdry x)
    (p q : ℝ) (ω : ConfigSpace (Sym2 V)) :
    wiredFkProb G bdry p q (reCfg σ ω) = wiredFkProb G bdry p q ω

Uses 13 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Relabelling of an edge configuration by a vertex permutation · Wired random-cluster probability of a configuration

Proof usesBernoulli edge product · Boundary-preserving automorphism as an isomorphism of wired graphs · Wired random-cluster weight · Wired random-cluster partition function · Open edge in a bond configuration · Complete graph on the boundary vertices · Number of open clusters with wired boundary conditions · Open subgraph of a bond configuration · Boundary wiring relation · Wired open graph

Used byBoundary-preserving automorphisms preserve wired FK edge marginals

LemmaGraph automorphisms preserve free FK edge marginals#✓fully proved

Under the free FK measure, the edges e and σ e are open with the same probability.

lemma fkTI_edgeMargProb_fkProb_reCfg (σ : V ≃ V)
    (hσ : ∀ x y, G.Adj (σ x) (σ y) ↔ G.Adj x y) (p q : ℝ) (e : Sym2 V) :
    edgeMargProb (fkProb G p q) (Sym2.map σ e) = edgeMargProb (fkProb G p q) e

Uses 6 · Used by 2

Statement usesEdge marginal of a mass function · Probability of an ambient FK configuration

Proof usesConfiguration space of a statistical-mechanics model · Graph automorphisms preserve the free FK probability · Relabelling of an edge configuration by a vertex permutation · Relabelling as a permutation of the configuration space

Used byPer-box uniqueness of the random-cluster measures off a countable set · Box symmetries preserve the free \(q = 2\) density of box edges

LemmaBoundary-preserving automorphisms preserve wired FK edge marginals#✓fully proved

Under the wired FK measure, the edges e and σ e are open with the same probability.

lemma fkTI_edgeMargProb_wiredFkProb_reCfg (σ : V ≃ V)
    (hσ : ∀ x y, G.Adj (σ x) (σ y) ↔ G.Adj x y) (hbdry : ∀ x, bdry (σ x) ↔ bdry x)
    (p q : ℝ) (e : Sym2 V) :
    edgeMargProb (wiredFkProb G bdry p q) (Sym2.map σ e)
      = edgeMargProb (wiredFkProb G bdry p q) e

Uses 6 · Used by 2

Statement usesEdge marginal of a mass function · Wired random-cluster probability of a configuration

Proof usesConfiguration space of a statistical-mechanics model · Boundary-preserving automorphisms preserve the wired FK probability · Relabelling of an edge configuration by a vertex permutation · Relabelling as a permutation of the configuration space

Used byPer-box uniqueness of the random-cluster measures off a countable set · Box symmetries preserve the wired \(q = 2\) density of box edges

StructureBox symmetry of \(\mathbb{Z}^d\)#✓fully proved

A symmetry of ℤ^d that preserves nearest-neighbour adjacency and every centered box Λ_n = [-n, n]^d, such as a coordinate reflection or a coordinate permutation.

structure BoxSym (d : ℕ) where
  /-- The underlying permutation of the sites. -/
  τ : Site d ≃ Site d
  /-- `τ` preserves nearest-neighbour adjacency. -/
  adj : ∀ x y, (hypercubicLattice d).Adj (τ x) (τ y) ↔ (hypercubicLattice d).Adj x y
  /-- `τ` maps each centered box onto itself. -/
  box_mem : ∀ n x, τ x ∈ box d n ↔ x ∈ box d n

Uses 3 · Used by 14

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byPer-box uniqueness of the random-cluster measures off a countable set · Unit edges at the origin have the free density of \(\{0, e_0\}\) · Box symmetries preserve the free \(q = 2\) density of any pair of sites · Coordinate permutation as a box symmetry · Unit edges at the origin have the wired density of \(\{0, e_0\}\) · Box symmetries preserve the wired \(q = 2\) density of any pair of sites · Box symmetries preserve the free \(q = 2\) density of box edges · Coordinate reflection as a box symmetry · Box symmetries preserve the wired \(q = 2\) density of box edges · Restriction of a box symmetry to a box · Free edge density is constant on orbits of a box symmetry · Free upper bound on expected open edges along a box-symmetry orbit · Wired edge density is constant on orbits of a box symmetry · Wired lower bound on expected open edges along a box-symmetry orbit

DefinitionRestriction of a box symmetry to a box#✓fully proved

The restriction of a box symmetry to a permutation of the vertices of the box Λ_n.

def BoxSym.lift (S : BoxSym d) (n : ℕ) : boxVerts d n ≃ boxVerts d n where
  toFun := fun x => ⟨S.τ x.val, (S.box_mem n x.val).mpr x.property⟩
  invFun := fun x => ⟨S.τ.symm x.val, by
    rw [← S.box_mem n (S.τ.symm x.val), Equiv.apply_symm_apply]; exact x.property⟩
  left_inv := by intro x; apply Subtype.ext; simp
  right_inv := by intro x; apply Subtype.ext; simp

Uses 4 · Used by 9

Statement usesBox symmetry of \(\mathbb{Z}^d\) · Vertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byPer-box uniqueness of the random-cluster measures off a countable set · Box symmetries preserve the free \(q = 2\) density of any pair of sites · Box symmetries preserve the wired \(q = 2\) density of any pair of sites · Box symmetries preserve the free \(q = 2\) density of box edges · Box symmetries preserve the wired \(q = 2\) density of box edges · Free edge density is constant on orbits of a box symmetry · Free upper bound on expected open edges along a box-symmetry orbit · Wired edge density is constant on orbits of a box symmetry · Wired lower bound on expected open edges along a box-symmetry orbit

LemmaBox symmetries preserve the wired \(q = 2\) density of box edges#✓fully proved

Box symmetries preserve the wired q = 2 infinite-volume edge density. See also rot_wired_density_boxSym for the statement on edges of ℤ^d.

lemma fkTI_wired_density_shift_inv (S : BoxSym d) (N : ℕ) (eb : Sym2 (boxVerts d N))
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    wiredEdgeDensity d 2 (edgeIncl d N eb) p
      = wiredEdgeDensity d 2 (edgeIncl d N (Sym2.map (S.lift N) eb)) p

Uses 27 · Used by 2

Statement usesBox symmetry of \(\mathbb{Z}^d\) · Restriction of a box symmetry to a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Wired infinite-volume edge density

Proof usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Event that a box edge is open · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Inclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Edge marginal of a mass function · Event that an edge is open · Boundary-preserving automorphisms preserve wired FK edge marginals · Wired infinite-volume measure as limit on increasing cylinder events · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired random-cluster measure on a box · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired random-cluster probability of a configuration · Wired infinite-volume random-cluster measure · Increasing event · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Inner vertex boundary of a box

Used byBox symmetries preserve the wired \(q = 2\) density of any pair of sites · Wired edge density is constant on orbits of a box symmetry

LemmaBox symmetries preserve the free \(q = 2\) density of box edges#✓fully proved

Box symmetries preserve the free q = 2 infinite-volume edge density. See also rot_free_density_boxSym for the statement on edges of ℤ^d.

lemma fkTI_free_density_shift_inv (S : BoxSym d) (N : ℕ) (eb : Sym2 (boxVerts d N))
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    freeEdgeDensity d 2 (edgeIncl d N eb) p
      = freeEdgeDensity d 2 (edgeIncl d N (Sym2.map (S.lift N) eb)) p

Uses 25 · Used by 2

Statement usesBox symmetry of \(\mathbb{Z}^d\) · Restriction of a box symmetry to a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density

Proof usesConfiguration space of a statistical-mechanics model · Event that a box edge is open · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Inclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Edge marginal of a mass function · Event that an edge is open · Probability of an ambient FK configuration · Graph automorphisms preserve free FK edge marginals · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Free random-cluster measure on a box · Free box measure of a cylinder event as a finite sum · Free infinite-volume random-cluster measure · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Increasing event · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byBox symmetries preserve the free \(q = 2\) density of any pair of sites · Free edge density is constant on orbits of a box symmetry

DefinitionReflection of \(\mathbb{Z}^d\) in one coordinate#✓fully proved

The reflection x ↦ x with the j-th coordinate negated.

def fkTI_signFlipEquiv (d : ℕ) (j : Fin d) : Site d ≃ Site d where
  toFun := fun x i => if i = j then -(x i) else x i
  invFun := fun x i => if i = j then -(x i) else x i
  left_inv := by intro x; funext i; by_cases h : i = j <;> simp [h]
  right_inv := by intro x; funext i; by_cases h : i = j <;> simp [h]

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byCoordinate reflection as a box symmetry

DefinitionCoordinate reflection as a box symmetry#✓fully proved

The reflection in the j-th coordinate as a box symmetry.

StatMech.FK.fkTI_signFlip · 25 lines

def fkTI_signFlip (d : ℕ) (j : Fin d) : BoxSym d where
  τ := fkTI_signFlipEquiv d j
  adj := by
    intro x y
    simp only [hypercubicLattice_adj, fkTI_signFlipEquiv, Equiv.coe_fn_mk]
    have hcoord : ∀ i : Fin d,
        ((if i = j then -(x i) else x i) - (if i = j then -(y i) else y i)).natAbs
          = (x i - y i).natAbs := by
      intro i
      by_cases hh : i = j
      · rw [ite_eq_left hh, ite_eq_left hh, show -(x i) - -(y i) = -(x i - y i) by ring,
          Int.natAbs_neg]
      · rw [ite_eq_right hh, ite_eq_right hh]
    rw [Finset.sum_congr rfl (fun i _ => hcoord i)]
  box_mem := by
    intro n x
    simp only [mem_box, fkTI_signFlipEquiv, Equiv.coe_fn_mk]
    have hcoord : ∀ i : Fin d, (if i = j then -(x i) else x i).natAbs = (x i).natAbs := by
      intro i
      by_cases hh : i = j
      · rw [ite_eq_left hh, Int.natAbs_neg]
      · rw [ite_eq_right hh]
    constructor
    · intro h i; rw [← hcoord i]; exact h i
    · intro h i; rw [hcoord i]; exact h i

Uses 5 · Used by 3

Statement usesBox symmetry of \(\mathbb{Z}^d\) · Reflection of \(\mathbb{Z}^d\) in one coordinate · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byPer-box uniqueness of the random-cluster measures off a countable set · Unit edges at the origin have the free density of \(\{0, e_0\}\) · Unit edges at the origin have the wired density of \(\{0, e_0\}\)

DefinitionPull-back of an edge configuration along a vertex bijection#✓fully proved

The pull-back of a configuration ω on the edges of W along σ : V ≃ W: the edge e is open in reCfgIso σ ω iff σ e is open in ω. For V = W it is reCfg (fvs_reCfgIso_eq_reCfg).

noncomputable def reCfgIso (σ : V ≃ W) (ω : ConfigSpace (Sym2 W)) : ConfigSpace (Sym2 V) :=
  fun e => ω (Sym2.map σ e)

Uses 1 · Used by 9

Statement usesConfiguration space of a statistical-mechanics model

Used byTranslation covariance of free box masses · Translation covariance of wired box masses · Boundary-matching isomorphisms transport FK edge marginals · Isomorphic graphs have equal free FK probabilities after relabelling · Open-subgraph isomorphism for a pulled-back configuration · Pull-back along a permutation is relabelling · Boundary-matching isomorphisms preserve wired FK probabilities · Wired-graph isomorphism for a pulled-back configuration · Pull-back of configurations as an equivalence

DefinitionPull-back of configurations as an equivalence#✓fully proved

Pull-back along σ as an equivalence of configuration spaces, with inverse the pull-back along σ⁻¹.

noncomputable def reCfgIsoEquiv (σ : V ≃ W) :
    ConfigSpace (Sym2 W) ≃ ConfigSpace (Sym2 V) where
  toFun := reCfgIso σ
  invFun := reCfgIso σ.symm
  left_inv := fvs_reCfgIso_reCfgIso σ
  right_inv := fvs_reCfgIso_reCfgIso' σ

Uses 2 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Pull-back of an edge configuration along a vertex bijection

Used byTranslation covariance of free box masses · Translation covariance of wired box masses · Boundary-matching isomorphisms transport FK edge marginals · Isomorphic graphs have equal free FK probabilities after relabelling · Boundary-matching isomorphisms preserve wired FK probabilities

LemmaPull-back along a permutation is relabelling#✓fully proved

For a permutation σ of V, pulling back along σ is the relabelling reCfg σ.

lemma fvs_reCfgIso_eq_reCfg (σ : V ≃ V) (ω : ConfigSpace (Sym2 V)) :
    reCfgIso σ ω = reCfg σ ω

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · Relabelling of an edge configuration by a vertex permutation · Pull-back of an edge configuration along a vertex bijection

DefinitionOpen-subgraph isomorphism for a pulled-back configuration#✓fully proved

An isomorphism σ : G ≃ H is a graph isomorphism from the open subgraph of the pulled-back configuration reCfgIso σ ω to the open subgraph of ω.

noncomputable def fvs_openSubIso (σ : V ≃ W)
    (hσ : ∀ x y, G.Adj x y ↔ H.Adj (σ x) (σ y)) (ω : ConfigSpace (Sym2 W)) :
    openSub G (reCfgIso σ ω) ≃g openSub H ω where
  toEquiv := σ
  map_rel_iff' := by
    intro x y
    simp only [openSub_adj, reCfgIso]
    rw [Sym2.map_mk, hσ x y]

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of an edge configuration · Pull-back of an edge configuration along a vertex bijection

Used byIsomorphic graphs have equal free FK probabilities after relabelling

LemmaIsomorphic graphs have equal free FK probabilities after relabelling#✓fully proved

Isomorphic graphs have the same free FK probability, up to relabelling by the isomorphism. See also fkTI_fkProb_reCfg, the special case of an automorphism.

lemma fvs_fkProb_reCfgIso (σ : V ≃ W)
    (hσ : ∀ x y, G.Adj x y ↔ H.Adj (σ x) (σ y)) (p q : ℝ) (ω : ConfigSpace (Sym2 W)) :
    fkProb G p q (reCfgIso σ ω) = fkProb H p q ω

Uses 10 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Probability of an ambient FK configuration · Pull-back of an edge configuration along a vertex bijection

Proof usesBernoulli edge product · Unnormalized random-cluster weight · Ambient FK normalizer · Open-subgraph isomorphism for a pulled-back configuration · Number of open clusters · Open subgraph of an edge configuration · Pull-back of configurations as an equivalence

Used byTranslation covariance of free box masses · Boundary-matching isomorphisms transport FK edge marginals

DefinitionWired-graph isomorphism for a pulled-back configuration#✓fully proved

An isomorphism σ : G ≃ H matching the boundary sets is a graph isomorphism between the wired graphs of reCfgIso σ ω and ω.

StatMech.FK.fvs_wiredGraphIso · 17 lines

noncomputable def fvs_wiredGraphIso (σ : V ≃ W)
    (hσ : ∀ x y, G.Adj x y ↔ H.Adj (σ x) (σ y)) (hbdry : ∀ x, bdryV x ↔ bdryW (σ x))
    (ω : ConfigSpace (Sym2 W)) :
    StatMech.Lattice.wiredGraph G bdryV (reCfgIso σ ω)
      ≃g StatMech.Lattice.wiredGraph H bdryW ω where
  toEquiv := σ
  map_rel_iff' := by
    intro x y
    simp only [StatMech.Lattice.wiredGraph_adj, reCfgIso]
    rw [Sym2.map_mk, hσ x y, hbdry x, hbdry y]
    constructor
    · rintro (h | ⟨hne, hx, hy⟩)
      · exact Or.inl h
      · exact Or.inr ⟨fun h => hne (by rw [h]), hx, hy⟩
    · rintro (h | ⟨hne, hx, hy⟩)
      · exact Or.inl h
      · exact Or.inr ⟨fun h => hne (σ.injective h), hx, hy⟩

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Pull-back of an edge configuration along a vertex bijection · Complete graph on the boundary vertices · Open subgraph of a bond configuration · Boundary wiring relation · Wired open graph

Used byBoundary-matching isomorphisms preserve wired FK probabilities

LemmaBoundary-matching isomorphisms preserve wired FK probabilities#✓fully proved

Isomorphic graphs with matching boundary sets have the same wired FK probability, up to relabelling. See also fkTI_wiredFkProb_reCfg.

lemma fvs_wiredFkProb_reCfgIso (σ : V ≃ W)
    (hσ : ∀ x y, G.Adj x y ↔ H.Adj (σ x) (σ y)) (hbdry : ∀ x, bdryV x ↔ bdryW (σ x))
    (p q : ℝ) (ω : ConfigSpace (Sym2 W)) :
    wiredFkProb G bdryV p q (reCfgIso σ ω) = wiredFkProb H bdryW p q ω

Uses 14 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Pull-back of an edge configuration along a vertex bijection · Wired random-cluster probability of a configuration

Proof usesBernoulli edge product · Wired-graph isomorphism for a pulled-back configuration · Pull-back of configurations as an equivalence · Wired random-cluster weight · Wired random-cluster partition function · Open edge in a bond configuration · Complete graph on the boundary vertices · Number of open clusters with wired boundary conditions · Open subgraph of a bond configuration · Boundary wiring relation · Wired open graph

Used byTranslation covariance of wired box masses · Boundary-matching isomorphisms transport FK edge marginals

LemmaBoundary-matching isomorphisms transport FK edge marginals#✓fully proved

Graph isomorphisms transport the wired and the free FK edge marginals: σ e is open in H with the same probability as e in G.

lemma fvs_finiteVolume_shift_invariant (σ : V ≃ W)
    (hσ : ∀ x y, G.Adj x y ↔ H.Adj (σ x) (σ y)) (hbdry : ∀ x, bdryV x ↔ bdryW (σ x))
    (p q : ℝ) (e : Sym2 V) :
    edgeMargProb (wiredFkProb H bdryW p q) (Sym2.map σ e)
        = edgeMargProb (wiredFkProb G bdryV p q) e
      ∧ edgeMargProb (fkProb H p q) (Sym2.map σ e) = edgeMargProb (fkProb G p q) e

Uses 8 · Used by 1

Statement usesEdge marginal of a mass function · Probability of an ambient FK configuration · Wired random-cluster probability of a configuration

Proof usesConfiguration space of a statistical-mechanics model · Isomorphic graphs have equal free FK probabilities after relabelling · Boundary-matching isomorphisms preserve wired FK probabilities · Pull-back of an edge configuration along a vertex bijection · Pull-back of configurations as an equivalence

Used byTranslation covariance of FK edge marginals on boxes

DefinitionTranslated box in \(\mathbb{Z}^d\)#✓fully proved

The translated box v + Λ_m = {y ∈ ℤ^d : ‖y - v‖_∞ ≤ m}.

def fvs_transBox (d m : ℕ) (v : Site d) : Set (Site d) := {y | (y - v) ∈ box d m}

Uses 2 · Used by 34

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

Used byTranslation covariance of free box masses · Translation covariance of wired box masses · Free translation invariance from free placements of every shift · Equal free probabilities from eventually equal translated masses · Free placement for a shift via eventually equal box masses · Difference of wired all-open masses of an edge set and its translate · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Wired placement for a shift via eventually equal box masses · Off-centre carrier vanishes by translation covariance · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Wired-marginal difference between a box and its translate · 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 covariance of FK edge marginals on boxes · Vertex boundary of a translated box · Nearest-neighbour graph on a translated box · Some translated box leaves the centered box for \(d \ge 1\) · Vertex type of a translated box · Translation from the centered box onto a translated box · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure · Box edge set included into \(\Lambda_m\) and translated by \(v\) · Translation invariance of the wired \(q = 2\) infinite-volume measure · Wired all-open probability on a translated box · Translated wired box mass equals the centered box mass · Translated free box mass of an edge set · Translated free box mass equals the centred box probability · Edge inclusion of a translated box into \(\mathbb{Z}^d\) · Translated box edges are shifted centered box edges · Images of translated edge sets are shifted images

AbbreviationVertex type of a translated box#✓fully proved

The vertices of the translated box v + Λ_m, as a subtype of ℤ^d.

abbrev fvs_transBoxVerts (d m : ℕ) (v : Site d) : Type :=
  {y : Site d // y ∈ fvs_transBox d m v}

Uses 2 · Used by 32

Statement usesTranslated box in \(\mathbb{Z}^d\) · Site of the hypercubic lattice

Used byTranslation covariance of free box masses · Translation covariance of wired box masses · Free translation invariance from free placements of every shift · Equal free probabilities from eventually equal translated masses · Free placement for a shift via eventually equal box masses · Difference of wired all-open masses of an edge set and its translate · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Wired placement for a shift via eventually equal box masses · Off-centre carrier vanishes by translation covariance · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Wired-marginal difference between a box and its translate · 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 covariance of FK edge marginals on boxes · Vertex boundary of a translated box · Nearest-neighbour graph on a translated box · Translation from the centered box onto a translated box · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure · Box edge set included into \(\Lambda_m\) and translated by \(v\) · Translation invariance of the wired \(q = 2\) infinite-volume measure · Wired all-open probability on a translated box · Translated wired box mass equals the centered box mass · Translated free box mass of an edge set · Translated free box mass equals the centred box probability · Edge inclusion of a translated box into \(\mathbb{Z}^d\) · Translated box edges are shifted centered box edges · Images of translated edge sets are shifted images

DefinitionTranslation from the centered box onto a translated box#✓fully proved

The translation x ↦ x + v from the centered box Λ_m onto v + Λ_m.

noncomputable def fvs_transEquiv (d m : ℕ) (v : Site d) :
    boxVerts d m ≃ fvs_transBoxVerts d m v where
  toFun := fun x => ⟨(x : Site d) + v, by
    change ((x : Site d) + v - v) ∈ box d m
    rw [add_sub_cancel_right]; exact x.2⟩
  invFun := fun y => ⟨(y : Site d) - v, y.2⟩
  left_inv := by intro x; apply Subtype.ext; simp
  right_inv := by intro y; apply Subtype.ext; simp

Uses 5 · Used by 28

Statement usesVertices of the box \((-n, n)^d\) · Translated box in \(\mathbb{Z}^d\) · Vertex type of a translated box · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byTranslation covariance of free box masses · Translation covariance of wired box masses · Free translation invariance from free placements of every shift · Equal free probabilities from eventually equal translated masses · Free placement for a shift via eventually equal box masses · Difference of wired all-open masses of an edge set and its translate · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Wired placement for a shift via eventually equal box masses · Off-centre carrier vanishes by translation covariance · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Wired-marginal difference between a box and its translate · 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 covariance of FK edge marginals on boxes · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure · Box edge set included into \(\Lambda_m\) and translated by \(v\) · Translation invariance of the wired \(q = 2\) infinite-volume measure · Wired all-open probability on a translated box · Translated wired box mass equals the centered box mass · Translated free box mass of an edge set · Translated free box mass equals the centred box probability · Translated box edges are shifted centered box edges · Images of translated edge sets are shifted images

DefinitionNearest-neighbour graph on a translated box#✓fully proved

The nearest-neighbour graph of ℤ^d restricted to v + Λ_m.

def fvs_transBoxGraph (d m : ℕ) (v : Site d) : SimpleGraph (fvs_transBoxVerts d m v) :=
  SimpleGraph.comap Subtype.val (hypercubicLattice d)

Uses 4 · Used by 24

Statement usesTranslated box in \(\mathbb{Z}^d\) · Vertex type of a translated box · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byTranslation covariance of free box masses · Translation covariance of wired box masses · Free translation invariance from free placements of every shift · Equal free probabilities from eventually equal translated masses · Free placement for a shift via eventually equal box masses · Difference of wired all-open masses of an edge set and its translate · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Wired placement for a shift via eventually equal box masses · Off-centre carrier vanishes by translation covariance · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Wired-marginal difference between a box and its translate · 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 covariance of FK edge marginals on boxes · Ergodicity of the wired random-cluster measure · Translation invariance of the wired \(q = 2\) infinite-volume measure · Wired all-open probability on a translated box · Translated wired box mass equals the centered box mass · Translated free box mass of an edge set · Translated free box mass equals the centred box probability

DefinitionVertex boundary of a translated box#✓fully proved

The vertex boundary of v + Λ_m: the translate of the vertex boundary of Λ_m.

def fvs_transBoxBoundary (d m : ℕ) (v : Site d) (y : fvs_transBoxVerts d m v) : Prop :=
  ((y : Site d) - v) ∈ vertexBoundary d m

Uses 4 · Used by 18

Statement usesTranslated box in \(\mathbb{Z}^d\) · Vertex type of a translated box · Site of the hypercubic lattice · Inner vertex boundary of a box

Used byTranslation covariance of wired box masses · Difference of wired all-open masses of an edge set and its translate · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Wired placement for a shift via eventually equal box masses · Off-centre carrier vanishes by translation covariance · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Wired-marginal difference between a box and its translate · 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 covariance of FK edge marginals on boxes · Ergodicity of the wired random-cluster measure · Translation invariance of the wired \(q = 2\) infinite-volume measure · Wired all-open probability on a translated box · Translated wired box mass equals the centered box mass

LemmaTranslation covariance of FK edge marginals on boxes#✓fully proved

The wired and free FK edge marginals on the translated box v + Λ_m are the marginals on the centered box Λ_m, transported by x ↦ x + v.

lemma fvs_box_translation_edgeMarg (d m : ℕ) (v : Site d) (eb : Sym2 (boxVerts d m))
    {p q : ℝ} :
    edgeMargProb (wiredFkProb (fvs_transBoxGraph d m v) (fvs_transBoxBoundary d m v) p q)
          (Sym2.map (fvs_transEquiv d m v) eb)
        = edgeMargProb (wiredFkProb (boxGraph d m) (boxBoundary d m) p q) eb
      ∧ edgeMargProb (fkProb (fvs_transBoxGraph d m v) p q) (Sym2.map (fvs_transEquiv d m v) eb)
        = edgeMargProb (fkProb (boxGraph d m) p q) eb

Uses 16 · Used by 6

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Edge marginal of a mass function · Probability of an ambient FK configuration · Translated box in \(\mathbb{Z}^d\) · Vertex boundary of a translated box · Nearest-neighbour graph on a translated box · Vertex type of a translated box · Translation from the centered box onto a translated box · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesBoundary-matching isomorphisms transport FK edge marginals · Hypercubic lattice \(\mathbb{Z}^d\) · Inner vertex boundary of a box

Used byOff-centre carrier vanishes by translation covariance · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · 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

LemmaSome translated box leaves the centered box for \(d \ge 1\)#✓fully proved

For d ≥ 1, some translated box v + Λ_m is not contained in Λ_m, so translation is not a box symmetry in the sense of BoxSym.

lemma fvs_transBox_ne_box (d m : ℕ) (hd : 0 < d) :
    ∃ (v y : Site d), y ∈ fvs_transBox d m v ∧ y ∉ box d m

Uses 3

Statement usesTranslated box in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

LemmaMonotonicity of the open subgraph in the configuration#✓fully proved

The open subgraph is monotone in the configuration. The same statement is StatMech.Sharpness.openSub_mono in BkCriterion.

lemma openSub_mono {a b : ConfigSpace (Sym2 V)} (hab : a ≤ b) :
    openSub G a ≤ openSub G b

Uses 2 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of an edge configuration

Used byClosed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Convergence to the free two-point function under stochastic increase · Convergence to the wired two-point function under stochastic decrease · Origin-to-boundary connection is an increasing event · Boundary-connection event of \(\Lambda_n\) on \(\Lambda_m\) is increasing · FKG inequality for connection events for \(q \ge 1\)

DefinitionEvent that two vertices are joined by open edges#✓fully proved

The event that x and y are joined by a path of open edges of G.

def connEvent (x y : V) : Set (ConfigSpace (Sym2 V)) :=
  {ω | (openSub G ω).Reachable x y}

Uses 2 · Used by 11

Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of an edge configuration

Used byBox-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Event that two sites are joined by open edges inside a box · Free box measure of a box connection event is the two-point function · Convergence to the free two-point function under stochastic increase · Convergence to the wired two-point function under stochastic decrease · Cylinder form of the \(\Lambda_n\) boundary connection is measurable · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\) · Two-point function of the free random-cluster measure · FKG inequality for connection events for \(q \ge 1\)

DefinitionTwo-point function of the free random-cluster measure#✓fully proved

The two-point function of the free random-cluster measure on a finite graph: the probability φ(x ↔ y) that x and y are connected by open edges.

noncomputable def twoPointFun (p q : ℝ) (x y : V) : ℝ :=
  ∑ ω, fkProb G p q ω * (connEvent G x y).indicator (fun _ => (1 : ℝ)) ω

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Event that two vertices are joined by open edges · Probability of an ambient FK configuration

Used byFree box measure of a box connection event is the two-point function · FKG inequality for connection events for \(q \ge 1\)

LemmaFKG inequality for connection events for \(q \ge 1\)#✓fully proved

FKG for connection events: for q ≥ 1, φ(x ↔ y) φ(u ↔ v) ≤ φ(x ↔ y, u ↔ v).

lemma twoPointFun_fkg {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 1 ≤ q)
    (x y u v : V) :
    twoPointFun G p q x y * twoPointFun G p q u v
      ≤ ∑ ω, fkProb G p q ω *
          (connEvent G x y ∩ connEvent G u v).indicator (fun _ => (1 : ℝ)) ω

Uses 8

Statement usesConfiguration space of a statistical-mechanics model · Event that two vertices are joined by open edges · Probability of an ambient FK configuration · Two-point function of the free random-cluster measure

Proof usesFKG inequality for increasing random-cluster events · Open subgraph of an edge configuration · Monotonicity of the open subgraph in the configuration · Increasing event

77 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.