From the spin Kac-Ward identities to Onsager's formula

DefinitionSpin Kac-Ward identities at inverse temperature \(\beta\)#✓fully proved

The spin Kac-Ward identities at inverse temperature β: on every L × L torus with L > 2, each signed sector sum at tanh β squares to the corresponding sector determinant.

def ons_spinKacWardIdentities (beta : ℝ) : Prop :=
  ∀ (L : ℕ) (hL : 2 < L),
    letI : Fact (2 < L) := ⟨hL⟩
    ons_spin11 L (Real.tanh beta) ^ 2 = ons_spinDet L beta 0 0 ∧
    ons_spin01 L (Real.tanh beta) ^ 2 = ons_spinDet L beta 1 0 ∧
    ons_spin10 L (Real.tanh beta) ^ 2 = ons_spinDet L beta 0 1 ∧
    ons_spin00 L (Real.tanh beta) ^ 2 = ons_spinDet L beta 1 1

noncomputable def ons_spin11 (L : ℕ) [Fact (2 < L)] (x : ℝ) : ℝ :=
  ons_sector00 L x - ons_sector10 L x - ons_sector01 L x - ons_sector11 L x

PhyslibExt/CondensedMatter/IsingModel/Onsager/TorusSpinSectors.lean:170

noncomputable def ons_spinDet (L : ℕ) (β : ℝ) (a b : Fin 2) : ℝ :=
  ∏ i ∈ Finset.range L, ∏ j ∈ Finset.range L,
    ons_symbolDispersion β
      (2 * Real.pi * (i + (a.val : ℝ) / 2) / L)
      (2 * Real.pi * (j + (b.val : ℝ) / 2) / L)

PhyslibExt/CondensedMatter/IsingModel/Onsager/KWDetLimit.lean:187

noncomputable def ons_spin01 (L : ℕ) [Fact (2 < L)] (x : ℝ) : ℝ :=
  ons_sector00 L x + ons_sector10 L x - ons_sector01 L x + ons_sector11 L x

PhyslibExt/CondensedMatter/IsingModel/Onsager/TorusSpinSectors.lean:166

noncomputable def ons_spin10 (L : ℕ) [Fact (2 < L)] (x : ℝ) : ℝ :=
  ons_sector00 L x - ons_sector10 L x + ons_sector01 L x + ons_sector11 L x

PhyslibExt/CondensedMatter/IsingModel/Onsager/TorusSpinSectors.lean:162

noncomputable def ons_spin00 (L : ℕ) [Fact (2 < L)] (x : ℝ) : ℝ :=
  ons_sector00 L x + ons_sector10 L x + ons_sector01 L x - ons_sector11 L x

PhyslibExt/CondensedMatter/IsingModel/Onsager/TorusSpinSectors.lean:158

Uses 5 · Used by 4

Statement usesSigned sector sum \(Z_{00} + Z_{10} + Z_{01} - Z_{11}\) · Signed sector sum \(Z_{00} + Z_{10} - Z_{01} + Z_{11}\) · Signed sector sum \(Z_{00} - Z_{10} + Z_{01} + Z_{11}\) · Signed sector sum \(Z_{00} - Z_{10} - Z_{01} - Z_{11}\) · Sector determinant with boundary phases

Used byOnsager'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 · Onsager's formula

DefinitionSpin Kac-Ward identities via twisted Kac-Ward determinants#✓fully proved

The spin Kac-Ward identities written with the twisted Kac-Ward determinants det (1 - Λ_{ab}) at x = tanh β.

StatMech.Onsager.ons_spinKacWardMatrixIdentities · 15 lines

def ons_spinKacWardMatrixIdentities (beta : ℝ) : Prop :=
  ∀ (L : ℕ) (hL : 2 < L),
    letI : Fact (2 < L) := ⟨hL⟩
    ((ons_spin11 L (Real.tanh beta) : ℂ) ^ 2 =
      (1 - ons_KWmatPhase L (Real.tanh beta : ℂ) ons_turnRoot
        (ons_spinPhase L 0) (ons_spinPhase L 0)).det) ∧
    ((ons_spin01 L (Real.tanh beta) : ℂ) ^ 2 =
      (1 - ons_KWmatPhase L (Real.tanh beta : ℂ) ons_turnRoot
        (ons_spinPhase L 1) (ons_spinPhase L 0)).det) ∧
    ((ons_spin10 L (Real.tanh beta) : ℂ) ^ 2 =
      (1 - ons_KWmatPhase L (Real.tanh beta : ℂ) ons_turnRoot
        (ons_spinPhase L 0) (ons_spinPhase L 1)).det) ∧
    ((ons_spin00 L (Real.tanh beta) : ℂ) ^ 2 =
      (1 - ons_KWmatPhase L (Real.tanh beta : ℂ) ons_turnRoot
        (ons_spinPhase L 1) (ons_spinPhase L 1)).det)

noncomputable def ons_spin11 (L : ℕ) [Fact (2 < L)] (x : ℝ) : ℝ :=
  ons_sector00 L x - ons_sector10 L x - ons_sector01 L x - ons_sector11 L x

PhyslibExt/CondensedMatter/IsingModel/Onsager/TorusSpinSectors.lean:170

noncomputable def ons_KWmatPhase (L : ℕ) (x omega u v : ℂ) :
    Matrix (ons_Dart L) (ons_Dart L) ℂ :=
  fun d2 d1 => ons_dirPhase u v d1.2 * ons_KWmat L x omega d2 d1

PhyslibExt/CondensedMatter/IsingModel/Onsager/KWSpinFourier.lean:111

noncomputable def ons_turnRoot : ℂ := Complex.exp (Complex.I * (Real.pi / 4))

PhyslibExt/CondensedMatter/IsingModel/Onsager/KWDetLimit.lean:59

noncomputable def ons_spinPhase (L : ℕ) (a : Fin 2) : ℂ :=
  Complex.exp (Complex.I * ((Real.pi * a.val / L : ℝ) : ℂ))

PhyslibExt/CondensedMatter/IsingModel/Onsager/KWSpinFourier.lean:268

noncomputable def ons_spin01 (L : ℕ) [Fact (2 < L)] (x : ℝ) : ℝ :=
  ons_sector00 L x + ons_sector10 L x - ons_sector01 L x + ons_sector11 L x

PhyslibExt/CondensedMatter/IsingModel/Onsager/TorusSpinSectors.lean:166

noncomputable def ons_spin10 (L : ℕ) [Fact (2 < L)] (x : ℝ) : ℝ :=
  ons_sector00 L x - ons_sector10 L x + ons_sector01 L x + ons_sector11 L x

PhyslibExt/CondensedMatter/IsingModel/Onsager/TorusSpinSectors.lean:162

noncomputable def ons_spin00 (L : ℕ) [Fact (2 < L)] (x : ℝ) : ℝ :=
  ons_sector00 L x + ons_sector10 L x + ons_sector01 L x - ons_sector11 L x

PhyslibExt/CondensedMatter/IsingModel/Onsager/TorusSpinSectors.lean:158

Uses 8

Statement usesDarts of the square-lattice torus · Twisted Kac-Ward matrix with direction phases · Signed sector sum \(Z_{00} + Z_{10} + Z_{01} - Z_{11}\) · Signed sector sum \(Z_{00} + Z_{10} - Z_{01} + Z_{11}\) · Signed sector sum \(Z_{00} - Z_{10} + Z_{01} + Z_{11}\) · Signed sector sum \(Z_{00} - Z_{10} - Z_{01} - Z_{11}\) · Boundary phase \(e^{i\pi a/L}\) · Turning phase \(\omega = e^{i\pi/4}\)

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.