Homology and turning of loops on the square-lattice torus

DefinitionTotal displacement of a list of lattice directions#✓fully proved

The total displacement in ℤ² of a list of lattice directions.

def ons_pathDisplacement : List (Fin 4) → ℤ × ℤ
  | [] => 0
  | d :: ds => stepOf d + ons_pathDisplacement ds

Uses 1 · Used by 2

Statement usesUnit lattice step in a given direction

Used byLattice point of a period state · Onsager's formula

DefinitionLattice points visited by a path from the origin#✓fully proved

The lattice points visited by a path from the origin with the given directions.

def ons_pathVertices : List (Fin 4) → List (ℤ × ℤ)
  | [] => [0]
  | d :: ds => 0 :: (ons_pathVertices ds).map (stepOf d + ·)

Uses 1 · Used by 1

Statement usesUnit lattice step in a given direction

Used byOnsager's formula

DefinitionOpen turning sum of a direction list#✓fully proved

The total turning (in quarter turns) between consecutive directions of a list.

def ons_openTurnSum : List (Fin 4) → ℤ
  | [] => 0
  | [_] => 0
  | d :: e :: ds =>
      ons_turnPow d e + ons_openTurnSum (e :: ds)

Uses 1 · Used by 2

Statement usesInteger turn exponent between two directions

Used byCyclic turning sum of a direction list · Onsager's formula

DefinitionCyclic turning sum of a direction list#✓fully proved

The total turning of a direction list read cyclically, including the turn from the last direction back to the first.

def ons_cyclicTurnSum : List (Fin 4) → ℤ
  | [] => 0
  | d :: ds =>
      ons_openTurnSum (d :: ds) +
        ons_turnPow (d :: ds).getLast! d

Uses 2 · Used by 1

Statement usesOpen turning sum of a direction list · Integer turn exponent between two directions

Used byOnsager's formula

DefinitionOutside connector around the bounding box of a periodic arc#✓fully proved

A path east, north, west, south and east again that runs around the bounding box of a periodic arc with displacement (dx, dy) and height top.

def ons_outsideConnector (dx dy top : ℤ) : List (Fin 4) :=
  [0] ++
    List.replicate (top - dy).toNat 1 ++
    List.replicate (dx + 2).toNat 2 ++
    List.replicate top.toNat 3 ++ [0]

Used by 1

Used byOnsager's formula

DefinitionLattice points visited by the outside connector#✓fully proved

The lattice points visited by the outside connector.

def ons_outsideConnectorVertexList (dx dy top : ℤ) :
    List (ℤ × ℤ) :=
  [0] ++
    (List.range (top - dy).toNat).map
      (fun k ↦ (1, (k : ℤ))) ++
    (List.range (dx + 2).toNat).map
      (fun k ↦ (1 - (k : ℤ), top - dy)) ++
    (List.range top.toNat).map
      (fun k ↦ (-dx - 1, top - dy - (k : ℤ))) ++
    [(-dx - 1, -dy)]

Used by 1

Used byOnsager's formula

DefinitionStates of one period of a periodic walk#✓fully proved

The states (r, i) (period index r, position i) of one period of a periodic walk.

def ons_periodStateList (n r : ℕ) : List (ℕ × Fin n) :=
  List.ofFn (fun i : Fin n ↦ (r, i))

Used by 2

Used byStates of the first \(N + 1\) periods of a periodic walk · Onsager's formula

DefinitionStates of the first \(N + 1\) periods of a periodic walk#✓fully proved

The states of the first N periods of a periodic walk followed by the initial state of the next period.

def ons_allPeriodStates (n N : ℕ) : List (ℕ × Fin n) :=
  (List.range (N + 1)).flatMap (ons_periodStateList n)

Uses 1 · Used by 2

Statement usesStates of one period of a periodic walk

Used byStates of a periodic arc across \(N\) periods · Onsager's formula

DefinitionStates of a periodic arc across \(N\) periods#✓fully proved

The states of the periodic arc from position imin in the first period to position imax in period N.

def ons_periodicArcStates {n : ℕ} (N : ℕ)
    (imin imax : Fin n) : List (ℕ × Fin n) :=
  ((ons_allPeriodStates n N).drop imin.val).take
    (N * n + imax.val + 1 - imin.val)

Uses 1 · Used by 2

Statement usesStates of the first \(N + 1\) periods of a periodic walk

Used byDirections along a periodic arc · Onsager's formula

DefinitionLattice point of a period state#✓fully proved

The lattice point of the state (r, i): the i-th point of the lift shifted by r periods.

def ons_periodStateCoord {n : ℕ} [NeZero n]
    (d : Fin n → Fin 4) (z : ℕ × Fin n) : ℤ × ℤ :=
  pos d z.2 + z.1 • ons_pathDisplacement (List.ofFn d)

Uses 2 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Total displacement of a list of lattice directions

Used byOnsager's formula

DefinitionLast element of \(\{0, \ldots, n - 1\}\)#✓fully proved

The last element of Fin n.

def ons_lastFin (n : ℕ) [NeZero n] : Fin n :=
  ⟨n - 1, Nat.sub_lt (Nat.pos_of_ne_zero (NeZero.ne n)) (by omega)⟩

Used by 1

Used byOnsager's formula

DefinitionDirections along a periodic arc#✓fully proved

The directions along the periodic arc.

def ons_periodicArcDirections {n : ℕ}
    (d : Fin n → Fin 4) (N : ℕ) (imin imax : Fin n) :
    List (Fin 4) :=
  (ons_periodicArcStates N imin imax).dropLast.map
    (fun z ↦ d z.2)

Uses 1 · Used by 1

Statement usesStates of a periodic arc across \(N\) periods

Used byOnsager's formula

Definition\(N\) repetitions of a direction sequence#✓fully proved

N repetitions of the direction sequence.

def ons_directionPeriods {n : ℕ}
    (d : Fin n → Fin 4) (N : ℕ) : List (Fin 4) :=
  (List.range N).flatMap (fun _ ↦ List.ofFn d)

Used by 1

Used byOnsager's formula

DefinitionRotation of a lattice point by quarter turns#✓fully proved

Rotation of a lattice point by c quarter turns.

def ons_rotatePoint (c : Fin 4) (p : ℤ × ℤ) : ℤ × ℤ :=
  match c.val with
  | 0 => p
  | 1 => (-p.2, p.1)
  | 2 => (-p.1, -p.2)
  | _ => (p.2, -p.1)

Used by 1

Used byOnsager's formula

DefinitionReduction of a lattice site to the torus#✓fully proved

Reduction of a site of ℤ² to the torus ℤ_L × ℤ_L.

def ons_reduceSite (L : ℕ) (p : ℤ × ℤ) : ZMod L × ZMod L :=
  ((p.1 : ZMod L), (p.2 : ZMod L))

Used by 1

Used byOnsager's formula

DefinitionDirection sequence of the lift of a closed torus walk#✓fully proved

The direction sequence of a closed torus walk, read in the order of the lift to ℤ².

def ons_liftDir {L n : ℕ} [NeZero n] (v : Fin n → ons_Dart L) : Fin n → Fin 4 :=
  fun k => (v (-k)).2

Uses 1 · Used by 3

Statement usesDarts of the square-lattice torus

Used bySigned boundary coefficient along a torus loop · Points of the periodic lift of a torus loop · Onsager's formula

DefinitionSites of a closed torus walk in lift order#✓fully proved

The sites of a closed torus walk, in the order of the lift.

def ons_liftSite {L n : ℕ} [NeZero n]
    (v : Fin n → ons_Dart L) : Fin n → ZMod L × ZMod L :=
  fun k => (v (-k)).1

Uses 1 · Used by 3

Statement usesDarts of the square-lattice torus

Used byBase point in \(\mathbb{Z}^2\) over the start of a torus loop · Signed boundary coefficient along a torus loop · Onsager's formula

DefinitionIndicator bit of an edge in an edge set#✓fully proved

The indicator of e ∈ F in Fin 2.

def ons_edgeBit {V : Type*} [DecidableEq V]
    (F : Finset (Sym2 V)) (e : Sym2 V) : Fin 2 :=
  if e ∈ F then 1 else 0

Used by 3

Used byHorizontal edge bit of an edge set at a site · Vertical edge bit of an edge set at a site · Onsager's formula

DefinitionHorizontal edge bit of an edge set at a site#✓fully proved

Whether F contains the horizontal edge from p eastward.

def ons_horizontalBit {L : ℕ}
    (F : Finset (Sym2 (ZMod L × ZMod L)))
    (p : ZMod L × ZMod L) : Fin 2 :=
  ons_edgeBit F (ons_portEdge L (p, 0))

Uses 2 · Used by 3

Statement usesIndicator bit of an edge in an edge set · Torus edge underlying a dart

Used byMod 2 intersection number of two torus edge sets · Horizontal edge bit as an element of \(\mathbb{Z}/2\) · Onsager's formula

DefinitionVertical edge bit of an edge set at a site#✓fully proved

Whether F contains the vertical edge from p northward.

def ons_verticalBit {L : ℕ}
    (F : Finset (Sym2 (ZMod L × ZMod L)))
    (p : ZMod L × ZMod L) : Fin 2 :=
  ons_edgeBit F (ons_portEdge L (p, 1))

Uses 2 · Used by 3

Statement usesIndicator bit of an edge in an edge set · Torus edge underlying a dart

Used byMod 2 intersection number of two torus edge sets · Vertical edge bit as an element of \(\mathbb{Z}/2\) · Onsager's formula

DefinitionMod 2 intersection number of two torus edge sets#✓fully proved

The mod-2 intersection number of edge sets F and G on the torus.

noncomputable def ons_edgeCycleIntersection
    {L : ℕ} [NeZero L]
    (F G : Finset (Sym2 (ZMod L × ZMod L))) : Fin 2 :=
  ∑ p : ZMod L × ZMod L,
    (ons_horizontalBit F p *
        ons_verticalBit G (p.1, p.2 - 1) +
      ons_verticalBit F p *
        ons_horizontalBit G (p.1 - 1, p.2))

Uses 2 · Used by 1

Statement usesHorizontal edge bit of an edge set at a site · Vertical edge bit of an edge set at a site

Used byOnsager's formula

DefinitionHorizontal edge bit as an element of \(\mathbb{Z}/2\)#✓fully proved

The horizontal edge bit as an element of ZMod 2.

def ons_horizontalZBit {L : ℕ}
    (F : Finset (Sym2 (ZMod L × ZMod L)))
    (p : ZMod L × ZMod L) : ZMod 2 :=
  (ons_horizontalBit F p : ZMod 2)

Uses 1 · Used by 4

Statement usesHorizontal edge bit of an edge set at a site

Used byIntersection number of torus edge sets in the field \(\mathbb{Z}/2\) · Horizontal flux of an edge set through a column · Horizontal part of the zero-flux potential construction · Onsager's formula

DefinitionVertical edge bit as an element of \(\mathbb{Z}/2\)#✓fully proved

The vertical edge bit as an element of ZMod 2.

def ons_verticalZBit {L : ℕ}
    (F : Finset (Sym2 (ZMod L × ZMod L)))
    (p : ZMod L × ZMod L) : ZMod 2 :=
  (ons_verticalBit F p : ZMod 2)

Uses 1 · Used by 4

Statement usesVertical edge bit of an edge set at a site

Used byIntersection number of torus edge sets in the field \(\mathbb{Z}/2\) · Vertical flux of an edge set through a row · Vertical part of the zero-flux potential construction · Onsager's formula

DefinitionHorizontal flux of an edge set through a column#✓fully proved

The number mod 2 of horizontal edges of F leaving column x eastward.

noncomputable def ons_xFlux {L : ℕ} [NeZero L]
    (F : Finset (Sym2 (ZMod L × ZMod L))) (x : ZMod L) : ZMod 2 :=
  ∑ y : ZMod L, ons_horizontalZBit F (x, y)

Uses 1 · Used by 2

Statement usesHorizontal edge bit as an element of \(\mathbb{Z}/2\)

Used byHorizontal part of the zero-flux potential construction · Onsager's formula

DefinitionVertical flux of an edge set through a row#✓fully proved

The number mod 2 of vertical edges of F leaving row y northward.

noncomputable def ons_yFlux {L : ℕ} [NeZero L]
    (F : Finset (Sym2 (ZMod L × ZMod L))) (y : ZMod L) : ZMod 2 :=
  ∑ x : ZMod L, ons_verticalZBit F (x, y)

Uses 1 · Used by 2

Statement usesVertical edge bit as an element of \(\mathbb{Z}/2\)

Used byVertical part of the zero-flux potential construction · Onsager's formula

DefinitionVertical-seam edge in a given row#✓fully proved

The edge of the vertical seam in row y.

def ons_xSeamPortEdge (L : ℕ) (y : ZMod L) :
    Sym2 (ZMod L × ZMod L) :=
  ons_portEdge L (((-1 : ZMod L), y), 0)

Uses 1 · Used by 1

Statement usesTorus edge underlying a dart

Used byOnsager's formula

DefinitionHorizontal-seam edge in a given column#✓fully proved

The edge of the horizontal seam in column x.

def ons_ySeamPortEdge (L : ℕ) (x : ZMod L) :
    Sym2 (ZMod L × ZMod L) :=
  ons_portEdge L ((x, (-1 : ZMod L)), 1)

Uses 1 · Used by 1

Statement usesTorus edge underlying a dart

Used byOnsager's formula

DefinitionPrefix sum of a function on \(\mathbb{Z}/L\)#✓fully proved

The prefix sum ∑_{k < x} f k along ZMod L, using the representatives 0, …, L - 1.

noncomputable def ons_zmodPrefix
    {A : Type*} [AddCommMonoid A]
    {L : ℕ} [NeZero L] (f : ZMod L → A) (z : ZMod L) : A :=
  ∑ i ∈ Finset.range z.val, f ((i + 1 : ℕ) : ZMod L)

Used by 2

Used byFace potential of an even subgraph of zero homology · Onsager's formula

DefinitionHorizontal part of the zero-flux potential construction#✓fully proved

The horizontal part of the potential construction for an edge set of zero flux.

noncomputable def ons_zeroFluxHorizontal
    {L : ℕ} [NeZero L]
    (F : Finset (Sym2 (ZMod L × ZMod L)))
    (p : ZMod L × ZMod L) : ZMod 2 :=
  ons_horizontalZBit F p +
    if p.2 = 0 then ons_xFlux F (-1) else 0

Uses 2 · Used by 2

Statement usesHorizontal edge bit as an element of \(\mathbb{Z}/2\) · Horizontal flux of an edge set through a column

Used byFace potential of an even subgraph of zero homology · Onsager's formula

DefinitionVertical part of the zero-flux potential construction#✓fully proved

The vertical part of the potential construction for an edge set of zero flux.

noncomputable def ons_zeroFluxVertical
    {L : ℕ} [NeZero L]
    (F : Finset (Sym2 (ZMod L × ZMod L)))
    (p : ZMod L × ZMod L) : ZMod 2 :=
  ons_verticalZBit F p +
    if p.1 = 0 then ons_yFlux F (-1) else 0

Uses 2 · Used by 2

Statement usesVertical edge bit as an element of \(\mathbb{Z}/2\) · Vertical flux of an edge set through a row

Used byFace potential of an even subgraph of zero homology · Onsager's formula

DefinitionFace potential of an even subgraph of zero homology#✓fully proved

A face potential P whose boundary is a given even subgraph of zero homology.

noncomputable def ons_zeroFluxPotential
    {L : ℕ} [NeZero L]
    (F : Finset (Sym2 (ZMod L × ZMod L)))
    (p : ZMod L × ZMod L) : ZMod 2 :=
  ons_zmodPrefix (fun y ↦ ons_zeroFluxHorizontal F (0, y)) p.2 +
    ons_zmodPrefix (fun x ↦ ons_zeroFluxVertical F (x, p.2)) p.1

Uses 3 · Used by 1

Statement usesHorizontal part of the zero-flux potential construction · Vertical part of the zero-flux potential construction · Prefix sum of a function on \(\mathbb{Z}/L\)

Used byOnsager's formula

DefinitionIntersection number of torus edge sets in the field \(\mathbb{Z}/2\)#✓fully proved

The intersection number of two edge sets, valued in ZMod 2.

noncomputable def ons_edgeCycleZIntersection
    {L : ℕ} [NeZero L]
    (F G : Finset (Sym2 (ZMod L × ZMod L))) : ZMod 2 :=
  ∑ p : ZMod L × ZMod L,
    (ons_horizontalZBit F p *
        ons_verticalZBit G (p.1, p.2 - 1) +
      ons_verticalZBit F p *
        ons_horizontalZBit G (p.1 - 1, p.2))

Uses 2 · Used by 1

Statement usesHorizontal edge bit as an element of \(\mathbb{Z}/2\) · Vertical edge bit as an element of \(\mathbb{Z}/2\)

Used byOnsager's formula

DefinitionParity of an integer as a bit#✓fully proved

The parity of an integer as an element of Fin 2.

noncomputable def ons_intParity (m : ℤ) : Fin 2 :=
  if Even m then 0 else 1

Used by 2

Used byMod 2 homology class of a winding · Onsager's formula

DefinitionMod 2 homology class of a winding#✓fully proved

The homology class mod 2 of the winding (m₁, m₂).

noncomputable def ons_windingParity (mx my : ℤ) : Fin 2 × Fin 2 :=
  (ons_intParity mx, ons_intParity my)

Uses 1 · Used by 1

Statement usesParity of an integer as a bit

Used byOnsager's formula

DefinitionLinear character of the boundary phases#✓fully proved

The linear character (-1)^{a h₁ + b h₂} of the boundary phases on homology classes mod 2.

def ons_spinLinearCharacter (a b : Fin 2) (h : Fin 2 × Fin 2) : ℂ :=
  (-1 : ℂ) ^ (a.val * h.1.val + b.val * h.2.val)

Used by 1

Used byOnsager's formula

DefinitionCrossing of the vertical seam by a dart#✓fully proved

A dart crosses the vertical seam between the columns x = -1 and x = 0.

def ons_xWrap {L : ℕ} (d : ons_Dart L) : Prop :=
  (d.2 = 0 ∧ d.1.1 = -1) ∨ (d.2 = 2 ∧ d.1.1 = 0)

Uses 1 · Used by 1

Statement usesDarts of the square-lattice torus

Used byOnsager's formula

DefinitionCrossing of the horizontal seam by a dart#✓fully proved

A dart crosses the horizontal seam between the rows y = -1 and y = 0.

def ons_yWrap {L : ℕ} (d : ons_Dart L) : Prop :=
  (d.2 = 1 ∧ d.1.2 = -1) ∨ (d.2 = 3 ∧ d.1.2 = 0)

Uses 1 · Used by 1

Statement usesDarts of the square-lattice torus

Used byOnsager's formula

DefinitionSigned crossing of the vertical seam by a dart#✓fully proved

The signed crossing of the vertical seam by a dart: 1 eastward, -1 westward, 0 otherwise.

def ons_xWrapSign {L : ℕ} (d : ons_Dart L) : ℤ :=
  if d.2 = 0 ∧ d.1.1 = -1 then 1
  else if d.2 = 2 ∧ d.1.1 = 0 then -1 else 0

Uses 1 · Used by 2

Statement usesDarts of the square-lattice torus

Used byOnsager's formula · Seam sign of a dart

DefinitionSigned crossing of the horizontal seam by a dart#✓fully proved

The signed crossing of the horizontal seam by a dart: 1 northward, -1 southward, 0 otherwise.

def ons_yWrapSign {L : ℕ} (d : ons_Dart L) : ℤ :=
  if d.2 = 1 ∧ d.1.2 = -1 then 1
  else if d.2 = 3 ∧ d.1.2 = 0 then -1 else 0

Uses 1 · Used by 2

Statement usesDarts of the square-lattice torus

Used byOnsager's formula · Seam sign of a dart

DefinitionEdge set of a closed walk of darts#✓fully proved

The set of torus edges traversed by a closed walk of darts.

noncomputable def ons_dartEdgeSet {L n : ℕ}
    (d : Fin n → ons_Dart L) :
    Finset (Sym2 (ZMod L × ZMod L)) :=
  Finset.univ.image (fun k => ons_portEdge L (d k))

Uses 2 · Used by 1

Statement usesDarts of the square-lattice torus · Torus edge underlying a dart

Used byOnsager's formula

DefinitionTranslation of \(\mathbb{Z}^2\) for a winding around the torus#✓fully proved

The translation (L m₁, L m₂) of ℤ² corresponding to winding (m₁, m₂) around the torus.

def ons_windingTranslation (L : ℕ) (mx my : ℤ) : ℤ × ℤ :=
  ((L : ℤ) * mx, (L : ℤ) * my)

Used by 1

Used byOnsager's formula

DefinitionPoints of the periodic lift of a torus loop#✓fully proved

The i-th point of the r-th period of the lift of a torus loop with winding (m₁, m₂), relative to the starting point.

def ons_periodicLiftVertex {L n : ℕ} [NeZero n]
    (v : Fin n → ons_Dart L) (mx my r : ℤ) (i : Fin n) : ℤ × ℤ :=
  pos (ons_liftDir v) i +
    ((L : ℤ) * (r * mx), (L : ℤ) * (r * my))

Uses 3 · Used by 2

Statement usesVertices of a lattice walk from its step directions · Darts of the square-lattice torus · Direction sequence of the lift of a closed torus walk

Used byPeriodic lift anchored at the base point · Onsager's formula

DefinitionBase point in \(\mathbb{Z}^2\) over the start of a torus loop#✓fully proved

A base point in ℤ² over the starting site of a torus loop.

def ons_liftBase {L n : ℕ} [NeZero n]
    (v : Fin n → ons_Dart L) : ℤ × ℤ :=
  (((ons_liftSite v 0).1.val : ℤ),
    ((ons_liftSite v 0).2.val : ℤ))

Uses 2 · Used by 2

Statement usesDarts of the square-lattice torus · Sites of a closed torus walk in lift order

Used byPeriodic lift anchored at the base point · Onsager's formula

DefinitionPeriodic lift anchored at the base point#✓fully proved

The periodic lift translated to start at the base point over the starting site.

def ons_anchoredPeriodicLiftVertex {L n : ℕ} [NeZero n]
    (v : Fin n → ons_Dart L) (mx my r : ℤ) (i : Fin n) : ℤ × ℤ :=
  ons_liftBase v + ons_periodicLiftVertex v mx my r i

Uses 3 · Used by 1

Statement usesDarts of the square-lattice torus · Base point in \(\mathbb{Z}^2\) over the start of a torus loop · Points of the periodic lift of a torus loop

Used byOnsager's formula

DefinitionSigned potential difference across a horizontal edge#✓fully proved

The signed difference of a face potential across the horizontal edge at p.

def ons_signedHorizontalBoundary
    {L : ℕ} (P : (ZMod L × ZMod L) → ZMod 2)
    (p : ZMod L × ZMod L) : ℤ :=
  (P p).val - (P (p.1, p.2 - 1)).val

Used by 2

Used bySigned boundary coefficient on an outgoing edge · Onsager's formula

DefinitionSigned potential difference across a vertical edge#✓fully proved

The signed difference of a face potential across the vertical edge at p.

def ons_signedVerticalBoundary
    {L : ℕ} (P : (ZMod L × ZMod L) → ZMod 2)
    (p : ZMod L × ZMod L) : ℤ :=
  (P (p.1 - 1, p.2)).val - (P p).val

Used by 2

Used bySigned boundary coefficient on an outgoing edge · Onsager's formula

DefinitionSigned boundary coefficient on an outgoing edge#✓fully proved

The signed boundary coefficient of a potential on the edge leaving p in direction μ.

def ons_outgoingBoundaryCoeff
    {L : ℕ} (P : (ZMod L × ZMod L) → ZMod 2)
    (p : ZMod L × ZMod L) (mu : Fin 4) : ℤ :=
  match mu.val with
  | 0 => ons_signedHorizontalBoundary P p
  | 1 => ons_signedVerticalBoundary P p
  | 2 => -ons_signedHorizontalBoundary P (p.1 - 1, p.2)
  | _ => -ons_signedVerticalBoundary P (p.1, p.2 - 1)

Uses 2 · Used by 2

Statement usesSigned potential difference across a horizontal edge · Signed potential difference across a vertical edge

Used bySigned boundary coefficient along a torus loop · Onsager's formula

DefinitionSigned boundary coefficient along a torus loop#✓fully proved

The signed boundary coefficient on the k-th step of a torus loop.

def ons_loopBoundaryCoeff
    {L n : ℕ} [NeZero n]
    (P : (ZMod L × ZMod L) → ZMod 2)
    (v : Fin n → ons_Dart L) (k : Fin n) : ℤ :=
  ons_outgoingBoundaryCoeff P (ons_liftSite v k) (ons_liftDir v k)

Uses 4 · Used by 1

Statement usesDarts of the square-lattice torus · Direction sequence of the lift of a closed torus walk · Sites of a closed torus walk in lift order · Signed boundary coefficient on an outgoing edge

Used byOnsager's formula

DefinitionEdges crossing the vertical seam of the torus#✓fully proved

Edges of the torus crossing the vertical seam between the columns x = -1 and x = 0.

def ons_xSeamEdge (L : ℕ) (e : Sym2 (ZMod L × ZMod L)) : Prop :=
  ∃ y : ZMod L, e = s(((0 : ZMod L), y), (-1, y))

Used by 2

Used byMod 2 homology class of an edge set · Onsager's formula

DefinitionEdges crossing the horizontal seam of the torus#✓fully proved

Edges of the torus crossing the horizontal seam between the rows y = -1 and y = 0.

def ons_ySeamEdge (L : ℕ) (e : Sym2 (ZMod L × ZMod L)) : Prop :=
  ∃ x : ZMod L, e = s((x, (0 : ZMod L)), (x, -1))

Used by 2

Used byMod 2 homology class of an edge set · Onsager's formula

DefinitionMod 2 homology class of an edge set#✓fully proved

The homology class mod 2 of an edge set: the parities of its numbers of edges crossing the vertical and the horizontal seam.

noncomputable def ons_evenHomology (L : ℕ)
    (F : Finset (Sym2 (ZMod L × ZMod L))) : Fin 2 × Fin 2 :=
  by
    classical
    exact (⟨(F.filter (ons_xSeamEdge L)).card % 2, Nat.mod_lt _ (by decide)⟩,
      ⟨(F.filter (ons_ySeamEdge L)).card % 2, Nat.mod_lt _ (by decide)⟩)

Uses 2 · Used by 15

Statement usesEdges crossing the vertical seam of the torus · Edges crossing the horizontal seam of the torus

Used bySector weight of a homology class · Spin-character sum over even subgraphs of 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 · Edge-weighted root identity from the decorated-torus formal identity · Log-coefficient polynomial over the cycles of a decomposition · Decorated spin polynomial · Spin weight of a decorated even subgraph · Edge-weighted spin weight of a decorated even subgraph · Onsager's formula · Sector weight of a homology class as a polynomial · Edge-weighted spin-character sum over even subgraphs · Weighted character sum over even subgraphs containing an edge · Decorated character sum with weights on all edges

DefinitionSector weight of a homology class#✓fully proved

The sector weight Z_h(x) = ∑ x^|F| over even subgraphs F of the torus with homology class h.

noncomputable def ons_sectorWeight (L : ℕ) [Fact (2 < L)] (x : ℝ) (h : Fin 2 × Fin 2) : ℝ :=
  ∑ F ∈ evenSubgraphs (onsTorusGraph L) with ons_evenHomology L F = h, x ^ F.card

Uses 4 · Used by 8

Statement usesEven subgraphs of a graph · Nearest-neighbor adjacency on the discrete torus · The \(L \times L\) square-lattice torus graph · Mod 2 homology class of an edge set

Used bySector weight of the trivial homology class · Sector weight of the homology class \((0, 1)\) · Sector weight of the homology class \((1, 0)\) · Sector weight of the homology class \((1, 1)\) · 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

DefinitionSector weight of the trivial homology class#✓fully proved

The sector weight of the trivial homology class.

noncomputable def ons_sector00 (L : ℕ) [Fact (2 < L)] (x : ℝ) : ℝ :=
  ons_sectorWeight L x (0, 0)

Uses 1 · Used by 6

Statement usesSector weight of a homology class

Used bySigned 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}\) · Onsager's formula from the spin Kac-Ward identities · Onsager's formula

DefinitionSector weight of the homology class \((1, 0)\)#✓fully proved

The sector weight of the homology class (1, 0).

noncomputable def ons_sector10 (L : ℕ) [Fact (2 < L)] (x : ℝ) : ℝ :=
  ons_sectorWeight L x (1, 0)

Uses 1 · Used by 6

Statement usesSector weight of a homology class

Used bySigned 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}\) · Onsager's formula from the spin Kac-Ward identities · Onsager's formula

DefinitionSector weight of the homology class \((0, 1)\)#✓fully proved

The sector weight of the homology class (0, 1).

noncomputable def ons_sector01 (L : ℕ) [Fact (2 < L)] (x : ℝ) : ℝ :=
  ons_sectorWeight L x (0, 1)

Uses 1 · Used by 6

Statement usesSector weight of a homology class

Used bySigned 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}\) · Onsager's formula from the spin Kac-Ward identities · Onsager's formula

DefinitionSector weight of the homology class \((1, 1)\)#✓fully proved

The sector weight of the homology class (1, 1).

noncomputable def ons_sector11 (L : ℕ) [Fact (2 < L)] (x : ℝ) : ℝ :=
  ons_sectorWeight L x (1, 1)

Uses 1 · Used by 6

Statement usesSector weight of a homology class

Used bySigned 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}\) · Onsager's formula from the spin Kac-Ward identities · Onsager's formula

DefinitionSigned sector sum \(Z_{00} + Z_{10} + Z_{01} - Z_{11}\)#✓fully proved

The signed sector sum Z₀₀ + Z₁₀ + Z₀₁ - Z₁₁.

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

Uses 4 · Used by 7

Statement usesSector weight of the trivial homology class · Sector weight of the homology class \((0, 1)\) · Sector weight of the homology class \((1, 0)\) · Sector weight of the homology class \((1, 1)\)

Used bySpin Kac-Ward identities at inverse temperature \(\beta\) · Spin Kac-Ward identities via twisted Kac-Ward determinants · 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 · Four spin Kac-Ward identities on the torus at activity \(x\)

DefinitionSigned sector sum \(Z_{00} - Z_{10} + Z_{01} + Z_{11}\)#✓fully proved

The signed sector sum Z₀₀ - Z₁₀ + Z₀₁ + Z₁₁.

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

Uses 4 · Used by 7

Statement usesSector weight of the trivial homology class · Sector weight of the homology class \((0, 1)\) · Sector weight of the homology class \((1, 0)\) · Sector weight of the homology class \((1, 1)\)

Used bySpin Kac-Ward identities at inverse temperature \(\beta\) · Spin Kac-Ward identities via twisted Kac-Ward determinants · 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 · Four spin Kac-Ward identities on the torus at activity \(x\)

DefinitionSigned sector sum \(Z_{00} + Z_{10} - Z_{01} + Z_{11}\)#✓fully proved

The signed sector sum Z₀₀ + Z₁₀ - Z₀₁ + Z₁₁.

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

Uses 4 · Used by 7

Statement usesSector weight of the trivial homology class · Sector weight of the homology class \((0, 1)\) · Sector weight of the homology class \((1, 0)\) · Sector weight of the homology class \((1, 1)\)

Used bySpin Kac-Ward identities at inverse temperature \(\beta\) · Spin Kac-Ward identities via twisted Kac-Ward determinants · 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 · Four spin Kac-Ward identities on the torus at activity \(x\)

DefinitionSigned sector sum \(Z_{00} - Z_{10} - Z_{01} - Z_{11}\)#✓fully proved

The signed sector sum Z₀₀ - Z₁₀ - Z₀₁ - Z₁₁.

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

Uses 4 · Used by 7

Statement usesSector weight of the trivial homology class · Sector weight of the homology class \((0, 1)\) · Sector weight of the homology class \((1, 0)\) · Sector weight of the homology class \((1, 1)\)

Used bySpin Kac-Ward identities at inverse temperature \(\beta\) · Spin Kac-Ward identities via twisted Kac-Ward determinants · 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 · Four spin Kac-Ward identities on the torus at activity \(x\)

DefinitionSpin-structure character of a mod 2 homology class#✓fully proved

The spin-structure character (-1)^{(1 + a) h₁ + (1 + b) h₂ + h₁ h₂} of a homology class h mod 2, for boundary phases a, b.

def ons_spinCharacter (a b : Fin 2) (h : Fin 2 × Fin 2) : ℝ :=
  (-1 : ℝ) ^ ((1 + a.val) * h.1.val + (1 + b.val) * h.2.val +
    h.1.val * h.2.val)

Used by 12

Used bySpin-character sum over even subgraphs of the torus · 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 · Log-coefficient polynomial over the cycles of a decomposition · Decorated spin polynomial · Spin weight of a decorated even subgraph · Edge-weighted spin weight of a decorated even subgraph · Onsager's formula · Edge-weighted spin-character sum over even subgraphs · Weighted character sum over even subgraphs containing an edge · Decorated character sum with weights on all edges

DefinitionIntersection form on the mod 2 homology of the torus#✓fully proved

The intersection form h₁ k₂ + h₂ k₁ on H₁(T², ℤ/2) = (ℤ/2)².

def ons_homologyIntersection (h k : Fin 2 × Fin 2) : Fin 2 :=
  h.1 * k.2 + h.2 * k.1

Used by 1

Used byOnsager's formula

DefinitionSpin-character sum over even subgraphs of the torus#✓fully proved

The even-subgraph sum of the torus with each subgraph weighted by the spin character of its homology class.

noncomputable def ons_spinCharacterSum (L : ℕ) [Fact (2 < L)]
    (x : ℝ) (a b : Fin 2) : ℝ :=
  ∑ F ∈ evenSubgraphs (onsTorusGraph L),
    ons_spinCharacter a b (ons_evenHomology L F) * x ^ F.card

Uses 5 · Used by 4

Statement usesEven subgraphs of a graph · Nearest-neighbor adjacency on the discrete torus · The \(L \times L\) square-lattice torus graph · Mod 2 homology class of an edge set · Spin-structure character of a mod 2 homology class

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Spin Kac-Ward identities from the edge-weighted root identity · Onsager's formula · Spin-character sums squared as twisted determinants at activity \(x\)

63 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.