Free energy of the random-cluster model

DefinitionNegative log ambient normalizer of the box \(\Lambda_n\)#✓fully proved

The negative log ambient normalizer -log (fkZ Λ_n (logistic t) 2) of the box Λ_n.

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

Uses 6 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Ambient FK normalizer · Logistic function \(e^t/(1+e^t)\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byDoubling bound at the dyadic scales \(2^j\)

DefinitionEdge count of the box \(\Lambda_n\)#✓fully proved

The number of edges of the box Λ_n.

noncomputable def bxt_E (d n : ℕ) : ℝ := ((boxGraph d n).edgeFinset.card : ℝ)

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 byDoubling bound at the dyadic scales \(2^j\)

DefinitionDoubling bound at the dyadic scales \(2^j\)#✓fully proved

Doubling bound at the dyadic scales: u(2^{j+1}) ≤ 2^d u(2^j) + I_j (-log(1 - p)) with |2^d E(2^j) - E(2^{j+1})| ≤ I_j and ∑_j I_j / E(2^{j+1}) < ∞.

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

Uses 3

Statement usesEdge count of the box \(\Lambda_n\) · Negative log ambient normalizer of the box \(\Lambda_n\) · Logistic function \(e^t/(1+e^t)\)

DefinitionInterface edges of a graph on a disjoint union#✓fully proved

The interface edges of K: edges not in the disjoint union G ⊕ H.

noncomputable def fis_interface : Finset (Sym2 (V ⊕ W)) :=
  K.edgeFinset \ (G ⊕g H).edgeFinset

Used by 6

Used byNumber of edges between a vertex subset and its complement · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Interface edges of a split are at most the straddling edges · Peeling bound for \(-\log Z\) of a tagged graph · Van Hove tiling bound for the edge partition function · Interface subadditivity of \(-\log\) of the edge partition function

StructureGraph glued from two graphs along an interface#✓fully proved

K contains G ⊕ H and adds no edges inside V or inside W; all extra edges join V to W.

structure fis_CrossInterface : Prop where
  le : (G ⊕g H) ≤ K
  inl : ∀ a b, K.Adj (Sum.inl a) (Sum.inl b) → G.Adj a b
  inr : ∀ c d, K.Adj (Sum.inr c) (Sum.inr d) → H.Adj c d

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\) · Peeling bound for \(-\log Z\) of a tagged graph · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Interface subadditivity of \(-\log\) of the edge partition function · Mean-field lower bound for the spontaneous magnetization

AbbreviationGraph induced on the vertices satisfying a predicate#✓fully proved

The graph induced by K₀ on {x | P x}.

abbrev agl_left : SimpleGraph {x // P x} := K₀.comap (Subtype.val)

Used by 15

Used byNumber of edges between a vertex subset and its complement · Isomorphism of a box with its translated copy in the predicate part · Doubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Orthant blocks have the FK partition function of \(\Lambda_K\) · Interface edges of a split are at most the straddling edges · Left part of a tag split has the block partition function · Peeling bound for \(-\log Z\) of a tagged graph · Right part of a tag split has the restricted partition function · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Sub-box as an induced subgraph of a larger box · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Simon–Lieb inequality in the infinite-volume plus state

AbbreviationGraph induced on the vertices failing a predicate#✓fully proved

The graph induced by K₀ on {x | ¬ P x}.

abbrev agl_right : SimpleGraph {x // ¬ P x} := K₀.comap (Subtype.val)

Used by 10

Used byNumber of edges between a vertex subset and its complement · Isomorphism of a box with its translated copy in the complement part · Doubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Interface edges of a split are at most the straddling edges · Peeling bound for \(-\log Z\) of a tagged graph · Right part of a tag split has the restricted partition function · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Mean-field lower bound for the spontaneous magnetization

DefinitionVertex set as a disjoint sum of a subset and its complement#✓fully proved

The identification {P} ⊕ {¬P} ≃ U.

noncomputable def agl_sumEquiv : ({x // P x} ⊕ {x // ¬ P x}) ≃ U := Equiv.sumCompl P

Used by 11

Used byGraph transported to the sum of a subset and its complement · Isomorphism between a graph and its transported copy · Doubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Interface edges of a split are at most the straddling edges · Peeling bound for \(-\log Z\) of a tagged graph · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Simon–Lieb inequality in the infinite-volume plus state

DefinitionGraph transported to the sum of a subset and its complement#✓fully proved

K₀ transported to {P} ⊕ {¬P}.

noncomputable def agl_glueGraph : SimpleGraph ({x // P x} ⊕ {x // ¬ P x}) :=
  K₀.comap (agl_sumEquiv P)

Uses 1 · Used by 9

Statement usesVertex set as a disjoint sum of a subset and its complement

Used byNumber of edges between a vertex subset and its complement · Isomorphism between a graph and its transported copy · Doubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Interface edges of a split are at most the straddling edges · Peeling bound for \(-\log Z\) of a tagged graph · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Mean-field lower bound for the spontaneous magnetization

DefinitionIsomorphism between a graph and its transported copy#✓fully proved

K₀ is isomorphic to its transport agl_glueGraph.

noncomputable def agl_iso : K₀ ≃g agl_glueGraph K₀ P where
  toEquiv := (agl_sumEquiv P).symm
  map_rel_iff' := by
    intro a b
    rw [agl_glueGraph_adj]
    simp only [Equiv.apply_symm_apply]

Uses 2 · Used by 5

Statement usesGraph transported to the sum of a subset and its complement · Vertex set as a disjoint sum of a subset and its complement

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

DefinitionNumber of edges between a vertex subset and its complement#✓fully proved

The number of edges of K₀ joining {P} to {¬P}.

noncomputable def agl_interfaceCard : ℕ :=
  (fis_interface (agl_left K₀ P) (agl_right K₀ P) (agl_glueGraph K₀ P)).card

Uses 4 · Used by 6

Statement usesGraph transported to the sum of a subset and its complement · Graph induced on the vertices satisfying a predicate · Graph induced on the vertices failing a predicate · Interface edges of a graph on a disjoint union

Used byDoubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Interface edges of a split are at most the straddling edges · Peeling bound for \(-\log Z\) of a tagged graph · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function

DefinitionIsomorphism of translated induced lattice graphs#✓fully proved

Translating vertex embeddings by v gives isomorphic induced lattice graphs.

noncomputable def agl_transBlockIso (d : ℕ) (v : Site d) (f : V → Site d) (g : W → Site d)
    (φ : V ≃ W) (hfg : ∀ x, g (φ x) = f x + v) :
    (hypercubicLattice d).comap f ≃g (hypercubicLattice d).comap g where
  toEquiv := φ
  map_rel_iff' := by
    intro x y
    simp only [comap_adj, hfg]
    exact agl_nn_translate d v (f x) (f y)

Uses 2

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

DefinitionIsomorphism of a box with its translated copy in the predicate part#✓fully proved

A translated copy of Λ_m inside {P} induces a graph isomorphic to Λ_m.

noncomputable def agl_leftBlockIso {d : ℕ} (N m : ℕ) (P : boxVerts d N → Prop) [DecidablePred P]
    (v : Site d) (φ : boxVerts d m ≃ {x // P x})
    (hφ : ∀ y : boxVerts d m, ((φ y : boxVerts d N) : Site d) = (y : Site d) + v) :
    boxGraph d m ≃g agl_left (boxGraph d N) P where
  toEquiv := φ
  map_rel_iff' := by
    intro y z
    show (agl_left (boxGraph d N) P).Adj (φ y) (φ z) ↔ (boxGraph d m).Adj y z
    unfold agl_left boxGraph
    simp only [comap_adj]
    rw [hφ y, hφ z]
    exact agl_nn_translate d v (y : Site d) (z : Site d)

Uses 6 · Used by 4

Statement usesGraph induced on the vertices satisfying a predicate · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byDoubling bound for the box free energy when \(q \ge 1\) · Orthant blocks have the FK partition function of \(\Lambda_K\) · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Sub-box as an induced subgraph of a larger box

DefinitionIsomorphism of a box with its translated copy in the complement part#✓fully proved

A translated copy of Λ_m inside {¬P} induces a graph isomorphic to Λ_m.

noncomputable def agl_rightBlockIso {d : ℕ} (N m : ℕ) (P : boxVerts d N → Prop) [DecidablePred P]
    (v : Site d) (φ : boxVerts d m ≃ {x // ¬ P x})
    (hφ : ∀ y : boxVerts d m, ((φ y : boxVerts d N) : Site d) = (y : Site d) + v) :
    boxGraph d m ≃g agl_right (boxGraph d N) P where
  toEquiv := φ
  map_rel_iff' := by
    intro y z
    show (agl_right (boxGraph d N) P).Adj (φ y) (φ z) ↔ (boxGraph d m).Adj y z
    unfold agl_right boxGraph
    simp only [comap_adj]
    rw [hφ y, hφ z]
    exact agl_nn_translate d v (y : Site d) (z : Site d)

Uses 6

Statement usesGraph induced on the vertices failing a predicate · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

DefinitionScales \(K_j = 2^{j+1} - 1\)#✓fully proved

The scales K_j = 2^{j+1} - 1, with K_0 = 1 and K_{j+1} = 2 K_j + 1.

def agl_K (j : ℕ) : ℕ := 2 ^ (j + 1) - 1

Used by 14

Used byAssumed doubling, boundedness and oscillation data along \(K_j\) · Additive doubling bound along the scales \(K_j\) · Doubling-bound property of the box free energy along \(K_j\) · Box free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\) · Per-edge free energy converges along \(K_j\) for \(d, q \ge 1\) · Van Hove limit · Box Fekete data from a uniform bound and an oscillation bound · Additive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model · Summability of doubling corrections relative to edge counts · Additive doubling bound for the edge partition function · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Vanishing 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\)

DefinitionNegative log ambient normalizer of a box#✓fully proved

The negative log ambient normalizer of Λ_n; the same as bxt_ambientNegLogZ.

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

Uses 6 · Used by 5

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Ambient FK normalizer · Logistic function \(e^t/(1+e^t)\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byAssumed doubling, boundedness and oscillation data along \(K_j\) · Additive doubling bound along the scales \(K_j\) · Box Fekete data from a uniform bound and an oscillation bound · Additive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model · Doubling inequality for \(-\log Z\) of the free \(q = 2\) FK model

DefinitionNumber of edges of a box#✓fully proved

The number of edges of Λ_n; the same as bxt_E.

noncomputable def agl_E (n : ℕ) : ℝ := ((boxGraph d n).edgeFinset.card : ℝ)

Uses 4 · Used by 12

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 byAssumed doubling, boundedness and oscillation data along \(K_j\) · Additive doubling bound along the scales \(K_j\) · Doubling-bound property of the box free energy along \(K_j\) · Box free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\) · Per-edge free energy converges along \(K_j\) for \(d, q \ge 1\) · Box Fekete data from a uniform bound and an oscillation bound · Additive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model · Summability of doubling corrections relative to edge counts · Additive doubling bound for the edge partition function · Boxes 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\)

DefinitionAdditive doubling bound along the scales \(K_j\)#✓fully proved

Doubling bound along the scales K_j: u(K_{j+1}) ≤ 2^d u(K_j) + I_j (-log(1 - p)) with |2^d E(K_j) - E(K_{j+1})| ≤ I_j and ∑_j I_j / E(K_{j+1}) < ∞.

def agl_AdditiveDoublingBound (t : ℝ) : Prop :=
  ∃ (I : ℕ → ℝ),
    (∀ j, 0 ≤ I j)
    ∧ Summable (fun j => I j / agl_E d (agl_K (j + 1)))
    ∧ (∀ j, agl_ambientNegLogZ d t (agl_K (j + 1))
        ≤ (2 : ℝ) ^ d * agl_ambientNegLogZ 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 ambient normalizer of a box · Logistic function \(e^t/(1+e^t)\)

Used byAssumed doubling, boundedness and oscillation data along \(K_j\) · Box Fekete data from a uniform bound and an oscillation bound · Additive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model

DefinitionAssumed doubling, boundedness and oscillation data along \(K_j\)#✓fully proved

The doubling bound along K_j, a uniform bound on the ambient per-edge values agl_ambientNegLogZ / agl_E at those scales, and vanishing oscillation of ivp2_ambientTiltLogZ between Λ_n and Λ_{K_{b(n)}}. These are assumptions, not a box-convergence result.

def agl_AdditiveBoxFeketeData (t : ℝ) : Prop :=
  agl_AdditiveDoublingBound d t
    ∧ (∃ M : ℝ, ∀ j, |agl_ambientNegLogZ d t (agl_K j) / agl_E d (agl_K j)| ≤ M)
    ∧ (∃ (bj : ℕ → ℕ) (osc : ℕ → ℝ), Tendsto bj atTop atTop ∧ Tendsto osc atTop (𝓝 0)
        ∧ (∀ n, |ivp2_ambientTiltLogZ (boxGraph d n) 2 t
            - ivp2_ambientTiltLogZ (boxGraph d (agl_K (bj n))) 2 t| ≤ osc (bj n)))

Uses 9 · Used by 1

Statement usesAdditive doubling bound along the scales \(K_j\) · Number of edges of a box · Scales \(K_j = 2^{j+1} - 1\) · Negative log ambient normalizer of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Ambient tilted log normalizer of a finite graph · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byBox Fekete data from a uniform bound and an oscillation bound

LemmaFekete's lemma with a general normalization#✓fully proved

Fekete's lemma normalized by e n instead of n: if u is subadditive with u n / n bounded below and e n / n → c ≠ 0, then u n / e n → lim / c. Built on Mathlib's Subadditive.tendsto_lim.

lemma fkl_tendsto_div_of_subadditive (u : ℕ → ℝ) (hsub : Subadditive u)
    (hbdd : BddBelow (Set.range fun n => u n / n))
    (e : ℕ → ℝ) (c : ℝ) (hc : c ≠ 0)
    (he : Tendsto (fun n => e n / n) atTop (𝓝 c)) :
    Tendsto (fun n => u n / e n) atTop (𝓝 (hsub.lim / c))

Used by 1

Used byHypotheses of the normalized Fekete lemma are satisfiable

LemmaHypotheses of the normalized Fekete lemma are satisfiable#✓fully proved

The hypotheses of fkl_tendsto_div_of_subadditive hold together for u = 0, e n = n.

lemma fkl_superMultiplicative_satisfiable :
    ∃ (u : ℕ → ℝ) (hsub : Subadditive u) (e : ℕ → ℝ) (c : ℝ),
      c ≠ 0 ∧ BddBelow (Set.range fun n => u n / n)
        ∧ Tendsto (fun n => e n / n) atTop (𝓝 c)
        ∧ Tendsto (fun n => u n / e n) atTop (𝓝 (hsub.lim / c))

Uses 1

Proof usesFekete's lemma with a general normalization

DefinitionDyadic convergence data for the ambient tilted log normalizer#✓fully proved

The ambient tilted log normalizer of Λ_{2^j} is increasing in j up to summable defects and bounded above, and the ambient tilted log normalizer of Λ_n differs from that of the dyadic box below it by a vanishing oscillation.

def bpv_AmbientTiltLogZConvergenceData (d : ℕ) (t : ℝ) : Prop :=
  ∃ (δ osc : ℕ → ℝ),
    (∀ j, 0 ≤ δ j)
    ∧ Summable δ
    ∧ (∀ j, ivp2_ambientTiltLogZ (boxGraph d (2 ^ j)) 2 t - δ j
        ≤ ivp2_ambientTiltLogZ (boxGraph d (2 ^ (j + 1))) 2 t)
    ∧ BddAbove (range (fun j => ivp2_ambientTiltLogZ (boxGraph d (2 ^ j)) 2 t))
    ∧ Tendsto osc atTop (𝓝 0)
    ∧ (∀ n, 1 ≤ n → |ivp2_ambientTiltLogZ (boxGraph d n) 2 t
        - ivp2_ambientTiltLogZ (boxGraph d (2 ^ (Nat.log 2 n))) 2 t| ≤ osc (Nat.log 2 n))

Uses 5

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

LemmaFekete's lemma with a sublinear correction#✓fully proved

Fekete's lemma with an o(n) correction: if u n + c n is subadditive and bounded below after dividing by n, and c n / n → 0, then u n / n converges. See also Mathlib's Subadditive.tendsto_lim.

lemma bfd_tendsto_div_of_nearSubadditive (u c : ℕ → ℝ)
    (hsub : Subadditive (fun n => u n + c n))
    (hbdd : BddBelow (Set.range fun n => (u n + c n) / n))
    (hc : Tendsto (fun n => c n / n) atTop (𝓝 0)) :
    Tendsto (fun n => u n / n) atTop (𝓝 hsub.lim)

DefinitionComponents of a disjoint union sent to components of the summands#✓fully proved

The map sending a component of G ⊕g H to the corresponding component of G or H.

StatMech.FK.fsm_ccToSum · 16 lines

noncomputable def fsm_ccToSum :
    (G ⊕g H).ConnectedComponent → G.ConnectedComponent ⊕ H.ConnectedComponent :=
  Quot.lift
    (fun x => Sum.elim (fun a => Sum.inl (G.connectedComponentMk a))
                       (fun b => Sum.inr (H.connectedComponentMk b)) x)
    (by
      intro x y hxy
      match x, y, hxy with
      | Sum.inl a, Sum.inl b, hxy =>
        simp only [Sum.elim_inl]; congr 1
        exact ConnectedComponent.sound ((fsm_reach_inl_inl G H a b).mp hxy)
      | Sum.inr a, Sum.inr b, hxy =>
        simp only [Sum.elim_inr]; congr 1
        exact ConnectedComponent.sound ((fsm_reach_inr_inr G H a b).mp hxy)
      | Sum.inl a, Sum.inr b, hxy => exact absurd hxy (not_reachable_sum_inl_inr a b)
      | Sum.inr a, Sum.inl b, hxy => exact absurd hxy.symm (not_reachable_sum_inl_inr b a))

Used by 1

Used byConnected components of a disjoint union of graphs

DefinitionInclusion of summand components into a disjoint union#✓fully proved

The inclusion of the components of G and of H into those of G ⊕g H.

noncomputable def fsm_sumToCC :
    G.ConnectedComponent ⊕ H.ConnectedComponent → (G ⊕g H).ConnectedComponent :=
  Sum.elim (ConnectedComponent.map Embedding.sumInl.toHom)
           (ConnectedComponent.map Embedding.sumInr.toHom)

Used by 1

Used byConnected components of a disjoint union of graphs

DefinitionConnected components of a disjoint union of graphs#✓fully proved

The connected components of G ⊕g H are those of G and those of H.

noncomputable def fsm_ccSumEquiv :
    (G ⊕g H).ConnectedComponent ≃ G.ConnectedComponent ⊕ H.ConnectedComponent where
  toFun := fsm_ccToSum G H
  invFun := fsm_sumToCC G H
  left_inv := by
    refine ConnectedComponent.ind ?_; rintro (a | b) <;> rfl
  right_inv := by
    rintro (c | c)
    · induction c using ConnectedComponent.ind with | _ a => rfl
    · induction c using ConnectedComponent.ind with | _ b => rfl

Uses 2 · Used by 3

Statement usesComponents of a disjoint union sent to components of the summands · Inclusion of summand components into a disjoint union

Used byAmbient FK normalizer is supermultiplicative under disjoint union · Peeling bound for \(-\log Z\) of a tagged graph · Interface subadditivity of \(-\log\) of the edge partition function

DefinitionGluing edge configurations on a disjoint union#✓fully proved

Gluing edge configurations: σ on edges inside V, τ on edges inside W, and closed on pairs joining V to W.

noncomputable def fsm_combine (σ : Sym2 V → Bool) (τ : Sym2 W → Bool) :
    Sym2 (V ⊕ W) → Bool :=
  Sym2.lift ⟨fun x y =>
    match x, y with
    | Sum.inl a, Sum.inl b => σ s(a, b)
    | Sum.inr c, Sum.inr d => τ s(c, d)
    | _, _ => false,
    by
      intro x y
      match x, y with
      | Sum.inl a, Sum.inl b => simp [Sym2.eq_swap]
      | Sum.inr c, Sum.inr d => simp [Sym2.eq_swap]
      | Sum.inl a, Sum.inr d => rfl
      | Sum.inr c, Sum.inl b => rfl⟩

Used by 3

Used byAmbient FK normalizer is supermultiplicative under disjoint union · Peeling bound for \(-\log Z\) of a tagged graph · Interface subadditivity of \(-\log\) of the edge partition function

LemmaAmbient FK normalizer is supermultiplicative under disjoint union#✓fully proved

The ambient FK normalizer is supermultiplicative under disjoint union: Z_G Z_H ≤ Z_{G ⊕g H}. Each Z sums over all Sym2 configurations.

lemma fsm_fkZ_sum_ge {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    fkZ G p q * fkZ H p q ≤ fkZ (G ⊕g H) p q

Uses 8 · Used by 1

Statement usesAmbient FK normalizer

Proof usesConfiguration space of a statistical-mechanics model · 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 bySubadditivity of \(-\log Z\) along a juxtaposition sequence

DefinitionBijection of unordered pairs induced by a bijection#✓fully proved

The equivalence Sym2 V ≃ Sym2 W induced by V ≃ W.

def fsm_sym2Congr (φ : V ≃ W) : Sym2 V ≃ Sym2 W where
  toFun := Sym2.map φ
  invFun := Sym2.map φ.symm
  left_inv z := by induction z using Sym2.ind with | _ a b => simp [Sym2.map_mk]
  right_inv z := by induction z using Sym2.ind with | _ a b => simp [Sym2.map_mk]

Used by 5

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

DefinitionGraph isomorphism restricted to open subgraphs#✓fully proved

A graph isomorphism G ≃g H restricts to an isomorphism of open subgraphs, with the configuration on G pulled back from H.

noncomputable def fsm_openSubIso (φ : G ≃g H) (ω : Sym2 W → Bool) :
    openSub G (fun e => ω (Sym2.map φ.toEquiv e)) ≃g openSub H ω where
  toEquiv := φ.toEquiv
  map_rel_iff' := by
    intro a b
    simp only [openSub_adj, Sym2.map_mk]
    exact and_congr φ.map_rel_iff Iff.rfl

Uses 2 · Used by 1

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

Used byIsomorphism invariance of the ambient FK normalizer

LemmaIsomorphism invariance of the ambient FK normalizer#✓fully proved

The ambient FK normalizer is invariant under graph isomorphism.

lemma fsm_fkZ_iso (φ : G ≃g H) (p q : ℝ) :
    fkZ G p q = fkZ H p q

Uses 8 · Used by 10

Statement usesAmbient FK normalizer

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Unnormalized random-cluster weight · Graph isomorphism restricted to open subgraphs · Bijection of unordered pairs induced by a bijection · 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\) · Subadditivity of \(-\log Z\) along a juxtaposition sequence · Orthant blocks have the FK partition function of \(\Lambda_K\) · Iterated and single induced graphs share the FK partition function · Induced graphs with equal range have equal FK partition functions · Peeling bound for \(-\log Z\) of a tagged graph · The all-tag restriction has the partition function of \(\Lambda_{2K+1}\) · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function

LemmaSubadditivity of \(-\log Z\) along a juxtaposition sequence#✓fully proved

Along a sequence with G_{m+n} ≅ G_m ⊕g G_n, the sequence -log Z_{G_n} is subadditive.

lemma fsm_subadditive_neglog_fkZ {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (hjux : ∀ m n, Gn (m + n) ≃g Gn m ⊕g Gn n) :
    Subadditive (fun n => -Real.log (fkZ (Gn n) p q))

Uses 7

Statement usesAmbient FK normalizer

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Unnormalized random-cluster weight · Isomorphism invariance of the ambient FK normalizer · Ambient FK normalizer is supermultiplicative under disjoint union · Number of open clusters

LemmaEdgeless graphs satisfy the juxtaposition hypothesis#✓fully proved

Edgeless graphs on Fin n satisfy the juxtaposition hypothesis G_{m+n} ≅ G_m ⊕g G_n.

lemma fsm_juxtaposition_satisfiable (m n : ℕ) :
    Nonempty ((⊥ : SimpleGraph (Fin (m + n))) ≃g
      (⊥ : SimpleGraph (Fin m)) ⊕g (⊥ : SimpleGraph (Fin n)))

DefinitionIsomorphism of induced graphs from injections with equal range#✓fully proved

Graphs induced on K₀ by two injections with the same range are isomorphic.

noncomputable def qp_comapIsoOfRangeEq {V W : Type*} (f : V → U) (g : W → U)
    (hf : Function.Injective f) (hg : Function.Injective g) (hr : Set.range f = Set.range g) :
    K₀.comap f ≃g K₀.comap g where
  toEquiv :=
    (Equiv.ofInjective f hf).trans ((Set.equivOfEq hr).trans (Equiv.ofInjective g hg).symm)
  map_rel_iff' := by
    intro a b
    simp only [comap_adj, Equiv.trans_apply]
    have key : ∀ z : V,
        g ((Equiv.ofInjective g hg).symm ((Set.equivOfEq hr) ((Equiv.ofInjective f hf) z))) = f z :=
      fun z => by rw [Equiv.apply_ofInjective_symm hg]; rfl
    rw [key a, key b]

Used by 1

Used byInduced graphs with equal range have equal FK partition functions

LemmaInduced graphs with equal range have equal FK partition functions#✓fully proved

Graphs induced by two injections with the same range have the same FK partition function.

lemma qp_fkZ_comap_range {V W : Type*} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W]
    (f : V → U) (g : W → U) (hf : Function.Injective f) (hg : Function.Injective g)
    (hr : Set.range f = Set.range g) (p q : ℝ)
    [DecidableRel (K₀.comap f).Adj] [DecidableRel (K₀.comap g).Adj] :
    fkZ (K₀.comap f) p q = fkZ (K₀.comap g) p q

Uses 3

Statement usesAmbient FK normalizer

Proof usesIsomorphism invariance of the ambient FK normalizer · Isomorphism of induced graphs from injections with equal range

LemmaFK partition function at least the all-closed weight for \(q \ge 1\)#✓fully proved

For q ≥ 1, the FK partition function is at least the weight (1 - p)^{|E|} of the all- closed configuration.

lemma qp_fkZ_ge_allClosed {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
    [DecidableRel G.Adj] {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq1 : 1 ≤ q) :
    (1 - p) ^ G.edgeFinset.card ≤ fkZ G p q

Uses 5 · Used by 1

Statement usesAmbient FK normalizer

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Unnormalized random-cluster weight · Number of open clusters

Used byBound \(-\log Z \le |E|\,(-\log(1-p))\) for \(q \ge 1\)

LemmaBound \(-\log Z \le |E|\,(-\log(1-p))\) for \(q \ge 1\)#✓fully proved

For q ≥ 1, -log Z ≤ |E| · (-log (1 - p)).

lemma qp_neglogZ_le_edges {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
    [DecidableRel G.Adj] {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq1 : 1 ≤ q) :
    -Real.log (fkZ G p q) ≤ (G.edgeFinset.card : ℝ) * (-Real.log (1 - p))

Uses 6 · Used by 1

Statement usesAmbient FK normalizer

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli edge product · Unnormalized random-cluster weight · Number of open clusters · FK partition function at least the all-closed weight for \(q \ge 1\)

Used byDoubling inequality for \(-\log Z\) of the free \(q = 2\) FK model

DefinitionGraph induced on vertices with tags in \(S\)#✓fully proved

The graph induced on the vertices whose tag lies in S.

noncomputable def qp_restG (S : Finset T) : SimpleGraph {x : U // tag x ∈ S} :=
  K₀.comap Subtype.val

Used by 12

Used byDoubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Doubling inequality for \(-\log Z\) of the free \(q = 2\) FK model · Left part of a tag split has the block partition function · Peeling bound for \(-\log Z\) of a tagged graph · Restriction does not increase straddling edges of a tag · The all-tag restriction has the partition function of \(\Lambda_{2K+1}\) · Isomorphism from the all-tag restriction to \(\Lambda_{2K+1}\) · Right part of a tag split has the restricted partition function · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Restriction of a box to all tiling tags

DefinitionBlock of a tag: graph induced on its vertices#✓fully proved

The block of tag τ: the graph induced on the vertices with tag τ.

noncomputable def qp_blkG (τ : T) : SimpleGraph {x : U // tag x = τ} := K₀.comap Subtype.val

Used by 10

Used byDoubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · The hyperplane block has at most \(2d|J|\) edges · Orthant blocks have the FK partition function of \(\Lambda_K\) · Doubling inequality for \(-\log Z\) of the free \(q = 2\) FK model · Left part of a tag split has the block partition function · Peeling bound for \(-\log Z\) of a tagged graph · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function · Graph isomorphism between a sub-box and a tiling cell

DefinitionStraddling of a predicate by an edge#✓fully proved

An edge straddles P if exactly one endpoint satisfies P.

def qp_straddleP (P : U → Prop) [DecidablePred P] : Sym2 U → Prop :=
  Sym2.lift ⟨fun a b => (P a ∧ ¬ P b) ∨ (¬ P a ∧ P b),
    by intro a b; by_cases ha : P a <;> by_cases hb : P b <;> simp [ha, hb]⟩

Used by 4

Used byInterface edges of a split are at most the straddling edges · Restriction does not increase straddling edges of a tag · Set of edges straddling a predicate · Edges straddling a tag are incident to the hyperplane set

DefinitionSet of edges straddling a predicate#✓fully proved

The edges of K₀ that straddle P.

noncomputable def qp_straddleEdges (P : U → Prop) [DecidablePred P] : Finset (Sym2 U) :=
  K₀.edgeFinset.filter (qp_straddleP P)

Uses 1 · Used by 8

Statement usesStraddling of a predicate by an edge

Used byDoubling bound for the box free energy when \(q \ge 1\) · Doubling inequality for \(-\log Z\) of the free \(q = 2\) FK model · Interface edges of a split are at most the straddling edges · Peeling bound for \(-\log Z\) of a tagged graph · Restriction does not increase straddling edges of a tag · At most \(2d|J|\) edges straddle an orthant tag · Edges straddling a tag are incident to the hyperplane set · Boxes satisfy the additive doubling bound for \(d \ge 1\)

DefinitionIsomorphism of an iterated induced graph with a single one#✓fully proved

An iterated induced graph is isomorphic to the graph induced by any injection with the same range as the composite.

noncomputable def qp_comapComapIso {V W X : Type*} (g : W → U) (f : V → W) (h : X → U)
    (hgf : Function.Injective (g ∘ f)) (hh : Function.Injective h)
    (hr : Set.range (g ∘ f) = Set.range h) :
    (K₀.comap g).comap f ≃g K₀.comap h where
  toEquiv := (Equiv.ofInjective (g ∘ f) hgf).trans
    ((Set.equivOfEq hr).trans (Equiv.ofInjective h hh).symm)
  map_rel_iff' := by
    intro a b; simp only [comap_adj, Equiv.trans_apply]
    have key : ∀ z : V,
        h ((Equiv.ofInjective h hh).symm ((Set.equivOfEq hr) ((Equiv.ofInjective (g ∘ f) hgf) z)))
          = g (f z) := fun z => by rw [Equiv.apply_ofInjective_symm hh]; rfl
    rw [key a, key b]

Used by 5

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

LemmaIterated and single induced graphs share the FK partition function#✓fully proved

An iterated induced graph has the FK partition function of the graph induced by any injection with the same range.

lemma qp_fkZ_comapComap {V W X : Type*} [Fintype V] [Fintype X] [DecidableEq V] [DecidableEq X]
    (g : W → U) (f : V → W) (h : X → U) (hgf : Function.Injective (g ∘ f))
    (hh : Function.Injective h) (hr : Set.range (g ∘ f) = Set.range h) (p q : ℝ)
    [DecidableRel ((K₀.comap g).comap f).Adj] [DecidableRel (K₀.comap h).Adj] :
    fkZ ((K₀.comap g).comap f) p q = fkZ (K₀.comap h) p q

Uses 3 · Used by 2

Statement usesAmbient FK normalizer

Proof usesIsomorphism invariance of the ambient FK normalizer · Isomorphism of an iterated induced graph with a single one

Used byLeft part of a tag split has the block partition function · Right part of a tag split has the restricted partition function

LemmaLeft part of a tag split has the block partition function#✓fully proved

The left part of the restriction to insert τ S, split by tag τ, has the partition function of the block of τ.

lemma qp_left_eq (τ : T) (S : Finset T) (hτ : τ ∉ S) (p q : ℝ) :
    fkZ (agl_left (qp_restG K₀ tag (insert τ S)) (fun x => tag x.1 = τ)) p q
      = fkZ (qp_blkG K₀ tag τ) p q

Uses 5 · Used by 1

Statement usesGraph induced on the vertices satisfying a predicate · Ambient FK normalizer · Block of a tag: graph induced on its vertices · Graph induced on vertices with tags in \(S\)

Proof usesIterated and single induced graphs share the FK partition function

Used byPeeling bound for \(-\log Z\) of a tagged graph

LemmaRight part of a tag split has the restricted partition function#✓fully proved

The right part of the restriction to insert τ S, split by tag τ, has the partition function of the restriction to S.

lemma qp_right_eq (τ : T) (S : Finset T) (hτ : τ ∉ S) (p q : ℝ) :
    fkZ (agl_right (qp_restG K₀ tag (insert τ S)) (fun x => tag x.1 = τ)) p q
      = fkZ (qp_restG K₀ tag S) p q

Uses 5 · Used by 1

Statement usesGraph induced on the vertices failing a predicate · Ambient FK normalizer · Graph induced on vertices with tags in \(S\)

Proof usesGraph induced on the vertices satisfying a predicate · Iterated and single induced graphs share the FK partition function

Used byPeeling bound for \(-\log Z\) of a tagged graph

LemmaInterface edges of a split are at most the straddling edges#✓fully proved

The interface of the left/right split by P has at most as many edges as there are edges straddling P.

lemma qp_interface_le_straddle (P : U → Prop) [DecidablePred P] :
    agl_interfaceCard K₀ P ≤ (qp_straddleEdges K₀ P).card

Uses 8 · Used by 3

Statement usesNumber of edges between a vertex subset and its complement · Set of edges straddling a predicate

Proof usesGraph transported to the sum of a subset and its complement · 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 · Interface edges of a graph on a disjoint union · Straddling of a predicate by an edge

Used byDoubling bound for the box free energy when \(q \ge 1\) · Peeling bound for \(-\log Z\) of a tagged graph · Boxes satisfy the additive doubling bound for \(d \ge 1\)

LemmaRestriction does not increase straddling edges of a tag#✓fully proved

Restricting to insert τ S does not increase the number of edges straddling tag τ.

lemma qp_restG_straddle_le (τ : T) (S : Finset T) :
    (qp_straddleEdges (qp_restG K₀ tag (insert τ S)) (fun x => tag x.1 = τ)).card
      ≤ (qp_straddleEdges K₀ (fun u => tag u = τ)).card

Uses 3 · Used by 3

Statement usesGraph induced on vertices with tags in \(S\) · Set of edges straddling a predicate

Proof usesStraddling of a predicate by an edge

Used byDoubling bound for the box free energy when \(q \ge 1\) · Peeling bound for \(-\log Z\) of a tagged graph · Boxes satisfy the additive doubling bound for \(d \ge 1\)

LemmaFK partition function of a graph with no vertices is one#✓fully proved

The FK partition function of a graph with no vertices is 1.

lemma qp_fkZ_empty {V : Type*} [Fintype V] [DecidableEq V] [IsEmpty V] (G : SimpleGraph V)
    [DecidableRel G.Adj] (p q : ℝ) : fkZ G p q = 1

Uses 6 · Used by 5

Statement usesAmbient FK normalizer

Proof usesConfiguration space of a statistical-mechanics model · 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\) · Peeling bound for \(-\log Z\) of a tagged graph · Boxes satisfy the additive doubling bound for \(d \ge 1\) · Van Hove tiling bound for the edge partition function

DefinitionNegative log of the ambient FK normalizer#✓fully proved

The negative log ambient normalizer -log (fkZ G p q), including unused coordinates.

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

Uses 1 · Used by 2

Statement usesAmbient FK normalizer

Used byDoubling inequality for \(-\log Z\) of the free \(q = 2\) FK model · Peeling bound for \(-\log Z\) of a tagged graph

LemmaPeeling bound for \(-\log Z\) of a tagged graph#✓fully proved

Peeling: -log Z of the restriction to S is at most the sum over τ ∈ S of -log Z of the blocks plus I · (-log (1 - p)), with I at most the number of edges straddling the tags in S.

lemma qp_peel_le (p q : ℝ) (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    ∀ S : Finset T, ∃ I : ℕ,
      qp_ambientNegLogZ (qp_restG K₀ tag S) p q
          ≤ (∑ τ ∈ S, qp_ambientNegLogZ (qp_blkG K₀ tag τ) p q) + (I : ℝ) * (-Real.log (1 - p))
        ∧ I ≤ ∑ τ ∈ S, (qp_straddleEdges K₀ (fun u => tag u = τ)).card

Uses 26 · Used by 1

Statement usesNegative log of the ambient FK normalizer · Block of a tag: graph induced on its vertices · Graph induced on vertices with tags in \(S\) · Set of edges straddling a predicate

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 · 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 · Connected components of a disjoint union of graphs · Gluing edge configurations on a disjoint union · Isomorphism invariance of the ambient FK normalizer · Number of open clusters · Open subgraph of an edge configuration · FK partition function of a graph with no vertices is one · Interface edges of a split are at most the straddling edges · Left part of a tag split has the block partition function · Restriction does not increase straddling edges of a tag · Right part of a tag split has the restricted partition function

Used byDoubling inequality for \(-\log Z\) of the free \(q = 2\) FK model

DefinitionOrdered nearest-neighbour pairs of \(\Lambda_n\) in direction \(i\)#✓fully proved

The ordered nearest-neighbor pairs of Λ_n that differ in coordinate i.

noncomputable def edgeAxisI (d n : ℕ) (i : Fin d) : Finset (Site d × Site d) :=
  (boxSV_edgeF d n).filter (fun p => p.1 i ≠ p.2 i)

Uses 2 · Used by 6

Statement usesSite of the hypercubic lattice · Nearest-neighbour pairs inside the box \((-n, n)^d\)

Used by\(\Lambda_n\) has \(4n(2n+1)^{d-1}\) ordered pairs in each direction · Ordered pairs in different directions are disjoint · Pairs in direction \(i\) are the forward and backward shifts · \(\Lambda_n\) has \(4dn(2n+1)^{d-1}\) ordered nearest-neighbour pairs · Ordered neighbour pairs of \(\Lambda_n\) as a union over directions · Unit shifts of sites staying in the box are pairs in direction \(i\)

DefinitionSites of \(\Lambda_n\) whose shift in coordinate \(i\) stays in the box#✓fully proved

The sites of Λ_n whose shift by b in coordinate i stays in Λ_n.

noncomputable def shiftDom (d n : ℕ) (i : Fin d) (b : ℤ) : Finset (Site d) :=
  (boxSV_boxF d n).filter (fun x => x i + b ∈ Finset.Icc (-(n : ℤ)) n)

Uses 2 · Used by 5

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) as a finite set of sites

Used by\(\Lambda_n\) has \(4n(2n+1)^{d-1}\) ordered pairs in each direction · \(2n(2n+1)^{d-1}\) sites of \(\Lambda_n\) stay inside after a unit shift · Pairs in direction \(i\) are the forward and backward shifts · Forward and backward shift pairs are disjoint · Unit shifts of sites staying in the box are pairs in direction \(i\)

DefinitionShift map \(x \mapsto (x, x + b e_i)\)#✓fully proved

The ordered pair (x, x + b e_i).

noncomputable def shiftMap (d n : ℕ) (i : Fin d) (b : ℤ) (x : Site d) : Site d × Site d :=
  (x, Function.update x i (x i + b))

Uses 1 · Used by 5

Statement usesSite of the hypercubic lattice

Used by\(\Lambda_n\) has \(4n(2n+1)^{d-1}\) ordered pairs in each direction · Pairs in direction \(i\) are the forward and backward shifts · Forward and backward shift pairs are disjoint · Injectivity of the shift map · Unit shifts of sites staying in the box are pairs in direction \(i\)

LemmaA site is adjacent to its unit shift in one coordinate#✓fully proved

A site is adjacent to its shift by ±1 in one coordinate.

lemma shift_adj (d n : ℕ) (i : Fin d) (x : Site d) (b : ℤ) (hb : b = 1 ∨ b = -1) :
    (hypercubicLattice d).Adj x (Function.update x i (x i + b))

Uses 2 · Used by 1

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byUnit shifts of sites staying in the box are pairs in direction \(i\)

Lemma\(2n(2n+1)^{d-1}\) sites of \(\Lambda_n\) stay inside after a unit shift#✓fully proved

For b = ±1, 2n (2n + 1)^{d-1} sites of Λ_n stay in Λ_n after the shift.

lemma card_shiftDom (d n : ℕ) (i : Fin d) (b : ℤ) (hb : b = 1 ∨ b = -1) (hd : 1 ≤ d) :
    (shiftDom d n i b).card = (2 * n) * (2 * n + 1) ^ (d - 1)

Uses 3 · Used by 1

Statement usesSites of \(\Lambda_n\) whose shift in coordinate \(i\) stays in the box · Site of the hypercubic lattice

Proof usesBox \((-n, n)^d\) as a finite set of sites

Used by\(\Lambda_n\) has \(4n(2n+1)^{d-1}\) ordered pairs in each direction

LemmaUnit shifts of sites staying in the box are pairs in direction \(i\)#✓fully proved

For b = ±1, the shift of a site that stays in the box gives a pair in direction i.

lemma shiftMap_mem (d n : ℕ) (i : Fin d) (b : ℤ) (hb : b = 1 ∨ b = -1) (x : Site d)
    (hx : x ∈ shiftDom d n i b) : shiftMap d n i b x ∈ edgeAxisI d n i

Uses 8 · Used by 1

Statement usesOrdered nearest-neighbour pairs of \(\Lambda_n\) in direction \(i\) · Sites of \(\Lambda_n\) whose shift in coordinate \(i\) stays in the box · Shift map \(x \mapsto (x, x + b e_i)\) · Site of the hypercubic lattice

Proof usesA site is adjacent to its unit shift in one coordinate · Box \((-n, n)^d\) as a finite set of sites · Nearest-neighbour pairs inside the box \((-n, n)^d\) · Hypercubic lattice \(\mathbb{Z}^d\)

Used byPairs in direction \(i\) are the forward and backward shifts

LemmaInjectivity of the shift map#✓fully proved

The shift map is injective.

lemma shiftMap_inj (d n : ℕ) (i : Fin d) (b : ℤ) : Function.Injective (shiftMap d n i b)

Uses 2 · Used by 1

Statement usesShift map \(x \mapsto (x, x + b e_i)\) · Site of the hypercubic lattice

Used by\(\Lambda_n\) has \(4n(2n+1)^{d-1}\) ordered pairs in each direction

LemmaPairs in direction \(i\) are the forward and backward shifts#✓fully proved

The pairs in direction i are the forward and the backward shifts.

lemma edgeAxisI_eq (d n : ℕ) (i : Fin d) :
    edgeAxisI d n i = (shiftDom d n i 1).image (shiftMap d n i 1)
        ∪ (shiftDom d n i (-1)).image (shiftMap d n i (-1))

Uses 8 · Used by 1

Statement usesOrdered nearest-neighbour pairs of \(\Lambda_n\) in direction \(i\) · Sites of \(\Lambda_n\) whose shift in coordinate \(i\) stays in the box · Shift map \(x \mapsto (x, x + b e_i)\) · Site of the hypercubic lattice

Proof usesUnit shifts of sites staying in the box are pairs in direction \(i\) · Box \((-n, n)^d\) as a finite set of sites · Nearest-neighbour pairs inside the box \((-n, n)^d\) · Hypercubic lattice \(\mathbb{Z}^d\)

Used by\(\Lambda_n\) has \(4n(2n+1)^{d-1}\) ordered pairs in each direction

LemmaForward and backward shift pairs are disjoint#✓fully proved

Forward and backward pairs in one direction are disjoint.

lemma fwd_bwd_disjoint (d n : ℕ) (i : Fin d) :
    Disjoint ((shiftDom d n i 1).image (shiftMap d n i 1))
        ((shiftDom d n i (-1)).image (shiftMap d n i (-1)))

Uses 3 · Used by 1

Statement usesSites of \(\Lambda_n\) whose shift in coordinate \(i\) stays in the box · Shift map \(x \mapsto (x, x + b e_i)\) · Site of the hypercubic lattice

Used by\(\Lambda_n\) has \(4n(2n+1)^{d-1}\) ordered pairs in each direction

Lemma\(\Lambda_n\) has \(4n(2n+1)^{d-1}\) ordered pairs in each direction#✓fully proved

There are 2 · 2n (2n + 1)^{d-1} ordered pairs in each direction.

lemma card_edgeAxisI (d n : ℕ) (i : Fin d) (hd : 1 ≤ d) :
    (edgeAxisI d n i).card = 2 * ((2 * n) * (2 * n + 1) ^ (d - 1))

Uses 8 · Used by 1

Statement usesOrdered nearest-neighbour pairs of \(\Lambda_n\) in direction \(i\) · Site of the hypercubic lattice

Proof uses\(2n(2n+1)^{d-1}\) sites of \(\Lambda_n\) stay inside after a unit shift · Pairs in direction \(i\) are the forward and backward shifts · Forward and backward shift pairs are disjoint · Sites of \(\Lambda_n\) whose shift in coordinate \(i\) stays in the box · Shift map \(x \mapsto (x, x + b e_i)\) · Injectivity of the shift map

Used by\(\Lambda_n\) has \(4dn(2n+1)^{d-1}\) ordered nearest-neighbour pairs

LemmaOrdered neighbour pairs of \(\Lambda_n\) as a union over directions#✓fully proved

The ordered nearest-neighbor pairs of Λ_n are the union over directions.

lemma edgeF_biUnion (d n : ℕ) :
    (boxSV_edgeF d n) = Finset.univ.biUnion (fun i : Fin d => edgeAxisI d n i)

Uses 5 · Used by 1

Statement usesOrdered nearest-neighbour pairs of \(\Lambda_n\) in direction \(i\) · Site of the hypercubic lattice · Nearest-neighbour pairs inside the box \((-n, n)^d\)

Proof usesBox \((-n, n)^d\) as a finite set of sites · Hypercubic lattice \(\mathbb{Z}^d\)

Used by\(\Lambda_n\) has \(4dn(2n+1)^{d-1}\) ordered nearest-neighbour pairs

LemmaOrdered pairs in different directions are disjoint#✓fully proved

Pairs in different directions are disjoint.

lemma edgeAxis_disjoint (d n : ℕ) (i j : Fin d) (hij : i ≠ j) :
    Disjoint (edgeAxisI d n i) (edgeAxisI d n j)

Uses 5 · Used by 1

Statement usesOrdered nearest-neighbour pairs of \(\Lambda_n\) in direction \(i\) · Site of the hypercubic lattice

Proof usesBox \((-n, n)^d\) as a finite set of sites · Nearest-neighbour pairs inside the box \((-n, n)^d\) · Hypercubic lattice \(\mathbb{Z}^d\)

Used by\(\Lambda_n\) has \(4dn(2n+1)^{d-1}\) ordered nearest-neighbour pairs

Lemma\(\Lambda_n\) has \(4dn(2n+1)^{d-1}\) ordered nearest-neighbour pairs#✓fully proved

The box Λ_n has d · 2 · 2n (2n + 1)^{d-1} ordered nearest-neighbor pairs.

lemma edgeCard_eq (d n : ℕ) (hd : 1 ≤ d) :
    boxSV_edgeCard d n = d * (2 * ((2 * n) * (2 * n + 1) ^ (d - 1)))

Uses 7 · Used by 1

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

Proof uses\(\Lambda_n\) has \(4n(2n+1)^{d-1}\) ordered pairs in each direction · Ordered nearest-neighbour pairs of \(\Lambda_n\) in direction \(i\) · Ordered pairs in different directions are disjoint · Ordered neighbour pairs of \(\Lambda_n\) as a union over directions · Site of the hypercubic lattice · Nearest-neighbour pairs inside the box \((-n, n)^d\)

Used by\(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges

Lemma\(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges#✓fully proved

The box Λ_n has d · 2n (2n + 1)^{d-1} edges.

lemma boxGraph_edgeCard (d n : ℕ) (hd : 1 ≤ d) :
    (boxGraph d n).edgeFinset.card = d * ((2 * n) * (2 * n + 1) ^ (d - 1))

Uses 9 · Used by 9

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 uses\(\Lambda_n\) has \(4dn(2n+1)^{d-1}\) ordered nearest-neighbour pairs · 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-edge free energy converges along \(K_j\) for \(d, q \ge 1\) · Van Hove limit · Uniform upper bound on the box free energy for \(d, n, q \ge 1\) · 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\) · Per-box \(q = 2\) uniqueness off a countable set of tilts · Per-edge free energy of boxes converges for \(d \ge 1\) · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set

DefinitionTranslation vector onto an orthant of \(\Lambda_{2K+1}\)#✓fully proved

The translation vector (±(K + 1))_i that moves Λ_K onto the orthant with sign pattern s.

def qp_vshift (d K : ℕ) (s : Fin d → Bool) : Site d :=
  fun i => if s i then (K + 1 : ℤ) else -(K + 1 : ℤ)

Uses 1 · Used by 4

Statement usesSite of the hypercubic lattice

Used byDoubling bound for the box free energy when \(q \ge 1\) · Orthant blocks have the FK partition function of \(\Lambda_K\) · Translation of \(\Lambda_K\) onto an orthant block of \(\Lambda_{2K+1}\) · Boxes satisfy the additive doubling bound for \(d \ge 1\)

Lemma\(|x| \le n\) iff \(-n \le x \le n\) for an integer \(x\)#✓fully proved

|x| ≤ n for an integer, written with natAbs.

lemma qp_natAbs_iff (x : ℤ) (n : ℕ) : x.natAbs ≤ n ↔ -(n : ℤ) ≤ x ∧ x ≤ n

Used by 3

Used byCoordinate description of the sites with a given orthant tag · Translation of \(\Lambda_K\) onto an orthant block of \(\Lambda_{2K+1}\) · Translation between a sub-box and a tiling cell

DefinitionOrthant tag of a site of \(\Lambda_{2K+1}\)#✓fully proved

The orthant tag of a site of Λ_{2K+1}: none on a coordinate hyperplane, otherwise its sign pattern.

noncomputable def qp_boxTag (d K : ℕ) (x : boxVerts d (2 * K + 1)) : Option (Fin d → Bool) :=
  if (∃ i, (x : Site d) i = 0) then none else some (fun i => decide (0 < (x : Site d) i))

Uses 3 · Used by 14

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

Used byDoubling bound for the box free energy when \(q \ge 1\) · The hyperplane block has at most \(2d|J|\) edges · Orthant blocks have the FK partition function of \(\Lambda_K\) · Doubling inequality for \(-\log Z\) of the free \(q = 2\) FK model · Coordinate description of the sites with a given orthant tag · Translation of \(\Lambda_K\) onto an orthant block of \(\Lambda_{2K+1}\) · The all-tag restriction has the partition function of \(\Lambda_{2K+1}\) · Isomorphism from the all-tag restriction to \(\Lambda_{2K+1}\) · At most \(2d|J|\) edges straddle an orthant tag · An edge leaving an orthant ends on a coordinate hyperplane · An edge between differently tagged sites meets a coordinate hyperplane · Edges straddling a tag are incident to the hyperplane set · Untagged sites are exactly those on a coordinate hyperplane · Boxes satisfy the additive doubling bound for \(d \ge 1\)

LemmaCoordinate description of the sites with a given orthant tag#✓fully proved

A site has tag s iff each coordinate lies in [1, 2K + 1] or [-(2K + 1), -1] according to s.

lemma qp_boxTag_some_iff (d K : ℕ) (x : boxVerts d (2 * K + 1)) (s : Fin d → Bool) :
    qp_boxTag d K x = some s ↔ ∀ i, if s i then (1 ≤ (x : Site d) i ∧ (x : Site d) i ≤ 2 * K + 1)
              else (-(2 * K + 1 : ℤ) ≤ (x : Site d) i ∧ (x : Site d) i ≤ -1)

Uses 5 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Orthant tag of a site of \(\Lambda_{2K+1}\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof uses\(|x| \le n\) iff \(-n \le x \le n\) for an integer \(x\)

Used byTranslation of \(\Lambda_K\) onto an orthant block of \(\Lambda_{2K+1}\)

DefinitionTranslation of \(\Lambda_K\) onto an orthant block of \(\Lambda_{2K+1}\)#✓fully proved

The translation of Λ_K onto the sites of Λ_{2K+1} with tag s.

StatMech.FK.qp_quadφ · 20 lines

noncomputable def qp_quadφ (d K : ℕ) (s : Fin d → Bool) :
    boxVerts d K ≃ {x : boxVerts d (2 * K + 1) // qp_boxTag d K x = some s} where
  toFun y := ⟨⟨fun i => (y : Site d) i + qp_vshift d K s i, by
      intro i; have hy := (qp_natAbs_iff ((y : Site d) i) K).mp (y.2 i)
      rw [qp_natAbs_iff]; simp only [qp_vshift]
      by_cases hs : s i <;> simp only [hs, ite_true, Bool.false_eq_true, ite_false] <;> omega⟩,
    by rw [qp_boxTag_some_iff]; intro i; have hy := (qp_natAbs_iff ((y : Site d) i) K).mp (y.2 i)
       simp only [qp_vshift]
       by_cases hs : s i <;> simp only [hs, ite_true, Bool.false_eq_true, ite_false] <;>
         omega⟩
  invFun x := ⟨fun i => (x.1 : Site d) i - qp_vshift d K s i, by
      intro i
      have hP : (if s i then (1 ≤ (x.1.1 : Site d) i ∧ (x.1.1 : Site d) i ≤ 2 * K + 1)
              else (-(2 * K + 1 : ℤ) ≤ (x.1.1 : Site d) i ∧ (x.1.1 : Site d) i ≤ -1)) :=
        (qp_boxTag_some_iff d K x.1 s).mp x.2 i
      rw [qp_natAbs_iff]; simp only [qp_vshift]
      by_cases hs : s i <;> simp only [hs, ite_true, Bool.false_eq_true, ite_false] at hP ⊢ <;>
        omega⟩
  left_inv y := by apply Subtype.ext; funext i; simp
  right_inv x := by apply Subtype.ext; apply Subtype.ext; funext i; simp

Uses 7 · Used by 3

Statement usesVertices of the box \((-n, n)^d\) · Orthant tag of a site of \(\Lambda_{2K+1}\) · Coordinate description of the sites with a given orthant tag · \(|x| \le n\) iff \(-n \le x \le n\) for an integer \(x\) · Translation vector onto an orthant of \(\Lambda_{2K+1}\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byDoubling bound for the box free energy when \(q \ge 1\) · Orthant blocks have the FK partition function of \(\Lambda_K\) · Boxes satisfy the additive doubling bound for \(d \ge 1\)

LemmaOrthant blocks have the FK partition function of \(\Lambda_K\)#✓fully proved

Each orthant block of Λ_{2K+1} has the FK partition function of Λ_K.

lemma qp_block_fkZ (d K : ℕ) (s : Fin d → Bool) (p q : ℝ) :
    fkZ (qp_blkG (boxGraph d (2 * K + 1)) (qp_boxTag d K) (some s)) p q
      = fkZ (boxGraph d K) p q

Uses 12 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Ambient FK normalizer · Block of a tag: graph induced on its vertices · Orthant tag of a site of \(\Lambda_{2K+1}\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesGraph induced on the vertices satisfying a predicate · Isomorphism of a box with its translated copy in the predicate part · Isomorphism invariance of the ambient FK normalizer · Translation of \(\Lambda_K\) onto an orthant block of \(\Lambda_{2K+1}\) · Translation vector onto an orthant of \(\Lambda_{2K+1}\)

Used byDoubling inequality for \(-\log Z\) of the free \(q = 2\) FK model

DefinitionHyperplane set of \(\Lambda_{2K+1}\)#✓fully proved

The hyperplane set: sites of Λ_{2K+1} with some coordinate equal to 0.

noncomputable def qp_Jset (d K : ℕ) : Finset (boxVerts d (2 * K + 1)) :=
  Finset.univ.filter (fun x => ∃ i, (x : Site d) i = 0)

Uses 3 · Used by 10

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

Used byBox free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\) · Doubling bound for the box free energy when \(q \ge 1\) · Additive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model · The hyperplane block has at most \(2d|J|\) edges · Doubling inequality for \(-\log Z\) of the free \(q = 2\) FK model · The hyperplane set has at most \(d(4K+3)^{d-1}\) sites · Hyperplane set lies in the union of the coordinate slabs · At most \(2d|J|\) edges straddle an orthant tag · Edges straddling a tag are incident to the hyperplane set · Boxes satisfy the additive doubling bound for \(d \ge 1\)

DefinitionCoordinate slab of \(\Lambda_{2K+1}\)#✓fully proved

The sites of Λ_{2K+1} with coordinate i equal to 0.

noncomputable def qp_Jslab (d K : ℕ) (i : Fin d) : Finset (boxVerts d (2 * K + 1)) :=
  Finset.univ.filter (fun x => (x : Site d) i = 0)

Uses 3 · Used by 3

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

Used byThe hyperplane set has at most \(d(4K+3)^{d-1}\) sites · Hyperplane set lies in the union of the coordinate slabs · A coordinate slab has at most \((4K+3)^{d-1}\) sites

LemmaHyperplane set lies in the union of the coordinate slabs#✓fully proved

The hyperplane set is the union of the coordinate slabs.

lemma qp_Jset_subset_biUnion (d K : ℕ) :
    qp_Jset d K ⊆ Finset.univ.biUnion (fun i : Fin d => qp_Jslab d K i)

Uses 5 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Hyperplane set of \(\Lambda_{2K+1}\) · Coordinate slab of \(\Lambda_{2K+1}\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byThe hyperplane set has at most \(d(4K+3)^{d-1}\) sites

LemmaA coordinate slab has at most \((4K+3)^{d-1}\) sites#✓fully proved

Each coordinate slab has at most (4K + 3)^{d-1} sites.

lemma qp_Jslab_card (d K : ℕ) (hd : 1 ≤ d) (i : Fin d) :
    (qp_Jslab d K i).card ≤ (2 * (2 * K + 1) + 1) ^ (d - 1)

Uses 4 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Coordinate slab of \(\Lambda_{2K+1}\)

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

Used byThe hyperplane set has at most \(d(4K+3)^{d-1}\) sites

LemmaThe hyperplane set has at most \(d(4K+3)^{d-1}\) sites#✓fully proved

The hyperplane set has at most d (4K + 3)^{d-1} sites.

lemma qp_Jset_card_le (d K : ℕ) (hd : 1 ≤ d) :
    (qp_Jset d K).card ≤ d * (2 * (2 * K + 1) + 1) ^ (d - 1)

Uses 7 · Used by 3

Statement usesVertices of the box \((-n, n)^d\) · Hyperplane set of \(\Lambda_{2K+1}\)

Proof usesHyperplane set lies in the union of the coordinate slabs · Coordinate slab of \(\Lambda_{2K+1}\) · A coordinate slab has at most \((4K+3)^{d-1}\) sites · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byBox free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\) · Additive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model · Boxes satisfy the additive doubling bound for \(d \ge 1\)

LemmaVertex degrees in a box are at most \(2d\)#✓fully proved

Every vertex of a box has degree at most 2d. See also MathlibExt...PlanarTopology.degree_le for ℤ^d.

lemma qp_boxGraph_degree_le (d n : ℕ) (v : boxVerts d n) : (boxGraph d n).degree v ≤ 2 * d

Uses 9 · Used by 2

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 usesNearest neighbours in \(\mathbb{Z}^d\) · 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 byThe hyperplane block has at most \(2d|J|\) edges · At most \(2d|J|\) edges straddle an orthant tag

LemmaAn edge leaving an orthant ends on a coordinate hyperplane#✓fully proved

An edge leaving an orthant has an endpoint on a coordinate hyperplane.

lemma qp_straddle_endpoint_in_J (d K : ℕ) (s : Fin d → Bool) (x y : boxVerts d (2 * K + 1))
    (hadj : (boxGraph d (2 * K + 1)).Adj x y) (hx : qp_boxTag d K x = some s)
    (hy : qp_boxTag d K y ≠ some s) : ∃ i, (y : Site d) i = 0

Uses 6 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Orthant tag of a site of \(\Lambda_{2K+1}\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesHypercubic lattice \(\mathbb{Z}^d\)

Used byAn edge between differently tagged sites meets a coordinate hyperplane

LemmaUntagged sites are exactly those on a coordinate hyperplane#✓fully proved

A site has tag none iff it lies on a coordinate hyperplane.

lemma qp_tag_none_iff (d K : ℕ) (x : boxVerts d (2 * K + 1)) :
    qp_boxTag d K x = none ↔ ∃ i, (x : Site d) i = 0

Uses 4 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Orthant tag of a site of \(\Lambda_{2K+1}\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byAn edge between differently tagged sites meets a coordinate hyperplane

LemmaAn edge between differently tagged sites meets a coordinate hyperplane#✓fully proved

An edge between sites of different tags has an endpoint on a coordinate hyperplane.

lemma qp_straddle_endpoint_in_J_all (d K : ℕ) (τ : Option (Fin d → Bool))
    (x y : boxVerts d (2 * K + 1)) (hadj : (boxGraph d (2 * K + 1)).Adj x y)
    (hx : qp_boxTag d K x = τ) (hy : qp_boxTag d K y ≠ τ) :
    (∃ i, (x : Site d) i = 0) ∨ (∃ i, (y : Site d) i = 0)

Uses 7 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Orthant tag of a site of \(\Lambda_{2K+1}\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesAn edge leaving an orthant ends on a coordinate hyperplane · Untagged sites are exactly those on a coordinate hyperplane

Used byEdges straddling a tag are incident to the hyperplane set

LemmaEdges straddling a tag are incident to the hyperplane set#✓fully proved

The edges straddling a tag are incident to the hyperplane set.

lemma qp_straddle_subset_all (d K : ℕ) (τ : Option (Fin d → Bool)) :
    qp_straddleEdges (boxGraph d (2 * K + 1)) (fun x => qp_boxTag d K x = τ)
      ⊆ (qp_Jset d K).biUnion (fun v => (boxGraph d (2 * K + 1)).incidenceFinset v)

Uses 9 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Hyperplane set of \(\Lambda_{2K+1}\) · Orthant tag of a site of \(\Lambda_{2K+1}\) · Set of edges straddling a predicate · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesStraddling of a predicate by an edge · An edge between differently tagged sites meets a coordinate hyperplane

Used byAt most \(2d|J|\) edges straddle an orthant tag

LemmaAt most \(2d|J|\) edges straddle an orthant tag#✓fully proved

At most 2d |J| edges straddle a tag.

lemma qp_straddle_card_le_all (d K : ℕ) (τ : Option (Fin d → Bool)) :
    (qp_straddleEdges (boxGraph d (2 * K + 1)) (fun x => qp_boxTag d K x = τ)).card
      ≤ 2 * d * (qp_Jset d K).card

Uses 9 · Used by 3

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Hyperplane set of \(\Lambda_{2K+1}\) · Orthant tag of a site of \(\Lambda_{2K+1}\) · Set of edges straddling a predicate · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesVertex degrees in a box are at most \(2d\) · Edges straddling a tag are incident to the hyperplane set

Used byDoubling bound for the box free energy when \(q \ge 1\) · Doubling inequality for \(-\log Z\) of the free \(q = 2\) FK model · Boxes satisfy the additive doubling bound for \(d \ge 1\)

LemmaThe hyperplane block has at most \(2d|J|\) edges#✓fully proved

The hyperplane block has at most 2d |J| edges.

lemma qp_blkNone_edge_le (d K : ℕ) :
    (qp_blkG (boxGraph d (2 * K + 1)) (qp_boxTag d K) none).edgeFinset.card
      ≤ 2 * d * (qp_Jset d K).card

Uses 8 · Used by 3

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Hyperplane set of \(\Lambda_{2K+1}\) · Block of a tag: graph induced on its vertices · Orthant tag of a site of \(\Lambda_{2K+1}\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesVertex degrees in a box are at most \(2d\)

Used byDoubling bound for the box free energy when \(q \ge 1\) · Doubling inequality for \(-\log Z\) of the free \(q = 2\) FK model · Boxes satisfy the additive doubling bound for \(d \ge 1\)

DefinitionIsomorphism from the all-tag restriction to \(\Lambda_{2K+1}\)#✓fully proved

The restriction of Λ_{2K+1} to all tags is Λ_{2K+1}.

noncomputable def qp_restGUnivIso (d K : ℕ) :
    qp_restG (boxGraph d (2 * K + 1)) (qp_boxTag d K) Finset.univ ≃g boxGraph d (2 * K + 1) where
  toEquiv := Equiv.subtypeUnivEquiv (fun x => Finset.mem_univ (qp_boxTag d K x))
  map_rel_iff' := by intro a b; rfl

Uses 4 · Used by 3

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Orthant tag of a site of \(\Lambda_{2K+1}\) · Graph induced on vertices with tags in \(S\)

Used byDoubling bound for the box free energy when \(q \ge 1\) · The all-tag restriction has the partition function of \(\Lambda_{2K+1}\) · Boxes satisfy the additive doubling bound for \(d \ge 1\)

LemmaThe all-tag restriction has the partition function of \(\Lambda_{2K+1}\)#✓fully proved

The restriction to all tags has the partition function of Λ_{2K+1}.

lemma qp_restG_univ_fkZ (d K : ℕ) (p q : ℝ) :
    fkZ (qp_restG (boxGraph d (2 * K + 1)) (qp_boxTag d K) Finset.univ) p q
      = fkZ (boxGraph d (2 * K + 1)) p q

Uses 9 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Ambient FK normalizer · Orthant tag of a site of \(\Lambda_{2K+1}\) · Graph induced on vertices with tags in \(S\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesIsomorphism invariance of the ambient FK normalizer · Isomorphism from the all-tag restriction to \(\Lambda_{2K+1}\)

Used byDoubling inequality for \(-\log Z\) of the free \(q = 2\) FK model

LemmaDoubling inequality for \(-\log Z\) of the free \(q = 2\) FK model#✓fully proved

The doubling inequality u(2K + 1) ≤ 2^d u(K) + I_K · (-log (1 - p)) for u = -log Z of the free q = 2 FK model, with I_K = (2^d + 2) · 2d |J|.

lemma qp_box_neglog_doubling (d K : ℕ) (t : ℝ) :
    agl_ambientNegLogZ d t (2 * K + 1) ≤ (2 : ℝ) ^ d * agl_ambientNegLogZ d t K
      + ((2 * d * (qp_Jset d K).card + (2 ^ d + 1) * (2 * d * (qp_Jset d K).card) : ℕ) : ℝ)
          * (-Real.log (1 - fsc_logistic t))

Uses 19 · Used by 1

Statement usesNegative log ambient normalizer of a box · Vertices of the box \((-n, n)^d\) · Logistic function \(e^t/(1+e^t)\) · Hyperplane set of \(\Lambda_{2K+1}\)

Proof usesNearest-neighbour graph on a box · Ambient FK normalizer · Negative log of the ambient FK normalizer · Block of a tag: graph induced on its vertices · The hyperplane block has at most \(2d|J|\) edges · Orthant blocks have the FK partition function of \(\Lambda_K\) · Orthant tag of a site of \(\Lambda_{2K+1}\) · Bound \(-\log Z \le |E|\,(-\log(1-p))\) for \(q \ge 1\) · Peeling bound for \(-\log Z\) of a tagged graph · Graph induced on vertices with tags in \(S\) · The all-tag restriction has the partition function of \(\Lambda_{2K+1}\) · Set of edges straddling a predicate · At most \(2d|J|\) edges straddle an orthant tag · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byAdditive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model

Lemma\(\Lambda_{2K+1}\) has at least \(2^d\) times as many edges as \(\Lambda_K\)#✓fully proved

The 2^d orthant copies of Λ_K have at most as many edges as Λ_{2K+1}.

lemma qp_edge_le (d K : ℕ) (hd : 1 ≤ d) :
    (2 : ℝ) ^ d * ((boxGraph d K).edgeFinset.card)
      ≤ ((boxGraph d (2 * K + 1)).edgeFinset.card)

Uses 5 · 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

Proof uses\(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges

Used byBox free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\) · Additive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model · Boxes satisfy the additive doubling bound for \(d \ge 1\)

LemmaBound on the edge gap \(|E(\Lambda_{2K+1})| - 2^d |E(\Lambda_K)|\)#✓fully proved

The edge-number gap |E(Λ_{2K+1})| - 2^d |E(Λ_K)| is at most d (d + 2)(4K + 3)^{d-1}.

lemma qp_edge_gap_le (d K : ℕ) (hd : 1 ≤ d) :
    (((boxGraph d (2 * K + 1)).edgeFinset.card : ℝ))
        - (2 : ℝ) ^ d * ((boxGraph d K).edgeFinset.card)
      ≤ (d : ℝ) * (d + 2) * (4 * K + 3) ^ (d - 1)

Uses 5 · 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

Proof uses\(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges

Used byBox free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\) · Additive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model · Boxes satisfy the additive doubling bound for \(d \ge 1\)

LemmaLower bound \(n(2n+1)^{d-1}\) on the number of edges of \(\Lambda_n\)#✓fully proved

The box Λ_n has at least n (2n + 1)^{d-1} edges.

lemma qp_edge_lower (d n : ℕ) (hd : 1 ≤ d) :
    (n : ℝ) * (2 * (n : ℝ) + 1) ^ (d - 1) ≤ ((boxGraph d n).edgeFinset.card : ℝ)

Uses 9 · 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

Proof usesBox \((-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 · Hypercubic lattice \(\mathbb{Z}^d\)

Used bySummability of doubling corrections relative to edge counts

LemmaSummability of doubling corrections relative to edge counts#✓fully proved

Corrections of order K_j^{d-1} divided by |E(Λ_{K_{j+1}})| are summable along K_j = 2^{j+1} - 1.

lemma qp_summable_ratio (d : ℕ) (hd : 1 ≤ d) (I : ℕ → ℝ)
    (hIbd : ∀ j,
      I j ≤ ((2 ^ d + 2) * (2 * d * d) + d * (d + 2) : ℝ) * (4 * (agl_K j : ℝ) + 3) ^ (d - 1))
    (hI0 : ∀ j, 0 ≤ I j) :
    Summable (fun j => I j / agl_E d (agl_K (j + 1)))

Uses 7 · Used by 3

Statement usesNumber of edges of a box · Scales \(K_j = 2^{j+1} - 1\)

Proof usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Lower bound \(n(2n+1)^{d-1}\) on the number of edges of \(\Lambda_n\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byBox free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\) · Additive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model · Boxes satisfy the additive doubling bound for \(d \ge 1\)

LemmaAdditive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model#✓fully proved

The additive doubling bound for u = -log Z of the free q = 2 FK model along the doubling boxes K_j = 2^{j+1} - 1, in every dimension d ≥ 1.

lemma qp_additiveDoublingBound (d : ℕ) (hd : 1 ≤ d) (t : ℝ) : agl_AdditiveDoublingBound d t

Uses 15 · Used by 1

Statement usesAdditive doubling bound along the scales \(K_j\)

Proof usesNumber of edges of a box · Scales \(K_j = 2^{j+1} - 1\) · Negative log ambient normalizer of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Logistic function \(e^t/(1+e^t)\) · Hyperplane set of \(\Lambda_{2K+1}\) · The hyperplane set has at most \(d(4K+3)^{d-1}\) sites · Doubling inequality for \(-\log Z\) of the free \(q = 2\) FK model · 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\) · Summability of doubling corrections relative to edge counts · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byBox Fekete data from a uniform bound and an oscillation bound

LemmaBox Fekete data from a uniform bound and an oscillation bound#✓fully proved

The box Fekete data for the free q = 2 FK model from a uniform bound on u / |E| along doubling boxes and an oscillation bound between general and doubling boxes.

lemma qp_additiveBoxFeketeData (d : ℕ) (hd : 1 ≤ d) (t : ℝ)
    (hbdd : ∃ M : ℝ, ∀ j, |agl_ambientNegLogZ d t (agl_K j) / agl_E d (agl_K j)| ≤ M)
    (hosc : ∃ (bj : ℕ → ℕ) (osc : ℕ → ℝ), Tendsto bj atTop atTop ∧ Tendsto osc atTop (𝓝 0)
        ∧ (∀ n, |ivp2_ambientTiltLogZ (boxGraph d n) 2 t
            - ivp2_ambientTiltLogZ (boxGraph d (agl_K (bj n))) 2 t| ≤ osc (bj n))) :
    agl_AdditiveBoxFeketeData d t

Uses 11

Statement usesAssumed doubling, boundedness and oscillation data along \(K_j\) · Number of edges of a box · Scales \(K_j = 2^{j+1} - 1\) · Negative log ambient normalizer of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Ambient tilted log normalizer of a finite graph · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesAdditive doubling bound along the scales \(K_j\) · Additive doubling bound for \(-\log Z\) of the free \(q = 2\) FK model

LemmaRandom-cluster weight is at most \(q^{|V|}\) for \(q \ge 1\)#✓fully proved

For q ≥ 1 every random-cluster weight is at most q ^ |V|. The case q = 2 is ecz_fkWeight_le.

lemma fkc_fkWeight_le {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq1 : 1 ≤ q)
    (ω : ConfigSpace (Sym2 V)) :
    fkWeight G p q ω ≤ q ^ Fintype.card V

Uses 5 · Used by 1

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

Proof usesBernoulli edge product · Number of open clusters · Open subgraph of an edge configuration

Used byEdge partition function is at most \(2^{|E|} q^{|V|}\) for \(q \ge 1\)

LemmaEdge partition function is at most \(2^{|E|} q^{|V|}\) for \(q \ge 1\)#✓fully proved

For q ≥ 1 the edge partition function is at most 2 ^ |E| q ^ |V|. The case q = 2 is ecz_fkZEdge_le.

lemma fkc_fkZEdge_le {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq1 : 1 ≤ q) :
    ecz_fkZEdge G p q ≤ (2 : ℝ) ^ G.edgeFinset.card * q ^ Fintype.card V

Uses 5 · Used by 1

Statement usesEdge partition function of the random-cluster model

Proof usesConfiguration space of a statistical-mechanics model · Configurations closed off the edges of a graph · Unnormalized random-cluster weight · Random-cluster weight is at most \(q^{|V|}\) for \(q \ge 1\)

Used byUniform upper bound on the box free energy for \(d, n, q \ge 1\)

DefinitionEdge-normalized box free energy of the random-cluster model#✓fully proved

The edge-normalized free energy of the random-cluster model on the box of side 2n + 1 in dimension d, in the logit parameter s: log Z^E / |E| + log (1 + eˢ) with Z^E = ecz_fkZEdge (boxGraph d n) (fsc_logistic s) q.

noncomputable def fkc_edgeFreeEnergy (d : ℕ) (s q : ℝ) (n : ℕ) : ℝ :=
  Real.log (ecz_fkZEdge (boxGraph d n) (fsc_logistic s) q) / ((boxGraph d n).edgeFinset.card : ℝ)
    + Real.log (1 + Real.exp s)

Uses 6 · Used by 3

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 byPer-edge free energy converges along \(K_j\) for \(d, q \ge 1\) · Uniform upper bound on the box free energy for \(d, n, q \ge 1\) · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\)

LemmaUniform upper bound on the box free energy for \(d, n, q \ge 1\)#✓fully proved

For d, n ≥ 1 and q ≥ 1 the box free energy is at most log 2 + 2 log q + log (1 + eˢ). The case q = 2 is ecz_edgeFE_le_const.

lemma fkc_rq_bdd (d n : ℕ) (hd : 1 ≤ d) (hn : 1 ≤ n) (s q : ℝ) (hq1 : 1 ≤ q) :
    fkc_edgeFreeEnergy d s q n ≤ (Real.log 2 + 2 * Real.log q) + Real.log (1 + Real.exp s)

Uses 15 · Used by 1

Statement usesEdge-normalized box free energy of the random-cluster model

Proof usesConfiguration space of a statistical-mechanics model · \(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Configurations closed off the edges of a graph · Edge partition function of the random-cluster model · Bernoulli edge product · Unnormalized random-cluster weight · Logistic function \(e^t/(1+e^t)\) · Number of open clusters · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \((-n, n)^d\) as a finite set of sites · Edge partition function is at most \(2^{|E|} q^{|V|}\) for \(q \ge 1\)

Used byPer-edge free energy converges along \(K_j\) for \(d, q \ge 1\)

DefinitionBox free energy \(-\log Z^E\) of the random-cluster model#✓fully proved

The box free energy -log Z^E of the random-cluster model on [-n, n]^d at edge parameter fsc_logistic s, over configurations closed off the box edges.

noncomputable def fkc_u (d : ℕ) (s q : ℝ) (n : ℕ) : ℝ :=
  -Real.log (ecz_fkZEdge (boxGraph d n) (fsc_logistic s) q)

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 byDoubling-bound property of the box free energy along \(K_j\) · Box free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\) · Doubling bound for the box free energy when \(q \ge 1\) · Van Hove subadditivity of the box free energy for \(q \ge 1\) · Per-edge free energy converges along \(K_j\) for \(d, q \ge 1\) · Per-edge box free energy · Van Hove limit · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\)

DefinitionPer-edge box free energy#✓fully proved

The per-edge box free energy fkc_u / |E|.

noncomputable def fkc_f (d : ℕ) (s q : ℝ) (n : ℕ) : ℝ :=
  fkc_u d s q n / ((boxGraph d n).edgeFinset.card : ℝ)

Uses 5 · 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 · Box free energy \(-\log Z^E\) of the random-cluster model

Used byPer-edge free energy converges along \(K_j\) for \(d, q \ge 1\) · Limit of the van Hove upper bound for a fixed box side · Convergence of the per-edge box free energy · Van Hove limit · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\)

LemmaDoubling bound for the box free energy when \(q \ge 1\)#✓fully proved

Doubling bound: the free energy of the box of side 2(2K + 1) + 1 is at most 2^d times that of side 2K + 1 plus -log (1 - p) times the number of boundary edges.

lemma fkc_box_neglog_doubling (d K : ℕ) (s q : ℝ) (hq : 1 ≤ q) :
    fkc_u d s q (2 * K + 1) ≤ (2 : ℝ) ^ d * fkc_u d s q K
      + ((2 * d * (qp_Jset d K).card + (2 ^ d + 1) * (2 * d * (qp_Jset d K).card) : ℕ) : ℝ)
          * (-Real.log (1 - fsc_logistic s))

Uses 41 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Logistic function \(e^t/(1+e^t)\) · Hyperplane set of \(\Lambda_{2K+1}\) · Box free energy \(-\log Z^E\) of the random-cluster model

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 · 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 · 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 graph · Bernoulli edge product · Graph glued from two graphs along an interface · 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 · 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 · 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 · Translation vector onto an orthant of \(\Lambda_{2K+1}\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byBox free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\)

LemmaVan Hove subadditivity of the box free energy for \(q \ge 1\)#✓fully proved

Van Hove subadditivity: packing T^d copies of the side-(2m + 1) box into the side-(2n + 1) box, the free energy is at most T^d fkc_u m plus -log (1 - p) per remaining edge.

lemma fkc_box_vanHove_subadd (d m n : ℕ) (s q : ℝ) (hq : 1 ≤ q) :
    fkc_u d s q n ≤ ((ecz_T m n) ^ d : ℝ) * fkc_u d s q m
      + (((boxGraph d n).edgeFinset.card : ℝ)
          - ((ecz_T m n) ^ d : ℝ) * ((boxGraph d m).edgeFinset.card : ℝ))
          * (-Real.log (1 - fsc_logistic s))

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 · Logistic function \(e^t/(1+e^t)\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box free energy \(-\log Z^E\) of the random-cluster model

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 byVan Hove limit

DefinitionDoubling-bound property of the box free energy along \(K_j\)#✓fully proved

A doubling bound along the dyadic sides agl_K j with nonnegative errors I j whose per-edge values are summable.

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

Uses 4 · Used by 2

Statement usesNumber of edges of a box · Scales \(K_j = 2^{j+1} - 1\) · Logistic function \(e^t/(1+e^t)\) · Box free energy \(-\log Z^E\) of the random-cluster model

Used byBox free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\) · Per-edge free energy converges along \(K_j\) for \(d, q \ge 1\)

LemmaBox free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\)#✓fully proved

The doubling bound holds for all q ≥ 1.

lemma fkc_additiveDoublingBound (d : ℕ) (hd : 1 ≤ d) (s q : ℝ) (hq : 1 ≤ q) :
    fkc_AdditiveDoublingBound d s q

Uses 15 · Used by 1

Statement usesDoubling-bound property of the box free energy along \(K_j\)

Proof usesNumber of edges of a box · Scales \(K_j = 2^{j+1} - 1\) · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Logistic function \(e^t/(1+e^t)\) · Hyperplane set of \(\Lambda_{2K+1}\) · The hyperplane set has at most \(d(4K+3)^{d-1}\) sites · 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\) · Summability of doubling corrections relative to edge counts · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Doubling bound for the box free energy when \(q \ge 1\) · Box free energy \(-\log Z^E\) of the random-cluster model

Used byPer-edge free energy converges along \(K_j\) for \(d, q \ge 1\)

LemmaPer-edge free energy converges along \(K_j\) for \(d, q \ge 1\)#✓fully proved

The per-edge free energy converges along the dyadic sides agl_K j.

lemma fkc_dyadic_f_tendsto (d : ℕ) (hd : 1 ≤ d) (s q : ℝ) (hq : 1 ≤ q) :
    ∃ L : ℝ, Tendsto (fun j => fkc_f d s q (agl_K j)) atTop (nhds L)

Uses 20 · Used by 1

Statement usesScales \(K_j = 2^{j+1} - 1\) · Per-edge box free energy

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 · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Configurations closed off the edges of a graph · Edge partition function of the random-cluster model · Bernoulli edge product · Unnormalized random-cluster weight · Logistic function \(e^t/(1+e^t)\) · Number of open clusters · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Doubling-bound property of the box free energy along \(K_j\) · Box free-energy doubling bound along \(K_j\) holds for \(d, q \ge 1\) · Edge-normalized box free energy of the random-cluster model · 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

Used byVan Hove limit

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

The per-edge box free energy fkc_f d s q n converges as n → ∞.

def fkc_PerEdgeDensityConverges (d : ℕ) (s q : ℝ) : Prop :=
  ∃ ρ : ℝ, Tendsto (fun n => fkc_f d s q n) atTop (nhds ρ)

Uses 1 · Used by 2

Statement usesPer-edge box free energy

Used byVan Hove limit · Convex limit of centered tilt free energies of boxes for \(d, q \ge 1\)

DefinitionLimit of the van Hove upper bound for a fixed box side#✓fully proved

The limit of the van Hove upper bound for a fixed side 2m + 1.

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

Uses 2 · Used by 1

Statement usesLogistic function \(e^t/(1+e^t)\) · Per-edge box free energy

Used byVan Hove limit

TheoremVan Hove limit#✓fully proved

Van Hove limit of the random-cluster free energy: for d ≥ 1 and q ≥ 1, the per-edge free energy on the box [-n, n]^d converges. See D. Ruelle, Statistical Mechanics: Rigorous Results (1969), and G. Grimmett, The Random-Cluster Model (2006), Chapter 4.

theorem fkc_perEdgeDensityConverges (d : ℕ) (hd : 1 ≤ d) (s q : ℝ) (hq : 1 ≤ q) :
    fkc_PerEdgeDensityConverges d s q

Uses 14 · Used by 1

Statement usesConvergence of the per-edge box free energy

Proof uses\(\Lambda_n\) has \(d \cdot 2n(2n+1)^{d-1}\) edges · Scales \(K_j = 2^{j+1} - 1\) · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Number of sub-box translates along a side of a box · Logistic function \(e^t/(1+e^t)\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · 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\) · Per-edge box free energy · Limit of the van Hove upper bound for a fixed box side · Box free energy \(-\log Z^E\) of the random-cluster model

Used byConvex limit of centered tilt free energies of boxes for \(d, q \ge 1\)

105 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.