Kac–Ward matrices

AbbreviationSites of the square-lattice torus#✓fully proved

The sites ℤ_L × ℤ_L of the L × L square-lattice torus.

abbrev ons_V (L : ℕ) := ZMod L × ZMod L

DefinitionNeighbouring site in a given direction on the torus#✓fully proved

The neighbor of a site in direction μ: 0 east, 1 north, 2 west, 3 south.

def ons_dirStep (L : ℕ) (μ : Fin 4) (s : ZMod L × ZMod L) : ZMod L × ZMod L :=
  match μ with
  | 0 => (s.1 + 1, s.2)
  | 1 => (s.1, s.2 + 1)
  | 2 => (s.1 - 1, s.2)
  | 3 => (s.1, s.2 - 1)

Used by 29

Used byReverse of a dart · Kac–Ward matrix of the square-lattice torus · Edge-weighted Kac-Ward matrix · 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 · Scalar of a Kac-Ward transition · Onsager's formula · Port-pattern bit of an unordered decorated edge · Interior points of the route of a decorated edge · Four finer-torus darts along the route of a decorated edge · Four-step route of a decorated edge in the finer torus · Five points of the route of a decorated edge · Head-to-tail relation between darts · Decorated graph of the torus · Closed decorated walk of a valid Kac-Ward loop · Decorated edge whose route passes through an interior micro point · Reversal-invariant internal factor of the augmented matrix · Row factor of the rank-two middle-edge term · Decorated walk of a Kac-Ward transition · Decorated walk of a chain of darts · 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 · Torus walk of four lattice steps · Endpoint of four lattice steps · Twisted Kac-Ward matrix with decorated transition weights · Torus edge underlying a dart · Port pattern of an even decorated subgraph

AbbreviationDarts of the square-lattice torus#✓fully proved

Darts (directed edges) of the torus: a starting site and a direction.

abbrev ons_Dart (L : ℕ) := (ZMod L × ZMod L) × Fin 4

Used by 149

Used byReverse of a dart · Periodic lift anchored at the base point · Edge set of a closed walk of darts · Base point in \(\mathbb{Z}^2\) over the start of a torus loop · Direction sequence of the lift of a closed torus walk · Sites of a closed torus walk in lift order · Signed boundary coefficient along a torus loop · Points of the periodic lift of a torus loop · Crossing of the vertical seam by a dart · Signed crossing of the vertical seam by a dart · Crossing of the horizontal seam by a dart · Signed crossing of the horizontal seam by a dart · Convergence radius of the twisted Kac-Ward walk expansion · Kac–Ward matrix of the square-lattice torus · Twisted Kac-Ward matrix with direction phases · Edge-weighted Kac-Ward matrix · Edge-weighted Kac-Ward matrix with direction phases · Masked edge-weighted bucket: walks through a dart, not its reverse · Masked edge-weighted bucket: walks avoiding a dart and its reverse · Translation of a dart by a lattice vector · Edge-weighted twisted bucket: walks through a dart, not its reverse · Edge-weighted twisted bucket: walks avoiding a dart and its reverse · Spin Kac-Ward identities via twisted Kac-Ward determinants · 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 · Adding a dart and its reverse to the masked set · Kac-Ward bucket: walks through a dart, not its reverse · Kac-Ward bucket: walks avoiding a dart and its reverse · Reverse of a closed walk · Masked darts after pairwise elimination along a list · Product of first-return factors along a dart elimination · Masked twisted bucket: walks through a dart, not its reverse · Masked twisted bucket: walks avoiding a dart and its reverse · Exponential of minus half the series avoiding a dart and its reverse · Twisted bucket: walks through a dart, not its reverse · Twisted bucket: walks avoiding a dart and its reverse · Sherman's convergence radius for the torus Kac-Ward matrix · Walk-series square root of the twisted Kac-Ward determinant · Log-coefficient polynomial over the cycles of a decomposition · Decorated edges as formal-series variables · Projection of a decorated edge to the torus · One-edge decorated walk along an external edge · Formal-logarithm term from closed walks of given length and exponent · Coefficient of the formal Kac-Ward logarithm · Monomial of a Kac-Ward transition · Externality of a decorated edge · Exponent of a closed Kac-Ward walk · External part of a loop exponent · Internal part of a loop exponent · Rotations of a loop and of its reversal · Darts of a loop with their reverses · Scalar of a closed Kac-Ward walk · Masked closed-walk weight through a dart but not its reverse · Masked closed-walk weight avoiding a dart and its reverse · Column-scaled augmented Kac-Ward matrix · Column weights of the column-scaled augmented matrix · Row weights of the column-scaled augmented matrix · Closed-walk weight through a dart but not its reverse · Closed-walk weight avoiding a dart and its reverse · Kac-Ward loops with a given squarefree exponent and nonzero scalar · Exponent of a Kac-Ward transition · Scalar of a Kac-Ward transition · 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 · External edges of a decorated edge set · Decorated spin polynomial · Onsager's formula · Torus even subgraph of a decorated even subgraph · Decorated weights with one edge weight scaled by t · Spin-character sums squared as twisted determinants at activity \(x\) · External edges used by a decorated walk · Torus edges underlying a decorated walk · Edge coefficient identity on the \(L \times L\) torus · Edge-weighted root identity on the torus · Adjacency of the decorated torus graph · Internal edge of the path at a site · Internal edges between two ports at a site · Dart list of a rooted decorated cycle · Closed dart walk of a rooted decorated cycle · First-return loop of a rooted decorated cycle · Test for a dart traversing an external edge · Route points of a decorated edge after its start · Port-pattern bit of an unordered decorated edge · Interior points of the route of a decorated edge · Four finer-torus darts along the route of a decorated edge · Four-step route of a decorated edge in the finer torus · Step directions of the route of a decorated edge · Five points of the route of a decorated edge · Position of a dart in the 8L × 8L torus · Image of a decorated walk in the finer torus · Expanded dart list of a decorated walk in the finer torus · Expanded loop of a decorated cycle in walking order · Expanded loop of a decorated cycle in Kac-Ward order · First dart of the expanded dart list of a decorated cycle · Darts of a Kac-Ward loop in walking order · Head-to-tail relation between darts · Decorated graph of the torus · Internal adjacency of the torus decoration · Internal neighbors of a dart in the decoration · Decorated weights with internal edges weighted by t · Transition exponent sum along a dart chain · Last dart of a dart chain · Closed decorated walk of a valid Kac-Ward loop · Decorated edge whose route passes through an interior micro point · Directions of augmented states · Reversal on augmented states · Augmented Kac-Ward matrix with two side states · Balanced augmented Kac-Ward matrix · Column weights of the balanced augmented matrix · Row weights of the balanced augmented matrix · Column weights of the augmented Kac-Ward matrix · Reversal-invariant internal factor of the augmented matrix · Row weights of the augmented Kac-Ward matrix · Gauge on the states of the augmented matrix · Column factor of the rank-two middle-edge term · Row factor of the rank-two middle-edge term · Port-pattern bit of the decorated edge between two darts · Internal path between two ports at a site · Internal walk between two ports at a site · Micro point at which a dart is placed · Decorated weights induced by torus edge weights · Decorated walk of a Kac-Ward transition · Decorated weight of a Kac-Ward transition · Edge multiset of a decorated walk as an exponent · External darts of a decorated walk in order · Decorated walk of a chain of darts · Internal-edge bits of a decorated edge set at a site · Even decorated subgraph determined by a port pattern · Decorated character sum with weights on all edges · Port bit of a dart in a decorated edge set · 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 · Twisted Kac-Ward matrix with decorated transition weights · Port bit of a dart for a torus edge set · Internal-edge bits at a site from a port pattern · Torus edge underlying a dart · Port pattern on the darts of the torus · Torus edge set of a port pattern · Port pattern of an even decorated subgraph · Seam sign of a dart · Decorated weights twisted by seam signs · Directions of the expanded dart list of a decorated walk · Directions of the external darts of a decorated walk

DefinitionTurn weight between two lattice directions#✓fully proved

The turn weight from direction μ to direction ν: 1 straight, ω for a left turn, 0 for a U-turn, ω⁻¹ for a right turn.

noncomputable def ons_turnW (ω : ℂ) (μ ν : Fin 4) : ℂ :=
  if ν = μ then 1
  else if ν = μ + 1 then ω
  else if ν = μ + 2 then 0
  else ω⁻¹

Used by 12

Used byKac–Ward matrix of the square-lattice torus · Edge-weighted Kac-Ward matrix · 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 · Reversible turn matrix on a state space with directions · State-weighted reversible turn matrix · Scalar of a Kac-Ward transition · Onsager's formula · Column factor of the rank-two middle-edge term · Row factor of the rank-two middle-edge term · Twisted Kac-Ward matrix with decorated transition weights

DefinitionKac–Ward matrix of the square-lattice torus#✓fully proved

The Kac-Ward matrix: the entry from d₁ to d₂ is x * ons_turnW ω d₁.2 d₂.2 when d₂ starts at the head of d₁, and 0 otherwise.

noncomputable def ons_KWmat (L : ℕ) (x ω : ℂ) : Matrix (ons_Dart L) (ons_Dart L) ℂ :=
  fun d₂ d₁ => if d₂.1 = ons_dirStep L d₁.2 d₁.1 then x * ons_turnW ω d₁.2 d₂.2 else 0

Uses 3 · Used by 7

Statement usesDarts of the square-lattice torus · Neighbouring site in a given direction on the torus · Turn weight between two lattice directions

Used by4 × 4 block of the Kac-Ward matrix between a site and the origin · Twisted Kac-Ward matrix with direction phases · Spin Kac-Ward identities from the decorated-torus formal identity · Spin Kac-Ward identities from the edge-weighted root identity · Kac-Ward bucket: walks through a dart, not its reverse · Kac-Ward bucket: walks avoiding a dart and its reverse · Onsager's formula

DefinitionTranslation of a dart by a lattice vector#✓fully proved

Translation of a dart by a lattice vector t.

def ons_shiftDart (L : ℕ) (t : ZMod L × ZMod L) (d : ons_Dart L) : ons_Dart L :=
  ((d.1.1 + t.1, d.1.2 + t.2), d.2)

Uses 1 · Used by 3

Statement usesDarts of the square-lattice torus

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Spin Kac-Ward identities from the edge-weighted root identity · Onsager's formula

LemmaTrace of a power as a power sum of characteristic roots#✓fully proved

The trace of φ ^ k is the sum of the k-th powers of the roots of the characteristic polynomial of φ. See also Matrix.trace_eq_sum_roots_charpoly, the case k = 1.

lemma trace_pow_endo {V : Type*} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
    (φ : Module.End ℂ V) (k : ℕ) :
    LinearMap.trace ℂ V (φ ^ k) = (φ.charpoly.roots.map (fun α => α ^ k)).sum

Used by 3

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Spin Kac-Ward identities from the edge-weighted root identity · Onsager's formula

DefinitionWalk-series square root of det(1 − Λ)#✓fully proved

The walk-series square root of det (1 - Λ): the exponential of minus one half of ∑ₙ (∑ over closed walks of length n + 1 of their weight) / (n + 1).

noncomputable def ons_detWalkRoot {E : Type*} [Fintype E] [DecidableEq E]
    (Λ : Matrix E E ℂ) : ℂ :=
  Complex.exp (-(∑' n : ℕ,
    (∑ v : Fin (n + 1) → E,
      ∏ k : Fin (n + 1), Λ (v k) (v (k + 1))) / (n + 1)) / 2)

Used by 8

Used bySpin 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 · Walk-series square root of the twisted Kac-Ward determinant · Cycle removal identity for decorated even subgraphs · Onsager's formula · Edge coefficient identity on the \(L \times L\) torus · Edge-weighted root identity on the torus

DefinitionMatrix with forbidden rows and columns set to zero#✓fully proved

The matrix Λ with every row and column indexed by a state of forbidden set to zero.

def ons_maskMatrix {E : Type*} [DecidableEq E]
    (forbidden : Finset E) (Λ : Matrix E E ℂ) : Matrix E E ℂ :=
  fun i j => if i ∈ forbidden ∨ j ∈ forbidden then 0 else Λ i j

Used by 10

Used byMasked edge-weighted bucket: walks through a dart, not its reverse · Masked edge-weighted bucket: walks avoiding a dart and its reverse · Product of first-return factors along a dart elimination · Masked twisted bucket: walks through a dart, not its reverse · Masked twisted bucket: walks avoiding a dart and its reverse · Masked closed-walk weight through a dart but not its reverse · Masked closed-walk weight avoiding a dart and its reverse · Cycle removal identity for decorated even subgraphs · Onsager's formula · Edge coefficient identity on the \(L \times L\) torus

DefinitionMatrix with selected columns scaled#✓fully proved

The matrix Λ with every column indexed by an element of S multiplied by t.

def ons_scaleColumns {E : Type*} [DecidableEq E]
    (S : Finset E) (t : ℂ) (Lambda : Matrix E E ℂ) : Matrix E E ℂ :=
  fun i j => if j ∈ S then t * Lambda i j else Lambda i j

Used by 1

Used byOnsager's formula

DefinitionTurning phase \(\omega = e^{i\pi/4}\)#✓fully proved

The turning phase ω = e^{iπ/4}, so a turn by ±π/2 contributes ω^{±1} and ω² = i.

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

Used by 19

Used bySpin Kac-Ward identities via twisted Kac-Ward determinants · 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 · Product of first-return factors along a dart elimination · Exponential of minus half the series avoiding a dart and its reverse · Walk-series square root of the twisted Kac-Ward determinant · Vanishing of repeated-edge coefficients of the formal Kac-Ward root · Masked closed-walk weight through a dart but not its reverse · Masked closed-walk weight avoiding a dart and its reverse · Closed-walk weight through a dart but not its reverse · Closed-walk weight avoiding a dart and its reverse · Kac-Ward loops with a given squarefree exponent and nonzero scalar · Cycle removal identity for decorated even subgraphs · Formal Kac-Ward identity on the torus · Onsager's formula · Spin-character sums squared as twisted determinants at activity \(x\) · Edge coefficient identity on the \(L \times L\) torus · Edge-weighted root identity on the torus

DefinitionPrimitive L-th root of unity \(e^{2\pi i/L}\)#✓fully proved

The primitive L-th root of unity e^{2πi/L}.

noncomputable def ons_spaceRoot (L : ℕ) : ℂ :=
  Complex.exp (2 * Real.pi * Complex.I / L)

Used by 3

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Spin Kac-Ward identities from the edge-weighted root identity · Onsager's formula

DefinitionSector determinant with boundary phases#✓fully proved

The sector determinant: the product of ons_symbolDispersion β over the momenta (2π(i + a/2) / L, 2π(j + b/2) / L), i, j < L, for boundary phases a, b ∈ {0, 1}.

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)

Uses 1 · Used by 5

Statement usesKac-Ward symbol determinant at t = tanh β

Used bySpin Kac-Ward identities at inverse temperature \(\beta\) · 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 · Onsager's formula

DefinitionEdge weight function with one weight scaled by t#✓fully proved

The edge weight function with the weight of edge multiplied by t.

def ons_scaleEdgeWeight
    {L : ℕ} (weight : Sym2 (ZMod L × ZMod L) → ℂ)
    (edge : Sym2 (ZMod L × ZMod L)) (t : ℂ) :
    Sym2 (ZMod L × ZMod L) → ℂ :=
  fun f => if f = edge then t * weight f else weight f

Definition4 × 4 block of the Kac-Ward matrix between a site and the origin#✓fully proved

The 4 × 4 block of the Kac-Ward matrix between the darts at site g and the darts at the origin.

noncomputable def ons_KWblock (L : ℕ) (x ωt : ℂ) (g : ZMod L × ZMod L) : Matrix (Fin 4) (Fin 4) ℂ :=
  fun a b => ons_KWmat L x ωt (g, a) (0, b)

Uses 1

Statement usesKac–Ward matrix of the square-lattice torus

DefinitionConvergence radius of the twisted Kac-Ward walk expansion#✓fully proved

The radius 1 / (number of darts) = 1 / (4L²) below which the walk expansion of the twisted Kac-Ward determinant converges.

noncomputable def ons_KWconvergenceRadius (L : ℕ) [NeZero L] : ℝ :=
  (Fintype.card (ons_Dart L) : ℝ)⁻¹

Uses 1

Statement usesDarts of the square-lattice torus

DefinitionBoundary phase of a step in a direction#✓fully proved

The phase of a step in direction μ: u, v, u⁻¹, v⁻¹ for east, north, west, south.

noncomputable def ons_dirPhase (u v : ℂ) (mu : Fin 4) : ℂ :=
  match mu with
  | 0 => u
  | 1 => v
  | 2 => u⁻¹
  | 3 => v⁻¹

Used by 9

Used byTwisted Kac-Ward matrix with direction phases · Edge-weighted Kac-Ward matrix with direction phases · 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 · Scalar of a Kac-Ward transition · Onsager's formula · Row factor of the rank-two middle-edge term · Twisted Kac-Ward matrix with decorated transition weights

DefinitionHorizontal displacement of a step in a direction#✓fully proved

The horizontal displacement 1, 0, -1, 0 of a step in direction μ.

def ons_dirExponentX (mu : Fin 4) : ℤ :=
  match mu with
  | 0 => 1
  | 1 => 0
  | 2 => -1
  | 3 => 0

Used by 1

Used byOnsager's formula

DefinitionVertical displacement of a step in a direction#✓fully proved

The vertical displacement 0, 1, 0, -1 of a step in direction μ.

def ons_dirExponentY (mu : Fin 4) : ℤ :=
  match mu with
  | 0 => 0
  | 1 => 1
  | 2 => 0
  | 3 => -1

Used by 1

Used byOnsager's formula

DefinitionTwisted Kac-Ward matrix with direction phases#✓fully proved

The Kac-Ward matrix with each step multiplied by its direction phase ons_dirPhase u v.

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

Uses 3 · Used by 12

Statement usesDarts of the square-lattice torus · Kac–Ward matrix of the square-lattice torus · Boundary phase of a step in a direction

Used byBlock of the twisted Kac-Ward matrix between a site and the origin · Spin Kac-Ward identities via twisted Kac-Ward determinants · Spin Kac-Ward identities from the decorated-torus formal identity · Spin Kac-Ward identities from the edge-weighted root identity · Product of first-return factors along a dart elimination · Masked twisted bucket: walks through a dart, not its reverse · Masked twisted bucket: walks avoiding a dart and its reverse · Twisted bucket: walks through a dart, not its reverse · Twisted bucket: walks avoiding a dart and its reverse · Walk-series square root of the twisted Kac-Ward determinant · Onsager's formula · Spin-character sums squared as twisted determinants at activity \(x\)

DefinitionBlock of the twisted Kac-Ward matrix between a site and the origin#✓fully proved

The 4 × 4 block of the twisted Kac-Ward matrix between the darts at g and at the origin.

noncomputable def ons_KWblockPhase (L : ℕ) (x omega u v : ℂ)
    (g : ZMod L × ZMod L) : Matrix (Fin 4) (Fin 4) ℂ :=
  fun a b => ons_KWmatPhase L x omega u v (g, a) (0, b)

Uses 1 · Used by 3

Statement usesTwisted Kac-Ward matrix with direction phases

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Spin Kac-Ward identities from the edge-weighted root identity · Onsager's formula

DefinitionBoundary phase \(e^{i\pi a/L}\)#✓fully proved

The boundary phase e^{iπa/L}, whose L-th power is (-1)^a.

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

Used by 27

Used byMasked edge-weighted bucket: walks through a dart, not its reverse · Masked edge-weighted bucket: walks avoiding a dart and its reverse · Edge-weighted twisted bucket: walks through a dart, not its reverse · Edge-weighted twisted bucket: walks avoiding a dart and its reverse · Spin Kac-Ward identities via twisted Kac-Ward determinants · 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 · Product of first-return factors along a dart elimination · Masked twisted bucket: walks through a dart, not its reverse · Masked twisted bucket: walks avoiding a dart and its reverse · Twisted bucket: walks through a dart, not its reverse · Twisted bucket: walks avoiding a dart and its reverse · Walk-series square root of the twisted Kac-Ward determinant · Vanishing of repeated-edge coefficients of the formal Kac-Ward root · Masked closed-walk weight through a dart but not its reverse · Masked closed-walk weight avoiding a dart and its reverse · Closed-walk weight through a dart but not its reverse · Closed-walk weight avoiding a dart and its reverse · Kac-Ward loops with a given squarefree exponent and nonzero scalar · Cycle removal identity for decorated even subgraphs · Formal Kac-Ward identity on the torus · Onsager's formula · Spin-character sums squared as twisted determinants at activity \(x\) · Edge coefficient identity on the \(L \times L\) torus · Edge-weighted root identity on the torus · Spin boundary-phase gauge at a site

DefinitionEdge-weighted Kac-Ward matrix#✓fully proved

The edge-weighted Kac-Ward matrix: the entry from d₁ to d₂ is the weight of the torus edge of d₁ times the turn weight, when d₂ starts at the head of d₁.

noncomputable def ons_KWmatWeighted (L : ℕ)
    (weight : Sym2 (ZMod L × ZMod L) → ℂ) (omega : ℂ) :
    Matrix (ons_Dart L) (ons_Dart L) ℂ :=
  fun d2 d1 =>
    if d2.1 = ons_dirStep L d1.2 d1.1 then
      weight (ons_portEdge L d1) * ons_turnW omega d1.2 d2.2
    else 0

Uses 4 · Used by 5

Statement usesDarts of the square-lattice torus · Neighbouring site in a given direction on the torus · Torus edge underlying a dart · Turn weight between two lattice directions

Used byEdge-weighted Kac-Ward matrix with direction phases · 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 · Onsager's formula

DefinitionEdge-weighted Kac-Ward matrix with direction phases#✓fully proved

The edge-weighted Kac-Ward matrix with each step multiplied by its direction phase.

noncomputable def ons_KWmatWeightedPhase (L : ℕ)
    (weight : Sym2 (ZMod L × ZMod L) → ℂ) (omega u v : ℂ) :
    Matrix (ons_Dart L) (ons_Dart L) ℂ :=
  fun d2 d1 =>
    ons_dirPhase u v d1.2 * ons_KWmatWeighted L weight omega d2 d1

Uses 3 · Used by 11

Statement usesDarts of the square-lattice torus · Edge-weighted Kac-Ward matrix · Boundary phase of a step in a direction

Used byMasked edge-weighted bucket: walks through a dart, not its reverse · Masked edge-weighted bucket: walks avoiding a dart and its reverse · Edge-weighted twisted bucket: walks through a dart, not its reverse · Edge-weighted twisted bucket: walks avoiding a dart and its reverse · 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 · Cycle removal identity for decorated even subgraphs · Onsager's formula · Edge coefficient identity on the \(L \times L\) torus · Edge-weighted root identity on the torus

DefinitionEdge-weighted twisted bucket: walks through a dart, not its reverse#✓fully proved

The total edge-weighted twisted Kac-Ward weight of closed walks of length n + 1 visiting e but not its reverse.

noncomputable def ons_weightedPhaseBucketE
    (L : ℕ) [NeZero L]
    (weight : Sym2 (ZMod L × ZMod L) → ℂ)
    (omega : ℂ) (a b : Fin 2)
    (e : ons_Dart L) (n : ℕ) : ℂ :=
  ∑ d ∈ Finset.univ.filter (fun d : Fin (n + 1) → ons_Dart L =>
      (∃ i, d i = e) ∧ ¬ (∃ j, d j = ons_dartRev L e)),
    ons_loopWeight (ons_KWmatWeightedPhase L weight omega
      (ons_spinPhase L a) (ons_spinPhase L b)) d

Uses 5

Statement usesDarts of the square-lattice torus · Edge-weighted Kac-Ward matrix with direction phases · Reverse of a dart · Weight of a cyclic sequence · Boundary phase \(e^{i\pi a/L}\)

DefinitionEdge-weighted twisted bucket: walks avoiding a dart and its reverse#✓fully proved

The total edge-weighted twisted Kac-Ward weight of closed walks of length n + 1 visiting neither e nor its reverse.

noncomputable def ons_weightedPhaseBucketN
    (L : ℕ) [NeZero L]
    (weight : Sym2 (ZMod L × ZMod L) → ℂ)
    (omega : ℂ) (a b : Fin 2)
    (e : ons_Dart L) (n : ℕ) : ℂ :=
  ∑ d ∈ Finset.univ.filter (fun d : Fin (n + 1) → ons_Dart L =>
      ¬ (∃ i, d i = e) ∧ ¬ (∃ j, d j = ons_dartRev L e)),
    ons_loopWeight (ons_KWmatWeightedPhase L weight omega
      (ons_spinPhase L a) (ons_spinPhase L b)) d

Uses 5

Statement usesDarts of the square-lattice torus · Edge-weighted Kac-Ward matrix with direction phases · Reverse of a dart · Weight of a cyclic sequence · Boundary phase \(e^{i\pi a/L}\)

DefinitionMasked edge-weighted bucket: walks through a dart, not its reverse#✓fully proved

As ons_weightedPhaseBucketE, with the darts of forbidden masked.

noncomputable def ons_maskWeightedPhaseBucketE
    (L : ℕ) [NeZero L]
    (weight : Sym2 (ZMod L × ZMod L) → ℂ)
    (omega : ℂ) (a b : Fin 2)
    (forbidden : Finset (ons_Dart L)) (e : ons_Dart L) (n : ℕ) : ℂ :=
  ∑ d ∈ Finset.univ.filter (fun d : Fin (n + 1) → ons_Dart L =>
      (∃ i, d i = e) ∧ ¬ (∃ j, d j = ons_dartRev L e)),
    ons_loopWeight
      (ons_maskMatrix forbidden (ons_KWmatWeightedPhase L weight omega
        (ons_spinPhase L a) (ons_spinPhase L b))) d

Uses 6

Statement usesDarts of the square-lattice torus · Edge-weighted Kac-Ward matrix with direction phases · Reverse of a dart · Weight of a cyclic sequence · Matrix with forbidden rows and columns set to zero · Boundary phase \(e^{i\pi a/L}\)

DefinitionMasked edge-weighted bucket: walks avoiding a dart and its reverse#✓fully proved

As ons_weightedPhaseBucketN, with the darts of forbidden masked.

noncomputable def ons_maskWeightedPhaseBucketN
    (L : ℕ) [NeZero L]
    (weight : Sym2 (ZMod L × ZMod L) → ℂ)
    (omega : ℂ) (a b : Fin 2)
    (forbidden : Finset (ons_Dart L)) (e : ons_Dart L) (n : ℕ) : ℂ :=
  ∑ d ∈ Finset.univ.filter (fun d : Fin (n + 1) → ons_Dart L =>
      ¬ (∃ i, d i = e) ∧ ¬ (∃ j, d j = ons_dartRev L e)),
    ons_loopWeight
      (ons_maskMatrix forbidden (ons_KWmatWeightedPhase L weight omega
        (ons_spinPhase L a) (ons_spinPhase L b))) d

Uses 6

Statement usesDarts of the square-lattice torus · Edge-weighted Kac-Ward matrix with direction phases · Reverse of a dart · Weight of a cyclic sequence · Matrix with forbidden rows and columns set to zero · Boundary phase \(e^{i\pi a/L}\)

DefinitionFourier symbol of one minus the Kac-Ward matrix#✓fully proved

The 4 × 4 Fourier symbol of 1 - ons_KWmat at zⱼ = e^{i kⱼ}, rows and columns indexed by the directions east, north, west, south.

noncomputable def ons_KWsymbolMat (x ω z₁ z₂ : ℂ) : Matrix (Fin 4) (Fin 4) ℂ :=
  !![ 1 - x*z₁,             -x*(-Complex.I*ω)*z₂, 0,                      -x*ω*z₂⁻¹ ;
      -x*ω*z₁,              1 - x*z₂,             -x*(-Complex.I*ω)*z₁⁻¹, 0 ;
      0,                    -x*ω*z₂,              1 - x*z₁⁻¹,             -x*(-Complex.I*ω)*z₂⁻¹ ;
      -x*(-Complex.I*ω)*z₁, 0,                    -x*ω*z₁⁻¹,              1 - x*z₂⁻¹ ]

Used by 3

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Spin Kac-Ward identities from the edge-weighted root identity · Onsager's formula

29 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.