Kramers–Wannier duality

DefinitionImage of an edge set under a vertex bijection#✓fully proved

The image of an edge set under a vertex equivalence V ≃ W.

def transportEdges (e : V ≃ W) (F : Finset (Sym2 V)) : Finset (Sym2 W) :=
  F.image (Sym2.map e)

DefinitionNumber of edges of an edge set incident to a vertex#✓fully proved

The number of edges of F incident to v.

def incCount (F : Finset (Sym2 V)) (v : V) : ℕ :=
  (F.filter (fun e => v ∈ e)).card

Used by 35

Used byClosed Eulerian walk of a component of an even edge set · Proportionality of the cut sum and the dual even-subgraph sum · Dual high-temperature expansion proportional to the partition function · Edge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from closed-walk parities and walk decompositions · Edge crossing from cycle-parity compatibility of even subgraphs · Edge crossing from side colourings of dual walks · Even subgraphs of a finite graph decompose into closed walks · Even subgraphs of a graph · Even subgraphs defined by a Boolean test · Even subgraph condition on an edge set · High-temperature expansion · Kramers–Wannier duality · Kramers–Wannier duality · Self-dual edge crossing of K₄ by complementary edges · Even-subgraph generating function of a graph · Finite-volume pressure decomposition for \(\beta \ge 0\) · Onsager's formula from the spin Kac-Ward identities · Pressure decomposition on the \(L \times L\) torus for \(\beta \ge 0\) · Split of a decorated even subgraph into a rooted cycle and remainder · Chosen split of a decorated even subgraph at an external edge · Onsager's formula · Equivalence between even decorated subgraphs and port patterns · Equivalence between even torus subgraphs and port patterns · Port pattern of an even subgraph of the torus · Port pattern of an even decorated subgraph · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Edge set with prescribed odd-degree vertices · Chosen first-exit data · Edge sets with a given boundary · High-temperature switching map · Switching map between valid inputs and outputs · Simon–Lieb inequality on a finite graph

DefinitionEven subgraph condition on an edge set#✓fully proved

Every vertex has even degree in the edge set F.

def IsEvenSubgraph (F : Finset (Sym2 V)) : Prop := ∀ v : V, Even (incCount F v)

Uses 1 · Used by 31

Statement usesNumber of edges of an edge set incident to a vertex

Used byClosed Eulerian walk of a component of an even edge set · Proportionality of the cut sum and the dual even-subgraph sum · Dual high-temperature expansion proportional to the partition function · Edge crossing between a graph and its dual · Edge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from region-bounding dual walks, no decomposition needed · Edge crossing from closed-walk parities and walk decompositions · Edge crossing from cycle-parity compatibility of even subgraphs · Edge crossing from side colourings of dual walks · Even subgraphs of a finite graph decompose into closed walks · Even subgraphs of a graph · Even subgraphs defined by a Boolean test · High-temperature expansion · Kramers–Wannier duality · Kramers–Wannier duality · Kramers–Wannier duality · Self-dual edge crossing of K₄ by complementary edges · Even-subgraph generating function of a graph · Finite-volume pressure decomposition for \(\beta \ge 0\) · Onsager's formula from the spin Kac-Ward identities · Pressure decomposition on the \(L \times L\) torus for \(\beta \ge 0\) · Chosen split of a decorated even subgraph at an external edge · Onsager's formula · Equivalence between even decorated subgraphs and port patterns · Equivalence between even torus subgraphs and port patterns · Port pattern of an even subgraph of the torus · Port pattern of an even decorated subgraph · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality on a finite graph

TheoremHigh-temperature expansion#✓fully proved

At zero field, Z(β) = 2^{|V|} (cosh β)^{|E|} ∑_{F even} (tanh β)^{|F|}.

S. Friedli and Y. Velenik, Statistical Mechanics of Lattice Systems, Cambridge University Press (2017), Section 3.7.

theorem isingZ_high_temp_expansion (β : ℝ) :
    isingZ G β 0
      = (2 : ℝ) ^ Fintype.card V * (Real.cosh β) ^ G.edgeFinset.card
        * ∑ F ∈ G.edgeFinset.powerset.filter IsEvenSubgraph,
            (Real.tanh β) ^ F.card

Uses 9 · Used by 3

Statement usesEven subgraph condition on an edge set · Number of edges of an edge set incident to a vertex · Ising partition function

Proof usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Bond variable takes values \(\pm 1\) · Ising Hamiltonian on a finite graph · Boltzmann weight of an Ising configuration · Spin of a configuration at a site

Used byKramers–Wannier duality · Kramers–Wannier duality · High-temperature expansion

DefinitionDual high-temperature expansion proportional to the partition function#✓fully proved

tanh β* = exp (-2β) and the high-temperature expansion of Gd at β* equals c times Z_{Gp}(β).

def DualContourMatching (β βstar c : ℝ) : Prop :=
  Real.tanh βstar = Real.exp (-2 * β) ∧
    (2 : ℝ) ^ Fintype.card V * (Real.cosh βstar) ^ Gd.edgeFinset.card
        * ∑ F ∈ Gd.edgeFinset.powerset.filter IsEvenSubgraph,
            (Real.tanh βstar) ^ F.card
      = c * isingZ Gp β 0

Uses 3 · Used by 2

Statement usesEven subgraph condition on an edge set · Number of edges of an edge set incident to a vertex · Ising partition function

Used byKramers–Wannier duality · Kramers–Wannier duality

DefinitionEdges cut by a spin configuration#✓fully proved

The edges {x, y} of G whose endpoints have different spins in s.

noncomputable def cutEdges (s : ConfigSpace V) : Finset (Sym2 V) :=
  G.edgeFinset.filter (fun e => bond s e = -1)

Uses 2 · Used by 10

Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair

Used byProportionality of the cut sum and the dual even-subgraph sum · Cut space of a graph · Edge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from closed-walk parities and walk decompositions · Edge crossing from cycle-parity compatibility of even subgraphs · Edge crossing from side colourings of dual walks · Kramers–Wannier duality · Kramers–Wannier duality · Self-dual edge crossing of K₄ by complementary edges · Edge boundary of a region in a graph

DefinitionProportionality of the cut sum and the dual even-subgraph sum#✓fully proved

The cut sum ∑_s t^{|∂s|} of Gp equals mult times the even-subgraph sum ∑_F t^{|F|} of Gd.

def CutEvenSubgraphMatching (t mult : ℝ) : Prop :=
  (∑ s : ConfigSpace V, t ^ (cutEdges Gp s).card)
    = mult * ∑ F ∈ Gd.edgeFinset.powerset.filter IsEvenSubgraph, t ^ F.card

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Even subgraph condition on an edge set · Edges cut by a spin configuration · Number of edges of an edge set incident to a vertex

Used byKramers–Wannier duality · Kramers–Wannier duality

DefinitionCut space of a graph#✓fully proved

The cut space: the edge sets ∂s cut by configurations s.

noncomputable def cutSpace : Finset (Finset (Sym2 V)) :=
  Finset.univ.image (fun s : ConfigSpace V => cutEdges Gp s)

Uses 2 · Used by 10

Statement usesConfiguration space of a statistical-mechanics model · Edges cut by a spin configuration

Used byEdge crossing between a graph and its dual · Edge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from region-bounding dual walks, no decomposition needed · Edge crossing from closed-walk parities and walk decompositions · Edge crossing from cycle-parity compatibility of even subgraphs · Edge crossing from side colourings of dual walks · Kramers–Wannier duality · Kramers–Wannier duality · Kramers–Wannier duality · Self-dual edge crossing of K₄ by complementary edges

DefinitionEven subgraphs of a graph#✓fully proved

The even subgraphs of G.

noncomputable def evenSubgraphs : Finset (Finset (Sym2 V)) :=
  Gd.edgeFinset.powerset.filter IsEvenSubgraph

Uses 2 · Used by 34

Statement usesEven subgraph condition on an edge set · Number of edges of an edge set incident to a vertex

Used bySector weight of a homology class · Spin-character sum over even subgraphs of the torus · Edge crossing between a graph and its dual · Edge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from closed-walk parities and walk decompositions · Edge crossing from cycle-parity compatibility of even subgraphs · Edge crossing from side colourings of dual walks · Closed-walk decomposition property of even subgraphs · Even subgraphs of a finite graph decompose into closed walks · Kramers–Wannier duality · Kramers–Wannier duality · Self-dual edge crossing of K₄ by complementary edges · Onsager's formula from the spin Kac-Ward identities · Spin Kac-Ward identities from the decorated-torus formal identity · Spin Kac-Ward identities from the edge-weighted root identity · Edge-weighted root identity from the decorated-torus formal identity · Decorated even subgraphs containing a given external edge · Cycle removal identity for decorated even subgraphs · Split of a decorated even subgraph into a rooted cycle and remainder · Chosen split of a decorated even subgraph at an external edge · Even subgraphs of the decorated torus graph · Decorated spin polynomial · Onsager's formula · Torus even subgraph of a decorated even subgraph · Sector weight of a homology class as a polynomial · Even subgraphs of the L × L torus · Edge-weighted spin-character sum over even subgraphs · Weighted character sum over even subgraphs containing an edge · Decorated character sum with weights on all edges · Equivalence between even decorated subgraphs and port patterns · Equivalence between even subgraphs of the torus and its decoration · Equivalence between even torus subgraphs and port patterns · Port pattern of an even subgraph of the torus · Port pattern of an even decorated subgraph

DefinitionSpin disagreement test across an edge#✓fully proved

Whether the spins of s differ at the endpoints of e.

def edgeDiff (s : ConfigSpace V) (e : Sym2 V) : Bool :=
  Sym2.lift ⟨fun x y => s x != s y, fun _ _ => by simp [bne_comm]⟩ e

Uses 1 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model

Used byEdges cut by a configuration via the edge disagreement test · Kramers–Wannier duality · Self-dual edge crossing of K₄ by complementary edges

DefinitionEdges cut by a configuration via the edge disagreement test#✓fully proved

The edges cut by s, defined through edgeDiff.

def cutEdgesB (s : ConfigSpace V) : Finset (Sym2 V) :=
  G.edgeFinset.filter (fun e => edgeDiff s e)

Uses 2 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Spin disagreement test across an edge

Used byCut space defined through Boolean cut edges · Kramers–Wannier duality · Self-dual edge crossing of K₄ by complementary edges

DefinitionCut space defined through Boolean cut edges#✓fully proved

The cut space, defined through cutEdgesB.

def cutSpaceB : Finset (Finset (Sym2 V)) :=
  Finset.univ.image (fun s : ConfigSpace V => cutEdgesB G s)

Uses 2 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Edges cut by a configuration via the edge disagreement test

Used byKramers–Wannier duality · Self-dual edge crossing of K₄ by complementary edges

DefinitionEven subgraphs defined by a Boolean test#✓fully proved

The even subgraphs, defined with a Boolean test.

def evenSubgraphsB : Finset (Finset (Sym2 V)) :=
  G.edgeFinset.powerset.filter IsEvenSubgraph

Uses 2 · Used by 2

Statement usesEven subgraph condition on an edge set · Number of edges of an edge set incident to a vertex

Used byKramers–Wannier duality · Self-dual edge crossing of K₄ by complementary edges

AbbreviationComplete graph on four vertices#✓fully proved

The complete graph K₄ on Fin 4.

abbrev K4 : SimpleGraph (Fin 4) := ⊤

Used by 2

Used byKramers–Wannier duality · Self-dual edge crossing of K₄ by complementary edges

TheoremKramers–Wannier duality#✓fully proved

Kramers–Wannier duality on the self-dual graph K₄: if tanh β* = e^{-2β} then Z(β*) = (2⁴ (cosh β*)^{|E|} / (e^{β|E|} · 2)) Z(β) at zero field.

H. A. Kramers and G. H. Wannier, Statistics of the two-dimensional ferromagnet. Part I, Phys. Rev. 60 (1941).

theorem isingZ_self_dual_K4 (β βstar : ℝ)
    (htemp : Real.tanh βstar = Real.exp (-2 * β)) :
    isingZ (K4) βstar 0
      = ((2 : ℝ) ^ Fintype.card (Fin 4) * (Real.cosh βstar) ^ (K4).edgeFinset.card
        / (Real.exp (β * (K4).edgeFinset.card) * 2)) * isingZ (K4) β 0

Uses 20

Statement usesComplete graph on four vertices · Ising partition function

Proof usesConfiguration space of a statistical-mechanics model · Proportionality of the cut sum and the dual even-subgraph sum · Dual high-temperature expansion proportional to the partition function · Even subgraph condition on an edge set · Bond variable of an unordered pair · Bond variable takes values \(\pm 1\) · Edges cut by a spin configuration · Edges cut by a configuration via the edge disagreement test · Cut space of a graph · Cut space defined through Boolean cut edges · Spin disagreement test across an edge · Even subgraphs of a graph · Even subgraphs defined by a Boolean test · Ising Hamiltonian on a finite graph · Number of edges of an edge set incident to a vertex · Boltzmann weight of an Ising configuration · High-temperature expansion · Spin of a configuration at a site

DefinitionNumber of disagreeing steps along a walk#✓fully proved

The number of steps of a walk whose endpoints have different spins in s.

def walkDis : {x y : V} → Gp.Walk x y → ℕ
  | _, _, .nil => 0
  | _, _, .cons (u := u) (v := v) _ p => (if s u ≠ s v then 1 else 0) + walkDis p

Uses 1

Statement usesConfiguration space of a statistical-mechanics model

StructureEdge crossing between a graph and its dual#✓fully proved

An edge bijection ψ from Gp to Gd carrying edges to edges, cuts to even subgraphs, and even subgraphs back to cuts.

structure EdgeCrossing where

  ψ : Sym2 V ≃ Sym2 V

  edge_mem : ∀ e ∈ Gp.edgeFinset, ψ e ∈ Gd.edgeFinset

  cut_to_even : ∀ δ ∈ cutSpace Gp, IsEvenSubgraph (δ.image ψ)


  even_to_cut : ∀ F ∈ evenSubgraphs Gd, (F.image ψ.symm) ∈ cutSpace Gp

Uses 3 · Used by 7

Statement usesEven subgraph condition on an edge set · Cut space of a graph · Even subgraphs of a graph

Used byEdge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from region-bounding dual walks, no decomposition needed · Edge crossing from closed-walk parities and walk decompositions · Edge crossing from cycle-parity compatibility of even subgraphs · Edge crossing from side colourings of dual walks · Kramers–Wannier duality · Self-dual edge crossing of K₄ by complementary edges

TheoremKramers–Wannier duality#✓fully proved

For a preconnected graph Gp with an edge crossing to Gd and tanh β* = e^{-2β}, Z_{Gd}(β*) = (2^{|V|} (cosh β*)^{|E_d|} / (e^{β|E_p|} · 2)) Z_{Gp}(β) at zero field.

H. A. Kramers and G. H. Wannier, Statistics of the two-dimensional ferromagnet. Part I, Phys. Rev. 60 (1941).

theorem isingZ_self_dual_of_edgeCrossing [Nonempty V] (hG : Gp.Preconnected)
    (Φ : EdgeCrossing Gp Gd) (β βstar : ℝ)
    (htemp : Real.tanh βstar = Real.exp (-2 * β)) :
    isingZ Gd βstar 0
      = ((2 : ℝ) ^ Fintype.card V * (Real.cosh βstar) ^ Gd.edgeFinset.card
        / (Real.exp (β * Gp.edgeFinset.card) * 2)) * isingZ Gp β 0

Uses 16 · Used by 1

Statement usesEdge crossing between a graph and its dual · Ising partition function

Proof usesConfiguration space of a statistical-mechanics model · Proportionality of the cut sum and the dual even-subgraph sum · Dual high-temperature expansion proportional to the partition function · Even subgraph condition on an edge set · Bond variable of an unordered pair · Bond variable takes values \(\pm 1\) · Edges cut by a spin configuration · Cut space of a graph · Even subgraphs of a graph · Ising Hamiltonian on a finite graph · Number of edges of an edge set incident to a vertex · Boltzmann weight of an Ising configuration · High-temperature expansion · Spin of a configuration at a site

Used byKramers–Wannier duality

DefinitionVertices of K₄ outside a given pair#✓fully proved

The two vertices of Fin 4 other than a and b.

def k4Missing (a b : Fin 4) : List (Fin 4) :=
  ([0, 1, 2, 3] : List (Fin 4)).filter (fun k => k ≠ a ∧ k ≠ b)

Used by 1

Used byComplementary edge of a pair in K₄

DefinitionComplementary edge of a pair in K₄#✓fully proved

The edge of K₄ complementary to {a, b}.

def k4CompPair (a b : Fin 4) : Sym2 (Fin 4) :=
  match k4Missing a b with
  | [c, d] => s(c, d)
  | _ => s(a, b)

Uses 1 · Used by 1

Statement usesVertices of K₄ outside a given pair

Used byComplementary-edge map of K₄ on unordered pairs

DefinitionComplementary-edge map of K₄ on unordered pairs#✓fully proved

The complementary edge of K₄, as a function on Sym2 (Fin 4).

def k4Comp (e : Sym2 (Fin 4)) : Sym2 (Fin 4) :=
  Sym2.lift ⟨k4CompPair, by decide⟩ e

Uses 1 · Used by 2

Statement usesComplementary edge of a pair in K₄

Used byEdge complementation of K₄ as an involutive equivalence · Self-dual edge crossing of K₄ by complementary edges

DefinitionEdge complementation of K₄ as an involutive equivalence#✓fully proved

Complementation of edges of K₄ as an involutive equivalence.

def k4CompEquiv : Sym2 (Fin 4) ≃ Sym2 (Fin 4) :=
  Function.Involutive.toPerm k4Comp k4Comp_involutive

Uses 1 · Used by 1

Statement usesComplementary-edge map of K₄ on unordered pairs

Used bySelf-dual edge crossing of K₄ by complementary edges

DefinitionSelf-dual edge crossing of K₄ by complementary edges#✓fully proved

The edge crossing of the self-dual graph K₄ given by complementary edges.

StatMech.Ising.k4EdgeCrossing · 18 lines

noncomputable def k4EdgeCrossing : EdgeCrossing (K4) (K4) where
  ψ := k4CompEquiv
  edge_mem := by
    intro e he
    rw [mem_K4_edgeFinset_iff] at he ⊢
    rw [k4CompEquiv_apply]
    exact k4Comp_not_diag e he
  cut_to_even := by
    intro δ hδ
    rw [cutSpace_eq_cutSpaceB] at hδ
    have := k4Comp_cut_to_even δ hδ
    exact this
  even_to_cut := by
    intro F hF
    rw [show evenSubgraphs (K4) = evenSubgraphsB (K4) from rfl] at hF
    rw [cutSpace_eq_cutSpaceB]
    have := k4Comp_even_to_cut F hF
    exact this

Uses 16

Statement usesConfiguration space of a statistical-mechanics model · Edge crossing between a graph and its dual · Even subgraph condition on an edge set · Complete graph on four vertices · Bond variable of an unordered pair · Edges cut by a spin configuration · Edges cut by a configuration via the edge disagreement test · Cut space of a graph · Cut space defined through Boolean cut edges · Spin disagreement test across an edge · Even subgraphs of a graph · Even subgraphs defined by a Boolean test · Number of edges of an edge set incident to a vertex · Complementary-edge map of K₄ on unordered pairs · Edge complementation of K₄ as an involutive equivalence · Spin of a configuration at a site

DefinitionCrossing parity of a walk with respect to an edge set#✓fully proved

The parity of the number of steps of a walk that use an edge of δ.

def walkParity : {x y : V} → Gp.Walk x y → Bool
  | _, _, .nil => false
  | _, _, .cons (u := u) (v := v) _ p => (decide (s(u, v) ∈ δ)).xor (walkParity p)

Used by 6

Used byEdge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from closed-walk parities and walk decompositions · Edge crossing from cycle-parity compatibility of even subgraphs · Edge crossing from side colourings of dual walks · Evenness of an edge set on every closed walk · Spin configuration from crossing parities along walks

DefinitionEvenness of an edge set on every closed walk#✓fully proved

Every closed walk of Gp uses edges of δ an even number of times.

def EvenOnCycles : Prop := ∀ (x : V) (p : Gp.Walk x x), walkParity Gp δ p = false

Uses 1 · Used by 7

Statement usesCrossing parity of a walk with respect to an edge set

Used byCycle-parity compatibility of closed dual walks · Cycle-parity compatibility of a dual edge set · Edge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from closed-walk parities and walk decompositions · Edge crossing from cycle-parity compatibility of even subgraphs · Edge crossing from side colourings of dual walks · Cycle-parity compatibility of a family of dual cycle sets

DefinitionSpin configuration from crossing parities along walks#✓fully proved

The configuration assigning to v the crossing parity of δ along a walk from v₀ to v.

noncomputable def parityConfig (hG : Gp.Preconnected) (v₀ : V) : ConfigSpace V :=
  fun v => walkParity Gp δ (hG v₀ v).some

Uses 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Crossing parity of a walk with respect to an edge set

Used byEdge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from closed-walk parities and walk decompositions · Edge crossing from cycle-parity compatibility of even subgraphs · Edge crossing from side colourings of dual walks

DefinitionCycle-parity compatibility of a dual edge set#✓fully proved

Every closed walk of Gp crosses the pullback of F an even number of times.

def CycleParityCompatible (Gp : SimpleGraph V) [DecidableRel Gp.Adj]
    (ψ : Sym2 V ≃ Sym2 V) (F : Finset (Sym2 V)) : Prop :=
  EvenOnCycles Gp (F.image ψ.symm)

Uses 1 · Used by 4

Statement usesEvenness of an edge set on every closed walk

Used byEdge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from closed-walk parities and walk decompositions · Edge crossing from cycle-parity compatibility of even subgraphs · Edge crossing from side colourings of dual walks

DefinitionEdge crossing from cycle-parity compatibility of even subgraphs#✓fully proved

An edge crossing built from cycle-parity compatibility of all even subgraphs of Gd.

noncomputable def edgeCrossing_of_cycleParity [Nonempty V] (hG : Gp.Preconnected)
    (ψ : Sym2 V ≃ Sym2 V)
    (hedge : ∀ e ∈ Gp.edgeFinset, ψ e ∈ Gd.edgeFinset)
    (hsymm : ∀ e ∈ Gd.edgeFinset, ψ.symm e ∈ Gp.edgeFinset)
    (hfwd : ∀ δ ∈ cutSpace Gp, IsEvenSubgraph (δ.image ψ))
    (hcyc : ∀ F ∈ evenSubgraphs Gd, CycleParityCompatible Gp ψ F) :
    EdgeCrossing Gp Gd where
  ψ := ψ
  edge_mem := hedge
  cut_to_even := hfwd
  even_to_cut := even_to_cut_of_cycleParity hG ψ hsymm hcyc

Uses 13

Statement usesConfiguration space of a statistical-mechanics model · Cycle-parity compatibility of a dual edge set · Edge crossing between a graph and its dual · Evenness of an edge set on every closed walk · Even subgraph condition on an edge set · Bond variable of an unordered pair · Edges cut by a spin configuration · Cut space of a graph · Even subgraphs of a graph · Number of edges of an edge set incident to a vertex · Spin configuration from crossing parities along walks · Spin of a configuration at a site · Crossing parity of a walk with respect to an edge set

DefinitionCycle-parity compatibility of a family of dual cycle sets#✓fully proved

Every edge set in cycleSets is cycle-parity compatible.

def SingleDualCycleParity (Gp : SimpleGraph V) [DecidableRel Gp.Adj]
    (ψ : Sym2 V ≃ Sym2 V) (cycleSets : Finset (Sym2 V) → Prop) : Prop :=
  ∀ C : Finset (Sym2 V), cycleSets C → EvenOnCycles Gp (C.image ψ.symm)

Uses 1 · Used by 3

Statement usesEvenness of an edge set on every closed walk

Used byEdge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from closed-walk parities and walk decompositions · Edge crossing from side colourings of dual walks

DefinitionCycle-parity compatibility of closed dual walks#✓fully proved

Every closed walk of Gd has edge set whose pullback is cycle-parity compatible.

def ClosedDualWalkParity (Gp Gd : SimpleGraph V) [DecidableRel Gp.Adj]
    (ψ : Sym2 V ≃ Sym2 V) : Prop :=
  ∀ {w : V} (W : Gd.Walk w w), EvenOnCycles Gp ((W.edges.toFinset).image ψ.symm)

Uses 1 · Used by 3

Statement usesEvenness of an edge set on every closed walk

Used byEdge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from closed-walk parities and walk decompositions · Edge crossing from side colourings of dual walks

DefinitionClosed-walk decomposition property of even subgraphs#✓fully proved

Every even subgraph of Gd is a symmetric difference of edge sets of closed walks.

def EvenSubgraphWalkDecomp (Gd : SimpleGraph V) [DecidableRel Gd.Adj] : Prop :=
  ∀ F ∈ evenSubgraphs Gd, ∃ (ι : Type) (_ : DecidableEq ι) (s : Finset ι)
      (w : ι → V) (W : (i : ι) → Gd.Walk (w i) (w i)),
    F = s.biUnion (fun i => (W i).edges.toFinset) ∧
    (s : Set ι).PairwiseDisjoint (fun i => (W i).edges.toFinset)

Uses 1 · Used by 4

Statement usesEven subgraphs of a graph

Used byEdge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from closed-walk parities and walk decompositions · Edge crossing from side colourings of dual walks · Even subgraphs of a finite graph decompose into closed walks

DefinitionEdge crossing from closed-walk parities and walk decompositions#✓fully proved

An edge crossing built from closed-walk parities and the decomposition of even subgraphs into closed walks.

noncomputable def edgeCrossing_of_closedWalkParity [Nonempty V] (hG : Gp.Preconnected)
    (ψ : Sym2 V ≃ Sym2 V)
    (hedge : ∀ e ∈ Gp.edgeFinset, ψ e ∈ Gd.edgeFinset)
    (hsymm : ∀ e ∈ Gd.edgeFinset, ψ.symm e ∈ Gp.edgeFinset)
    (hfwd : ∀ δ ∈ cutSpace Gp, IsEvenSubgraph (δ.image ψ))
    (hdecomp : EvenSubgraphWalkDecomp Gd)
    (hlink : ClosedDualWalkParity Gp Gd ψ) :
    EdgeCrossing Gp Gd where
  ψ := ψ
  edge_mem := hedge
  cut_to_even := hfwd
  even_to_cut := even_to_cut_of_closedWalkParity hG ψ hsymm hdecomp hlink

Uses 16

Statement usesConfiguration space of a statistical-mechanics model · Cycle-parity compatibility of closed dual walks · Cycle-parity compatibility of a dual edge set · Edge crossing between a graph and its dual · Evenness of an edge set on every closed walk · Closed-walk decomposition property of even subgraphs · Even subgraph condition on an edge set · Cycle-parity compatibility of a family of dual cycle sets · Bond variable of an unordered pair · Edges cut by a spin configuration · Cut space of a graph · Even subgraphs of a graph · Number of edges of an edge set incident to a vertex · Spin configuration from crossing parities along walks · Spin of a configuration at a site · Crossing parity of a walk with respect to an edge set

DefinitionSide-colouring property of closed dual walks#✓fully proved

Every closed walk of Gd has a two-colouring of the vertices of Gp whose boundary is the pullback of its edges.

def DualWalkHasSideColouring (Gp Gd : SimpleGraph V) [DecidableRel Gp.Adj]
    (ψ : Sym2 V ≃ Sym2 V) : Prop :=
  ∀ {w : V} (W : Gd.Walk w w), ∃ c : V → Bool,
    ∀ {u v : V}, Gp.Adj u v →
      (s(u, v) ∈ (W.edges.toFinset).image ψ.symm ↔ c u ≠ c v)

Used by 2

Used byEdge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from side colourings of dual walks

DefinitionEdge crossing from side colourings of dual walks#✓fully proved

An edge crossing built from side colourings of dual walks.

noncomputable def edgeCrossing_of_sideColouring [Nonempty V] (hG : Gp.Preconnected)
    (ψ : Sym2 V ≃ Sym2 V)
    (hedge : ∀ e ∈ Gp.edgeFinset, ψ e ∈ Gd.edgeFinset)
    (hsymm : ∀ e ∈ Gd.edgeFinset, ψ.symm e ∈ Gp.edgeFinset)
    (hfwd : ∀ δ ∈ cutSpace Gp, IsEvenSubgraph (δ.image ψ))
    (hdecomp : EvenSubgraphWalkDecomp Gd)
    (hside : DualWalkHasSideColouring Gp Gd ψ) :
    EdgeCrossing Gp Gd where
  ψ := ψ
  edge_mem := hedge
  cut_to_even := hfwd
  even_to_cut := even_to_cut_of_sideColouring hG ψ hsymm hdecomp hside

Uses 17

Statement usesConfiguration space of a statistical-mechanics model · Cycle-parity compatibility of closed dual walks · Cycle-parity compatibility of a dual edge set · Side-colouring property of closed dual walks · Edge crossing between a graph and its dual · Evenness of an edge set on every closed walk · Closed-walk decomposition property of even subgraphs · Even subgraph condition on an edge set · Cycle-parity compatibility of a family of dual cycle sets · Bond variable of an unordered pair · Edges cut by a spin configuration · Cut space of a graph · Even subgraphs of a graph · Number of edges of an edge set incident to a vertex · Spin configuration from crossing parities along walks · Spin of a configuration at a site · Crossing parity of a walk with respect to an edge set

DefinitionSimple graph spanned by an edge set#✓fully proved

The simple graph with edge set F.

def subgraphF (F : Finset (Sym2 V)) : SimpleGraph V := SimpleGraph.fromEdgeSet (↑F : Set (Sym2 V))

Used by 4

Used byClosed Eulerian walk of a component of an even edge set · Component of a vertex in the graph spanned by an edge set · Vertex set of a component of the graph spanned by an edge set · Even subgraphs of a finite graph decompose into closed walks

DefinitionComponent of a vertex in the graph spanned by an edge set#✓fully proved

The component of f in the graph spanned by F.

def compF (F : Finset (Sym2 V)) (f : V) : SimpleGraph V where
  Adj a b := (subgraphF F).Adj a b ∧ (subgraphF F).Reachable f a ∧ (subgraphF F).Reachable f b
  symm := ⟨fun a b ⟨h, ha, hb⟩ => ⟨h.symm, hb, ha⟩⟩
  loopless := by refine ⟨fun a ⟨h, _, _⟩ => (subgraphF F).irrefl h⟩

Uses 1 · Used by 2

Statement usesSimple graph spanned by an edge set

Used byClosed Eulerian walk of a component of an even edge set · Even subgraphs of a finite graph decompose into closed walks

DefinitionVertex set of a component of the graph spanned by an edge set#✓fully proved

The vertices of the component of f in the graph spanned by F.

noncomputable def compSuppF (F : Finset (Sym2 V)) (f : V) : Finset V :=
  Finset.univ.filter (fun g => (subgraphF F).Reachable f g)

Uses 1 · Used by 2

Statement usesSimple graph spanned by an edge set

Used byClosed Eulerian walk of a component of an even edge set · Even subgraphs of a finite graph decompose into closed walks

DefinitionClosed Eulerian walk of a component of an even edge set#✓fully proved

A closed Eulerian walk of the component of f in an even edge set F.

noncomputable def compEulerWalk (F : Finset (Sym2 V)) (hF : ∀ e ∈ F, ¬ e.IsDiag)
    (hev : IsEvenSubgraph F) (f : V) : (compF F f).Walk f f :=
  (compF_eulerCircuit F hF hev f).choose

Uses 6 · Used by 1

Statement usesEven subgraph condition on an edge set · Component of a vertex in the graph spanned by an edge set · Vertex set of a component of the graph spanned by an edge set · Number of edges of an edge set incident to a vertex · Simple graph spanned by an edge set · Euler's theorem for a graph supported on a finite connected set

Used byEven subgraphs of a finite graph decompose into closed walks

LemmaEven subgraphs of a finite graph decompose into closed walks#✓fully proved

Every even subgraph decomposes into closed walks.

lemma evenSubgraphWalkDecomp_general (Gd : SimpleGraph V) [DecidableRel Gd.Adj] :
    EvenSubgraphWalkDecomp Gd

Uses 9 · Used by 1

Statement usesClosed-walk decomposition property of even subgraphs

Proof usesEven subgraph condition on an edge set · Closed Eulerian walk of a component of an even edge set · Component of a vertex in the graph spanned by an edge set · Vertex set of a component of the graph spanned by an edge set · Even subgraphs of a graph · Number of edges of an edge set incident to a vertex · Simple graph spanned by an edge set · Euler's theorem for a graph supported on a finite connected set

Used byEdge crossing from region-bounding dual walks, no decomposition needed

DefinitionEdge boundary of a region in a graph#✓fully proved

The edges of Gp whose endpoints lie on different sides of the region S.

noncomputable def regionBoundary (Gp : SimpleGraph V) [DecidableRel Gp.Adj] (S : V → Bool) :
    Finset (Sym2 V) :=
  cutEdges Gp S

Uses 1

Statement usesEdges cut by a spin configuration

DefinitionRegion-bounding property of closed dual walks#✓fully proved

Every closed walk of Gd pulls back to the boundary of a region of Gp.

def DualWalkBoundsRegion (Gp Gd : SimpleGraph V) [DecidableRel Gp.Adj]
    (ψ : Sym2 V ≃ Sym2 V) : Prop :=
  ∀ {w : V} (W : Gd.Walk w w), ∃ S : V → Bool,
    ∀ {u v : V}, Gp.Adj u v →
      (s(u, v) ∈ (W.edges.toFinset).image ψ.symm ↔ S u ≠ S v)

Used by 3

Used byEdge crossing from region-bounding dual walks and a walk decomposition · Edge crossing from region-bounding dual walks, no decomposition needed · Kramers–Wannier duality

DefinitionEdge crossing from region-bounding dual walks and a walk decomposition#✓fully proved

An edge crossing built from dual walks bounding regions.

noncomputable def edgeCrossing_of_boundsRegion [Nonempty V] (hG : Gp.Preconnected)
    (ψ : Sym2 V ≃ Sym2 V)
    (hedge : ∀ e ∈ Gp.edgeFinset, ψ e ∈ Gd.edgeFinset)
    (hsymm : ∀ e ∈ Gd.edgeFinset, ψ.symm e ∈ Gp.edgeFinset)
    (hfwd : ∀ δ ∈ cutSpace Gp, IsEvenSubgraph (δ.image ψ))
    (hdecomp : EvenSubgraphWalkDecomp Gd)
    (hreg : DualWalkBoundsRegion Gp Gd ψ) :
    EdgeCrossing Gp Gd where
  ψ := ψ
  edge_mem := hedge
  cut_to_even := hfwd
  even_to_cut := even_to_cut_of_boundsRegion hG ψ hsymm hdecomp hreg

Uses 18 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Cycle-parity compatibility of closed dual walks · Cycle-parity compatibility of a dual edge set · Region-bounding property of closed dual walks · Side-colouring property of closed dual walks · Edge crossing between a graph and its dual · Evenness of an edge set on every closed walk · Closed-walk decomposition property of even subgraphs · Even subgraph condition on an edge set · Cycle-parity compatibility of a family of dual cycle sets · Bond variable of an unordered pair · Edges cut by a spin configuration · Cut space of a graph · Even subgraphs of a graph · Number of edges of an edge set incident to a vertex · Spin configuration from crossing parities along walks · Spin of a configuration at a site · Crossing parity of a walk with respect to an edge set

Used byEdge crossing from region-bounding dual walks, no decomposition needed

DefinitionBoolean indicator of a set of sites of ℤ²#✓fully proved

The indicator of a set of sites of ℤ², as a Boolean function.

noncomputable def latticeSide (S : Set (Site 2)) : Site 2 → Bool :=
  fun x => @decide (x ∈ S) (Classical.propDecidable _)

Uses 1

Statement usesSite of the hypercubic lattice

DefinitionEdge crossing from region-bounding dual walks, no decomposition needed#✓fully proved

An edge crossing built from dual walks bounding regions (variant using even_to_cut_of_boundsRegion').

noncomputable def edgeCrossing_of_boundsRegion' [Nonempty V] (hG : Gp.Preconnected)
    (ψ : Sym2 V ≃ Sym2 V)
    (hedge : ∀ e ∈ Gp.edgeFinset, ψ e ∈ Gd.edgeFinset)
    (hsymm : ∀ e ∈ Gd.edgeFinset, ψ.symm e ∈ Gp.edgeFinset)
    (hfwd : ∀ δ ∈ cutSpace Gp, IsEvenSubgraph (δ.image ψ))
    (hreg : DualWalkBoundsRegion Gp Gd ψ) :
    EdgeCrossing Gp Gd :=
  edgeCrossing_of_boundsRegion hG ψ hedge hsymm hfwd (evenSubgraphWalkDecomp_general Gd) hreg

Uses 6 · Used by 1

Statement usesRegion-bounding property of closed dual walks · Edge crossing between a graph and its dual · Even subgraph condition on an edge set · Cut space of a graph · Edge crossing from region-bounding dual walks and a walk decomposition · Even subgraphs of a finite graph decompose into closed walks

Used byKramers–Wannier duality

TheoremKramers–Wannier duality#✓fully proved

Kramers–Wannier duality for a preconnected graph Gp and a graph Gd whose closed walks pull back to region boundaries, for tanh β* = e^{-2β}.

H. A. Kramers and G. H. Wannier, Statistics of the two-dimensional ferromagnet. Part I, Phys. Rev. 60 (1941).

theorem isingZ_self_dual_of_boundsRegion [Nonempty V] (hG : Gp.Preconnected)
    (ψ : Sym2 V ≃ Sym2 V)
    (hedge : ∀ e ∈ Gp.edgeFinset, ψ e ∈ Gd.edgeFinset)
    (hsymm : ∀ e ∈ Gd.edgeFinset, ψ.symm e ∈ Gp.edgeFinset)
    (hfwd : ∀ δ ∈ cutSpace Gp, IsEvenSubgraph (δ.image ψ))
    (hreg : DualWalkBoundsRegion Gp Gd ψ)
    (β βstar : ℝ) (htemp : Real.tanh βstar = Real.exp (-2 * β)) :
    isingZ Gd βstar 0
      = ((2 : ℝ) ^ Fintype.card V * (Real.cosh βstar) ^ Gd.edgeFinset.card
        / (Real.exp (β * Gp.edgeFinset.card) * 2)) * isingZ Gp β 0

Uses 6

Statement usesRegion-bounding property of closed dual walks · Even subgraph condition on an edge set · Cut space of a graph · Ising partition function

Proof usesEdge crossing from region-bounding dual walks, no decomposition needed · Kramers–Wannier duality

45 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.