Bridges between the StatMech Ising model and Physlib

8 fully proved

A. The Hamiltonian as Physlib's Ising energy

LemmaBoolean spin agrees with Physlib's Ising spin#✓fully proved

The Boolean spin value spinB is Physlib's CondensedMatter.IsingModel.spin.

lemma spinB_eq_isingModelSpin : spinB = CondensedMatter.IsingModel.spin

Uses 1

Statement usesSpin value of a Boolean

LemmaEdge bond sum is half the sum over ordered adjacent pairs#✓fully proved

The edge sum of bond s is half the sum of σ_x σ_y over ordered adjacent pairs.

lemma two_mul_sum_bond (s : ConfigSpace V) :
    2 * ∑ e ∈ G.edgeFinset, bond s e =
      ∑ x, ∑ y, if G.Adj x y then spin s x * spin s y else 0

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Spin of a configuration at a site

Used byHamiltonian agrees with Physlib's Ising energy

LemmaHamiltonian agrees with Physlib's Ising energy#✓fully proved

The Hamiltonian hamiltonian G h is Physlib's Ising energy CondensedMatter.IsingModel.energy of the model with coupling J = 1 and field h, on the region of all vertices.

lemma hamiltonian_eq_energy (h : ℝ) (s : ConfigSpace V) :
    hamiltonian G h s = (⟨1, h⟩ : CondensedMatter.IsingModel G).energy Finset.univ s

Uses 5

Statement usesConfiguration space of a statistical-mechanics model · Ising Hamiltonian on a finite graph

Proof usesBond variable of an unordered pair · Spin of a configuration at a site · Edge bond sum is half the sum over ordered adjacent pairs

B. The finite canonical ensemble

DefinitionIsing model as a Physlib canonical ensemble#✓fully proved

The Ising model on a finite graph G with field h, as Physlib's finite canonical ensemble: microstates are spin configurations, the energy is hamiltonian G h, and the measure is the counting measure.

noncomputable def canonicalEnsemble (h : ℝ) : CanonicalEnsemble (ConfigSpace V) where
  energy := hamiltonian G h
  dof := 0
  energy_measurable := measurable_of_finite _
  μ := MeasureTheory.Measure.count

Uses 2 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Ising Hamiltonian on a finite graph

Used byIsing Gibbs probability agrees with Physlib's canonical probability · Ising partition function agrees with Physlib's partition function

LemmaIsing partition function agrees with Physlib's partition function#✓fully proved

The Ising partition function at inverse temperature T.β is Physlib's mathematical partition function of canonicalEnsemble G h at temperature T.

lemma isingZ_eq_mathematicalPartitionFunction (h : ℝ) (T : Temperature) :
    isingZ G T.β h = (canonicalEnsemble G h).mathematicalPartitionFunction T

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Ising model as a Physlib canonical ensemble · Ising partition function

Used byIsing Gibbs probability agrees with Physlib's canonical probability

LemmaIsing Gibbs probability agrees with Physlib's canonical probability#✓fully proved

The Ising Gibbs probability at inverse temperature T.β is Physlib's canonical probability of canonicalEnsemble G h at temperature T.

lemma isingProb_eq_probability (h : ℝ) (T : Temperature) (s : ConfigSpace V) :
    isingProb G T.β h s = (canonicalEnsemble G h).probability T s

Uses 5

Statement usesConfiguration space of a statistical-mechanics model · Ising model as a Physlib canonical ensemble · Gibbs probability of an Ising configuration

Proof usesIsing partition function · Ising partition function agrees with Physlib's partition function

C. The hypercubic lattice as a crystal graph

LemmaSites at \(\ell^1\) distance one are those differing by a unit vector#✓fully proved

Two sites of ℤ^d are at ℓ¹ distance one exactly when they differ by a unit vector.

lemma natAbs_sum_eq_one_iff {d : ℕ} (x y : Fin d → ℤ) :
    (∑ i, (x i - y i).natAbs) = 1 ↔
      ∃ j, y = x + Pi.single j 1 ∨ x = y + Pi.single j 1

Used by 1

Used byIsomorphism of the hypercubic lattice with Physlib's crystal graph

DefinitionIsomorphism of the hypercubic lattice with Physlib's crystal graph#✓fully proved

The nearest-neighbour graph hypercubicLattice d on ℤ^d is isomorphic to the bond graph of Physlib's hypercubic crystal CondensedMatter.Crystal.hypercubicGraph d, by sending x to the site in cell x.

StatMech.hypercubicLatticeIsoCrystal · 21 lines

def hypercubicLatticeIsoCrystal (d : ℕ) :
    hypercubicLattice d ≃g (hypercubicGraph d).toSimpleGraph where
  toFun x := ⟨x, ()⟩
  invFun p := p.cell
  left_inv _ := rfl
  right_inv _ := rfl
  map_rel_iff' {x y} := by
    change ((⟨x, ()⟩ : CellSite (Fin d → ℤ) Unit) ≠ ⟨y, ()⟩ ∧ ∃ b ∈ hypercubicBonds d,
      b.Links ⟨x, ()⟩ ⟨y, ()⟩ ∨ b.Links ⟨y, ()⟩ ⟨x, ()⟩) ↔ (hypercubicLattice d).Adj x y
    rw [hypercubicLattice_adj, natAbs_sum_eq_one_iff]
    simp only [hypercubicBonds, List.mem_ofFn, Bond.Links]
    constructor
    · rintro ⟨-, b, ⟨j, rfl⟩, h⟩
      exact ⟨j, by simpa using h⟩
    · rintro ⟨j, h⟩
      refine ⟨?_, _, ⟨j, rfl⟩, by simpa using h⟩
      intro hxy
      have hxy' : x = y := congrArg CellSite.cell hxy
      subst hxy'
      rcases h with h | h <;>
        simpa using congrFun (add_eq_left.1 h.symm) j

Uses 3

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Sites at \(\ell^1\) distance one are those differing by a unit vector

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.