The square-lattice torus

3 fully proved

A. The torus graph

DefinitionNearest-neighbor adjacency on the discrete torus#✓fully proved

Nearest-neighbor adjacency on ℤ_L × ℤ_L: the two sites differ by ±1 in exactly one coordinate.

def onsTorusAdj (L : ℕ) (u v : ZMod L × ZMod L) : Prop :=
  (u.1 = v.1 ∧ (u.2 = v.2 + 1 ∨ u.2 = v.2 - 1)) ∨ (u.2 = v.2 ∧ (u.1 = v.1 + 1 ∨ u.1 = v.1 - 1))

Used by 20

Used bySector weight of a homology class · Spin-character sum over even subgraphs of the torus · Torus pressure sequence of the zero-field Ising model · Limit statement for \(\log X_L(\tanh\beta)/L^2\) on the torus · 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 · Pressure decomposition on the \(L \times L\) torus for \(\beta \ge 0\) · Edge-weighted root identity from the decorated-torus formal identity · The \(L \times L\) square-lattice torus graph · The torus graph is a circulant graph with jumps \((1,0)\) and \((0,1)\) · 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 · 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

DefinitionThe \(L \times L\) square-lattice torus graph#✓fully proved

The L × L square-lattice torus as a simple graph on ℤ_L × ℤ_L, for L > 2.

StatMech.Onsager.onsTorusGraph · 20 lines

def onsTorusGraph (L : ℕ) [Fact (2 < L)] : SimpleGraph (ZMod L × ZMod L) where
  Adj := onsTorusAdj L
  symm := by
    refine ⟨?_⟩
    rintro u v (⟨h1, h2 | h2⟩ | ⟨h1, h2 | h2⟩)
    · exact Or.inl ⟨h1.symm, Or.inr (by rw [h2]; ring)⟩
    · exact Or.inl ⟨h1.symm, Or.inl (by rw [h2]; ring)⟩
    · exact Or.inr ⟨h1.symm, Or.inr (by rw [h2]; ring)⟩
    · exact Or.inr ⟨h1.symm, Or.inl (by rw [h2]; ring)⟩
  loopless := by
    have hne1 : (1 : ZMod L) ≠ 0 := by
      have : Fact (1 < L) := ⟨by have := (Fact.out : 2 < L); omega⟩
      exact one_ne_zero
    have hnem1 : (-1 : ZMod L) ≠ 0 := neg_ne_zero.mpr hne1
    refine ⟨?_⟩
    rintro v (⟨_, h2 | h2⟩ | ⟨_, h2 | h2⟩)
    · exact hne1 (by linear_combination -h2)
    · exact hnem1 (by linear_combination -h2)
    · exact hne1 (by linear_combination -h2)
    · exact hnem1 (by linear_combination -h2)

Uses 1 · Used by 21

Statement usesNearest-neighbor adjacency on the discrete torus

Used bySector weight of a homology class · Spin-character sum over even subgraphs of the torus · Torus pressure sequence of the zero-field Ising model · Limit statement for \(\log X_L(\tanh\beta)/L^2\) on the torus · 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 · Pressure decomposition on the \(L \times L\) torus for \(\beta \ge 0\) · Edge-weighted root identity from the decorated-torus formal identity · The torus graph is a circulant graph with jumps \((1,0)\) and \((0,1)\) · 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 · Finer 8L × 8L torus graph for the decorated graph · 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 · Torus walk of four lattice steps

C. Comparison with circulant graphs

LemmaThe torus graph is a circulant graph with jumps \((1,0)\) and \((0,1)\)#✓fully proved

The torus graph is the circulant graph of ℤ_L × ℤ_L with jumps (1, 0) and (0, 1).

lemma onsTorusGraph_eq_circulantGraph (L : ℕ) [Fact (2 < L)] :
    onsTorusGraph L = SimpleGraph.circulantGraph {((1 : ZMod L), (0 : ZMod L)), (0, 1)}

Uses 2

Statement usesThe \(L \times L\) square-lattice torus graph

Proof usesNearest-neighbor adjacency on the discrete torus

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.