Per-box agreement of free and wired random-cluster measures

DefinitionWired-marginal difference between a box and its translate#✓fully proved

The difference between the wired marginal of eb' on Λ_{N+k} and on the translate of Λ_{N+k} by v, evaluated at the translated edge.

noncomputable def fbd_offCentreCarrier (N : ℕ) (v : Site d) (eb' : Sym2 (boxVerts d N))
    (p q : ℝ) (k : ℕ) : ℝ :=
  edgeMargProb (wiredFkProb (boxGraph d (N + k)) (boxBoundary d (N + k)) p q)
      (innerEdgeLE d (Nat.le_add_right N k) eb')
    - edgeMargProb
        (wiredFkProb (fvs_transBoxGraph d (N + k) v) (fvs_transBoxBoundary d (N + k) v) p q)
        (Sym2.map (fvs_transEquiv d (N + k) v) (innerEdgeLE d (Nat.le_add_right N k) eb'))

Uses 13 · Used by 3

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 · 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 · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byOff-centre carrier tends to zero · Off-centre carrier vanishes by translation covariance · Equal wired densities from equal translated marginals

LemmaMonotone-coupled laws with equal edge marginals agree on up-sets#✓fully proved

Two monotonically coupled probability vectors with equal edge marginals agree on increasing events. Restatement of eventMass_eq_of_edgeMarg_eq (EdgeMarginal), kept because other modules use this name.

lemma fk_unique_of_edgeMarg_eq {P : ConfigSpace E × ConfigSpace E → ℝ}
    {μ ν : ConfigSpace E → ℝ} (hP : IsMonotoneCouplingFun P μ ν)
    (hmarg : ∀ e : E, edgeMargProb μ e = edgeMargProb ν e)
    {A : Set (ConfigSpace E)} (hA : IsIncreasing A) :
    eventMassProb μ A = eventMassProb ν A

Uses 6 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Monotone coupling of two mass functions · Edge marginal of a mass function · Mass of an event under a mass function · Increasing event

Proof usesMonotone couplings with equal edge marginals agree on up-sets

Used byCountably many parameters admit a separating increasing event · Per-box uniqueness of the random-cluster measures off a countable set · Parametric agreement on increasing events off a countable set

LemmaAgreement with a monotone map at continuity points fails countably#✓fully proved

If a agrees with a monotone b at every continuity point of b, then {p | a p ≠ b p} is countable.

lemma countable_edgeMarg_ne (hb : Monotone b)
    (heq_at_cont : ∀ p : ℝ, ContinuousAt b p → a p = b p) :
    {p : ℝ | a p ≠ b p}.Countable

LemmaParametric agreement on increasing events off a countable set#✓fully proved

Parametric agreement: if for each p there is a monotone coupling of μ p and ν p, and edge marginals agree at every continuity point of the monotone map p ↦ ν_p(ω(e) = 1), then μ p and ν p agree on increasing events for all p outside a countable set.

lemma phi0_eq_phi1_off_countable
    (μ ν : ℝ → ConfigSpace E → ℝ) (e : E)
    (P : ℝ → ConfigSpace E × ConfigSpace E → ℝ)
    (hcoup : ∀ p, IsMonotoneCouplingFun (P p) (μ p) (ν p))
    (hb : Monotone (fun p => edgeMargProb (ν p) e))
    (heq_at_cont : ∀ p : ℝ, ContinuousAt (fun p => edgeMargProb (ν p) e) p →
      ∀ e' : E, edgeMargProb (μ p) e' = edgeMargProb (ν p) e') :
    ∃ S : Set ℝ, S.Countable ∧
      ∀ p ∉ S, ∀ {A : Set (ConfigSpace E)}, IsIncreasing A →
        eventMassProb (μ p) A = eventMassProb (ν p) A

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Monotone coupling of two mass functions · Edge marginal of a mass function · Mass of an event under a mass function · Increasing event

Proof usesMonotone-coupled laws with equal edge marginals agree on up-sets

Used byCoupled measures agree off a countable set, given a convex pressure

LemmaCountably many parameters admit a separating increasing event#✓fully proved

Under the hypotheses of phi0_eq_phi1_off_countable, the set of p for which some increasing event separates μ p and ν p is countable.

lemma countable_phi_ne
    (μ ν : ℝ → ConfigSpace E → ℝ) (e : E)
    (P : ℝ → ConfigSpace E × ConfigSpace E → ℝ)
    (hcoup : ∀ p, IsMonotoneCouplingFun (P p) (μ p) (ν p))
    (hb : Monotone (fun p => edgeMargProb (ν p) e))
    (heq_at_cont : ∀ p : ℝ, ContinuousAt (fun p => edgeMargProb (ν p) e) p →
      ∀ e' : E, edgeMargProb (μ p) e' = edgeMargProb (ν p) e') :
    {p : ℝ | ∃ A : Set (ConfigSpace E), IsIncreasing A ∧
        eventMassProb (μ p) A ≠ eventMassProb (ν p) A}.Countable

Uses 6 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Monotone coupling of two mass functions · Edge marginal of a mass function · Mass of an event under a mass function · Increasing event

Proof usesMonotone-coupled laws with equal edge marginals agree on up-sets

Used bySet where coupled measures differ is countable under a convex pressure · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\)

DefinitionEvent that an edge is open#✓fully proved

The event that the edge e is open.

def fkEdgeOpenEvent {E : Type*} (e : E) : Set (ConfigSpace E) := {ω | ω e = true}

Uses 1 · Used by 30

Statement usesConfiguration space of a statistical-mechanics model

Used byLeft-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · Wired \(q = 2\) edge density is monotone in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Secant bound gives free–wired density agreement off a countable set · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Per-box \(q = 2\) uniqueness off a countable set of tilts · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free infinite-volume edge density · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Free unit-edge marginals converge to the free density · Wired unit-edge marginals converge to the wired density · Every lattice edge has the free \(q = 2\) density of \(\{0, e_0\}\) · Every lattice edge has the wired \(q = 2\) density of \(\{0, e_0\}\) · Free \(q = 2\) edge density lies in \((0, 1)\) · Wired \(q = 2\) edge density lies in \((0, 1)\) · Wired infinite-volume edge density · Box symmetries preserve the free \(q = 2\) density of box edges · Box symmetries preserve the wired \(q = 2\) density of box edges · Free \(q = 2\) box edge marginals are at most the free density · Wired \(q = 2\) box edge marginals are at least the wired density · Constant free density gives an upper bound on expected open edges · Equal free densities from merging free marginals · Constant wired density gives a lower bound on expected open edges · Equal wired densities from merging wired marginals · Decay of the edge-indicator functional from equal wired densities

DefinitionWired infinite-volume edge density#✓fully proved

The edge density φ^1_{p,q}(e open) of the wired infinite-volume random-cluster measure on ℤ^d, set to 0 outside p ∈ (0, 1), q > 0.

noncomputable def wiredEdgeDensity (d : ℕ) (q : ℝ) (e : Sym2 (Site d)) (p : ℝ) : ℝ :=
  if h : 0 < p ∧ p < 1 ∧ 0 < q then
    (wiredInfiniteVolume d h.1 h.2.1 h.2.2 : Measure (ConfigSpace (Sym2 (Site d)))).real
      (fkEdgeOpenEvent e)
  else 0

Uses 4 · Used by 47

Statement usesConfiguration space of a statistical-mechanics model · Event that an edge is open · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Used byWired edge densities on a box as right derivatives · Wired edge densities on a box bounded by right derivatives · Finite-volume tilt data for a box edge at \(q = 2\) · Infinite-volume edge densities as one-sided derivatives · Convex free-energy hypothesis for a box edge at \(q = 2\) · Convex free energy gives wired density at \(p'\) at most free at \(p > p'\) · Tilt data give wired density at \(p'\) at most free density at \(p > p'\) · Wired \(q = 2\) edge density is monotone in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Average wired density collapse at \(q = 2\) · Secant bound gives free–wired density agreement off a countable set · 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–free gap in the \(q = 2\) density of a box edge · Per-box \(q = 2\) uniqueness off a countable set of tilts · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Total deviation of wired unit-edge marginals from a wired density · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Wired average edge density collapse on boxes · Wired densities of genuine box edges as right derivatives · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Homogeneous free-energy data on a box at \(q = 2\) · Two-sided wired \(q = 2\) bulk bounds from the wired sandwich · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Wired unit-edge marginals converge to the wired density · Upper bound on wired bulk edge marginals · Total deviation of wired unit-edge marginals from the density · Wired off-centre sandwich from wired rotation residues · Wired rotation residue for a box pair · 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 · Every lattice edge has the wired \(q = 2\) density of \(\{0, e_0\}\) · All box edges have the same wired \(q = 2\) density · Wired \(q = 2\) edge density lies in \((0, 1)\) · Wired uniform bulk deviation at \(q = 2\) · Box symmetries preserve the wired \(q = 2\) density of box edges · Wired off-centre sandwich hypothesis · Wired \(q = 2\) box edge marginals are at least the wired density · Translation invariance of free and wired densities if marginals merge · Wired edge density is constant on orbits of a box symmetry · Constant wired density gives a lower bound on expected open edges · Wired lower bound on expected open edges along a box-symmetry orbit · Equal wired densities from merging wired marginals · Translation invariance of the wired density given merging marginals · Decay of the edge-indicator functional from equal wired densities

DefinitionFree infinite-volume edge density#✓fully proved

The edge density φ^0_{p,q}(e open) of the free infinite-volume random-cluster measure on ℤ^d, set to 0 outside p ∈ (0, 1), q > 0.

noncomputable def freeEdgeDensity (d : ℕ) (q : ℝ) (e : Sym2 (Site d)) (p : ℝ) : ℝ :=
  if h : 0 < p ∧ p < 1 ∧ 0 < q then
    (freeInfiniteVolume d h.1 h.2.1 h.2.2 : Measure (ConfigSpace (Sym2 (Site d)))).real
      (fkEdgeOpenEvent e)
  else 0

Uses 4 · Used by 45

Statement usesConfiguration space of a statistical-mechanics model · Event that an edge is open · Free infinite-volume random-cluster measure · Site of the hypercubic lattice

Used byFree edge densities on a box as left derivatives · Finite-volume tilt data for a box edge at \(q = 2\) · Collapse of average edge densities to the free density · Infinite-volume edge densities as one-sided derivatives · Convex free-energy hypothesis for a box edge at \(q = 2\) · Convex free energy gives wired density at \(p'\) at most free at \(p > p'\) · Tilt data give wired density at \(p'\) at most free density at \(p > p'\) · Left-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · Secant bound gives free–wired density agreement off a countable set · Free density is at most each translated wired marginal · Wired–free gap in the \(q = 2\) density of a box edge · Per-box \(q = 2\) uniqueness off a countable set of tilts · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Total deviation of free unit-edge marginals from a free density · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free average edge density collapse on boxes · Free densities of genuine box edges as left derivatives · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Homogeneous free-energy data on a box at \(q = 2\) · 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 · Total deviation of free unit-edge marginals from the density · Free off-centre sandwich from free rotation residues · Free rotation residue for a box pair · Free unit-edge marginals converge to the free density · 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 · Every lattice edge has the free \(q = 2\) density of \(\{0, e_0\}\) · All box edges have the same free \(q = 2\) density · Free \(q = 2\) edge density lies in \((0, 1)\) · Free growing-box collapse at \(q = 2\) · Free uniform bulk deviation at \(q = 2\) · Box symmetries preserve the free \(q = 2\) density of box edges · 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 · Free edge density is constant on orbits of a box symmetry · 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

DefinitionWired–free gap in the \(q = 2\) density of a box edge#✓fully proved

The gap φ^1_{p,2}(eb open) - φ^0_{p,2}(eb open) between the wired and free infinite-volume densities of the edge eb of Λ_N.

noncomputable def docGap (d N : ℕ) (eb : Sym2 (boxVerts d N)) (p : ℝ) : ℝ :=
  wiredEdgeDensity d 2 (edgeIncl d N eb) p - freeEdgeDensity d 2 (edgeIncl d N eb) p

Uses 4

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density · Wired infinite-volume edge density

LemmaShell edge fraction is at most \(4d^2(n-m)/n\)#✓fully proved

The fraction of ordered edges of Λ_n outside Λ_m is at most 4 d² (n - m)/n.

lemma ocs_edgeCard_shell_fraction_le (d : ℕ) (hd : 1 ≤ d) (n m : ℕ) (hn : 1 ≤ n) (hmn : m ≤ n) :
    ((boxSV_edgeCard d n - boxSV_edgeCard d m : ℕ) : ℝ) / (boxSV_edgeCard d n)
      ≤ 4 * (d : ℝ) ^ 2 * (((n - m : ℕ) : ℝ) / n)

Uses 10 · Used by 1

Statement usesNumber of nearest-neighbour pairs inside the box \((-n, n)^d\)

Proof usesNearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) as a finite set of sites · Nearest-neighbour pairs inside the box \((-n, n)^d\) · Box sites with a forward neighbour in the box · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Hypercubic lattice \(\mathbb{Z}^d\) · Shift of a site along a coordinate

Used byVanishing shell edge fraction when \((n - m(n))/n \to 0\)

LemmaVanishing shell edge fraction when \((n - m(n))/n \to 0\)#✓fully proved

If (n - m(n))/n → 0, the edges of Λ_n outside Λ_{m(n)} form a vanishing fraction of the edges of Λ_n.

lemma ocs_edgeFinset_shell_fraction_tendsto_zero (d : ℕ) (hd : 1 ≤ d) (m : ℕ → ℕ)
    (hm : ∀ n, m n ≤ n) (hgap : Tendsto (fun n => ((n - m n : ℕ) : ℝ) / n) atTop (𝓝 0)) :
    Tendsto (fun n => (((boxGraph d n).edgeFinset.card
          - (boxGraph d (m n)).edgeFinset.card : ℝ))
        / (boxGraph d n).edgeFinset.card) atTop (𝓝 0)

Uses 9 · Used by 5

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesShell edge fraction is at most \(4d^2(n-m)/n\) · Box \((-n, n)^d\) as a finite set of sites · Number of nearest-neighbour pairs inside the box \((-n, n)^d\) · Nearest-neighbour pairs inside the box \((-n, n)^d\) · Hypercubic lattice \(\mathbb{Z}^d\)

Used byPer-box uniqueness of the random-cluster measures off a countable set · Free \(q = 2\) bulk sandwich from equal free edge densities · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Free off-centre sandwich from free rotation residues · Wired off-centre sandwich from wired rotation residues

LemmaFree off-centre lower bound by the recentred small-box marginal#✓fully proved

For u, v adjacent in Λ_{n-R}, the free marginal in Λ_n of the edge {u, v} is at least the free marginal in Λ_R of the recentered edge {0, v - u}.

lemma ocs_free_offCentre_lower (d R n : ℕ) (hRn : R ≤ n) (hmn : n - R ≤ n)
    (u v : boxVerts d (n - R)) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (c0 : (0 : Site d) ∈ box d R) (cw : ((v : Site d) - (u : Site d)) ∈ box d R) :
    edgeMargProb (fkProb (boxGraph d R) p 2)
        (s((⟨(0 : Site d), c0⟩ : boxVerts d R), (⟨(v : Site d) - (u : Site d), cw⟩ : boxVerts d R)))
      ≤ edgeMargProb (fkProb (boxGraph d n) p 2)
          (innerEdgeLE d hmn (s(u, v) : Sym2 (boxVerts d (n - R))))

Uses 51 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Edge marginal of a mass function · Probability of an ambient FK configuration · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Empty wiring gives the free random-cluster measure · Random-cluster comparison of boundary conditions for \(q \ge 1\) · Random-cluster weight with a boundary wiring · Partition function with a boundary wiring · Empty boundary predicate · Vertex boundary of a box · Inclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Conditional random-cluster measure with a boundary wiring · Fibre of configurations agreeing off an edge set · Bernoulli edge product · Unnormalized random-cluster weight · Ambient FK normalizer · Inclusion of a subset of sites into a larger one · Translation covariance of FK edge marginals on boxes · 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 · Event that all edges of a finite set are open · Mass of the all-open event under a weight function · Number of open clusters · Number of clusters under a boundary wiring · Adjacency matching of the inner embedding · Law of total probability over outside configurations · Conditional outer probability as an induced-wiring probability · Wiring induced on the inner graph · Image of an inner-graph edge in the outer graph · Finite set of inner edges · Restriction of an outer configuration to inner edges · Restriction pulls back all-open events to their images · Restricting a glued configuration recovers the inner one · Lattice inclusion matches induced adjacency · Projection closing every inner edge · Gluing of inner and outer configurations · Outer wired fibre masses sum to one · Open subgraph of an edge configuration · Wired random-cluster probability of a configuration · Increasing event · Complete graph on the boundary vertices · Hypercubic lattice \(\mathbb{Z}^d\) · Boundary wiring relation

Used byLower bound on free bulk edge marginals

LemmaWired off-centre upper bound by the recentred small-box marginal#✓fully proved

For u, v adjacent in Λ_{n-R-1} and R ≥ 1, the wired marginal in Λ_n of {u, v} is at most the wired marginal in Λ_R of the recentered edge {0, v - u}.

lemma ocs_wired_offCentre_upper (d R n : ℕ) (hR : 1 ≤ R) (hRn1 : R + 1 ≤ n) (hmn : n - R - 1 ≤ n)
    (u v : boxVerts d (n - R - 1)) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (c0 : (0 : Site d) ∈ box d R) (cw : ((v : Site d) - (u : Site d)) ∈ box d R) :
    edgeMargProb (wiredFkProb (boxGraph d n) (boxBoundary d n) p 2)
        (innerEdgeLE d hmn (s(u, v) : Sym2 (boxVerts d (n - R - 1))))
      ≤ edgeMargProb (wiredFkProb (boxGraph d R) (boxBoundary d R) p 2)
          (s((⟨(0 : Site d), c0⟩ : boxVerts d R),
            (⟨(v : Site d) - (u : Site d), cw⟩ : boxVerts d R)))

Uses 24 · Used by 1

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 · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Inclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Probability of an ambient FK configuration · Inclusion of a subset of sites into a larger one · Translation covariance of FK edge marginals on boxes · 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 · Event that all edges of a finite set are open · Mass of the all-open event under a weight function · Image of an inner-graph edge in the outer graph · Outer wired all-open probability at most the inner wired one · Nearest neighbours in \(\mathbb{Z}^d\) · Hypercubic lattice \(\mathbb{Z}^d\)

Used byUpper bound on wired bulk edge marginals

LemmaAdjacent box vertices differ by a signed unit vector#✓fully proved

The difference of adjacent box vertices is a signed unit vector. See also rot_edge_dir.

lemma ocs_edge_dir_candMap (d m : ℕ) (u v : boxVerts d m) (hadj : (boxGraph d m).Adj u v) :
    ∃ p : Fin d × Bool, (v : Site d) - (u : Site d) = candMap d (0 : Site d) p

Uses 8 · Used by 3

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Neighbour of a site in a coordinate direction

Proof usesNearest neighbours in \(\mathbb{Z}^d\) · Hypercubic lattice \(\mathbb{Z}^d\) · Shift of a site along a coordinate

Used byPer-box uniqueness of the random-cluster measures off a countable set · Lower bound on free bulk edge marginals · Upper bound on wired bulk edge marginals

DefinitionUnit edge \(\{0, \pm e_j\}\) of a box#✓fully proved

The unit edge {0, ±e_j} of the box Λ_R, R ≥ 1, indexed by (j, sign).

def ocs_unitEdge (d R : ℕ) (hR : 1 ≤ R) (p : Fin d × Bool) : Sym2 (boxVerts d R) :=
  s((⟨(0 : Site d), ocs_zero_mem_box d R⟩ : boxVerts d R),
    (⟨candMap d (0 : Site d) p, ocs_candMap_mem_box d R hR p⟩ : boxVerts d R))

Uses 4 · Used by 13

Statement usesVertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Neighbour of a site in a coordinate direction

Used byPer-box uniqueness of the random-cluster measures off a countable set · Free unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Wired unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Free \(q = 2\) bulk sandwich from equal free edge densities · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Lower bound on free bulk edge marginals · Free off-centre sandwich from free rotation residues · Free unit-edge marginals converge to the free density · Wired unit-edge marginals converge to the wired density · Free unit-edge marginal in the square-root box · Wired unit-edge marginal in the square-root box · Upper bound on wired bulk edge marginals · Wired off-centre sandwich from wired rotation residues

LemmaFree unit-edge marginals converge to the free density#✓fully proved

The free marginal of a unit edge in Λ_{⌊√n⌋} converges to its free q = 2 density.

lemma ocs_unitEdge_marg_tendsto (d : ℕ) (p : Fin d × Bool) {pr : ℝ} (hp : 0 < pr) (hp1 : pr < 1) :
    Tendsto (fun n =>
        if hR : 1 ≤ Nat.sqrt n then
          edgeMargProb (fkProb (boxGraph d (Nat.sqrt n)) pr 2) (ocs_unitEdge d (Nat.sqrt n) hR p)
        else (0 : ℝ)) atTop
      (𝓝 (freeEdgeDensity d 2 (edgeIncl d 1 (ocs_unitEdge d 1 (le_refl 1) p)) pr))

Uses 23 · Used by 2

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Probability of an ambient FK configuration · Free infinite-volume edge density · Unit edge \(\{0, \pm e_j\}\) of a box · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Event that a box edge is open · 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\) · Event that an edge is open · 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 · Neighbour of a site in a coordinate direction

Used byFree \(q = 2\) bulk sandwich from equal free edge densities · Free off-centre sandwich from free rotation residues

DefinitionFree rotation residue for a box pair#✓fully proved

The free rotation residue at tilt t for the box pair e': every lattice edge of every box has the free q = 2 density of e' at p = logistic t.

def ocs_FreeRotationResidue (N : ℕ) (e' : Sym2 (boxVerts d N)) (t : ℝ) : Prop :=
  ∀ (m : ℕ) (eb : Sym2 (boxVerts d m)), eb ∈ (boxGraph d m).edgeFinset →
    freeEdgeDensity d 2 (edgeIncl d m eb) (fsc_logistic t)
      = freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)

Uses 7 · Used by 3

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byFree \(q = 2\) bulk sandwich from equal free edge densities · Free off-centre sandwich from free rotation residues · All box edges have the same free \(q = 2\) density

DefinitionFree unit-edge marginal in the square-root box#✓fully proved

The free marginal at p = logistic t of the unit edge (j, sign) in Λ_{⌊√n⌋}, and 0 when ⌊√n⌋ = 0.

noncomputable def ocs_unitMarg (d n : ℕ) (p : Fin d × Bool) (t : ℝ) : ℝ :=
  if hR : 1 ≤ Nat.sqrt n then
    edgeMargProb (fkProb (boxGraph d (Nat.sqrt n)) (fsc_logistic t) 2)
      (ocs_unitEdge d (Nat.sqrt n) hR p)
  else 0

Uses 8 · Used by 4

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Edge marginal of a mass function · Probability of an ambient FK configuration · Logistic function \(e^t/(1+e^t)\) · Unit edge \(\{0, \pm e_j\}\) of a box · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byFree \(q = 2\) bulk sandwich from equal free edge densities · Lower bound on free bulk edge marginals · Total deviation of free unit-edge marginals from the density · Free off-centre sandwich from free rotation residues

DefinitionTotal deviation of free unit-edge marginals from the density#✓fully proved

The total deviation ∑_{(j, sign)} |density(e') - unit-edge marginal| of the free unit-edge marginals in Λ_{⌊√n⌋} from the free density of e'.

noncomputable def ocs_freeDelta (N : ℕ) (e' : Sym2 (boxVerts d N)) (t : ℝ) (n : ℕ) : ℝ :=
  ∑ p : Fin d × Bool,
    |freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) - ocs_unitMarg d n p t|

Uses 5 · Used by 3

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Free unit-edge marginal in the square-root box

Used byFree \(q = 2\) bulk sandwich from equal free edge densities · Lower bound on free bulk edge marginals · Free off-centre sandwich from free rotation residues

DefinitionBulk edges of \(\Lambda_n\)#✓fully proved

The bulk edges of Λ_n: the edges of the inner box Λ_{n - ⌊√n⌋}.

noncomputable def ocs_bulkSet (d n : ℕ) : Finset (Sym2 (boxVerts d n)) :=
  (boxGraph d (n - Nat.sqrt n)).edgeFinset.image (innerEdgeLE d (Nat.sub_le n (Nat.sqrt n)))

Uses 5 · Used by 3

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · 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 · Free \(q = 2\) bulk sandwich from equal free edge densities · Free off-centre sandwich from free rotation residues

LemmaLower bound on free bulk edge marginals#✓fully proved

Every bulk edge of Λ_n has free marginal at least density(e') - ocs_freeDelta.

lemma ocs_free_bulk_lower (N : ℕ) (e' : Sym2 (boxVerts d N)) (t : ℝ) (n : ℕ) (hn : 1 ≤ n)
    (u v : boxVerts d (n - Nat.sqrt n)) (hadj : (boxGraph d (n - Nat.sqrt n)).Adj u v) :
    freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) - ocs_freeDelta N e' t n
      ≤ edgeMargProb (fkProb (boxGraph d n) (fsc_logistic t) 2)
          (innerEdgeLE d (Nat.sub_le n (Nat.sqrt n))
            (s(u, v) : Sym2 (boxVerts d (n - Nat.sqrt n))))

Uses 16 · Used by 2

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Probability of an ambient FK configuration · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Total deviation of free unit-edge marginals from the density · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesAdjacent box vertices differ by a signed unit vector · Free off-centre lower bound by the recentred small-box marginal · Unit edge \(\{0, \pm e_j\}\) of a box · Free unit-edge marginal in the square-root box · Neighbour of a site in a coordinate direction

Used byFree \(q = 2\) bulk sandwich from equal free edge densities · Free off-centre sandwich from free rotation residues

LemmaFree off-centre sandwich from free rotation residues#✓fully proved

The free off-centre sandwich from the free rotation residues for all pairs e' of Λ_N.

lemma ocs_freeOffCentreSandwich_of_rotation (hd : 1 ≤ d) (N : ℕ)
    (hres : ∀ (e' : Sym2 (boxVerts d N)) (t : ℝ), ocs_FreeRotationResidue (d := d) N e' t) :
    bdp_FreeOffCentreSandwich (d := d) N

Uses 25

Statement usesFree off-centre sandwich hypothesis · Vertices of the box \((-n, n)^d\) · Free rotation residue for a box pair

Proof usesNearest-neighbour graph on a box · Inclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Edge marginal of a mass function · Probability of an ambient FK configuration · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Bulk edges of \(\Lambda_n\) · Vanishing shell edge fraction when \((n - m(n))/n \to 0\) · Total deviation of free unit-edge marginals from the density · Lower bound on free bulk edge marginals · Unit edge \(\{0, \pm e_j\}\) of a box · Free unit-edge marginals converge to the free density · Free unit-edge marginal in the square-root box · Nearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Neighbour of a site in a coordinate direction · Hypercubic lattice \(\mathbb{Z}^d\) · Shift of a site along a coordinate

LemmaWired unit-edge marginals converge to the wired density#✓fully proved

The wired marginal of a unit edge in Λ_{⌊√n⌋} converges to its wired q = 2 density.

lemma ocs_unitEdge_wired_marg_tendsto (d : ℕ) (p : Fin d × Bool) {pr : ℝ}
    (hp : 0 < pr) (hp1 : pr < 1) :
    Tendsto (fun n =>
        if hR : 1 ≤ Nat.sqrt n then
          edgeMargProb (wiredFkProb (boxGraph d (Nat.sqrt n)) (boxBoundary d (Nat.sqrt n)) pr 2)
            (ocs_unitEdge d (Nat.sqrt n) hR p)
        else (0 : ℝ)) atTop
      (𝓝 (wiredEdgeDensity d 2 (edgeIncl d 1 (ocs_unitEdge d 1 (le_refl 1) p)) pr))

Uses 24 · Used by 2

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Unit edge \(\{0, \pm e_j\}\) of a box · Wired infinite-volume edge density · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Event that a box edge is open · 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\) · Event that an edge is open · 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 infinite-volume random-cluster measure · Increasing event · Neighbour of a site in a coordinate direction

Used byWired \(q = 2\) bulk sandwich from equal wired edge densities · Wired off-centre sandwich from wired rotation residues

DefinitionWired rotation residue for a box pair#✓fully proved

The wired rotation residue at tilt t for the box pair e': every lattice edge of every box has the wired q = 2 density of e' at p = logistic t.

def ocs_WiredRotationResidue (N : ℕ) (e' : Sym2 (boxVerts d N)) (t : ℝ) : Prop :=
  ∀ (m : ℕ) (eb : Sym2 (boxVerts d m)), eb ∈ (boxGraph d m).edgeFinset →
    wiredEdgeDensity d 2 (edgeIncl d m eb) (fsc_logistic t)
      = wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)

Uses 7 · Used by 3

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Logistic function \(e^t/(1+e^t)\) · Wired infinite-volume edge density · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byWired \(q = 2\) bulk sandwich from equal wired edge densities · Wired off-centre sandwich from wired rotation residues · All box edges have the same wired \(q = 2\) density

DefinitionWired unit-edge marginal in the square-root box#✓fully proved

The wired marginal at p = logistic t of the unit edge (j, sign) in Λ_{⌊√n⌋}, and 0 when ⌊√n⌋ = 0.

noncomputable def ocs_unitWiredMarg (d n : ℕ) (p : Fin d × Bool) (t : ℝ) : ℝ :=
  if hR : 1 ≤ Nat.sqrt n then
    edgeMargProb
      (wiredFkProb (boxGraph d (Nat.sqrt n)) (boxBoundary d (Nat.sqrt n)) (fsc_logistic t) 2)
      (ocs_unitEdge d (Nat.sqrt n) hR p)
  else 0

Uses 9 · Used by 4

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 · Logistic function \(e^t/(1+e^t)\) · Unit edge \(\{0, \pm e_j\}\) of a box · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byWired \(q = 2\) bulk sandwich from equal wired edge densities · Upper bound on wired bulk edge marginals · Total deviation of wired unit-edge marginals from the density · Wired off-centre sandwich from wired rotation residues

DefinitionTotal deviation of wired unit-edge marginals from the density#✓fully proved

The total deviation of the wired unit-edge marginals in Λ_{⌊√n⌋} from the wired density of e'.

noncomputable def ocs_wiredDelta (N : ℕ) (e' : Sym2 (boxVerts d N)) (t : ℝ) (n : ℕ) : ℝ :=
  ∑ p : Fin d × Bool,
    |ocs_unitWiredMarg d n p t - wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)|

Uses 5 · Used by 3

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Logistic function \(e^t/(1+e^t)\) · Wired unit-edge marginal in the square-root box · Wired infinite-volume edge density

Used byWired \(q = 2\) bulk sandwich from equal wired edge densities · Upper bound on wired bulk edge marginals · Wired off-centre sandwich from wired rotation residues

DefinitionWired bulk edges of \(\Lambda_n\)#✓fully proved

The wired bulk edges of Λ_n: the edges of the inner box Λ_{n - ⌊√n⌋ - 1}.

noncomputable def ocs_wiredBulkSet (d n : ℕ) : Finset (Sym2 (boxVerts d n)) :=
  (boxGraph d (n - Nat.sqrt n - 1)).edgeFinset.image
    (innerEdgeLE d (Nat.sub_le (n - Nat.sqrt n) 1 |>.trans (Nat.sub_le n (Nat.sqrt n))))

Uses 5 · Used by 3

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · 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 · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Wired off-centre sandwich from wired rotation residues

LemmaUpper bound on wired bulk edge marginals#✓fully proved

Every wired bulk edge of Λ_n has wired marginal at most density(e') + ocs_wiredDelta.

lemma ocs_wired_bulk_upper (N : ℕ) (e' : Sym2 (boxVerts d N)) (t : ℝ) (n : ℕ) (hn : 2 ≤ n)
    (u v : boxVerts d (n - Nat.sqrt n - 1)) (hadj : (boxGraph d (n - Nat.sqrt n - 1)).Adj u v) :
    edgeMargProb (wiredFkProb (boxGraph d n) (boxBoundary d n) (fsc_logistic t) 2)
        (innerEdgeLE d (Nat.sub_le (n - Nat.sqrt n) 1 |>.trans (Nat.sub_le n (Nat.sqrt n)))
          (s(u, v) : Sym2 (boxVerts d (n - Nat.sqrt n - 1))))
      ≤ wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) + ocs_wiredDelta N e' t n

Uses 17 · Used by 2

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Logistic function \(e^t/(1+e^t)\) · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Total deviation of wired unit-edge marginals from the density · Wired infinite-volume edge density · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesAdjacent box vertices differ by a signed unit vector · Unit edge \(\{0, \pm e_j\}\) of a box · Wired unit-edge marginal in the square-root box · Wired off-centre upper bound by the recentred small-box marginal · Neighbour of a site in a coordinate direction

Used byWired \(q = 2\) bulk sandwich from equal wired edge densities · Wired off-centre sandwich from wired rotation residues

LemmaWired off-centre sandwich from wired rotation residues#✓fully proved

The wired off-centre sandwich from the wired rotation residues for all pairs e' of Λ_N.

lemma ocs_wiredOffCentreSandwich_of_rotation (hd : 1 ≤ d) (N : ℕ)
    (hres : ∀ (e' : Sym2 (boxVerts d N)) (t : ℝ), ocs_WiredRotationResidue (d := d) N e' t) :
    bdp_WiredOffCentreSandwich (d := d) N

Uses 26

Statement usesWired off-centre sandwich hypothesis · Vertices of the box \((-n, n)^d\) · Wired rotation residue for a box pair

Proof usesVertex boundary of a box · Nearest-neighbour graph on a box · Inclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Edge marginal of a mass function · Logistic function \(e^t/(1+e^t)\) · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Vanishing shell edge fraction when \((n - m(n))/n \to 0\) · Unit edge \(\{0, \pm e_j\}\) of a box · Wired unit-edge marginals converge to the wired density · Wired unit-edge marginal in the square-root box · Wired bulk edges of \(\Lambda_n\) · Total deviation of wired unit-edge marginals from the density · Upper bound on wired bulk edge marginals · Wired infinite-volume edge density · Wired random-cluster probability of a configuration · Nearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Neighbour of a site in a coordinate direction · Hypercubic lattice \(\mathbb{Z}^d\) · Shift of a site along a coordinate

LemmaFree \(q = 2\) bulk sandwich from equal free edge densities#✓fully proved

If every free q = 2 edge density equals that of e', then each box Λ_n has a bulk set of edges with that density whose free marginals are at least the density minus δ_n → 0, and the non-bulk edge fraction tends to zero.

lemma gec_freeSandwich_of_rotation (hd : 1 ≤ d) (N : ℕ) (e' : Sym2 (boxVerts d N)) (t : ℝ)
    (hres : ocs_FreeRotationResidue (d := d) N e' t) :
    ∃ (In : (n : ℕ) → Finset (Sym2 (boxVerts d n))) (δ : ℕ → ℝ),
      (∀ n, In n ⊆ (boxGraph d n).edgeFinset) ∧
      (∀ n, 0 ≤ δ n) ∧ Tendsto δ atTop (𝓝 0) ∧
      (∀ n, ∀ e ∈ In n,
        freeEdgeDensity d 2 (edgeIncl d n e) (fsc_logistic t)
          = freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)) ∧
      (∀ n, ∀ e ∈ In n,
        freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) - δ n
          ≤ edgeMargProb (fkProb (boxGraph d n) (fsc_logistic t) 2) e) ∧
      Tendsto (fun n =>
        (((boxGraph d n).edgeFinset.card - (In n).card : ℝ)) / (boxGraph d n).edgeFinset.card)
        atTop (𝓝 0)

Uses 24 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Probability of an ambient FK configuration · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Free rotation residue for a box pair · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesInclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Bulk edges of \(\Lambda_n\) · Vanishing shell edge fraction when \((n - m(n))/n \to 0\) · Total deviation of free unit-edge marginals from the density · Lower bound on free bulk edge marginals · Unit edge \(\{0, \pm e_j\}\) of a box · Free unit-edge marginals converge to the free density · Free unit-edge marginal in the square-root box · Nearest neighbours in \(\mathbb{Z}^d\) · Neighbour of a site in a coordinate direction · Hypercubic lattice \(\mathbb{Z}^d\) · Shift of a site along a coordinate

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts

LemmaWired \(q = 2\) bulk sandwich from equal wired edge densities#✓fully proved

If every wired q = 2 edge density equals that of e', then each box Λ_n has a bulk set of edges with that density whose wired marginals are at most the density plus δ_n → 0, and the non-bulk edge fraction tends to zero.

lemma gec_wiredSandwich_of_rotation (hd : 1 ≤ d) (N : ℕ) (e' : Sym2 (boxVerts d N)) (t : ℝ)
    (hres : ocs_WiredRotationResidue (d := d) N e' t) :
    ∃ (In : (n : ℕ) → Finset (Sym2 (boxVerts d n))) (δ : ℕ → ℝ),
      (∀ n, In n ⊆ (boxGraph d n).edgeFinset) ∧
      (∀ n, 0 ≤ δ n) ∧ Tendsto δ atTop (𝓝 0) ∧
      (∀ n, ∀ e ∈ In n,
        wiredEdgeDensity d 2 (edgeIncl d n e) (fsc_logistic t)
          = wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)) ∧
      (∀ n, ∀ e ∈ In n,
        edgeMargProb (wiredFkProb (boxGraph d n) (boxBoundary d n) (fsc_logistic t) 2) e
          ≤ wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) + δ n) ∧
      Tendsto (fun n =>
        (((boxGraph d n).edgeFinset.card - (In n).card : ℝ)) / (boxGraph d n).edgeFinset.card)
        atTop (𝓝 0)

Uses 25 · Used by 1

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Logistic function \(e^t/(1+e^t)\) · Wired rotation residue for a box pair · Wired infinite-volume edge density · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesInclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Vanishing shell edge fraction when \((n - m(n))/n \to 0\) · Unit edge \(\{0, \pm e_j\}\) of a box · Wired unit-edge marginals converge to the wired density · Wired unit-edge marginal in the square-root box · Wired bulk edges of \(\Lambda_n\) · Total deviation of wired unit-edge marginals from the density · Upper bound on wired bulk edge marginals · Nearest neighbours in \(\mathbb{Z}^d\) · Neighbour of a site in a coordinate direction · Hypercubic lattice \(\mathbb{Z}^d\) · Shift of a site along a coordinate

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts

LemmaTwo-sided free \(q = 2\) bulk bounds from the free sandwich#✓fully proved

The free sandwich gives two-sided bulk bounds: free marginals within δ_n of the density, since free marginals increase to the density.

StatMech.FK.gec_freeBulk_of_sandwich · 22 lines

lemma gec_freeBulk_of_sandwich (N : ℕ) (e' : Sym2 (boxVerts d N)) (t : ℝ)
    (hsand : ∃ (In : (n : ℕ) → Finset (Sym2 (boxVerts d n))) (δ : ℕ → ℝ),
      (∀ n, In n ⊆ (boxGraph d n).edgeFinset) ∧
      (∀ n, 0 ≤ δ n) ∧ Tendsto δ atTop (𝓝 0) ∧
      (∀ n, ∀ e ∈ In n,
        freeEdgeDensity d 2 (edgeIncl d n e) (fsc_logistic t)
          = freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)) ∧
      (∀ n, ∀ e ∈ In n,
        freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) - δ n
          ≤ edgeMargProb (fkProb (boxGraph d n) (fsc_logistic t) 2) e) ∧
      Tendsto (fun n =>
        (((boxGraph d n).edgeFinset.card - (In n).card : ℝ)) / (boxGraph d n).edgeFinset.card)
        atTop (𝓝 0)) :
    ∃ (In : (n : ℕ) → Finset (Sym2 (boxVerts d n))) (δ : ℕ → ℝ),
      (∀ n, In n ⊆ (boxGraph d n).edgeFinset) ∧
      (∀ n, 0 ≤ δ n) ∧ Tendsto δ atTop (𝓝 0) ∧
      (∀ n, ∀ e ∈ In n,
        |edgeMargProb (fkProb (boxGraph d n) (fsc_logistic t) 2) e
          - freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)| ≤ δ n) ∧
      Tendsto (fun n =>
        (((boxGraph d n).edgeFinset.card - (In n).card : ℝ)) / (boxGraph d n).edgeFinset.card)
        atTop (𝓝 0)

Uses 10 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Probability of an ambient FK configuration · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesFree \(q = 2\) box edge marginals are at most the free density

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts

LemmaTwo-sided wired \(q = 2\) bulk bounds from the wired sandwich#✓fully proved

The wired sandwich gives two-sided bulk bounds: wired marginals within δ_n of the density, since wired marginals decrease to the density.

StatMech.FK.gec_wiredBulk_of_sandwich · 22 lines

lemma gec_wiredBulk_of_sandwich (N : ℕ) (e' : Sym2 (boxVerts d N)) (t : ℝ)
    (hsand : ∃ (In : (n : ℕ) → Finset (Sym2 (boxVerts d n))) (δ : ℕ → ℝ),
      (∀ n, In n ⊆ (boxGraph d n).edgeFinset) ∧
      (∀ n, 0 ≤ δ n) ∧ Tendsto δ atTop (𝓝 0) ∧
      (∀ n, ∀ e ∈ In n,
        wiredEdgeDensity d 2 (edgeIncl d n e) (fsc_logistic t)
          = wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)) ∧
      (∀ n, ∀ e ∈ In n,
        edgeMargProb (wiredFkProb (boxGraph d n) (boxBoundary d n) (fsc_logistic t) 2) e
          ≤ wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) + δ n) ∧
      Tendsto (fun n =>
        (((boxGraph d n).edgeFinset.card - (In n).card : ℝ)) / (boxGraph d n).edgeFinset.card)
        atTop (𝓝 0)) :
    ∃ (In : (n : ℕ) → Finset (Sym2 (boxVerts d n))) (δ : ℕ → ℝ),
      (∀ n, In n ⊆ (boxGraph d n).edgeFinset) ∧
      (∀ n, 0 ≤ δ n) ∧ Tendsto δ atTop (𝓝 0) ∧
      (∀ n, ∀ e ∈ In n,
        |edgeMargProb (wiredFkProb (boxGraph d n) (boxBoundary d n) (fsc_logistic t) 2) e
          - wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)| ≤ δ n) ∧
      Tendsto (fun n =>
        (((boxGraph d n).edgeFinset.card - (In n).card : ℝ)) / (boxGraph d n).edgeFinset.card)
        atTop (𝓝 0)

Uses 11 · Used by 1

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Logistic function \(e^t/(1+e^t)\) · Wired infinite-volume edge density · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesWired \(q = 2\) box edge marginals are at least the wired density

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts

DefinitionCoordinate permutation of \(\mathbb{Z}^d\)#✓fully proved

The permutation of ℤ^d permuting coordinates by π: (x ∘ π⁻¹)_i = x_{π⁻¹ i}.

def rot_permEquiv (d : ℕ) (π : Equiv.Perm (Fin d)) : Site d ≃ Site d where
  toFun := fun x i => x (π.symm i)
  invFun := fun x i => x (π i)
  left_inv := by intro x; funext i; simp
  right_inv := by intro x; funext i; simp

Uses 1 · Used by 4

Statement usesSite of the hypercubic lattice

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\}\) · Coordinate permutation as a box symmetry · Unit edges at the origin have the wired density of \(\{0, e_0\}\)

DefinitionCoordinate permutation as a box symmetry#✓fully proved

A coordinate permutation as a box symmetry.

def rot_permBoxSym (d : ℕ) (π : Equiv.Perm (Fin d)) : BoxSym d where
  τ := rot_permEquiv d π
  adj := by
    intro x y
    simp only [hypercubicLattice_adj, rot_permEquiv_apply]
    rw [← Equiv.sum_comp π.symm (fun i => (x i - y i).natAbs)]
  box_mem := by
    intro n x
    simp only [mem_box, rot_permEquiv_apply]
    refine ⟨fun h i => ?_, fun h i => h (π.symm i)⟩
    have := h (π i); simpa using this

Uses 5 · Used by 3

Statement usesBox symmetry of \(\mathbb{Z}^d\) · Coordinate permutation of \(\mathbb{Z}^d\) · 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\}\)

LemmaBox symmetries preserve the free \(q = 2\) density of any pair of sites#✓fully proved

Box symmetries preserve the free q = 2 density of any edge of ℤ^d.

lemma rot_free_density_boxSym (S : BoxSym d) (e : Sym2 (Site d))
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    freeEdgeDensity d 2 (Sym2.map S.τ e) p = freeEdgeDensity d 2 e p

Uses 8 · Used by 1

Statement usesBox symmetry of \(\mathbb{Z}^d\) · Free infinite-volume edge density · Site of the hypercubic lattice

Proof usesRestriction of a box symmetry to a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Box symmetries preserve the free \(q = 2\) density of box edges · Box \((-n, n)^d\) in the hypercubic lattice

Used byUnit edges at the origin have the free density of \(\{0, e_0\}\)

LemmaBox symmetries preserve the wired \(q = 2\) density of any pair of sites#✓fully proved

Box symmetries preserve the wired q = 2 density of any edge of ℤ^d.

lemma rot_wired_density_boxSym (S : BoxSym d) (e : Sym2 (Site d))
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    wiredEdgeDensity d 2 (Sym2.map S.τ e) p = wiredEdgeDensity d 2 e p

Uses 8 · Used by 1

Statement usesBox symmetry of \(\mathbb{Z}^d\) · Wired infinite-volume edge density · Site of the hypercubic lattice

Proof usesRestriction of a box symmetry to a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Box symmetries preserve the wired \(q = 2\) density of box edges · Box \((-n, n)^d\) in the hypercubic lattice

Used byUnit edges at the origin have the wired density of \(\{0, e_0\}\)

DefinitionReference edge \(\{0, e_0\}\) of \(\mathbb{Z}^d\)#✓fully proved

The reference edge {0, e_0} of ℤ^d.

def rot_refUnitEdge (d : ℕ) (hd : 0 < d) : Sym2 (Site d) :=
  s((0 : Site d), candMap d (0 : Site d) (⟨0, hd⟩, true))

Uses 2 · Used by 8

Statement usesSite of the hypercubic lattice · Neighbour of a site in a coordinate direction

Used byPer-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Unit edges at the origin have the free density of \(\{0, e_0\}\) · Every lattice edge has the free \(q = 2\) density of \(\{0, e_0\}\) · All box edges have the same free \(q = 2\) density · Unit edges at the origin have the wired density of \(\{0, e_0\}\) · Every lattice edge has the wired \(q = 2\) density of \(\{0, e_0\}\) · All box edges have the same wired \(q = 2\) density

LemmaUnit edges at the origin have the free density of \(\{0, e_0\}\)#✓fully proved

Every unit edge {0, ±e_j} has the free density of {0, e_0}.

lemma rot_free_centred_unit_const (hd : 0 < d) (j : Fin d) (b : Bool) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1) :
    freeEdgeDensity d 2 (s((0 : Site d), candMap d (0 : Site d) (j, b)) : Sym2 (Site d)) p
      = freeEdgeDensity d 2 (rot_refUnitEdge d hd) p

Uses 10 · Used by 1

Statement usesFree infinite-volume edge density · Reference edge \(\{0, e_0\}\) of \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Neighbour of a site in a coordinate direction

Proof usesBox symmetry of \(\mathbb{Z}^d\) · Coordinate reflection as a box symmetry · Box symmetries preserve the free \(q = 2\) density of any pair of sites · Coordinate permutation as a box symmetry · Coordinate permutation of \(\mathbb{Z}^d\) · Box \((-n, n)^d\) in the hypercubic lattice

Used byEvery lattice edge has the free \(q = 2\) density of \(\{0, e_0\}\)

LemmaUnit edges at the origin have the wired density of \(\{0, e_0\}\)#✓fully proved

Every unit edge {0, ±e_j} has the wired density of {0, e_0}.

lemma rot_wired_centred_unit_const (hd : 0 < d) (j : Fin d) (b : Bool) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1) :
    wiredEdgeDensity d 2 (s((0 : Site d), candMap d (0 : Site d) (j, b)) : Sym2 (Site d)) p
      = wiredEdgeDensity d 2 (rot_refUnitEdge d hd) p

Uses 10 · Used by 1

Statement usesReference edge \(\{0, e_0\}\) of \(\mathbb{Z}^d\) · Wired infinite-volume edge density · Site of the hypercubic lattice · Neighbour of a site in a coordinate direction

Proof usesBox symmetry of \(\mathbb{Z}^d\) · Coordinate reflection as a box symmetry · Coordinate permutation as a box symmetry · Coordinate permutation of \(\mathbb{Z}^d\) · Box symmetries preserve the wired \(q = 2\) density of any pair of sites · Box \((-n, n)^d\) in the hypercubic lattice

Used byEvery lattice edge has the wired \(q = 2\) density of \(\{0, e_0\}\)

LemmaAdjacent sites differ by a signed unit vector#✓fully proved

The difference of adjacent sites is a signed unit vector. See also ocs_edge_dir_candMap, the same statement for vertices of a box.

lemma rot_edge_dir (x y : Site d) (hadj : (hypercubicLattice d).Adj x y) :
    ∃ p : Fin d × Bool, y - x = candMap d (0 : Site d) p

Uses 5 · Used by 3

Statement usesSite of the hypercubic lattice · Neighbour of a site in a coordinate direction · Hypercubic lattice \(\mathbb{Z}^d\)

Proof usesNearest neighbours in \(\mathbb{Z}^d\) · Shift of a site along a coordinate

Used byPer-box uniqueness of the random-cluster measures off a countable set · Every lattice edge has the free \(q = 2\) density of \(\{0, e_0\}\) · Every lattice edge has the wired \(q = 2\) density of \(\{0, e_0\}\)

LemmaEvery lattice edge has the free \(q = 2\) density of \(\{0, e_0\}\)#✓fully proved

Every nearest-neighbour edge of ℤ^d has the free q = 2 density of {0, e_0}.

lemma rot_free_edge_const (hd : 0 < d) (x y : Site d)
    (hadj : (hypercubicLattice d).Adj x y) {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    freeEdgeDensity d 2 (s(x, y) : Sym2 (Site d)) p
      = freeEdgeDensity d 2 (rot_refUnitEdge d hd) p

Uses 13 · Used by 1

Statement usesFree infinite-volume edge density · Reference edge \(\{0, e_0\}\) of \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Proof usesConfiguration space of a statistical-mechanics model · Translation-invariant measure on configuration space · Shift of a configuration by a group element · Translation invariance of the free \(q = 2\) infinite-volume measure · Event that an edge is open · Free infinite-volume random-cluster measure · Adjacent sites differ by a signed unit vector · Unit edges at the origin have the free density of \(\{0, e_0\}\) · Neighbour of a site in a coordinate direction

Used byAll box edges have the same free \(q = 2\) density

LemmaEvery lattice edge has the wired \(q = 2\) density of \(\{0, e_0\}\)#✓fully proved

Every nearest-neighbour edge of ℤ^d has the wired q = 2 density of {0, e_0}.

lemma rot_wired_edge_const (hd : 0 < d) (x y : Site d)
    (hadj : (hypercubicLattice d).Adj x y) {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    wiredEdgeDensity d 2 (s(x, y) : Sym2 (Site d)) p
      = wiredEdgeDensity d 2 (rot_refUnitEdge d hd) p

Uses 13 · Used by 2

Statement usesReference edge \(\{0, e_0\}\) of \(\mathbb{Z}^d\) · Wired infinite-volume edge density · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Proof usesConfiguration space of a statistical-mechanics model · Translation-invariant measure on configuration space · Shift of a configuration by a group element · Event that an edge is open · Translation invariance of the wired \(q = 2\) infinite-volume measure · Adjacent sites differ by a signed unit vector · Unit edges at the origin have the wired density of \(\{0, e_0\}\) · Wired infinite-volume random-cluster measure · Neighbour of a site in a coordinate direction

Used byCountable-exception \(q = 2\) uniqueness from one-sided derivative data · All box edges have the same wired \(q = 2\) density

LemmaAll box edges have the same free \(q = 2\) density#✓fully proved

The free rotation residue holds for every lattice edge e' of the box Λ_N.

lemma rot_freeRotationResidue (hd : 0 < d) (N : ℕ) (e' : Sym2 (boxVerts d N))
    (he' : e' ∈ (boxGraph d N).edgeFinset) (t : ℝ) :
    ocs_FreeRotationResidue (d := d) N e' t

Uses 11 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Free rotation residue for a box pair · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesInclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Every lattice edge has the free \(q = 2\) density of \(\{0, e_0\}\) · Reference edge \(\{0, e_0\}\) of \(\mathbb{Z}^d\) · Hypercubic lattice \(\mathbb{Z}^d\)

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts

LemmaAll box edges have the same wired \(q = 2\) density#✓fully proved

The wired rotation residue holds for every lattice edge e' of the box Λ_N.

lemma rot_wiredRotationResidue (hd : 0 < d) (N : ℕ) (e' : Sym2 (boxVerts d N))
    (he' : e' ∈ (boxGraph d N).edgeFinset) (t : ℝ) :
    ocs_WiredRotationResidue (d := d) N e' t

Uses 11 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Wired rotation residue for a box pair · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesInclusion of box edges into \(\mathbb{Z}^d\) · Logistic function \(e^t/(1+e^t)\) · Reference edge \(\{0, e_0\}\) of \(\mathbb{Z}^d\) · Every lattice edge has the wired \(q = 2\) density of \(\{0, e_0\}\) · Wired infinite-volume edge density · Hypercubic lattice \(\mathbb{Z}^d\)

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts

DefinitionFree growing-box collapse at \(q = 2\)#✓fully proved

Free growing-box collapse: for every edge e' of Λ_N and every t, the average free edge density of Λ_n converges to the free infinite-volume density of e'.

def ubd_FreeGrowingBoxCollapse (N : ℕ) : Prop :=
  ∀ (e' : Sym2 (boxVerts d N)) (t : ℝ),
    Tendsto (fun n => fpd_avgDensity (boxGraph d n) t) atTop
      (𝓝 (freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)))

Uses 8

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Average edge density of the \(q = 2\) random-cluster measure · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

LemmaFree \(q = 2\) edge density lies in \((0, 1)\)#✓fully proved

The free infinite-volume q = 2 edge density lies in [0, 1].

lemma ubd_freeEdgeDensity_mem_Icc (N : ℕ) (e' : Sym2 (boxVerts d N)) (t : ℝ) :
    freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) ∈ Set.Icc (0:ℝ) 1

Uses 25 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\)

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\) · Edge marginal of a mass function · Bernoulli edge product · Event that an edge is open · Probability of an ambient FK configuration · Unnormalized random-cluster weight · Ambient FK normalizer · 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\) · Number of open clusters · Increasing event · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts

LemmaNonnegativity of wired FK edge marginals#✓fully proved

Edge marginals of a wired FK measure are nonnegative.

lemma ubd_edgeMargProb_wiredFkProb_nonneg {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (bdry : V → Prop) [DecidablePred bdry]
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) (e : Sym2 V) :
    0 ≤ edgeMargProb (wiredFkProb G bdry p q) e

Uses 7 · Used by 3

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

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Wired random-cluster weight · Wired random-cluster partition function · Number of open clusters with wired boundary conditions

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set · Wired \(q = 2\) edge density lies in \((0, 1)\)

LemmaWired FK edge marginals are at most one#✓fully proved

Edge marginals of a wired FK measure are at most 1.

lemma ubd_edgeMargProb_wiredFkProb_le_one {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (bdry : V → Prop) [DecidablePred bdry]
    {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) (e : Sym2 V) :
    edgeMargProb (wiredFkProb G bdry p q) e ≤ 1

Uses 7 · Used by 3

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

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Wired random-cluster weight · Wired random-cluster partition function · Number of open clusters with wired boundary conditions

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts · Per-box uniqueness of the random-cluster measures off a countable set · Wired \(q = 2\) edge density lies in \((0, 1)\)

LemmaWired \(q = 2\) edge density lies in \((0, 1)\)#✓fully proved

The wired infinite-volume q = 2 edge density lies in [0, 1].

lemma ubd_wiredEdgeDensity_mem_Icc (N : ℕ) (e' : Sym2 (boxVerts d N)) (t : ℝ) :
    wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) ∈ Set.Icc (0:ℝ) 1

Uses 24 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Logistic function \(e^t/(1+e^t)\) · 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\) · Edge marginal of a mass function · Event that an edge is open · Wired infinite-volume measure as limit on increasing cylinder events · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired FK edge marginals are at most one · Nonnegativity of wired FK edge marginals · 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

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts

LemmaAverage wired \(q = 2\) edge density of a box as a mean of marginals#✓fully proved

The average wired edge density of Λ_n is the mean of the wired edge marginals.

lemma ubd_avgWiredDensity_eq_sum (n : ℕ) (t : ℝ) :
    wpd_avgWiredDensity (boxGraph d n) (boxBoundary d n) 2 t
      = (1 / ((boxGraph d n).edgeFinset.card : ℝ))
          * ∑ e ∈ (boxGraph d n).edgeFinset,
              edgeMargProb (wiredFkProb (boxGraph d n) (boxBoundary d n) (fsc_logistic t) 2) e

Uses 10 · Used by 1

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 · Logistic function \(e^t/(1+e^t)\) · Wired random-cluster probability of a configuration · Average wired edge density · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesAverage wired edge density as the mean of edge marginals

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts

DefinitionFree uniform bulk deviation at \(q = 2\)#✓fully proved

Free uniform bulk deviation: for every edge e' and t, each box Λ_n has a bulk edge set with free marginals within δ_n → 0 of the free density of e', and the non-bulk edge fraction tends to zero.

def ubd_FreeUniformBulkDeviation (N : ℕ) : Prop :=
  ∀ (e' : Sym2 (boxVerts d N)) (t : ℝ),
    ∃ (In : (n : ℕ) → Finset (Sym2 (boxVerts d n))) (δ : ℕ → ℝ),
      (∀ n, In n ⊆ (boxGraph d n).edgeFinset) ∧
      (∀ n, 0 ≤ δ n) ∧ Tendsto δ atTop (𝓝 0) ∧
      (∀ n, ∀ e ∈ In n,
        |edgeMargProb (fkProb (boxGraph d n) (fsc_logistic t) 2) e
          - freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)| ≤ δ n) ∧
      Tendsto (fun n =>
        (((boxGraph d n).edgeFinset.card - (In n).card : ℝ)) / (boxGraph d n).edgeFinset.card)
        atTop (𝓝 0)

Uses 9

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Probability of an ambient FK configuration · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

DefinitionWired uniform bulk deviation at \(q = 2\)#✓fully proved

Wired uniform bulk deviation: for every edge e' and t, each box Λ_n has a bulk edge set with wired marginals within δ_n → 0 of the wired density of e', and the non-bulk edge fraction tends to zero.

def ubd_WiredUniformBulkDeviation (N : ℕ) : Prop :=
  ∀ (e' : Sym2 (boxVerts d N)) (t : ℝ),
    ∃ (In : (n : ℕ) → Finset (Sym2 (boxVerts d n))) (δ : ℕ → ℝ),
      (∀ n, In n ⊆ (boxGraph d n).edgeFinset) ∧
      (∀ n, 0 ≤ δ n) ∧ Tendsto δ atTop (𝓝 0) ∧
      (∀ n, ∀ e ∈ In n,
        |edgeMargProb (wiredFkProb (boxGraph d n) (boxBoundary d n) (fsc_logistic t) 2) e
          - wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)| ≤ δ n) ∧
      Tendsto (fun n =>
        (((boxGraph d n).edgeFinset.card - (In n).card : ℝ)) / (boxGraph d n).edgeFinset.card)
        atTop (𝓝 0)

Uses 10

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Logistic function \(e^t/(1+e^t)\) · Wired infinite-volume edge density · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

DefinitionFree \(q = 2\) infinite-volume mass function on a box#✓fully proved

The mass function on configurations of Λ_N of the free q = 2 infinite-volume measure at p = logistic(t), restricted to Λ_N.

noncomputable def fuc_freeMass (d N : ℕ) (t : ℝ) : ConfigSpace (Sym2 (boxVerts d N)) → ℝ :=
  fun ω => (freeInfiniteVolume d (fsc_logistic_pos t) (fsc_logistic_lt_one t)
      (by norm_num : (0 : ℝ) < 2) : Measure (ConfigSpace (Sym2 (Site d)))).real
        (boxRestrict d N ⁻¹' {ω})

Uses 6 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Free infinite-volume random-cluster measure · Logistic function \(e^t/(1+e^t)\) · Site of the hypercubic lattice

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\)

DefinitionWired \(q = 2\) infinite-volume mass function on a box#✓fully proved

The mass function on configurations of Λ_N of the wired q = 2 infinite-volume measure at p = logistic(t), restricted to Λ_N.

noncomputable def fuc_wiredMass (d N : ℕ) (t : ℝ) : ConfigSpace (Sym2 (boxVerts d N)) → ℝ :=
  fun ω => (wiredInfiniteVolume d (fsc_logistic_pos t) (fsc_logistic_lt_one t)
      (by norm_num : (0 : ℝ) < 2) : Measure (ConfigSpace (Sym2 (Site d)))).real
        (boxRestrict d N ⁻¹' {ω})

Uses 6 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Logistic function \(e^t/(1+e^t)\) · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\)

DefinitionHomogeneous free-energy data on a box at \(q = 2\)#✓fully proved

There is a convex g whose right and left derivatives at t are the wired and free q = 2 edge densities at p = logistic(t), for every edge of Λ_N.

def fuc_HomogeneousFreeEnergyData (d N : ℕ) : Prop :=
  ∃ g : ℝ → ℝ, ConvexOn ℝ univ g
    ∧ (∀ (e' : Sym2 (boxVerts d N)) (t : ℝ),
        wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) = pressureRightDeriv g t)
    ∧ (∀ (e' : Sym2 (boxVerts d N)) (t : ℝ),
        freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) = pressureLeftDeriv g t)

Uses 7 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Left derivative of the pressure · Right derivative of the pressure · Wired infinite-volume edge density

Used byFree-energy data give \(q = 2\) box uniqueness off countably many \(t\)

LemmaFree-energy data give \(q = 2\) box uniqueness off countably many \(t\)#✓fully proved

Given fuc_HomogeneousFreeEnergyData, the free and wired q = 2 measures agree on every increasing event of Λ_N for all but countably many t.

lemma fuc_fk_uniqueness (d N : ℕ) (eb : Sym2 (boxVerts d N))
    (hdata : fuc_HomogeneousFreeEnergyData d N) :
    {t : ℝ | ∃ A : Set (ConfigSpace (Sym2 (boxVerts d N))), IsIncreasing A ∧
        eventMassProb (fuc_freeMass d N t) A
          ≠ eventMassProb (fuc_wiredMass d N t) A}.Countable

Uses 47

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Mass of an event under a mass function · Homogeneous free-energy data on a box at \(q = 2\) · Free \(q = 2\) infinite-volume mass function on a box · Wired \(q = 2\) infinite-volume mass function on a box · Increasing event · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesMonotone coupling of two mass functions · Random-cluster probability with a boundary wiring · Boundary clique gives the wired random-cluster measure · Boundary-graph FK measure increases in \(p\) for \(q \ge 1\) · 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\) · Monotonicity of restriction between boxes · Countably many parameters admit a separating increasing event · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Event that an edge is open · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Wired infinite-volume measure as limit on increasing cylinder events · Free infinite-volume edge density · Free random-cluster measure on a box · Free box measure dominated by the wired one for \(q \ge 1\) · Free infinite-volume random-cluster measure · Logistic function \(e^t/(1+e^t)\) · Finite measure with prescribed point masses · Left derivative of the pressure · Left derivative of a convex function is at most the right one · Right derivative of the pressure · Wired infinite-volume edge density · 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 · Complete graph on the boundary vertices · Boundary wiring relation · Monotone coupling of two measures · Stochastic domination of measures on configurations · Stochastic domination compares real-valued masses · Strassen's theorem · Set of coordinatewise ordered configuration pairs

LemmaToggle-invariant coordinates are open with probability one half#✓fully proved

A coordinate whose toggle preserves a probability mass function is open with probability 1/2.

lemma fpe2_edgeMargProb_half_of_toggle_invariant
    (μ : ConfigSpace (Sym2 V) → ℝ) (e : Sym2 V)
    (hsum : ∑ ω, μ ω = 1)
    (hinv : ∀ ψ : ConfigSpace (Sym2 V), μ (setOpen e ψ) = μ (setClosed e ψ)) :
    edgeMargProb μ e = 1 / 2

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Edge marginal of a mass function · 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

DefinitionPer-coordinate free energy on a box#✓fully proved

The per-coordinate free energy on Λ_N: G on edges of the box graph and s ↦ s/2 on non-edges.

noncomputable def fpe2_perEdgeG (d N : ℕ) (G : ℝ → ℝ) :
    Sym2 (boxVerts d N) → ℝ → ℝ :=
  fun e' => if e' ∈ (boxGraph d N).edgeFinset then G else (fun s => (1/2) * s)

Uses 4 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byCountable-exception \(q = 2\) uniqueness from one-sided derivative data

DefinitionFree densities of genuine box edges as left derivatives#✓fully proved

Every edge of Λ_N has free q = 2 density at p = logistic(t) equal to the left derivative G'₋(t).

def fpe2_GenuineFreeIsLeftDeriv (d N : ℕ) (G : ℝ → ℝ) : Prop :=
  ∀ e' ∈ (boxGraph d N).edgeFinset, ∀ t : ℝ,
    freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) = pressureLeftDeriv G t

Uses 8 · Used by 2

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Left derivative of the pressure · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts · Countable-exception \(q = 2\) uniqueness from one-sided derivative data

DefinitionWired densities of genuine box edges as right derivatives#✓fully proved

Every edge of Λ_N has wired q = 2 density at p = logistic(t) equal to the right derivative G'₊(t).

def fpe2_GenuineWiredIsRightDeriv (d N : ℕ) (G : ℝ → ℝ) : Prop :=
  ∀ e' ∈ (boxGraph d N).edgeFinset, ∀ t : ℝ,
    wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) = pressureRightDeriv G t

Uses 8 · Used by 2

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Logistic function \(e^t/(1+e^t)\) · Right derivative of the pressure · Wired infinite-volume edge density · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts · Countable-exception \(q = 2\) uniqueness from one-sided derivative data

LemmaCountable-exception \(q = 2\) uniqueness from one-sided derivative data#✓fully proved

If the free and wired densities of the edges of Λ_N are the left and right derivatives of one convex G, the free and wired q = 2 measures agree on increasing events of Λ_N for all but countably many t.

lemma fpe2_fk_uniqueness_of_genuine (hd : 0 < d) (N : ℕ) (eb : Sym2 (boxVerts d N))
    (heb : eb ∈ (boxGraph d N).edgeFinset) {G : ℝ → ℝ} (hG : ConvexOn ℝ univ G)
    (hfree : fpe2_GenuineFreeIsLeftDeriv d N G)
    (hwired : fpe2_GenuineWiredIsRightDeriv d N G) :
    {t : ℝ | ∃ A : Set (ConfigSpace (Sym2 (boxVerts d N))), IsIncreasing A ∧
        eventMassProb (fuc_freeMass d N t) A
          ≠ eventMassProb (fuc_wiredMass d N t) A}.Countable

Uses 70 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Mass of an event under a mass function · Free densities of genuine box edges as left derivatives · Wired densities of genuine box edges as right derivatives · Free \(q = 2\) infinite-volume mass function on a box · Wired \(q = 2\) infinite-volume mass function on a box · Increasing event · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesMonotone coupling of two mass functions · Random-cluster probability with a boundary wiring · Boundary clique gives the wired random-cluster measure · Boundary-graph FK measure increases in \(p\) for \(q \ge 1\) · Vertex boundary of a box · Event that a box edge is open · 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\) · Monotonicity of restriction between boxes · Inclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Countably many parameters admit a separating increasing event · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Bernoulli edge product · Event that an edge is open · Probability of an ambient FK configuration · Unnormalized random-cluster weight · Ambient FK normalizer · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Wired infinite-volume measure as limit on increasing cylinder events · Toggle-invariant coordinates are open with probability one half · Per-coordinate free energy on a box · Free infinite-volume edge density · Free random-cluster measure on a box · Free box measure dominated by the wired one for \(q \ge 1\) · Free box measure of a cylinder event as a finite sum · Free infinite-volume random-cluster measure · Logistic function \(e^t/(1+e^t)\) · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Finite measure with prescribed point masses · Number of open clusters · Open subgraph of an edge configuration · Toggling a non-edge leaves the open subgraph unchanged · Left derivative of the pressure · Left derivative of a convex function is at most the right one · Right derivative of the pressure · Reference edge \(\{0, e_0\}\) of \(\mathbb{Z}^d\) · Every lattice edge has the wired \(q = 2\) density of \(\{0, e_0\}\) · Wired infinite-volume edge density · 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 random-cluster weight · Wired random-cluster partition function · Wired infinite-volume random-cluster measure · Complete graph on the boundary vertices · Hypercubic lattice \(\mathbb{Z}^d\) · Number of open clusters with wired boundary conditions · Open subgraph of a bond configuration · Boundary wiring relation · Wired open graph · Monotone coupling of two measures · Stochastic domination of measures on configurations · Stochastic domination compares real-valued masses · Strassen's theorem · Set of coordinatewise ordered configuration pairs · Closing a coordinate of a configuration · Opening a coordinate of a configuration

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts

DefinitionFree average edge density collapse on boxes#✓fully proved

The average free edge density of Λ_n converges to the free infinite-volume density of every edge of Λ_N.

def fpe2_GenuineFreeCollapse (d N : ℕ) : Prop :=
  ∀ e' ∈ (boxGraph d N).edgeFinset, ∀ t : ℝ,
    Tendsto (fun n => fpd_avgDensity (boxGraph d n) t) atTop
      (𝓝 (freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)))

Uses 8 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Average edge density of the \(q = 2\) random-cluster measure · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts

DefinitionWired average edge density collapse on boxes#✓fully proved

The average wired edge density of Λ_n converges to the wired infinite-volume density of every edge of Λ_N.

def fpe2_GenuineWiredCollapse (d N : ℕ) : Prop :=
  ∀ e' ∈ (boxGraph d N).edgeFinset, ∀ t : ℝ,
    Tendsto (fun n => wpd_avgWiredDensity (boxGraph d n) (boxBoundary d n) 2 t) atTop
      (𝓝 (wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)))

Uses 9 · Used by 1

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Logistic function \(e^t/(1+e^t)\) · Wired infinite-volume edge density · Average wired edge density · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts

DefinitionConfigurations closed off the edges of a graph#✓fully proved

Configurations closed on every coordinate that is not an edge of G.

def ecz_ClosedOff : Type _ :=
  {ω : ConfigSpace (Sym2 V) // ∀ e, e ∉ G.edgeFinset → ω e = false}

Uses 1 · Used by 13

Statement usesConfiguration space of a statistical-mechanics model

Used byDoubling 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\) · 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\) · 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\)

DefinitionEdge partition function of the random-cluster model#✓fully proved

The edge partition function: the sum of FK weights over configurations closed off E(G).

noncomputable def ecz_fkZEdge (p q : ℝ) : ℝ :=
  ∑ ω : ecz_ClosedOff G, fkWeight G p q ω.val

Uses 3 · Used by 16

Statement usesConfiguration space of a statistical-mechanics model · Configurations closed off the edges of a graph · Unnormalized random-cluster weight

Used byDoubling 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\) · Edge-normalized box free energy of the random-cluster model · 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\) · Box free energy \(-\log Z^E\) of the random-cluster model · 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\) · Negative log edge partition function of a box · Negative log edge partition function of a graph · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\)

DefinitionNumber of non-edge coordinates of a graph#✓fully proved

The number of coordinates Sym2 V that are not edges of G.

noncomputable def ecz_NE : ℕ :=
  (Finset.univ.filter (fun e : Sym2 V => e ∉ G.edgeFinset)).card

Used by 7

Used byDoubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy 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 · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\)

LemmaEach non-edge contributes a factor 2 to the partition function#✓fully proved

fkZ G p q = 2^{#non-edges} · ecz_fkZEdge G p q: each non-edge coordinate contributes a free factor 2.

lemma ecz_factorization (p q : ℝ) :
    fkZ G p q = 2 ^ ecz_NE G * ecz_fkZEdge G p q

Uses 9 · Used by 6

Statement usesNumber of non-edge coordinates of a graph · Edge partition function of the random-cluster model · Ambient FK normalizer

Proof usesConfiguration space of a statistical-mechanics model · Configurations closed off the edges of a graph · Bernoulli edge product · Unnormalized random-cluster weight · Number of open clusters · Open subgraph of an edge configuration

Used byDoubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge 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\)

LemmaInterface subadditivity of \(-\log\) of the edge partition function#✓fully proved

-log ecz_fkZEdge is subadditive across an interface up to |interface| · (-log(1 - p)); compare fis_neglog_interface_le for fkZ.

lemma ecz_neglog_interface_le (hci : fis_CrossInterface G H K) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    - Real.log (ecz_fkZEdge K p q)
      ≤ - Real.log (ecz_fkZEdge G p q) + - Real.log (ecz_fkZEdge H p q)
        - (fis_interface G H K).card * Real.log (1 - p)

Uses 11 · Used by 4

Statement usesEdge partition function of the random-cluster model · Graph glued from two graphs along an interface · Interface edges of a graph on a disjoint union

Proof usesConfiguration space of a statistical-mechanics model · Configurations closed off the edges of a graph · Bernoulli edge product · Unnormalized random-cluster weight · Connected components of a disjoint union of graphs · Gluing edge configurations on a disjoint union · Number of open clusters · Open subgraph of an edge configuration

Used byDoubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function

DefinitionNegative log edge partition function of a graph#✓fully proved

-log ecz_fkZEdge G p q.

noncomputable def ecz_uu {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
    [DecidableRel G.Adj] (p q : ℝ) : ℝ := -Real.log (ecz_fkZEdge G p q)

Uses 1 · Used by 4

Statement usesEdge partition function of the random-cluster model

Used byDoubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function

DefinitionNegative log edge partition function of a box#✓fully proved

-log ecz_fkZEdge of the box Λ_n at p = logistic(t), q = 2.

noncomputable def ecz_u (d : ℕ) (t : ℝ) (n : ℕ) : ℝ :=
  -Real.log (ecz_fkZEdge (boxGraph d n) (fsc_logistic t) 2)

Uses 6 · Used by 8

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Edge partition function of the random-cluster model · Logistic function \(e^t/(1+e^t)\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byAdditive doubling bound for the edge partition function · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Per-edge free energy of a box in the tilt variable · Per-edge negative log edge partition function of a box · Per-box \(q = 2\) uniqueness off a countable set of tilts · Convergence of the per-edge free energy of boxes · Per-edge free energy of boxes converges for \(d \ge 1\)

DefinitionPer-edge free energy of a box in the tilt variable#✓fully proved

The per-edge free energy of Λ_n in the tilt variable, computed from ecz_fkZEdge.

noncomputable def ecz_edgeFreeEnergy (d : ℕ) (t : ℝ) (n : ℕ) : ℝ :=
  -(ecz_u d t n / ((boxGraph d n).edgeFinset.card : ℝ)) + Real.log (1 + Real.exp t)

Uses 5 · Used by 3

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Negative log edge partition function of a box · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byVanishing block oscillation of the edge free energy · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-edge free energy of boxes converges for \(d \ge 1\)

DefinitionAdditive doubling bound for the edge partition function#✓fully proved

The doubling bound agl_AdditiveDoublingBound with -log fkZ replaced by ecz_u.

def ecz_AdditiveDoublingBound (d : ℕ) (t : ℝ) : Prop :=
  ∃ (I : ℕ → ℝ),
    (∀ j, 0 ≤ I j)
    ∧ Summable (fun j => I j / agl_E d (agl_K (j + 1)))
    ∧ (∀ j, ecz_u d t (agl_K (j + 1))
        ≤ (2 : ℝ) ^ d * ecz_u d t (agl_K j) + I j * (-Real.log (1 - fsc_logistic t)))
    ∧ (∀ j, |(2 : ℝ) ^ d * agl_E d (agl_K j) - agl_E d (agl_K (j + 1))| ≤ I j)

Uses 4 · Used by 3

Statement usesNumber of edges of a box · Scales \(K_j = 2^{j+1} - 1\) · Negative log edge partition function of a box · Logistic function \(e^t/(1+e^t)\)

Used byBoxes satisfy the additive doubling bound for \(d \ge 1\) · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-edge free energy of boxes converges for \(d \ge 1\)

LemmaBoxes satisfy the additive doubling bound for \(d \ge 1\)#✓fully proved

For d ≥ 1, ecz_u satisfies the doubling bound along the scales K_j = 2^{j+1} - 1.

lemma ecz_additiveDoublingBound (d : ℕ) (hd : 1 ≤ d) (t : ℝ) :
    ecz_AdditiveDoublingBound d t

Uses 48 · Used by 2

Statement usesAdditive doubling bound for the edge partition function

Proof usesConfiguration space of a statistical-mechanics model · Number of edges of a box · Scales \(K_j = 2^{j+1} - 1\) · Graph transported to the sum of a subset and its complement · Number of edges between a vertex subset and its complement · Isomorphism between a graph and its transported copy · Graph induced on the vertices satisfying a predicate · Isomorphism of a box with its translated copy in the predicate part · Graph induced on the vertices failing a predicate · Vertex set as a disjoint sum of a subset and its complement · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Configurations closed off the edges of a graph · Number of non-edge coordinates of a graph · Each non-edge contributes a factor 2 to the partition function · Edge partition function of the random-cluster model · Interface subadditivity of \(-\log\) of the edge partition function · Negative log edge partition function of a box · Negative log edge partition function of a graph · Bernoulli edge product · Graph glued from two graphs along an interface · Unnormalized random-cluster weight · Ambient FK normalizer · Logistic function \(e^t/(1+e^t)\) · Isomorphism invariance of the ambient FK normalizer · Bijection of unordered pairs induced by a bijection · Number of open clusters · Hyperplane set of \(\Lambda_{2K+1}\) · The hyperplane set has at most \(d(4K+3)^{d-1}\) sites · Block of a tag: graph induced on its vertices · The hyperplane block has at most \(2d|J|\) edges · Orthant tag of a site of \(\Lambda_{2K+1}\) · Isomorphism of an iterated induced graph with a single one · Bound on the edge gap \(|E(\Lambda_{2K+1})| - 2^d |E(\Lambda_K)|\) · \(\Lambda_{2K+1}\) has at least \(2^d\) times as many edges as \(\Lambda_K\) · FK partition function of a graph with no vertices is one · Interface edges of a split are at most the straddling edges · Translation of \(\Lambda_K\) onto an orthant block of \(\Lambda_{2K+1}\) · Graph induced on vertices with tags in \(S\) · Isomorphism from the all-tag restriction to \(\Lambda_{2K+1}\) · Restriction does not increase straddling edges of a tag · Set of edges straddling a predicate · At most \(2d|J|\) edges straddle an orthant tag · Summability of doubling corrections relative to edge counts · Translation vector onto an orthant of \(\Lambda_{2K+1}\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts · Per-edge free energy of boxes converges for \(d \ge 1\)

DefinitionMembership of a box vertex in a sub-box#✓fully proved

A vertex of Λ_n lies in the sub-box Λ_a.

def ecz_subBoxPred (d a n : ℕ) : boxVerts d n → Prop := fun x => (x : Site d) ∈ box d a

Uses 3 · Used by 1

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

Used bySub-box as an induced subgraph of a larger box

DefinitionSub-box as an induced subgraph of a larger box#✓fully proved

Λ_a is isomorphic to the subgraph of Λ_n induced on Λ_a.

noncomputable def ecz_subBoxIso (a n : ℕ) (hle : a ≤ n) :
    boxGraph d a ≃g agl_left (boxGraph d n) (ecz_subBoxPred d a n) := by
  classical
  have hsub : box d a ⊆ box d n := box_mono d hle
  refine agl_leftBlockIso n a (ecz_subBoxPred d a n) 0 ?_ ?_
  · exact {
      toFun := fun y => ⟨⟨(y : Site d), hsub y.2⟩, y.2⟩
      invFun := fun z => ⟨(z.1 : Site d), z.2⟩
      left_inv := fun _ => rfl
      right_inv := fun _ => rfl }
  · intro y
    change ((⟨(y : Site d), hsub y.2⟩ : boxVerts d n) : Site d) = (y : Site d) + 0
    simp

Uses 7

Statement usesGraph induced on the vertices satisfying a predicate · Isomorphism of a box with its translated copy in the predicate part · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Membership of a box vertex in a sub-box · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

DefinitionConvergence of the per-edge free energy of boxes#✓fully proved

The per-edge free energy ecz_u d s n / |E(Λ_n)| converges as n → ∞.

def ecz_PerEdgeDensityConverges (d : ℕ) (s : ℝ) : Prop :=
  ∃ ρ : ℝ, Tendsto (fun n => ecz_u d s n / ((boxGraph d n).edgeFinset.card : ℝ)) atTop (𝓝 ρ)

Uses 5 · Used by 2

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Negative log edge partition function of a box · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts · Per-edge free energy of boxes converges for \(d \ge 1\)

DefinitionNumber of sub-box translates along a side of a box#✓fully proved

The number ⌊(2n + 1)/(2m + 1)⌋ of translates of Λ_m that fit along one side of Λ_n.

def ecz_T (m n : ℕ) : ℕ := (2 * n + 1) / (2 * m + 1)

Used by 9

Used byVan Hove subadditivity of the box free energy for \(q \ge 1\) · Van Hove limit · Van Hove tiling bound for the edge partition function · Graph isomorphism between a sub-box and a tiling cell · Translation between a sub-box and a tiling cell · Center of a cell in the tiling of a box by sub-boxes · Per-edge free energy of boxes converges for \(d \ge 1\) · Restriction of a box to all tiling tags · Tiling cell of a box vertex

DefinitionCenter of a cell in the tiling of a box by sub-boxes#✓fully proved

The center of the cell indexed by c in the tiling of Λ_n by translates of Λ_m.

def ecz_center (m n : ℕ) (c : Fin d → Fin (ecz_T m n)) : Site d :=
  fun i => (c i : ℤ) * (2 * m + 1) + (m : ℤ) - (n : ℤ)

Uses 2 · Used by 2

Statement usesNumber of sub-box translates along a side of a box · Site of the hypercubic lattice

Used byGraph isomorphism between a sub-box and a tiling cell · Translation between a sub-box and a tiling cell

DefinitionCoordinate index of the tiling cell containing a site#✓fully proved

The index along coordinate i of the tiling cell containing x.

def ecz_cellIdx (m n : ℕ) (x : Site d) (i : Fin d) : ℕ := ((x i + n).toNat) / (2 * m + 1)

Uses 1 · Used by 2

Statement usesSite of the hypercubic lattice

Used byTranslation between a sub-box and a tiling cell · Tiling cell of a box vertex

DefinitionTiling cell of a box vertex#✓fully proved

The tiling cell containing a vertex of Λ_n, or none if it lies in the leftover strip.

noncomputable def ecz_vanHoveTag (m n : ℕ) (x : boxVerts d n) :
    Option (Fin d → Fin (ecz_T m n)) :=
  if h : ∀ i, ecz_cellIdx m n (x : Site d) i < ecz_T m n then
    some (fun i => ⟨ecz_cellIdx m n (x : Site d) i, h i⟩)
  else none

Uses 5 · Used by 5

Statement usesVertices of the box \((-n, n)^d\) · Number of sub-box translates along a side of a box · Coordinate index of the tiling cell containing a site · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byVan Hove subadditivity of the box free energy for \(q \ge 1\) · Van Hove tiling bound for the edge partition function · Graph isomorphism between a sub-box and a tiling cell · Translation between a sub-box and a tiling cell · Restriction of a box to all tiling tags

DefinitionTranslation between a sub-box and a tiling cell#✓fully proved

The vertices of Λ_m correspond to the vertices of the cell c by translation.

noncomputable def ecz_cellEquiv (m n : ℕ) (c : Fin d → Fin (ecz_T m n)) :
    boxVerts d m ≃ {x : boxVerts d n // ecz_vanHoveTag m n x = some c} where
  toFun y := ⟨⟨fun i => (y : Site d) i + ecz_center m n c i,
      ecz_center_mem_box m n c (y : Site d) y.2⟩, by
    rw [ecz_vanHoveTag_eq_some_iff]; intro i; simp only [add_sub_cancel_right]
    exact (qp_natAbs_iff ((y : Site d) i) m).mpr ((qp_natAbs_iff ((y : Site d) i) m).mp (y.2 i))⟩
  invFun x := ⟨fun i => ((x : boxVerts d n) : Site d) i - ecz_center m n c i, by
    have h := (ecz_vanHoveTag_eq_some_iff m n x.1 c).mp x.2
    intro i; exact h i⟩
  left_inv y := by apply Subtype.ext; funext i; simp
  right_inv x := by
    apply Subtype.ext; apply Subtype.ext; funext i; simp

Uses 8 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Number of sub-box translates along a side of a box · Coordinate index of the tiling cell containing a site · Center of a cell in the tiling of a box by sub-boxes · Tiling cell of a box vertex · \(|x| \le n\) iff \(-n \le x \le n\) for an integer \(x\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byGraph isomorphism between a sub-box and a tiling cell

DefinitionGraph isomorphism between a sub-box and a tiling cell#✓fully proved

Each tiling cell induces a graph isomorphic to Λ_m.

noncomputable def ecz_cellBlockIso (m n : ℕ) (c : Fin d → Fin (ecz_T m n)) :
    boxGraph d m ≃g qp_blkG (boxGraph d n) (ecz_vanHoveTag m n) (some c) where
  toEquiv := ecz_cellEquiv m n c
  map_rel_iff' := by
    intro y z
    show (qp_blkG (boxGraph d n) (ecz_vanHoveTag m n) (some c)).Adj
        (ecz_cellEquiv m n c y) (ecz_cellEquiv m n c z) ↔ (boxGraph d m).Adj y z
    unfold qp_blkG boxGraph
    simp only [comap_adj]
    change (hypercubicLattice d).Adj
        (fun i => (y : Site d) i + ecz_center m n c i) (fun i => (z : Site d) i
            + ecz_center m n c i)
      ↔ (hypercubicLattice d).Adj (y : Site d) (z : Site d)
    exact agl_nn_translate d (ecz_center m n c) (y : Site d) (z : Site d)

Uses 10 · Used by 2

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Number of sub-box translates along a side of a box · Translation between a sub-box and a tiling cell · Center of a cell in the tiling of a box by sub-boxes · Tiling cell of a box vertex · Block of a tag: graph induced on its vertices · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byVan Hove subadditivity of the box free energy for \(q \ge 1\) · Van Hove tiling bound for the edge partition function

DefinitionRestriction of a box to all tiling tags#✓fully proved

Restricting Λ_n to all tags gives back Λ_n.

noncomputable def ecz_restUnivIso (m n : ℕ) :
    qp_restG (boxGraph d n) (ecz_vanHoveTag m n) Finset.univ ≃g boxGraph d n where
  toEquiv := Equiv.subtypeUnivEquiv (fun x => Finset.mem_univ (ecz_vanHoveTag m n x))
  map_rel_iff' := by intro a b; rfl

Uses 5 · Used by 2

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Number of sub-box translates along a side of a box · Tiling cell of a box vertex · Graph induced on vertices with tags in \(S\)

Used byVan Hove subadditivity of the box free energy for \(q \ge 1\) · Van Hove tiling bound for the edge partition function

LemmaVan Hove tiling bound for the edge partition function#✓fully proved

Van Hove bound: ecz_u d t n is at most T^d · ecz_u d t m plus the cost of the leftover strip and of the interfaces between cells, where T = ⌊(2n + 1)/(2m + 1)⌋.

lemma ecz_box_vanHove_subadd (m n : ℕ) (t : ℝ) :
    ecz_u d t n ≤ ((ecz_T m n) ^ d : ℝ) * ecz_u d t m
      + (((boxGraph d n).edgeFinset.card : ℝ)
          - ((ecz_T m n) ^ d : ℝ) * ((boxGraph d m).edgeFinset.card : ℝ))
          * (-Real.log (1 - fsc_logistic t))

Uses 35 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Number of sub-box translates along a side of a box · Negative log edge partition function of a box · Logistic function \(e^t/(1+e^t)\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Graph transported to the sum of a subset and its complement · Number of edges between a vertex subset and its complement · Isomorphism between a graph and its transported copy · Graph induced on the vertices satisfying a predicate · Graph induced on the vertices failing a predicate · Vertex set as a disjoint sum of a subset and its complement · Configurations closed off the edges of a graph · Number of non-edge coordinates of a graph · Graph isomorphism between a sub-box and a tiling cell · Each non-edge contributes a factor 2 to the partition function · Edge partition function of the random-cluster model · Interface subadditivity of \(-\log\) of the edge partition function · Restriction of a box to all tiling tags · Negative log edge partition function of a graph · Tiling cell of a box vertex · Bernoulli edge product · Graph glued from two graphs along an interface · Interface edges of a graph on a disjoint union · Unnormalized random-cluster weight · Ambient FK normalizer · Isomorphism invariance of the ambient FK normalizer · Bijection of unordered pairs induced by a bijection · Number of open clusters · Block of a tag: graph induced on its vertices · Isomorphism of an iterated induced graph with a single one · FK partition function of a graph with no vertices is one · Graph induced on vertices with tags in \(S\)

Used byPer-edge free energy of boxes converges for \(d \ge 1\)

DefinitionPer-edge negative log edge partition function of a box#✓fully proved

The per-edge free energy ecz_u d s n / |E(Λ_n)|.

noncomputable def ecz_f (d : ℕ) (s : ℝ) (n : ℕ) : ℝ :=
  ecz_u d s n / ((boxGraph d n).edgeFinset.card : ℝ)

Uses 5 · Used by 2

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Negative log edge partition function of a box · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byUpper envelope for the per-edge free energy · Per-edge free energy of boxes converges for \(d \ge 1\)

DefinitionUpper envelope for the per-edge free energy#✓fully proved

An upper envelope for ecz_f combining the per-edge value at scale m with the all-closed bound.

noncomputable def ecz_g (d : ℕ) (s : ℝ) (m : ℕ) : ℝ :=
  (2 * (m : ℝ) / (2 * m + 1)) * ecz_f d s m
    + (1 - 2 * (m : ℝ) / (2 * m + 1)) * (-Real.log (1 - fsc_logistic s))

Uses 2 · Used by 1

Statement usesPer-edge negative log edge partition function of a box · Logistic function \(e^t/(1+e^t)\)

Used byPer-edge free energy of boxes converges for \(d \ge 1\)

LemmaPer-edge free energy of boxes converges for \(d \ge 1\)#✓fully proved

For d ≥ 1, the per-edge free energy ecz_u d s n / |E(Λ_n)| converges.

lemma ecz_perEdgeDensityConverges (hd : 1 ≤ d) (s : ℝ)
    (hbox : ∀ n, 1 ≤ n → 0 < (boxGraph d n).edgeFinset.card) :
    ecz_PerEdgeDensityConverges d s

Uses 25 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Convergence of the per-edge free energy of boxes · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · \(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges · Number of edges of a box · Scales \(K_j = 2^{j+1} - 1\) · Additive doubling bound for the edge partition function · Configurations closed off the edges of a graph · Number of sub-box translates along a side of a box · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Per-edge free energy of a box in the tilt variable · Per-edge negative log edge partition function of a box · Edge partition function of the random-cluster model · Upper envelope for the per-edge free energy · Negative log edge partition function of a box · Bernoulli edge product · Unnormalized random-cluster weight · Logistic function \(e^t/(1+e^t)\) · Number of open clusters · Open subgraph of an edge configuration · Box \((-n, n)^d\) as a finite set of sites

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts

DefinitionVanishing block oscillation of the edge free energy#✓fully proved

The edge free energy of Λ_n differs from that of Λ_{K_{b(n)}} by a vanishing oscillation.

def ecz_BlockOscillation (d : ℕ) (s : ℝ) : Prop :=
  ∃ (bj : ℕ → ℕ) (osc : ℕ → ℝ), Tendsto bj atTop atTop ∧ Tendsto osc atTop (𝓝 0)
    ∧ (∀ n, |ecz_edgeFreeEnergy d s n - ecz_edgeFreeEnergy d s (agl_K (bj n))| ≤ osc (bj n))

Uses 2 · Used by 1

Statement usesScales \(K_j = 2^{j+1} - 1\) · Per-edge free energy of a box in the tilt variable

Used byPer-box \(q = 2\) uniqueness off a countable set of tilts

LemmaPer-box \(q = 2\) uniqueness off a countable set of tilts#✓fully proved

For d ≥ 1, a fixed box Λ_N with an edge witness, the free and wired q = 2 measures agree on every increasing event of Λ_N for all t = logit(p) outside a countable set in t. This is the per-box q = 2 case of fkgq_countable_free_wired_disagreement.

lemma ecz_fk_uniqueness (hd : 1 ≤ d) (N : ℕ) (eb : Sym2 (boxVerts d N))
    (heb : eb ∈ (boxGraph d N).edgeFinset) :
    {t : ℝ | ∃ A : Set (ConfigSpace (Sym2 (boxVerts d N))), IsIncreasing A ∧
        eventMassProb (fuc_freeMass d N t) A
          ≠ eventMassProb (fuc_wiredMass d N t) A}.Countable

Uses 95

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Mass of an event under a mass function · Free \(q = 2\) infinite-volume mass function on a box · Wired \(q = 2\) infinite-volume mass function on a box · Increasing event · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof uses\(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges · Number of edges of a box · Scales \(K_j = 2^{j+1} - 1\) · Vertex boundary of a box · Event that a box edge is open · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Centered free energy of a graph · Wired centered free energy · Number of closed edges · Number of open edges in a finite edge set · Additive doubling bound for the edge partition function · Vanishing block oscillation of the edge free energy · Configurations closed off the edges of a graph · Number of non-edge coordinates of a graph · Convergence of the per-edge free energy of boxes · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Per-edge free energy of a box in the tilt variable · Each non-edge contributes a factor 2 to the partition function · Edge partition function of the random-cluster model · Per-edge free energy of boxes converges for \(d \ge 1\) · Negative log edge partition function of a box · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Bernoulli edge product · Event that an edge is open · Random-cluster expectation of an observable · Probability of an ambient FK configuration · Unnormalized random-cluster weight · Ambient FK normalizer · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Wired infinite-volume measure as limit on increasing cylinder events · Average edge density of the \(q = 2\) random-cluster measure · Free average edge density collapse on boxes · Free densities of genuine box edges as left derivatives · Wired average edge density collapse on boxes · Wired densities of genuine box edges as right derivatives · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free infinite-volume edge density · Free random-cluster measure on a box · Free box measure dominated by the wired one for \(q \ge 1\) · Free infinite-volume random-cluster measure · Logistic function \(e^t/(1+e^t)\) · Two-sided free \(q = 2\) bulk bounds from the free sandwich · Free \(q = 2\) bulk sandwich from equal free edge densities · Two-sided wired \(q = 2\) bulk bounds from the wired sandwich · Wired \(q = 2\) bulk sandwich from equal wired edge densities · Log-sum-exp cumulant generating function · First moment exponential sum · Weighted exponential sum · Ambient tilted log normalizer of a finite graph · Convexity of the ambient tilted log normalizer · Pointwise limits of convex functions are convex · Cylinder events of a box are measurable · Number of open clusters · Number of open edges · Open subgraph of an edge configuration · Left-continuity of the free \(q = 2\) edge density in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · Left derivative of the pressure · Right derivative of the pressure · All box edges have the same free \(q = 2\) density · All box edges have the same wired \(q = 2\) density · Average wired \(q = 2\) edge density of a box as a mean of marginals · Wired FK edge marginals are at most one · Nonnegativity of wired FK edge marginals · Free \(q = 2\) edge density lies in \((0, 1)\) · Wired \(q = 2\) edge density lies in \((0, 1)\) · Wired infinite-volume edge density · Wired random-cluster measure on a box · Wired random-cluster probability of a configuration · Wired infinite-volume random-cluster measure · Free-wired log-normalizer gap \(\le |\partial|\log q/|E|\) for \(q \ge 1\) · Average wired edge density · Wired per-edge ambient tilted log normalizer · Convexity of the wired tilted log normalizer · Wired tilted log normalizer has derivative the mean open fraction · Expectation under the wired FK measure · Size of the vertex boundary of the box \((-n, n)^d\) · Box \((-n, n)^d\) as a finite set of sites · Number of nearest-neighbour pairs inside the box \((-n, n)^d\) · Nearest-neighbour pairs inside the box \((-n, n)^d\) · Box sites with a forward neighbour in the box · Vertex boundary of the box \((-n, n)^d\) as a finite set · Hypercubic lattice \(\mathbb{Z}^d\) · Inner vertex boundary of a box · Stochastic domination compares real-valued masses

LemmaSecant bound gives \(q = 2\) edge-event uniqueness off a countable set#✓fully proved

For q = 2: assuming φ^1_{p'}(e open) ≤ φ^0_p(e open) for p' < p in (0, 1), for all but countably many p every measure between the free and wired infinite-volume measures on the event {eb open} agrees with both.

StatMech.FK.fk_uniqueness_off_countable_q2_full · 18 lines

lemma fk_uniqueness_off_countable_q2_full (d N : ℕ) (eb : Sym2 (boxVerts d N))
    (hsecant : ∀ p ∈ Ioo (0 : ℝ) 1, ∀ p' ∈ Ioo (0 : ℝ) 1, p' < p →
      wiredEdgeDensity d 2 (edgeIncl d N eb) p' ≤ freeEdgeDensity d 2 (edgeIncl d N eb) p) :
    ∃ S : Set ℝ, S.Countable ∧
      ∀ p ∉ S, ∀ (hp : 0 < p) (hp1 : p < 1)
        (phi : Measure (ConfigSpace (Sym2 (Site d)))),
        ((freeInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2) : Measure _).real
            (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb)) ≤ phi.real
              (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))
          ∧ phi.real (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))
              ≤ (wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2) : Measure _).real
                  (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))) →
        phi.real (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))
            = (freeInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2) : Measure _).real
                (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))
          ∧ phi.real (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))
              = (wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2) : Measure _).real
                  (boxRestrict d N ⁻¹' (boxEdgeOpenEvent d N eb))

Uses 32 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Event that a box edge is open · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density · Free infinite-volume random-cluster measure · Wired infinite-volume edge density · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesRandom-cluster probability with a boundary wiring · Boundary clique gives the wired random-cluster measure · Boundary-graph FK measure increases in \(p\) for \(q \ge 1\) · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Monotonicity of restriction between boxes · Event that an edge is open · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Wired infinite-volume measure as limit on increasing cylinder events · Free random-cluster measure on a box · Free box measure dominated by the wired one for \(q \ge 1\) · Cylinder events of a box are measurable · 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 · Increasing event · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Boundary wiring relation · Stochastic domination compares real-valued masses

Used byBox-edge marginal uniqueness off a countable set under tilt data · Edge-marginal uniqueness off a countable set from convex free energy

LemmaConvex limit of centered tilt free energies of boxes for \(d, q \ge 1\)#✓fully proved

For d ≥ 1 and q ≥ 1, the centered tilt free energies of the boxes Λ_n converge pointwise to a convex function G with G(0) = 0.

lemma fkgq_centeredConvergence (d : ℕ) (hd : 1 ≤ d) (q : ℝ) (hq : 1 ≤ q) :
    ∃ G : ℝ → ℝ,
      (∀ s, Tendsto (fun n => cfe_centered (boxGraph d n) q s) atTop (nhds (G s)))
        ∧ ConvexOn ℝ Set.univ G ∧ G 0 = 0

Uses 24 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Centered free energy of a graph · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · \(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges · Configurations closed off the edges of a graph · Number of non-edge coordinates of a graph · Each non-edge contributes a factor 2 to the partition function · Edge partition function of the random-cluster model · Bernoulli edge product · Unnormalized random-cluster weight · Ambient FK normalizer · Logistic function \(e^t/(1+e^t)\) · Ambient tilted log normalizer of a finite graph · Convexity of the ambient tilted log normalizer · Pointwise limits of convex functions are convex · Number of open clusters · Convergence of the per-edge box free energy · Edge-normalized box free energy of the random-cluster model · Per-edge box free energy · Van Hove limit · Box free energy \(-\log Z^E\) of the random-cluster model

Used byPer-box uniqueness of the random-cluster measures off a countable set

DefinitionAverage edge density of a random-cluster measure#✓fully proved

The average edge density |E|^{-1} E_{φ_{G,p,q}}[#open edges] at p = logistic(s).

noncomputable def fkgq_avgDensity {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (q s : ℝ) : ℝ :=
  (1 / (G.edgeFinset.card : ℝ))
    * fkExpect G (fsc_logistic s) q (fun ω => (openCount G ω : ℝ))

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Random-cluster expectation of an observable · Logistic function \(e^t/(1+e^t)\) · Number of open edges

Used byPer-box uniqueness of the random-cluster measures off a countable set

DefinitionFree infinite-volume mass function on a box for \(q \ge 1\)#✓fully proved

The mass function on configurations of Λ_N of the free infinite-volume measure at p = logistic(s).

noncomputable def fkgq_freeMass (d N : ℕ) (q : ℝ) (hq : 1 ≤ q) (s : ℝ) :
    ConfigSpace (Sym2 (boxVerts d N)) → ℝ := fun ω =>
  (freeInfiniteVolume d (fsc_logistic_pos s) (fsc_logistic_lt_one s)
      (zero_lt_one.trans_le hq) : Measure (ConfigSpace (Sym2 (Site d)))).real
    (boxRestrict d N ⁻¹' {ω})

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Free infinite-volume random-cluster measure · Logistic function \(e^t/(1+e^t)\) · Site of the hypercubic lattice

Used byPer-box uniqueness of the random-cluster measures off a countable set

DefinitionWired infinite-volume mass function on a box for \(q \ge 1\)#✓fully proved

The mass function on configurations of Λ_N of the wired infinite-volume measure at p = logistic(s).

noncomputable def fkgq_wiredMass (d N : ℕ) (q : ℝ) (hq : 1 ≤ q) (s : ℝ) :
    ConfigSpace (Sym2 (boxVerts d N)) → ℝ := fun ω =>
  (wiredInfiniteVolume d (fsc_logistic_pos s) (fsc_logistic_lt_one s)
      (zero_lt_one.trans_le hq) : Measure (ConfigSpace (Sym2 (Site d)))).real
    (boxRestrict d N ⁻¹' {ω})

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Logistic function \(e^t/(1+e^t)\) · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Used byPer-box uniqueness of the random-cluster measures off a countable set

DefinitionFree unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\)#✓fully proved

The free marginal on Λ_{⌊√n⌋} of the unit edge at the origin in direction dir, at p = logistic(t).

noncomputable def fkgq_unitMarg (d : ℕ) (q : ℝ) (n : ℕ)
    (dir : Fin d × Bool) (t : ℝ) : ℝ :=
  if hR : 1 ≤ Nat.sqrt n then
    edgeMargProb (fkProb (boxGraph d (Nat.sqrt n)) (fsc_logistic t) q)
      (ocs_unitEdge d (Nat.sqrt n) hR dir)
  else 0

Uses 8 · Used by 2

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Edge marginal of a mass function · Probability of an ambient FK configuration · Logistic function \(e^t/(1+e^t)\) · Unit edge \(\{0, \pm e_j\}\) of a box · 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 · Total deviation of free unit-edge marginals from a free density

DefinitionWired unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\)#✓fully proved

The wired marginal on Λ_{⌊√n⌋} of the unit edge at the origin in direction dir, at p = logistic(t).

noncomputable def fkgq_unitWiredMarg (d : ℕ) (q : ℝ) (n : ℕ)
    (dir : Fin d × Bool) (t : ℝ) : ℝ :=
  if hR : 1 ≤ Nat.sqrt n then
    edgeMargProb (wiredFkProb (boxGraph d (Nat.sqrt n)) (boxBoundary d (Nat.sqrt n))
      (fsc_logistic t) q) (ocs_unitEdge d (Nat.sqrt n) hR dir)
  else 0

Uses 9 · Used by 2

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 · Logistic function \(e^t/(1+e^t)\) · Unit edge \(\{0, \pm e_j\}\) of a box · Wired random-cluster probability of a configuration · 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 · Total deviation of wired unit-edge marginals from a wired density

DefinitionTotal deviation of free unit-edge marginals from a free density#✓fully proved

The total deviation between the free density of e and the free unit-edge marginals on Λ_{⌊√n⌋}, summed over directions.

noncomputable def fkgq_freeDelta (N : ℕ) (e : Sym2 (boxVerts d N))
    (q t : ℝ) (n : ℕ) : ℝ :=
  ∑ dir : Fin d × Bool,
    |freeEdgeDensity d q (edgeIncl d N e) (fsc_logistic t) - fkgq_unitMarg d q n dir t|

Uses 5 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\)

Used byPer-box uniqueness of the random-cluster measures off a countable set

DefinitionTotal deviation of wired unit-edge marginals from a wired density#✓fully proved

The total deviation between the wired unit-edge marginals on Λ_{⌊√n⌋} and the wired density of e, summed over directions.

noncomputable def fkgq_wiredDelta (N : ℕ) (e : Sym2 (boxVerts d N))
    (q t : ℝ) (n : ℕ) : ℝ :=
  ∑ dir : Fin d × Bool,
    |fkgq_unitWiredMarg d q n dir t
      - wiredEdgeDensity d q (edgeIncl d N e) (fsc_logistic t)|

Uses 5 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Wired unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Logistic function \(e^t/(1+e^t)\) · Wired infinite-volume edge density

Used byPer-box uniqueness of the random-cluster measures off a countable set

TheoremPer-box uniqueness of the random-cluster measures off a countable set#✓fully proved

For d ≥ 1, q ≥ 1, and every box Λ_N, the free and wired infinite-volume random-cluster measures on ℤ^d at p = logistic(t) give the same mass to every increasing event of Λ_N, for all t outside a countable set.

This is a per-box statement only: the countable exceptional set may depend on N, the statement is in the logit parameter t rather than in p ∈ (0, 1) directly, and it concludes agreement on increasing events of that one finite restriction, not equality of the infinite-volume measures. No declaration here takes the countable union over N, transfers it to p, or derives equality of the infinite-volume measures. (Grimmett, The Random-Cluster Model, 2006, Theorem 4.60.)

theorem fkgq_countable_free_wired_disagreement (hd : 1 ≤ d) (N : ℕ)
    (q : ℝ) (hq : 1 ≤ q) :
    {t : ℝ | ∃ A : Set (ConfigSpace (Sym2 (boxVerts d N))), IsIncreasing A ∧
      eventMassProb (fkgq_freeMass d N q hq t) A ≠
        eventMassProb (fkgq_wiredMass d N q hq t) A}.Countable

Uses 157

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Mass of an event under a mass function · Free infinite-volume mass function on a box for \(q \ge 1\) · Wired infinite-volume mass function on a box for \(q \ge 1\) · Increasing event · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesBox symmetry of \(\mathbb{Z}^d\) · Restriction of a box symmetry to a box · \(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges · Monotone coupling of two mass functions · Random-cluster probability with a boundary wiring · Empty wiring gives the free random-cluster measure · Boundary clique gives the wired random-cluster measure · Random-cluster comparison of boundary conditions for \(q \ge 1\) · Random-cluster weight with a boundary wiring · Partition function with a boundary wiring · Empty boundary predicate · 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\) · Monotonicity of restriction between boxes · Inclusion of box vertices into the next box · Inclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Centered free energy of a graph · Wired centered free energy · Number of closed edges · Conditional random-cluster measure with a boundary wiring · Fibre of configurations agreeing off an edge set · Convex function has equal one-sided derivatives off a countable set · Number of open edges in a finite edge set · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Edge marginal of a mass function · Bernoulli edge product · Extension of a box configuration by closed edges · Event that an edge is open · Random-cluster expectation of an observable · Probability of an ambient FK configuration · Graph automorphisms preserve free FK edge marginals · Boundary-preserving automorphisms preserve wired FK edge marginals · Coordinate reflection as a box symmetry · Unnormalized random-cluster weight · Ambient FK normalizer · Monotone-coupled laws with equal edge marginals agree on up-sets · Average edge density of a random-cluster measure · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\) · Total deviation of free unit-edge marginals from a free density · Free unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Wired unit-edge marginal at \(0\) on \(\Lambda_{\lfloor\sqrt n\rfloor}\) · Total deviation of wired unit-edge marginals from a wired density · Inclusion of a subset of sites into a larger one · Toggle-invariant coordinates are open with probability one half · Free infinite-volume edge density · Free random-cluster measure on a box · Free box measure dominated by the wired one 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 · Free infinite-volume random-cluster measure · Free infinite-volume measure is a subsequential weak limit · One-step box monotonicity of free measures for \(q \ge 1\) · Logistic function \(e^t/(1+e^t)\) · Translation covariance of FK edge marginals on boxes · 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 · Inclusion of box edges into the next box · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Restriction of a next-box configuration to the inner edges · Cylinder events of a box are clopen · Log-sum-exp cumulant generating function · First moment exponential sum · Weighted exponential sum · Ambient tilted log normalizer of a finite graph · Convexity of the ambient tilted log normalizer · Finite measure with prescribed point masses · Event that all edges of a finite set are open · Mass of the all-open event under a weight function · Number of open clusters · Number of clusters under a boundary wiring · Adjacency matching of the inner embedding · Law of total probability over outside configurations · Conditional outer probability as an induced-wiring probability · Wiring induced on the inner graph · Image of an inner-graph edge in the outer graph · Finite set of inner edges · Restriction of an outer configuration to inner edges · Restriction pulls back all-open events to their images · Restricting a glued configuration recovers the inner one · Lattice inclusion matches induced adjacency · Outer wired all-open probability at most the inner wired one · Projection closing every inner edge · Gluing of inner and outer configurations · Outer wired fibre masses sum to one · Bulk edges of \(\Lambda_n\) · Vanishing shell edge fraction when \((n - m(n))/n \to 0\) · Adjacent box vertices differ by a signed unit vector · Unit edge \(\{0, \pm e_j\}\) of a box · Wired bulk edges of \(\Lambda_n\) · Number of open edges · Open subgraph of an edge configuration · Toggling a non-edge leaves the open subgraph unchanged · Left derivative of the pressure · Right derivative of the pressure · Adjacent sites differ by a signed unit vector · Coordinate permutation as a box symmetry · Coordinate permutation of \(\mathbb{Z}^d\) · Reference edge \(\{0, e_0\}\) of \(\mathbb{Z}^d\) · Wired FK edge marginals are at most one · Nonnegativity of wired FK edge marginals · Wired infinite-volume edge density · Wired random-cluster measure on a box · Wired random-cluster measure as a probability mass function · Wired random-cluster probability of a configuration · Wired random-cluster weight · Wired random-cluster partition function · Wired infinite-volume random-cluster measure · Wired infinite-volume measure is a subsequential weak limit · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Free-wired log-normalizer gap \(\le |\partial|\log q/|E|\) for \(q \ge 1\) · Average wired edge density · Average wired edge density as the mean of edge marginals · Wired per-edge ambient tilted log normalizer · Convexity of the wired tilted log normalizer · Wired tilted log normalizer has derivative the mean open fraction · Expectation under the wired FK measure · Nearest neighbours in \(\mathbb{Z}^d\) · Complete graph on the boundary vertices · Size of the vertex boundary of the box \((-n, n)^d\) · Box \((-n, n)^d\) as a finite set of sites · Number of nearest-neighbour pairs inside the box \((-n, n)^d\) · Nearest-neighbour pairs inside the box \((-n, n)^d\) · Box sites with a forward neighbour in the box · Vertex boundary of the box \((-n, n)^d\) as a finite set · Neighbour of a site in a coordinate direction · Hypercubic lattice \(\mathbb{Z}^d\) · Number of open clusters with wired boundary conditions · Open subgraph of a bond configuration · Shift of a site along a coordinate · Inner vertex boundary of a box · Boundary wiring relation · Wired open graph · Monotone coupling of two measures · Stochastic domination of measures on configurations · Stochastic domination compares real-valued masses · Weak convergence of probability measures on configuration space · Portmanteau theorem for clopen events · Strassen's theorem · Set of coordinatewise ordered configuration pairs · Closing a coordinate of a configuration · Opening a coordinate of a configuration

100 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.