Sherman's loop cancellations and product formula

DefinitionReversible turn matrix on a state space with directions#✓fully proved

The matrix q x y · turnW(dir y, dir x) on an abstract state space with directions.

noncomputable def ons_reversibleTurnMatrix
    {E : Type*} (dir : E → Fin 4) (omega : ℂ)
    (q : E → E → ℂ) : Matrix E E ℂ :=
  fun x y ↦ q x y * ons_turnW omega (dir y) (dir x)

Uses 1

Statement usesTurn weight between two lattice directions

DefinitionState-weighted reversible turn matrix#✓fully proved

The reversible turn matrix with additional row and column weights on states.

noncomputable def ons_stateWeightedReversibleTurnMatrix
    {E : Type*} (dir : E → Fin 4) (omega : ℂ)
    (rowWeight colWeight : E → ℂ) (q : E → E → ℂ) :
    Matrix E E ℂ :=
  fun x y ↦ rowWeight x * colWeight y * q x y *
    ons_turnW omega (dir y) (dir x)

Uses 1 · Used by 1

Statement usesTurn weight between two lattice directions

Used byOnsager's formula

DefinitionReversal of a cyclic sequence of states#✓fully proved

Reversal of a cyclic sequence of states: position k carries rev of the state at position -k.

def ons_involutiveLoopRev
    {E : Type*} {n : ℕ} [NeZero n]
    (rev : E → E) (loop : Fin n → E) : Fin n → E :=
  fun k ↦ rev (loop (-k))

Used by 1

Used byOnsager's formula

DefinitionMasked reversible factor#✓fully proved

The reversible factor with the rows and columns of forbidden set to zero.

noncomputable def ons_maskedReversibleFactor
    {E : Type*} [DecidableEq E]
    (forbidden : Finset E) (q : E → E → ℂ) : E → E → ℂ :=
  fun x y ↦ if x ∈ forbidden ∨ y ∈ forbidden then 0 else q x y

DefinitionMajorant \(q^{|s|-1}\) for the weight of a walk#✓fully proved

The majorant q^{|s| - 1} for the weight of a walk s with at least two states, and 0 for shorter lists.

def ons_factorMajorant (q : ℝ) (s : List E) : ℝ :=
  if s.length < 2 then 0 else q ^ (s.length - 1)

Used by 1

Used byOnsager's formula

DefinitionSherman's convergence radius for the torus Kac-Ward matrix#✓fully proved

The radius 1 / (2 (number of darts)²) below which Sherman's first-return series for the torus Kac-Ward matrix converges with total weight below 1.

noncomputable def ons_ShermanRadius (L : ℕ) [NeZero L] : ℝ :=
  (2 * (Fintype.card (ons_Dart L) : ℝ) ^ 2)⁻¹

Uses 1 · Used by 4

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 · Sherman's radius for \(L > 2\), with value 1 otherwise

LemmaProduct over a tuple equals the product over its list#✓fully proved

The product over a tuple equals the product over the list List.ofFn p; see also List.prod_ofFn and List.map_ofFn.

lemma ons_tupleProd_eq_listProd (wt : α → ℂ) {k : ℕ} (p : Fin k → α) :
    ∏ i : Fin k, wt (p i) = ((List.ofFn p).map wt).prod

Lemma\(1 - z \neq 0\) for \(|z| < 1\)#✓fully proved

1 - z ≠ 0 when ‖z‖ < 1.

lemma ons_one_sub_ne_zero_of_norm_lt_one {z : ℂ} (hz : ‖z‖ < 1) : (1 : ℂ) - z ≠ 0

Used by 1

Used byOnsager's formula

DefinitionFirst-return loop at a directed edge#✓fully proved

A cyclic sequence v is a first-return loop at e (avoiding rev e) if it starts at e, does not visit e again, and never uses the reverse edge rev e.

def ons_isFirstReturn (e : E) (rev : E → E) (v : Fin n → E) : Prop :=
  v 0 = e ∧ (∀ k : Fin n, k ≠ 0 → v k ≠ e) ∧ (∀ k : Fin n, v k ≠ rev e)

DefinitionCyclic sequences rooted at an edge avoiding its reverse#✓fully proved

The cyclic sequences of length n that start at e and never use rev e.

def ons_rootedAvoiding (e : E) (rev : E → E) : Finset (Fin n → E) :=
  {v ∈ (Finset.univ : Finset (Fin n → E)) | v 0 = e ∧ (∀ k : Fin n, v k ≠ rev e)}

DefinitionTerm of the list series: product of weights over length#✓fully proved

The term (∏_{a ∈ l} wt a) / |l| of the list series, set to 0 on the empty list.

noncomputable def ons_listSeriesTerm {alpha : Type*} (wt : alpha → ℂ)
    (l : List alpha) : ℂ :=
  if _h : l = [] then 0 else (l.map wt).prod / (l.length : ℂ)

Used by 1

Used byOnsager's formula

DefinitionWeight of a cyclic sequence#✓fully proved

The weight ∏ₖ Λ (v k) (v (k + 1)) of a cyclic sequence v : Fin n → E, indices taken modulo n.

noncomputable def ons_loopWeight {E : Type*} [Fintype E] [DecidableEq E] (Λ : Matrix E E ℂ)
    {n : ℕ} [NeZero n] (v : Fin n → E) : ℂ := ∏ k : Fin n, Λ (v k) (v (k + 1))

Used by 21

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 · Edge-weighted root identity from the decorated-torus formal identity · Kac-Ward bucket: walks through a dart, not its reverse · Kac-Ward bucket: walks avoiding a dart and its reverse · Sherman's Lemma 5 · Masked twisted bucket: walks through a dart, not its reverse · Masked twisted bucket: walks avoiding a dart and its reverse · Matrix bucket: walks through one state avoiding another · Matrix bucket: walks avoiding two given states · Twisted bucket: walks through a dart, not its reverse · Twisted bucket: walks avoiding a dart and its reverse · Loop sum vanishes under a fixed-point-free sign-reversing involution · 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 · Onsager's formula

DefinitionRotation of a cyclic sequence by one step#✓fully proved

Rotation of a cyclic sequence by one step: (ons_cyclicShift v) k = v (k + 1).

def ons_cyclicShift {E : Type*} {n : ℕ} [NeZero n] (v : Fin n → E) : Fin n → E :=
  fun k => v (k + 1)

Used by 2

Used byRotation-orbit equivalence on cyclic sequences · Onsager's formula

DefinitionKac-Ward bucket: walks through a dart, not its reverse#✓fully proved

The total Kac-Ward weight of closed walks of length n + 1 that visit e but not its reverse.

noncomputable def ons_bucketE (L : ℕ) [NeZero L] (x ω : ℂ) (e : ons_Dart L) (n : ℕ) : ℂ :=
  ∑ v ∈ Finset.univ.filter (fun v : Fin (n + 1) → ons_Dart L =>
      (∃ i, v i = e) ∧ ¬ (∃ j, v j = ons_dartRev L e)),
    ons_loopWeight (ons_KWmat L x ω) v

Uses 4

Statement usesDarts of the square-lattice torus · Kac–Ward matrix of the square-lattice torus · Reverse of a dart · Weight of a cyclic sequence

DefinitionKac-Ward bucket: walks avoiding a dart and its reverse#✓fully proved

The total Kac-Ward weight of closed walks of length n + 1 that visit neither e nor its reverse.

noncomputable def ons_bucketN (L : ℕ) [NeZero L] (x ω : ℂ) (e : ons_Dart L) (n : ℕ) : ℂ :=
  ∑ v ∈ Finset.univ.filter (fun v : Fin (n + 1) → ons_Dart L =>
      ¬ (∃ i, v i = e) ∧ ¬ (∃ j, v j = ons_dartRev L e)),
    ons_loopWeight (ons_KWmat L x ω) v

Uses 4

Statement usesDarts of the square-lattice torus · Kac–Ward matrix of the square-lattice torus · Reverse of a dart · Weight of a cyclic sequence

LemmaLoop sum vanishes under a fixed-point-free sign-reversing involution#✓fully proved

A fixed-point-free involution of S that reverses the sign of the loop weight forces the loop weights over S to sum to zero. See also Finset.sum_involution.

lemma ons_sum_zero_of_sign_involution {E} [Fintype E] [DecidableEq E] (Λ : Matrix E E ℂ)
    {n : ℕ} [NeZero n] (S : Finset (Fin n → E)) (g : (Fin n → E) → (Fin n → E))
    (hmaps : ∀ v ∈ S, g v ∈ S)
    (hsign : ∀ v ∈ S, ons_loopWeight Λ (g v) = - ons_loopWeight Λ v)
    (hinv : ∀ v ∈ S, g (g v) = v) (hne : ∀ v ∈ S, g v ≠ v) :
    ∑ v ∈ S, ons_loopWeight Λ v = 0

Uses 1

Statement usesWeight of a cyclic sequence

DefinitionCyclic sequences visiting two given states#✓fully proved

The cyclic sequences of length n that visit both a and b.

noncomputable def ons_loopSetBoth {E} [Fintype E] [DecidableEq E] {n : ℕ}
    (a b : E) : Finset (Fin n → E) :=
  {v ∈ (Finset.univ : Finset (Fin n → E)) | (∃ i, v i = a) ∧ (∃ j, v j = b)}

Used by 2

Used bySherman's Lemma 5 · Onsager's formula

DefinitionMirror position within a segment#✓fully proved

The mirror image l + m - k of a position k in the segment [l, m] (truncated to n - 1).

def ons_mir {n : ℕ} [NeZero n] (l m k : Fin n) : Fin n :=
  ⟨min (l.val + m.val - k.val) (n - 1), by have := NeZero.pos n; omega⟩

Used by 3

Used bySherman's Lemma 5 · Reversal of a segment of a cyclic sequence · Onsager's formula

DefinitionReversal of a segment of a cyclic sequence#✓fully proved

Reversal of the segment [l, m] of v: positions inside are mirrored and their entries replaced by their reverses; positions outside are unchanged.

def ons_revSeg {E} {n : ℕ} [NeZero n] (rev : E → E) (l m : Fin n) (v : Fin n → E) :
    Fin n → E :=
  fun k => if l ≤ k ∧ k ≤ m then rev (v (ons_mir l m k)) else v k

Uses 1 · Used by 3

Statement usesMirror position within a segment

Used bySherman's Lemma 5 · Sherman's segment-reversal surgery · Onsager's formula

DefinitionPositions where a sequence meets an edge or its reverse#✓fully proved

The positions where v meets e or rev e.

noncomputable def ons_hitSet {E} [DecidableEq E] {n : ℕ} (e : E) (rev : E → E)
    (v : Fin n → E) : Finset (Fin n) :=
  {k | v k = e ∨ v k = rev e}

Used by 3

Used byFirst position meeting an edge or its reverse · Sherman's Lemma 5 · Onsager's formula

DefinitionFirst position meeting an edge or its reverse#✓fully proved

The first position where v meets e or rev e (0 if there is none).

noncomputable def ons_l {E} [DecidableEq E] {n : ℕ} [NeZero n] (e : E) (rev : E → E)
    (v : Fin n → E) : Fin n :=
  if h : (ons_hitSet e rev v).Nonempty then (ons_hitSet e rev v).min' h else 0

Uses 1 · Used by 4

Statement usesPositions where a sequence meets an edge or its reverse

Used bySherman's Lemma 5 · Positions meeting the reverse of the first hit · Sherman's segment-reversal surgery · Onsager's formula

DefinitionPositions meeting the reverse of the first hit#✓fully proved

The positions where v meets the reverse of its entry at ons_l e rev v.

noncomputable def ons_mSet {E} [DecidableEq E] {n : ℕ} [NeZero n] (e : E) (rev : E → E)
    (v : Fin n → E) : Finset (Fin n) :=
  {j | v j = rev (v (ons_l e rev v))}

Uses 1 · Used by 3

Statement usesFirst position meeting an edge or its reverse

Used bySherman's Lemma 5 · Last position meeting the reverse of the first hit · Onsager's formula

DefinitionLast position meeting the reverse of the first hit#✓fully proved

The last position where v meets the reverse of its entry at ons_l e rev v (0 if there is none).

noncomputable def ons_m {E} [DecidableEq E] {n : ℕ} [NeZero n] (e : E) (rev : E → E)
    (v : Fin n → E) : Fin n :=
  if h : (ons_mSet e rev v).Nonempty then (ons_mSet e rev v).max' h else 0

Uses 1 · Used by 3

Statement usesPositions meeting the reverse of the first hit

Used bySherman's Lemma 5 · Sherman's segment-reversal surgery · Onsager's formula

DefinitionSherman's segment-reversal surgery#✓fully proved

Sherman's surgery: reverse the segment between ons_l and ons_m when v visits both e and rev e; otherwise leave v unchanged.

noncomputable def ons_surgery {E} [DecidableEq E] {n : ℕ} [NeZero n] (e : E) (rev : E → E)
    (v : Fin n → E) : Fin n → E :=
  if (∃ i, v i = e) ∧ (∃ j, v j = rev e) then
    ons_revSeg rev (ons_l e rev v) (ons_m e rev v) v
  else v

Uses 3 · Used by 2

Statement usesFirst position meeting an edge or its reverse · Last position meeting the reverse of the first hit · Reversal of a segment of a cyclic sequence

Used bySherman's Lemma 5 · Onsager's formula

LemmaSherman's Lemma 5#✓fully proved

If the surgery reverses the sign of loop weights, the loops that visit both e and rev e have total weight zero (S. Sherman, Combinatorial aspects of the Ising model for ferromagnetism. I, 1960).

lemma ons_lemma5 {E} [Fintype E] [DecidableEq E] (Λ : Matrix E E ℂ)
    {n : ℕ} [NeZero n] (e : E) (rev : E → E) (hrev : Function.Involutive rev)
    (hrne : rev e ≠ e)
    (hsign : ∀ v ∈ ons_loopSetBoth (n := n) e (rev e),
      ons_loopWeight Λ (ons_surgery e rev v) = - ons_loopWeight Λ v) :
    ∑ v ∈ ons_loopSetBoth (n := n) e (rev e), ons_loopWeight Λ v = 0

Uses 9 · Used by 1

Statement usesCyclic sequences visiting two given states · Weight of a cyclic sequence · Sherman's segment-reversal surgery

Proof usesPositions where a sequence meets an edge or its reverse · First position meeting an edge or its reverse · Last position meeting the reverse of the first hit · Positions meeting the reverse of the first hit · Mirror position within a segment · Reversal of a segment of a cyclic sequence

Used byOnsager's formula

DefinitionReverse of a closed walk#✓fully proved

The reverse of a closed walk: position k carries the reverse of the dart at position -k.

def ons_loopRev (L : ℕ) {n : ℕ} [NeZero n] (v : Fin n → ons_Dart L) : Fin n → ons_Dart L :=
  fun k => ons_dartRev L (v (-k))

Uses 2 · Used by 2

Statement usesDarts of the square-lattice torus · Reverse of a dart

Used byRotations of a loop and of its reversal · Onsager's formula

DefinitionRotation-orbit equivalence on cyclic sequences#✓fully proved

The rotation-orbit equivalence relation on cyclic sequences: v ∼ w when w is obtained from v by an iterated rotation.

StatMech.Onsager.ons_orbitSetoid · 17 lines

def ons_orbitSetoid (E : Type*) [Fintype E] [DecidableEq E] (n : ℕ) [NeZero n] :
    Setoid (Fin n → E) where
  r v w := ∃ j : ℕ, ons_cyclicShift^[j] v = w
  iseqv :=
    { refl := fun _ => ⟨0, rfl⟩
      symm := by
        rintro v w ⟨j, rfl⟩
        refine ⟨(n - 1) * j, ?_⟩
        have hmul : (n - 1) * j + j = n * j := by
          have h1 : n - 1 + 1 = n := Nat.succ_pred_eq_of_pos (Nat.pos_of_neZero n)
          calc (n - 1) * j + j = (n - 1) * j + 1 * j := by rw [one_mul]
            _ = (n - 1 + 1) * j := by rw [add_mul]
            _ = n * j := by rw [h1]
        rw [← Function.iterate_add_apply, hmul, ons_cyclicShift_iterate_mul_self]
      trans := by
        rintro u v w ⟨i, rfl⟩ ⟨j, rfl⟩
        exact ⟨j + i, by rw [Function.iterate_add_apply]⟩ }

Uses 1 · Used by 1

Statement usesRotation of a cyclic sequence by one step

Used byChosen representative of a rotation orbit

DefinitionChosen representative of a rotation orbit#✓fully proved

A chosen representative of the rotation orbit of v.

noncomputable def ons_rep (v : Fin n → E) : Fin n → E :=
  (Quotient.mk (ons_orbitSetoid E n) v).out

Uses 1 · Used by 1

Statement usesRotation-orbit equivalence on cyclic sequences

Used byNumber of sequences with a given orbit representative

DefinitionNumber of sequences with a given orbit representative#✓fully proved

The number of sequences whose chosen orbit representative is r; for a representative r this is the size of its rotation orbit, and 0 otherwise.

noncomputable def ons_orbitCard (r : Fin n → E) : ℕ :=
  (Finset.univ.filter (fun v => ons_rep v = r)).card

Uses 1

Statement usesChosen representative of a rotation orbit

DefinitionRotation of a cyclic sequence by \(k\) steps#✓fully proved

Rotation of a cyclic sequence by k steps: (ons_rotate k v) j = v (j + k).

def ons_rotate (k : Fin n) (v : Fin n → E) : Fin n → E :=
  fun j => v (j + k)

Used by 3

Used byRotation by \(k\) as an equivalence of sequences · Rotations of a loop and of its reversal · Onsager's formula

DefinitionRotation by \(k\) as an equivalence of sequences#✓fully proved

Rotation by k as an equivalence of Fin n → E, with inverse the rotation by -k.

def ons_rotateEquiv (k : Fin n) : (Fin n → E) ≃ (Fin n → E) where
  toFun := ons_rotate k
  invFun := ons_rotate (-k)
  left_inv v := by
    funext j
    simp [ons_rotate, add_assoc]
  right_inv v := by
    funext j
    simp [ons_rotate, add_assoc]

Uses 1 · Used by 1

Statement usesRotation of a cyclic sequence by \(k\) steps

Used byOnsager's formula

DefinitionNumber of visits of a sequence to a state#✓fully proved

The number of positions k with v k = e.

def ons_visitCount (e : E) (v : Fin n → E) : ℕ :=
  Fintype.card {k : Fin n // v k = e}

Used by 1

Used byOnsager's formula

DefinitionEdge weight of a walk#✓fully proved

The edge weight Λ e₀ e₁ * Λ e₁ e₂ * ⋯ * Λ eₖ₋₁ eₖ of a walk [e₀, …, eₖ]; walks with at most one entry have weight 1.

noncomputable def ons_edgeWeight (Λ : Matrix E E ℂ) : List E → ℂ
  | [] => 1
  | [_] => 1
  | a :: b :: t => Λ a b * ons_edgeWeight Λ (b :: t)

Used by 4

Used byWeight of a first-return segment avoiding a state · Rooted term: walk weight over its number of first-return factors · Cycle removal identity for decorated even subgraphs · Onsager's formula

DefinitionGluing of walk segments at a root#✓fully proved

Concatenation of walk segments sharing their end points at e: each segment except the last loses its final entry, and the result ends in e.

def ons_glue (e : E) (ss : List (List E)) : List E :=
  ss.foldr (fun s acc => s.dropLast ++ acc) [e]

Used by 2

Used byRooted closed walks as lists of first-return segments · Onsager's formula

DefinitionSplitting a list at the occurrences of a root#✓fully proved

Splitting of a list at the occurrences of e: each piece runs from one occurrence of e to the next.

def ons_firstReturnSplit (e : E) : List E → List (List E)
  | [] => []
  | x :: r =>
      match hpost : r.dropWhile (fun y => y ≠ e) with
      | [] => [x :: r]
      | e' :: post' =>
          (x :: r.takeWhile (fun y => y ≠ e) ++ [e']) :: ons_firstReturnSplit e (e' :: post')
  termination_by l => l.length
  decreasing_by
    have hle := List.length_dropWhile_le (fun y => decide (y ≠ e)) r
    rw [hpost] at hle
    simp only [List.length_cons] at hle ⊢
    omega

Used by 3

Used byFirst-return segments of a closed walk · Rooted closed walks as lists of first-return segments · Onsager's formula

DefinitionFirst-return segment at a state#✓fully proved

A first-return segment at e: a list e :: interior ++ [e] whose interior avoids e.

def ons_isFirstReturnSegment (e : E) (s : List E) : Prop :=
  ∃ interior : List E,
    s = e :: interior ++ [e] ∧ ∀ x ∈ interior, x ≠ e

Used by 4

Used byWeight of a first-return segment avoiding a state · Rooted closed walks as lists of first-return segments · List of first-return segments avoiding a state · Onsager's formula

DefinitionFirst-return segments of a closed walk#✓fully proved

The first-return segments of a closed walk at e, without the trailing one-element piece [e].

def ons_firstReturnFactors (e : E) (w : List E) : List (List E) :=
  (ons_firstReturnSplit e w).dropLast

Uses 1 · Used by 3

Statement usesSplitting a list at the occurrences of a root

Used byRooted closed walks as lists of first-return segments · Rooted term: walk weight over its number of first-return factors · Onsager's formula

DefinitionRooted closed walk at a state avoiding another#✓fully proved

A rooted closed walk at e avoiding r: a list starting and ending at e that never contains r.

def ons_validRootedList (e r : E) (w : List E) : Prop :=
  w.head? = some e ∧ w.getLast? = some e ∧ ∀ x ∈ w, x ≠ r

Used by 2

Used byRooted closed walks as lists of first-return segments · Onsager's formula

DefinitionList of first-return segments avoiding a state#✓fully proved

A list of first-return segments at e, none of which contains r.

def ons_validFactorList (e r : E) (ss : List (List E)) : Prop :=
  ∀ s ∈ ss, ons_isFirstReturnSegment e s ∧ ∀ x ∈ s, x ≠ r

Uses 1 · Used by 2

Statement usesFirst-return segment at a state

Used byRooted closed walks as lists of first-return segments · Onsager's formula

DefinitionRooted closed walks as lists of first-return segments#✓fully proved

Rooted closed walks at e avoiding r are equivalent to lists of first-return segments avoiding r, by splitting and gluing.

StatMech.Onsager.ons_rootedFactorEquiv · 28 lines

def ons_rootedFactorEquiv (e r : E) (her : e ≠ r) :
    {w : List E // ons_validRootedList e r w} ≃
      {ss : List (List E) // ons_validFactorList e r ss} where
  toFun w := ⟨ons_firstReturnFactors e w.1,
    firstReturnFactors_valid e r w.1 w.2⟩
  invFun ss := ⟨ons_glue e ss.1, by
    have hfirst : ∀ s ∈ ss.1, ons_isFirstReturnSegment e s :=
      fun s hs => (ss.2 s hs).1
    have hhead : ∀ s ∈ ss.1, s.head? = some e :=
      fun s hs => ons_firstReturnSegment_head (hfirst s hs)
    have hlast : ∀ s ∈ ss.1, s.getLast? = some e :=
      fun s hs => ons_firstReturnSegment_last (hfirst s hs)
    refine ⟨?_, ?_, avoids_glue e r her ss.1 ss.2⟩
    · obtain ⟨tail, htail⟩ := ons_glue_head e ss.1 hhead
      rw [htail]
      simp
    · exact glue_getLast e ss.1⟩
  left_inv w := by
    apply Subtype.ext
    exact (ons_firstReturnFactors_spec e w.1 w.2.1 w.2.2.1).2.2
  right_inv ss := by
    apply Subtype.ext
    have hfirst : ∀ s ∈ ss.1, ons_isFirstReturnSegment e s :=
      fun s hs => (ss.2 s hs).1
    change ons_firstReturnFactors e (ons_glue e ss.1) = ss.1
    unfold ons_firstReturnFactors
    rw [ons_firstReturnSplit_glue e ss.1 hfirst]
    simp

Uses 6 · Used by 1

Statement usesFirst-return segments of a closed walk · Splitting a list at the occurrences of a root · Gluing of walk segments at a root · First-return segment at a state · List of first-return segments avoiding a state · Rooted closed walk at a state avoiding another

Used byOnsager's formula

DefinitionWeight of a first-return segment avoiding a state#✓fully proved

The edge weight of s if s is a first-return segment at e avoiding r, and 0 otherwise.

noncomputable def ons_firstReturnWeight (Lambda : Matrix E E ℂ) (e r : E)
    (s : List E) : ℂ := by
  classical
  exact if ons_isFirstReturnSegment e s ∧ (∀ x ∈ s, x ≠ r) then
      ons_edgeWeight Lambda s
    else 0

Uses 2 · Used by 4

Statement usesEdge weight of a walk · First-return segment at a state

Used byProduct of first-return factors along a dart elimination · Cycle removal identity for decorated even subgraphs · Onsager's formula · Edge coefficient identity on the \(L \times L\) torus

DefinitionRooted term: walk weight over its number of first-return factors#✓fully proved

The rooted term of a walk: its edge weight divided by its number of first-return factors at e.

noncomputable def ons_rootedListTerm (Lambda : Matrix E E ℂ) (e : E)
    (w : List E) : ℂ :=
  ons_edgeWeight Lambda w / ((ons_firstReturnFactors e w).length : ℂ)

Uses 2 · Used by 1

Statement usesEdge weight of a walk · First-return segments of a closed walk

Used byOnsager's formula

DefinitionTwisted bucket: walks through a dart, not its reverse#✓fully proved

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

noncomputable def ons_phaseBucketE
    (L : ℕ) [NeZero L] (x 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_KWmatPhase L x omega
      (ons_spinPhase L a) (ons_spinPhase L b)) d

Uses 5

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

DefinitionTwisted bucket: walks avoiding a dart and its reverse#✓fully proved

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

noncomputable def ons_phaseBucketN
    (L : ℕ) [NeZero L] (x 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_KWmatPhase L x omega
      (ons_spinPhase L a) (ons_spinPhase L b)) d

Uses 5 · Used by 1

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

Used byExponential of minus half the series avoiding a dart and its reverse

DefinitionMasked twisted bucket: walks through a dart, not its reverse#✓fully proved

As ons_phaseBucketE, for the twisted matrix with the darts of forbidden masked.

noncomputable def ons_maskPhaseBucketE
    (L : ℕ) [NeZero L] (x 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_KWmatPhase L x omega
        (ons_spinPhase L a) (ons_spinPhase L b))) d

Uses 6

Statement usesDarts of the square-lattice torus · Twisted 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 twisted bucket: walks avoiding a dart and its reverse#✓fully proved

As ons_phaseBucketN, for the twisted matrix with the darts of forbidden masked.

noncomputable def ons_maskPhaseBucketN
    (L : ℕ) [NeZero L] (x 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_KWmatPhase L x omega
        (ons_spinPhase L a) (ons_spinPhase L b))) d

Uses 6

Statement usesDarts of the square-lattice torus · Twisted 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}\)

DefinitionWalk-series square root of the twisted Kac-Ward determinant#✓fully proved

The walk-series square root of the twisted Kac-Ward determinant with boundary phases a, b at activity x.

noncomputable def ons_spinWalkRoot
    (L : ℕ) [NeZero L] (x : ℝ) (a b : Fin 2) : ℂ :=
  ons_detWalkRoot (ons_KWmatPhase L (x : ℂ) ons_turnRoot
    (ons_spinPhase L a) (ons_spinPhase L b))

Uses 5

Statement usesDarts of the square-lattice torus · Twisted Kac-Ward matrix with direction phases · Walk-series square root of det(1 − Λ) · Boundary phase \(e^{i\pi a/L}\) · Turning phase \(\omega = e^{i\pi/4}\)

DefinitionExponential of minus half the series avoiding a dart and its reverse#✓fully proved

The exponential of minus one half of the series of closed walks avoiding e and its reverse.

noncomputable def ons_phaseAvoidRoot
    (L : ℕ) [NeZero L] (x : ℝ) (a b : Fin 2)
    (e : ons_Dart L) : ℂ :=
  Complex.exp (-(∑' n : ℕ,
    ons_phaseBucketN L (x : ℂ) ons_turnRoot a b e n /
      ((n : ℂ) + 1)) / 2)

Uses 3

Statement usesDarts of the square-lattice torus · Twisted bucket: walks avoiding a dart and its reverse · Turning phase \(\omega = e^{i\pi/4}\)

DefinitionAdding a dart and its reverse to the masked set#✓fully proved

Add a dart and its reverse to a set of masked darts.

def ons_addDartPair (L : ℕ) (forbidden : Finset (ons_Dart L))
    (e : ons_Dart L) : Finset (ons_Dart L) :=
  ({e, ons_dartRev L e} : Finset (ons_Dart L)) ∪ forbidden

Uses 2 · Used by 2

Statement usesDarts of the square-lattice torus · Reverse of a dart

Used byMasked darts after pairwise elimination along a list · Product of first-return factors along a dart elimination

DefinitionMasked darts after pairwise elimination along a list#✓fully proved

The set of masked darts after eliminating the darts of a list, pair by pair.

def ons_maskAfter (L : ℕ) (forbidden : Finset (ons_Dart L)) :
    List (ons_Dart L) → Finset (ons_Dart L)
  | [] => forbidden
  | e :: es => ons_maskAfter L (ons_addDartPair L forbidden e) es

Uses 2

Statement usesDarts of the square-lattice torus · Adding a dart and its reverse to the masked set

DefinitionProduct of first-return factors along a dart elimination#✓fully proved

The product of the factors 1 - λ_e along a list of darts, each first-return weight λ_e computed with the previously eliminated darts masked.

noncomputable def ons_maskEliminationProduct
    (L : ℕ) [NeZero L] (x : ℝ) (a b : Fin 2)
    (forbidden : Finset (ons_Dart L)) : List (ons_Dart L) → ℂ
  | [] => 1
  | e :: es =>
      (1 - ∑' s, ons_firstReturnWeight
        (ons_maskMatrix forbidden
          (ons_KWmatPhase L (x : ℂ) ons_turnRoot
            (ons_spinPhase L a) (ons_spinPhase L b)))
        e (ons_dartRev L e) s) *
      ons_maskEliminationProduct L x a b
        (ons_addDartPair L forbidden e) es

Uses 8

Statement usesDarts of the square-lattice torus · Twisted Kac-Ward matrix with direction phases · Adding a dart and its reverse to the masked set · Reverse of a dart · Weight of a first-return segment avoiding a state · Matrix with forbidden rows and columns set to zero · Boundary phase \(e^{i\pi a/L}\) · Turning phase \(\omega = e^{i\pi/4}\)

DefinitionMatrix bucket: walks through one state avoiding another#✓fully proved

The total weight of closed walks of length n + 1 of M that visit e but not r.

noncomputable def ons_matrixBucketE
    {E : Type*} [Fintype E] [DecidableEq E]
    (M : Matrix E E ℂ) (e r : E) (n : ℕ) : ℂ :=
  ∑ loop ∈ Finset.univ.filter
      (fun loop : Fin (n + 1) → E ↦
        (∃ i, loop i = e) ∧ ¬ ∃ j, loop j = r),
    ons_loopWeight M loop

Uses 1 · Used by 1

Statement usesWeight of a cyclic sequence

Used byOnsager's formula

DefinitionMatrix bucket: walks avoiding two given states#✓fully proved

The total weight of closed walks of length n + 1 of M that visit neither e nor r.

noncomputable def ons_matrixBucketN
    {E : Type*} [Fintype E] [DecidableEq E]
    (M : Matrix E E ℂ) (e r : E) (n : ℕ) : ℂ :=
  ∑ loop ∈ Finset.univ.filter
      (fun loop : Fin (n + 1) → E ↦
        ¬ (∃ i, loop i = e) ∧ ¬ ∃ j, loop j = r),
    ons_loopWeight M loop

Uses 1 · Used by 1

Statement usesWeight of a cyclic sequence

Used byOnsager's formula

53 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.