Trivalent decoration of the torus

DefinitionSpin boundary-phase gauge at a site#✓fully proved

The gauge u^{s₁} v^{s₂} at site s, with u, v the spin boundary phases.

noncomputable def ons_spinVertexGauge
    (L : ℕ) (a b : Fin 2) (site : ZMod L × ZMod L) : ℂ :=
  ons_spinPhase L a ^ (site.1.val : ℤ) *
    ons_spinPhase L b ^ (site.2.val : ℤ)

Uses 1 · Used by 2

Statement usesBoundary phase \(e^{i\pi a/L}\)

Used byOnsager's formula · Gauge on the states of the augmented matrix

DefinitionSeam sign of a dart#✓fully proved

The seam sign (-1)^{a · (signed vertical seam crossing) + b · (signed horizontal seam crossing)} of a dart.

noncomputable def ons_spinDartSeamSign
    {L : ℕ} (a b : Fin 2) (d : ons_Dart L) : ℂ :=
  (-1 : ℂ) ^ ((a.val : ℤ) * ons_xWrapSign d +
    (b.val : ℤ) * ons_yWrapSign d)

Uses 3 · Used by 2

Statement usesDarts of the square-lattice torus · Signed crossing of the vertical seam by a dart · Signed crossing of the horizontal seam by a dart

Used byOnsager's formula · Decorated weights twisted by seam signs

DefinitionDecorated weights twisted by seam signs#✓fully proved

Decorated weights with every external edge multiplied by the seam sign of its dart.

noncomputable def ons_spinSeamDecWeight
    {L : ℕ} (decWeight : ons_DecEdge L → ℂ)
    (a b : Fin 2) (edge : ons_DecEdge L) : ℂ := by
  classical
  exact if h : ons_decIsExternal edge then
    ons_spinDartSeamSign a b (Classical.choose h) * decWeight edge
  else decWeight edge

Uses 5 · Used by 1

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Reverse of a dart · Externality of a decorated edge · Seam sign of a dart

Used byOnsager's formula

DefinitionDiagonal gauge conjugation of a matrix#✓fully proved

Diagonal conjugation gauge i * M i j * (gauge j)⁻¹.

noncomputable def ons_diagonalGaugeMatrix
    {E : Type*} (gauge : E → ℂ) (M : Matrix E E ℂ) :
    Matrix E E ℂ :=
  fun i j ↦ gauge i * M i j * (gauge j)⁻¹

Used by 1

Used byOnsager's formula

DefinitionGauge on the states of the augmented matrix#✓fully proved

The gauge on the states of the augmented matrix: the site gauge on darts, and the gauge of site on the two side states.

noncomputable def ons_decMiddleStateGauge
    (L : ℕ) (a b : Fin 2) (site : ZMod L × ZMod L) :
    ons_Dart L ⊕ Fin 2 → ℂ
  | .inl d => ons_spinVertexGauge L a b d.1
  | .inr _ => ons_spinVertexGauge L a b site

Uses 2

Statement usesDarts of the square-lattice torus · Spin boundary-phase gauge at a site

DefinitionInternal adjacency of the torus decoration#✓fully proved

Internal adjacency of the decoration: two darts at the same site whose directions are consecutive in 0, 1, 2, 3.

def ons_decInternalAdj {L : ℕ} (d e : ons_Dart L) : Prop :=
  d.1 = e.1 ∧ (d.2.val + 1 = e.2.val ∨ e.2.val + 1 = d.2.val)

Uses 1 · Used by 22

Statement usesDarts of the square-lattice torus

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · One-edge decorated walk along an external edge · 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 · Decorated spin polynomial · Onsager's formula · Torus even subgraph of a decorated even subgraph · Adjacency of the decorated torus graph · Four-step route of a decorated edge in the finer torus · Decorated graph of the torus · Internal path between two ports at a site · Internal walk between two ports at a site · Decorated walk of a Kac-Ward transition · Even decorated subgraph determined by a port pattern · Decorated character sum with weights on all edges · Equivalence between even decorated subgraphs and port patterns · Equivalence between even subgraphs of the torus and its decoration · Port pattern of an even decorated subgraph

DefinitionAdjacency of the decorated torus graph#✓fully proved

Adjacency of the decorated graph: a dart is joined to its reverse and to its internal neighbors.

def ons_decAdj (L : ℕ) (d e : ons_Dart L) : Prop :=
  e = ons_dartRev L d ∨ ons_decInternalAdj d e

Uses 3 · Used by 17

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

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · 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 · Decorated spin polynomial · Onsager's formula · Torus even subgraph of a decorated even subgraph · Four-step route of a decorated edge in the finer torus · Decorated graph of the torus · Even decorated subgraph determined by a port pattern · Decorated character sum with weights on all edges · Equivalence between even decorated subgraphs and port patterns · Equivalence between even subgraphs of the torus and its decoration · Port pattern of an even decorated subgraph

DefinitionDecorated graph of the torus#✓fully proved

The decorated graph of the torus: vertices are darts, external edges join each dart to its reverse, and internal edges form the path (s, 0) - (s, 1) - (s, 2) - (s, 3) at each site s.

def ons_decGraph (L : ℕ) : SimpleGraph (ons_Dart L) where
  Adj := ons_decAdj L
  symm := ⟨fun _ _ h => ons_decAdj_symm L h⟩
  loopless := by
    refine ⟨?_⟩
    intro d hd
    rcases hd with hrev | hint
    · exact ons_dartRev_ne_self L d hrev.symm
    · rcases hint.2 with h | h <;> omega

Uses 5 · Used by 39

Statement usesDarts of the square-lattice torus · Reverse of a dart · Adjacency of the decorated torus graph · Internal adjacency of the torus decoration · Neighbouring site in a given direction on the torus

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Log-coefficient polynomial over the cycles of a decomposition · One-edge decorated walk along an external edge · 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 · Decorated spin polynomial · Onsager's formula · Torus even subgraph of a decorated even subgraph · External edges used by a decorated walk · Torus edges underlying a decorated walk · 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 · Four-step route of a decorated edge in the finer 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 · Closed decorated walk of a valid Kac-Ward loop · Internal path between two ports at a site · Internal walk between two ports at a site · Decorated walk 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 · Even decorated subgraph determined by a port pattern · Decorated character sum with weights on all edges · Equivalence between even decorated subgraphs and port patterns · Equivalence between even subgraphs of the torus and its decoration · Port pattern of an even decorated subgraph · Directions of the expanded dart list of a decorated walk · Directions of the external darts of a decorated walk

DefinitionInternal neighbors of a dart in the decoration#✓fully proved

The internal neighbors of a dart in the path at its site.

def ons_decInternalNeighbors {L : ℕ} (d : ons_Dart L) : Finset (ons_Dart L) :=
  match d.2 with
  | 0 => {(d.1, 1)}
  | 1 => {(d.1, 0), (d.1, 2)}
  | 2 => {(d.1, 1), (d.1, 3)}
  | 3 => {(d.1, 2)}

Uses 1 · Used by 4

Statement usesDarts of the square-lattice torus

Used byChosen split of a decorated even subgraph at an external edge · Onsager's formula · Equivalence between even decorated subgraphs and port patterns · Port pattern of an even decorated subgraph

DefinitionInternal-edge bits completing port bits at a site#✓fully proved

The internal-edge bits (b₀, b₀ + b₁, b₀ + b₁ + b₂) that complete port bits b₀, …, b₃ at one site to an even subgraph.

def ons_decChainCompletion (b0 b1 b2 : Fin 2) : Fin 3 → Fin 2 :=
  ![b0, b0 + b1, b0 + b1 + b2]

Used by 2

Used byEquivalence between even decorated subgraphs and port patterns · Internal-edge bits at a site from a port pattern

DefinitionParity condition of the decoration at one site#✓fully proved

Parity of the decorated subgraph at the four darts of one site, for port bits b₀, …, b₃ and internal-edge bits y.

def ons_decChainEven (b0 b1 b2 b3 : Fin 2) (y : Fin 3 → Fin 2) : Prop :=
  b0 + y 0 = 0 ∧
  b1 + y 0 + y 1 = 0 ∧
  b2 + y 1 + y 2 = 0 ∧
  b3 + y 2 = 0

Used by 2

Used byEquivalence between even decorated subgraphs and port patterns · Port pattern of an even decorated subgraph

StructurePort pattern on the darts of the torus#✓fully proved

A port pattern: one bit per dart, equal on a dart and its reverse, with an even number of ones at each site. Port patterns encode even subgraphs of the torus.

structure ons_PortPattern (L : ℕ) where
  bit : ons_Dart L → Fin 2
  rev_bit : ∀ d, bit (ons_dartRev L d) = bit d
  site_even : ∀ s : ZMod L × ZMod L,
    bit (s, 0) + bit (s, 1) + bit (s, 2) + bit (s, 3) = 0

Uses 2 · Used by 13

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

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Onsager's formula · Port-pattern bit of an unordered decorated edge · Port-pattern bit of the decorated edge between two darts · Even decorated subgraph determined by a port pattern · 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 · Internal-edge bits at a site from a port pattern · Torus edge set of a port pattern · Port pattern of an even decorated subgraph

DefinitionInternal-edge bits at a site from a port pattern#✓fully proved

The internal-edge bits at a site determined by a port pattern.

def ons_portChainBit {L : ℕ} (P : ons_PortPattern L)
    (s : ZMod L × ZMod L) : Fin 3 → Fin 2 :=
  ons_decChainCompletion (P.bit (s, 0)) (P.bit (s, 1)) (P.bit (s, 2))

Uses 3 · Used by 3

Statement usesDarts of the square-lattice torus · Port pattern on the darts of the torus · Internal-edge bits completing port bits at a site

Used byPort-pattern bit of an unordered decorated edge · Port-pattern bit of the decorated edge between two darts · Equivalence between even decorated subgraphs and port patterns

DefinitionPort-pattern bit of the decorated edge between two darts#✓fully proved

The bit of the decorated edge between d and e determined by a port pattern.

def ons_decNeighborBit {L : ℕ} (P : ons_PortPattern L)
    (d e : ons_Dart L) : Fin 2 :=
  if e = ons_dartRev L d then P.bit d else
    if d.1 = e.1 then
      match d.2, e.2 with
      | 0, 1 | 1, 0 => ons_portChainBit P d.1 0
      | 1, 2 | 2, 1 => ons_portChainBit P d.1 1
      | 2, 3 | 3, 2 => ons_portChainBit P d.1 2
      | _, _ => 0
    else 0

Uses 4 · Used by 2

Statement usesDarts of the square-lattice torus · Port pattern on the darts of the torus · Reverse of a dart · Internal-edge bits at a site from a port pattern

Used byPort-pattern bit of an unordered decorated edge · Equivalence between even decorated subgraphs and port patterns

DefinitionPort-pattern bit of an unordered decorated edge#✓fully proved

The bit of a decorated edge determined by a port pattern.

def ons_decEdgeBit {L : ℕ} (P : ons_PortPattern L) :
    Sym2 (ons_Dart L) → Fin 2 :=
  Sym2.lift ⟨ons_decNeighborBit P, ons_decNeighborBit_symm P⟩

Uses 6 · Used by 2

Statement usesDarts of the square-lattice torus · Port pattern on the darts of the torus · Reverse of a dart · Port-pattern bit of the decorated edge between two darts · Neighbouring site in a given direction on the torus · Internal-edge bits at a site from a port pattern

Used byEven decorated subgraph determined by a port pattern · Equivalence between even decorated subgraphs and port patterns

DefinitionEven decorated subgraph determined by a port pattern#✓fully proved

The even subgraph of the decorated graph determined by a port pattern.

noncomputable def ons_decoratedEdges {L : ℕ} [NeZero L]
    (P : ons_PortPattern L) : Finset (Sym2 (ons_Dart L)) :=
  (ons_decGraph L).edgeFinset.filter (fun e => ons_decEdgeBit P e = 1)

Uses 7 · Used by 1

Statement usesDarts of the square-lattice torus · Port pattern on the darts of the torus · Reverse of a dart · Adjacency of the decorated torus graph · Port-pattern bit of an unordered decorated edge · Decorated graph of the torus · Internal adjacency of the torus decoration

Used byEquivalence between even decorated subgraphs and port patterns

DefinitionTorus edge underlying a dart#✓fully proved

The torus edge underlying a dart.

def ons_portEdge (L : ℕ) (d : ons_Dart L) : Sym2 (ZMod L × ZMod L) :=
  s(d.1, ons_dirStep L d.2 d.1)

Uses 2 · Used by 15

Statement usesDarts of the square-lattice torus · Neighbouring site in a given direction on the torus

Used byEdge set of a closed walk of darts · Horizontal edge bit of an edge set at a site · Vertical edge bit of an edge set at a site · Vertical-seam edge in a given row · Horizontal-seam edge in a given column · 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 · Onsager's formula · Edge coefficient identity on the \(L \times L\) torus · Equivalence between even torus subgraphs and port patterns · Port pattern of an even subgraph of the torus · Port bit of a dart for a torus edge set · Torus edge set of a port pattern

DefinitionPort bit of a dart for a torus edge set#✓fully proved

The bit of a dart in the port pattern of an edge set F: 1 if its underlying torus edge lies in F.

def ons_portBit {L : ℕ} (F : Finset (Sym2 (ZMod L × ZMod L)))
    (d : ons_Dart L) : Fin 2 :=
  if ons_portEdge L d ∈ F then 1 else 0

Uses 2 · Used by 1

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

Used byPort pattern of an even subgraph of the torus

DefinitionPort pattern of an even subgraph of the torus#✓fully proved

The port pattern of an even subgraph of the torus.

StatMech.Onsager.ons_evenSubgraphPortPattern · 29 lines

noncomputable def ons_evenSubgraphPortPattern (L : ℕ) [Fact (2 < L)]
    (F : Finset (Sym2 (ZMod L × ZMod L)))
    (hF : F ∈ evenSubgraphs (onsTorusGraph L)) : ons_PortPattern L where
  bit := ons_portBit F
  rev_bit := by
    intro d
    simp only [ons_portBit, ons_portEdge_rev]
  site_even := by
    intro v
    have hdata := hF
    rw [evenSubgraphs, Finset.mem_filter, Finset.mem_powerset] at hdata
    have hFeq : F = (onsTorusGraph L).edgeFinset.filter (fun e => e ∈ F) := by
      ext e
      simp only [Finset.mem_filter]
      constructor
      · intro he
        exact ⟨hdata.1 he, he⟩
      · exact And.right
    have hcast : ((incCount F v : ℕ) : ZMod 2) = 0 := by
      apply (CharP.cast_eq_zero_iff (ZMod 2) 2 _).mpr
      exact even_iff_two_dvd.mp (hdata.2 v)
    have hsum := ons_cast_incCount_filter_eq_neighbor_sum
      (onsTorusGraph L) (fun e => e ∈ F) v
    rw [← hFeq, hcast] at hsum
    rw [ons_torus_neighbor_sum_eq_direction_sum] at hsum
    simp only [ons_portBit]
    replace hsum := hsum.symm
    simp only [ons_portEdge, Fin.sum_univ_four, add_assoc] at hsum ⊢
    exact hsum

Uses 11 · Used by 1

Statement usesEven subgraph condition on an edge set · Even subgraphs of a graph · Number of edges of an edge set incident to a vertex · Nearest-neighbor adjacency on the discrete torus · The \(L \times L\) square-lattice torus graph · Darts of the square-lattice torus · Port pattern on the darts of the torus · Reverse of a dart · Neighbouring site in a given direction on the torus · Port bit of a dart for a torus edge set · Torus edge underlying a dart

Used byEquivalence between even torus subgraphs and port patterns

DefinitionPort bit of a dart in a decorated edge set#✓fully proved

The port bit of a dart in a decorated edge set: whether the external edge at the dart is present.

def ons_decoratedPortBit {L : ℕ}
    (D : Finset (Sym2 (ons_Dart L))) (d : ons_Dart L) : Fin 2 :=
  if s(d, ons_dartRev L d) ∈ D then 1 else 0

Uses 2 · Used by 5

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

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Onsager's formula · Equivalence between even decorated subgraphs and port patterns · Port pattern of an even decorated subgraph

DefinitionInternal-edge bits of a decorated edge set at a site#✓fully proved

The three internal-edge bits of a decorated edge set at one site.

def ons_decoratedChainBits {L : ℕ}
    (D : Finset (Sym2 (ons_Dart L))) (s : ZMod L × ZMod L) :
    Fin 3 → Fin 2 :=
  ![if s((s, 0), (s, 1)) ∈ D then 1 else 0,
    if s((s, 1), (s, 2)) ∈ D then 1 else 0,
    if s((s, 2), (s, 3)) ∈ D then 1 else 0]

Uses 1 · Used by 2

Statement usesDarts of the square-lattice torus

Used byEquivalence between even decorated subgraphs and port patterns · Port pattern of an even decorated subgraph

DefinitionPort pattern of an even decorated subgraph#✓fully proved

The port pattern of an even subgraph of the decorated graph.

StatMech.Onsager.ons_portPatternOfDecorated · 16 lines

noncomputable def ons_portPatternOfDecorated (L : ℕ) [Fact (2 < L)]
    (D : Finset (Sym2 (ons_Dart L)))
    (hD : D ∈ evenSubgraphs (ons_decGraph L)) : ons_PortPattern L where
  bit := ons_decoratedPortBit D
  rev_bit := by
    intro d
    have hinv : ons_dartRev L (ons_dartRev L d) = d :=
      ons_dartRev_involutive L d
    have hedge : s(ons_dartRev L d, ons_dartRev L (ons_dartRev L d)) =
        s(d, ons_dartRev L d) := by
      rw [hinv]
      exact Sym2.eq_swap
    simp only [ons_decoratedPortBit, hedge]
  site_even := by
    intro s
    exact ons_decChainEven_port_even (ons_decorated_local_even L D hD s)

Uses 14 · Used by 4

Statement usesEven subgraph condition on an edge set · Even subgraphs of a graph · Number of edges of an edge set incident to a vertex · Darts of the square-lattice torus · Port pattern on the darts of the torus · Reverse of a dart · Adjacency of the decorated torus graph · Parity condition of the decoration at one site · Decorated graph of the torus · Internal adjacency of the torus decoration · Internal neighbors of a dart in the decoration · Internal-edge bits of a decorated edge set at a site · Port bit of a dart in a decorated edge set · Neighbouring site in a given direction on the torus

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Onsager's formula · Equivalence between even decorated subgraphs and port patterns

DefinitionTorus edge set of a port pattern#✓fully proved

The torus edge set of a port pattern.

noncomputable def ons_portPatternEdges (L : ℕ) [NeZero L]
    (P : ons_PortPattern L) :
    Finset (Sym2 (ZMod L × ZMod L)) :=
  (Finset.univ.filter (fun d : ons_Dart L => P.bit d = 1)).image
    (ons_portEdge L)

Uses 3 · Used by 4

Statement usesDarts of the square-lattice torus · Port pattern on the darts of the torus · Torus edge underlying a dart

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Onsager's formula · Equivalence between even torus subgraphs and port patterns

DefinitionEquivalence between even torus subgraphs and port patterns#✓fully proved

Even subgraphs of the torus are equivalent to port patterns.

noncomputable def ons_evenSubgraphPortEquiv (L : ℕ) [Fact (2 < L)] :
    {F : Finset (Sym2 (ZMod L × ZMod L)) //
      F ∈ evenSubgraphs (onsTorusGraph L)} ≃ ons_PortPattern L where
  toFun F := ons_evenSubgraphPortPattern L F.1 F.2
  invFun P := ⟨ons_portPatternEdges L P, ons_portPatternEdges_even L P⟩
  left_inv F := Subtype.ext (ons_portPatternEdges_evenSubgraphPortPattern L F.1 F.2)
  right_inv P := ons_evenSubgraphPortPattern_portPatternEdges L P

Uses 12 · Used by 1

Statement usesEven subgraph condition on an edge set · Even subgraphs of a graph · Number of edges of an edge set incident to a vertex · Nearest-neighbor adjacency on the discrete torus · The \(L \times L\) square-lattice torus graph · Darts of the square-lattice torus · Port pattern on the darts of the torus · Reverse of a dart · Neighbouring site in a given direction on the torus · Port pattern of an even subgraph of the torus · Torus edge underlying a dart · Torus edge set of a port pattern

Used byEquivalence between even subgraphs of the torus and its decoration

DefinitionEquivalence between even decorated subgraphs and port patterns#✓fully proved

Even subgraphs of the decorated graph are equivalent to port patterns.

noncomputable def ons_decoratedPortEquiv (L : ℕ) [Fact (2 < L)] :
    {D : Finset (Sym2 (ons_Dart L)) //
      D ∈ evenSubgraphs (ons_decGraph L)} ≃ ons_PortPattern L where
  toFun D := ons_portPatternOfDecorated L D.1 D.2
  invFun P := ⟨ons_decoratedEdges P, ons_decoratedEdges_even L P⟩
  left_inv D := Subtype.ext (ons_decoratedEdges_portPatternOfDecorated L D.1 D.2)
  right_inv P := ons_portPatternOfDecorated_decoratedEdges L P

Uses 20 · Used by 1

Statement usesEven subgraph condition on an edge set · Even subgraphs of a graph · Number of edges of an edge set incident to a vertex · Darts of the square-lattice torus · Port pattern on the darts of the torus · Reverse of a dart · Adjacency of the decorated torus graph · Internal-edge bits completing port bits at a site · Parity condition of the decoration at one site · Port-pattern bit of an unordered decorated edge · Decorated graph of the torus · Internal adjacency of the torus decoration · Internal neighbors of a dart in the decoration · Port-pattern bit of the decorated edge between two darts · Internal-edge bits of a decorated edge set at a site · Even decorated subgraph determined by a port pattern · Port bit of a dart in a decorated edge set · Neighbouring site in a given direction on the torus · Internal-edge bits at a site from a port pattern · Port pattern of an even decorated subgraph

Used byEquivalence between even subgraphs of the torus and its decoration

DefinitionEquivalence between even subgraphs of the torus and its decoration#✓fully proved

Even subgraphs of the torus are equivalent to even subgraphs of the decorated graph.

noncomputable def ons_decorationEquiv (L : ℕ) [Fact (2 < L)] :
    {F : Finset (Sym2 (ZMod L × ZMod L)) //
      F ∈ evenSubgraphs (onsTorusGraph L)} ≃
    {D : Finset (Sym2 (ons_Dart L)) //
      D ∈ evenSubgraphs (ons_decGraph L)} :=
  (ons_evenSubgraphPortEquiv L).trans (ons_decoratedPortEquiv L).symm

Uses 11 · Used by 4

Statement usesEven subgraphs of a graph · Nearest-neighbor adjacency on the discrete torus · The \(L \times L\) square-lattice torus graph · Darts of the square-lattice torus · Port pattern on the darts of the torus · Reverse of a dart · Adjacency of the decorated torus graph · Decorated graph of the torus · Internal adjacency of the torus decoration · Equivalence between even decorated subgraphs and port patterns · Equivalence between even torus subgraphs and port patterns

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Onsager's formula · Torus even subgraph of a decorated even subgraph

DefinitionOffset of a dart inside its 8 × 8 cell#✓fully proved

The offset of a dart in direction μ inside its 8 × 8 cell: east (6, 4), north (4, 6), west (2, 4), south (4, 2).

def ons_decEmbedOffset (mu : Fin 4) : ℕ × ℕ :=
  match mu with
  | 0 => (6, 4)
  | 1 => (4, 6)
  | 2 => (2, 4)
  | 3 => (4, 2)

Used by 3

Used byOnsager's formula · Four-step route of a decorated edge in the finer torus · Position of a dart in the 8L × 8L torus

DefinitionPosition of a dart in the 8L × 8L torus#✓fully proved

The position 8 s + offset(μ) of the dart (s, μ) in the 8L × 8L torus.

def ons_decEmbedVertex (L : ℕ) (d : ons_Dart L) :
    ZMod (8 * L) × ZMod (8 * L) :=
  ((8 * d.1.1.val + (ons_decEmbedOffset d.2).1 : ℕ),
    (8 * d.1.2.val + (ons_decEmbedOffset d.2).2 : ℕ))

Uses 2 · Used by 7

Statement usesDarts of the square-lattice torus · Offset of a dart inside its 8 × 8 cell

Used byOnsager's formula · Route points of a decorated edge after its start · 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 · Image of a decorated walk in the finer torus · First dart of the expanded dart list of a decorated cycle

DefinitionStep directions of the route of a decorated edge#✓fully proved

The four step directions of the route of the decorated edge from d to e: straight for an external edge, an L-shaped turn for an internal edge.

def ons_decEdgeRouteDirs (L : ℕ) (d e : ons_Dart L) : Fin 4 → Fin 4 :=
  if e = ons_dartRev L d then fun _ => d.2
  else
    match d.2, e.2 with
    | 0, 1 => ![1, 1, 2, 2]
    | 1, 0 => ![0, 0, 3, 3]
    | 1, 2 => ![2, 2, 3, 3]
    | 2, 1 => ![1, 1, 0, 0]
    | 2, 3 => ![3, 3, 0, 0]
    | 3, 2 => ![2, 2, 1, 1]
    | _, _ => ![0, 0, 0, 0]

Uses 2 · Used by 4

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

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

DefinitionEndpoint of four lattice steps#✓fully proved

The endpoint of four lattice steps in the given directions.

def ons_fourDirSteps (N : ℕ) (r : Fin 4 → Fin 4)
    (p : ZMod N × ZMod N) : ZMod N × ZMod N :=
  ons_dirStep N (r 3)
    (ons_dirStep N (r 2)
      (ons_dirStep N (r 1) (ons_dirStep N (r 0) p)))

Uses 1 · Used by 3

Statement usesNeighbouring site in a given direction on the torus

Used byOnsager's formula · Four-step route of a decorated edge in the finer torus · Torus walk of four lattice steps

DefinitionTorus walk of four lattice steps#✓fully proved

The torus walk of four lattice steps in the given directions.

def ons_fourDirStepWalk (N : ℕ) [Fact (2 < N)]
    (r : Fin 4 → Fin 4) (p : ZMod N × ZMod N) :
    (onsTorusGraph N).Walk p (ons_fourDirSteps N r p) :=
  .cons (ons_torusAdj_dirStep N p (r 0))
    (.cons (ons_torusAdj_dirStep N (ons_dirStep N (r 0) p) (r 1))
      (.cons (ons_torusAdj_dirStep N
          (ons_dirStep N (r 1) (ons_dirStep N (r 0) p)) (r 2))
        (.cons (ons_torusAdj_dirStep N
            (ons_dirStep N (r 2)
              (ons_dirStep N (r 1) (ons_dirStep N (r 0) p))) (r 3))
          .nil)))

Uses 3 · Used by 2

Statement usesThe \(L \times L\) square-lattice torus graph · Neighbouring site in a given direction on the torus · Endpoint of four lattice steps

Used byOnsager's formula · Four-step route of a decorated edge in the finer torus

DefinitionFiner 8L × 8L torus graph for the decorated graph#✓fully proved

The 8L × 8L torus graph in which the decorated graph is drawn.

def ons_decEmbedGraph (L : ℕ) [Fact (2 < L)] :
    SimpleGraph (ZMod (8 * L) × ZMod (8 * L)) := by
  letI : Fact (2 < 8 * L) := ⟨by have := (Fact.out : 2 < L); omega⟩
  exact onsTorusGraph (8 * L)

Uses 1 · Used by 4

Statement usesThe \(L \times L\) square-lattice torus graph

Used byOnsager's formula · Route points of a decorated edge after its start · Four-step route of a decorated edge in the finer torus · Image of a decorated walk in the finer torus

DefinitionFour-step route of a decorated edge in the finer torus#✓fully proved

The four-step route of the decorated edge from d to e in the finer torus.

def ons_decEdgeRoute (L : ℕ) [Fact (2 < L)] (d e : ons_Dart L)
    (hde : (ons_decGraph L).Adj d e) :
    (ons_decEmbedGraph L).Walk
      (ons_decEmbedVertex L d) (ons_decEmbedVertex L e) := by
  letI : Fact (2 < 8 * L) := ⟨by have := (Fact.out : 2 < L); omega⟩
  let w : (ons_decEmbedGraph L).Walk (ons_decEmbedVertex L d)
      (ons_fourDirSteps (8 * L) (ons_decEdgeRouteDirs L d e)
        (ons_decEmbedVertex L d)) := by
    simpa [ons_decEmbedGraph] using
      ons_fourDirStepWalk (8 * L) (ons_decEdgeRouteDirs L d e)
        (ons_decEmbedVertex L d)
  exact w.copy rfl (ons_decEdgeRoute_endpoint L d e hde)

Uses 12 · Used by 3

Statement usesDarts of the square-lattice torus · Reverse of a dart · Adjacency of the decorated torus graph · Step directions of the route of a decorated edge · Finer 8L × 8L torus graph for the decorated graph · Offset of a dart inside its 8 × 8 cell · Position of a dart in the 8L × 8L torus · Decorated graph of the torus · Internal adjacency of the torus decoration · Neighbouring site in a given direction on the torus · Torus walk of four lattice steps · Endpoint of four lattice steps

Used byOnsager's formula · Route points of a decorated edge after its start · Image of a decorated walk in the finer torus

DefinitionFive points of the route of a decorated edge#✓fully proved

The five points of the route of the decorated edge from d to e.

def ons_decEdgeRouteVertices
    (L : ℕ) (d e : ons_Dart L) : List (ZMod (8 * L) × ZMod (8 * L)) :=
  let r := ons_decEdgeRouteDirs L d e
  let p₀ := ons_decEmbedVertex L d
  let p₁ := ons_dirStep (8 * L) (r 0) p₀
  let p₂ := ons_dirStep (8 * L) (r 1) p₁
  let p₃ := ons_dirStep (8 * L) (r 2) p₂
  let p₄ := ons_dirStep (8 * L) (r 3) p₃
  [p₀, p₁, p₂, p₃, p₄]

Uses 4 · Used by 1

Statement usesDarts of the square-lattice torus · Step directions of the route of a decorated edge · Position of a dart in the 8L × 8L torus · Neighbouring site in a given direction on the torus

Used byOnsager's formula

StructureMicro point of the finer torus as a cell and an offset#✓fully proved

A point of the 8L × 8L torus given as a coarse cell and an offset in Fin 8 × Fin 8.

structure ons_DecMicroPoint (L : ℕ) where
  cell : ZMod L × ZMod L
  offsetX : Fin 8
  offsetY : Fin 8
deriving DecidableEq

Used by 5

Used byOnsager's formula · Interior points of the route of a decorated edge · Decorated edge whose route passes through an interior micro point · Point of the finer torus represented by a micro point · Micro point at which a dart is placed

DefinitionPoint of the finer torus represented by a micro point#✓fully proved

The point of the finer torus represented by a micro point.

def ons_decMicroVertex (L : ℕ) (z : ons_DecMicroPoint L) :
    ZMod (8 * L) × ZMod (8 * L) :=
  ((8 * z.cell.1.val + z.offsetX.val : ℕ),
    (8 * z.cell.2.val + z.offsetY.val : ℕ))

Uses 1 · Used by 1

Statement usesMicro point of the finer torus as a cell and an offset

Used byOnsager's formula

DefinitionInterior points of the route of a decorated edge#✓fully proved

The three interior points of the route of the decorated edge from d to e, as micro points.

StatMech.Onsager.ons_decEdgeInteriorData · 21 lines

def ons_decEdgeInteriorData (L : ℕ) (d e : ons_Dart L) :
    List (ons_DecMicroPoint L) :=
  if e = ons_dartRev L d then
    match d.2 with
    | 0 => [⟨d.1, 7, 4⟩, ⟨ons_dirStep L 0 d.1, 0, 4⟩,
      ⟨ons_dirStep L 0 d.1, 1, 4⟩]
    | 1 => [⟨d.1, 4, 7⟩, ⟨ons_dirStep L 1 d.1, 4, 0⟩,
      ⟨ons_dirStep L 1 d.1, 4, 1⟩]
    | 2 => [⟨d.1, 1, 4⟩, ⟨d.1, 0, 4⟩,
      ⟨ons_dirStep L 2 d.1, 7, 4⟩]
    | 3 => [⟨d.1, 4, 1⟩, ⟨d.1, 4, 0⟩,
      ⟨ons_dirStep L 3 d.1, 4, 7⟩]
  else
    match d.2, e.2 with
    | 0, 1 => [⟨d.1, 6, 5⟩, ⟨d.1, 6, 6⟩, ⟨d.1, 5, 6⟩]
    | 1, 0 => [⟨d.1, 5, 6⟩, ⟨d.1, 6, 6⟩, ⟨d.1, 6, 5⟩]
    | 1, 2 => [⟨d.1, 3, 6⟩, ⟨d.1, 2, 6⟩, ⟨d.1, 2, 5⟩]
    | 2, 1 => [⟨d.1, 2, 5⟩, ⟨d.1, 2, 6⟩, ⟨d.1, 3, 6⟩]
    | 2, 3 => [⟨d.1, 2, 3⟩, ⟨d.1, 2, 2⟩, ⟨d.1, 3, 2⟩]
    | 3, 2 => [⟨d.1, 3, 2⟩, ⟨d.1, 2, 2⟩, ⟨d.1, 2, 3⟩]
    | _, _ => []

Uses 4 · Used by 1

Statement usesDarts of the square-lattice torus · Micro point of the finer torus as a cell and an offset · Reverse of a dart · Neighbouring site in a given direction on the torus

Used byOnsager's formula

DefinitionDecorated edge whose route passes through an interior micro point#✓fully proved

The decorated edge whose route passes through a given interior micro point.

StatMech.Onsager.ons_decMicroCorridorEdge · 19 lines

def ons_decMicroCorridorEdge (L : ℕ) (z : ons_DecMicroPoint L) :
    Sym2 (ons_Dart L) :=
  match z.offsetX.val, z.offsetY.val with
  | 7, 4 => s((z.cell, 0), (ons_dirStep L 0 z.cell, 2))
  | 0, 4 => s((ons_dirStep L 2 z.cell, 0), (z.cell, 2))
  | 1, 4 => s((ons_dirStep L 2 z.cell, 0), (z.cell, 2))
  | 4, 7 => s((z.cell, 1), (ons_dirStep L 1 z.cell, 3))
  | 4, 0 => s((ons_dirStep L 3 z.cell, 1), (z.cell, 3))
  | 4, 1 => s((ons_dirStep L 3 z.cell, 1), (z.cell, 3))
  | 6, 5 => s((z.cell, 0), (z.cell, 1))
  | 6, 6 => s((z.cell, 0), (z.cell, 1))
  | 5, 6 => s((z.cell, 0), (z.cell, 1))
  | 3, 6 => s((z.cell, 1), (z.cell, 2))
  | 2, 6 => s((z.cell, 1), (z.cell, 2))
  | 2, 5 => s((z.cell, 1), (z.cell, 2))
  | 2, 3 => s((z.cell, 2), (z.cell, 3))
  | 2, 2 => s((z.cell, 2), (z.cell, 3))
  | 3, 2 => s((z.cell, 2), (z.cell, 3))
  | _, _ => s((z.cell, 0), (z.cell, 1))

Uses 3 · Used by 1

Statement usesDarts of the square-lattice torus · Micro point of the finer torus as a cell and an offset · Neighbouring site in a given direction on the torus

Used byOnsager's formula

DefinitionCell offsets used by interior route points#✓fully proved

The offsets inside a cell used by interior points of routes.

def ons_decInteriorOffsets : Finset (Fin 8 × Fin 8) :=
  {(7, 4), (0, 4), (1, 4), (4, 7), (4, 0), (4, 1),
    (6, 5), (6, 6), (5, 6), (3, 6), (2, 6), (2, 5),
    (2, 3), (2, 2), (3, 2)}

Used by 1

Used byOnsager's formula

DefinitionMicro point at which a dart is placed#✓fully proved

The micro point at which a dart is placed.

def ons_decPortMicroPoint (L : ℕ) (d : ons_Dart L) :
    ons_DecMicroPoint L :=
  match d.2 with
  | 0 => ⟨d.1, 6, 4⟩
  | 1 => ⟨d.1, 4, 6⟩
  | 2 => ⟨d.1, 2, 4⟩
  | 3 => ⟨d.1, 4, 2⟩

Uses 2 · Used by 1

Statement usesDarts of the square-lattice torus · Micro point of the finer torus as a cell and an offset

Used byOnsager's formula

DefinitionRoute points of a decorated edge after its start#✓fully proved

The points of the route of a decorated edge after its starting point.

def ons_decDartSegment (L : ℕ) [Fact (2 < L)]
    (a : (ons_decGraph L).Dart) :
    List (ZMod (8 * L) × ZMod (8 * L)) :=
  (ons_decEdgeRoute L a.fst a.snd a.adj).support.tail

Uses 5 · Used by 1

Statement usesDarts of the square-lattice torus · Four-step route of a decorated edge in the finer torus · Finer 8L × 8L torus graph for the decorated graph · Position of a dart in the 8L × 8L torus · Decorated graph of the torus

Used byOnsager's formula

DefinitionImage of a decorated walk in the finer torus#✓fully proved

The image of a decorated walk in the finer torus, obtained by concatenating the routes of its edges.

def ons_decEmbedWalk (L : ℕ) [Fact (2 < L)] {u v : ons_Dart L}
    (p : (ons_decGraph L).Walk u v) :
    (ons_decEmbedGraph L).Walk
      (ons_decEmbedVertex L u) (ons_decEmbedVertex L v) :=
  match p with
  | .nil => .nil
  | .cons huw p =>
      (ons_decEdgeRoute L u _ huw).append (ons_decEmbedWalk L p)

Uses 5 · Used by 1

Statement usesDarts of the square-lattice torus · Four-step route of a decorated edge in the finer torus · Finer 8L × 8L torus graph for the decorated graph · Position of a dart in the 8L × 8L torus · Decorated graph of the torus

Used byOnsager's formula

DefinitionFour finer-torus darts along the route of a decorated edge#✓fully proved

The four darts of the finer torus along the route of the decorated edge from d to e.

def ons_decEdgeMicroDarts (L : ℕ) (d e : ons_Dart L) :
    List (ons_Dart (8 * L)) :=
  let r := ons_decEdgeRouteDirs L d e
  let p₀ := ons_decEmbedVertex L d
  let p₁ := ons_dirStep (8 * L) (r 0) p₀
  let p₂ := ons_dirStep (8 * L) (r 1) p₁
  let p₃ := ons_dirStep (8 * L) (r 2) p₂
  [(p₀, r 0), (p₁, r 1), (p₂, r 2), (p₃, r 3)]

Uses 4 · Used by 2

Statement usesDarts of the square-lattice torus · Step directions of the route of a decorated edge · Position of a dart in the 8L × 8L torus · Neighbouring site in a given direction on the torus

Used byOnsager's formula · Expanded dart list of a decorated walk in the finer torus

DefinitionExpanded dart list of a decorated walk in the finer torus#✓fully proved

The darts of the finer torus along the image of a decorated walk.

def ons_decExpandedDartList
    (L : ℕ) [Fact (2 < L)] {u v : ons_Dart L}
    (p : (ons_decGraph L).Walk u v) : List (ons_Dart (8 * L)) :=
  p.darts.flatMap (fun a => ons_decEdgeMicroDarts L a.fst a.snd)

Uses 3 · Used by 5

Statement usesDarts of the square-lattice torus · Four finer-torus darts along the route of a decorated edge · Decorated graph of the torus

Used byOnsager's formula · 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 · Directions of the expanded dart list of a decorated walk

DefinitionFirst dart of the expanded dart list of a decorated cycle#✓fully proved

The first dart of the expanded dart list of a decorated cycle.

def ons_decExpandedRoot
    (L : ℕ) [Fact (2 < L)] {d : ons_Dart L}
    (q : (ons_decGraph L).Walk d d) : ons_Dart (8 * L) :=
  (ons_decExpandedDartList L q).headD (ons_decEmbedVertex L d, 0)

Uses 4 · Used by 1

Statement usesDarts of the square-lattice torus · Position of a dart in the 8L × 8L torus · Expanded dart list of a decorated walk in the finer torus · Decorated graph of the torus

Used byOnsager's formula

DefinitionExpanded loop of a decorated cycle in walking order#✓fully proved

The expanded dart list of a decorated cycle as a cyclic sequence, in walking order.

def ons_decExpandedGeometricLoop
    (L : ℕ) [Fact (2 < L)] {d : ons_Dart L}
    (q : (ons_decGraph L).Walk d d) :
    Fin (ons_decExpandedDartList L q).length → ons_Dart (8 * L) :=
  (ons_decExpandedDartList L q).get

Uses 3 · Used by 2

Statement usesDarts of the square-lattice torus · Expanded dart list of a decorated walk in the finer torus · Decorated graph of the torus

Used byOnsager's formula · Expanded loop of a decorated cycle in Kac-Ward order

DefinitionExpanded loop of a decorated cycle in Kac-Ward order#✓fully proved

The expanded dart list of a decorated cycle as a cyclic sequence in Kac-Ward order (reversed indexing).

def ons_decExpandedKWLoop
    (L : ℕ) [Fact (2 < L)] {d : ons_Dart L}
    (q : (ons_decGraph L).Walk d d) (hq : q.IsCycle) :
    Fin (ons_decExpandedDartList L q).length → ons_Dart (8 * L) := by
  letI : NeZero (ons_decExpandedDartList L q).length :=
    ⟨Nat.ne_of_gt (ons_decExpandedDartList_length_pos L q hq)⟩
  exact fun k => ons_decExpandedGeometricLoop L q (-k)

Uses 4 · Used by 1

Statement usesDarts of the square-lattice torus · Expanded dart list of a decorated walk in the finer torus · Expanded loop of a decorated cycle in walking order · Decorated graph of the torus

Used byOnsager's formula

DefinitionInternal edge of the path at a site#✓fully proved

The i-th internal edge (s, i) - (s, i + 1) of the path at a site.

def ons_decChainEdge {L : ℕ}
    (site : ZMod L × ZMod L) (i : Fin 3) : Sym2 (ons_Dart L) :=
  s((site, ⟨i.val, by omega⟩), (site, ⟨i.val + 1, by omega⟩))

Uses 1 · Used by 19

Statement usesDarts of the square-lattice torus

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Internal part of a loop exponent · Column-scaled augmented Kac-Ward matrix · Row weights of the column-scaled augmented matrix · Exponent of a Kac-Ward transition · Onsager's formula · Internal edges between two ports at a site · Augmented Kac-Ward matrix with two side states · Balanced augmented Kac-Ward matrix · Row weights of the balanced augmented matrix · Destination-side internal weight to a port · Reversal-invariant internal factor of the augmented matrix · Row weights of the augmented Kac-Ward matrix · Source-side internal weight from a port · Row factor of the rank-two middle-edge term · Internal path between two ports at a site · Internal walk between two ports at a site · Decorated weight of a Kac-Ward transition

DefinitionIndices of internal edges between two ports#✓fully proved

The indices of the internal edges on the path between ports a and b at one site.

def ons_decChainPathIndices (a b : Fin 4) : Finset (Fin 3) :=
  Finset.univ.filter fun i ↦ (i.val < a.val) ≠ (i.val < b.val)

Used by 10

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Internal part of a loop exponent · Exponent of a Kac-Ward transition · Onsager's formula · Internal edges between two ports at a site · Reversal-invariant internal factor of the augmented matrix · Internal path between two ports at a site · Internal walk between two ports at a site · Decorated weight of a Kac-Ward transition

DefinitionInternal edges between two ports at a site#✓fully proved

The internal edges on the path between ports a and b at a site.

def ons_decChainPathEdges {L : ℕ}
    (site : ZMod L × ZMod L) (a b : Fin 4) :
    Finset (Sym2 (ons_Dart L)) :=
  (ons_decChainPathIndices a b).image (ons_decChainEdge site)

Uses 3 · Used by 5

Statement usesDarts of the square-lattice torus · Internal edge of the path at a site · Indices of internal edges between two ports

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Onsager's formula · Internal path between two ports at a site · Internal walk between two ports at a site

DefinitionDecorated weight of a Kac-Ward transition#✓fully proved

The decorated weight of the Kac-Ward transition from d₁ to d₂: the weight of the external edge at d₁ times the weights of the internal edges from the port of d₁ + 2 to the port of d₂.

def ons_decTransitionWeight
    (L : ℕ) (decWeight : Sym2 (ons_Dart L) → ℂ)
    (d₂ d₁ : ons_Dart L) : ℂ :=
  decWeight s(d₁, ons_dartRev L d₁) *
    ∏ i ∈ ons_decChainPathIndices (d₁.2 + 2) d₂.2,
      decWeight (ons_decChainEdge d₂.1 i)

Uses 4 · Used by 4

Statement usesDarts of the square-lattice torus · Reverse of a dart · Internal edge of the path at a site · Indices of internal edges between two ports

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Onsager's formula · Twisted Kac-Ward matrix with decorated transition weights

DefinitionTwisted Kac-Ward matrix with decorated transition weights#✓fully proved

The twisted Kac-Ward matrix with decorated transition weights.

noncomputable def ons_KWmatDecorationWeightedPhase
    (L : ℕ) (decWeight : Sym2 (ons_Dart L) → ℂ)
    (omega u v : ℂ) : Matrix (ons_Dart L) (ons_Dart L) ℂ :=
  fun d₂ d₁ ↦
    if d₂.1 = ons_dirStep L d₁.2 d₁.1 then
      ons_dirPhase u v d₁.2 *
        (ons_decTransitionWeight L decWeight d₂ d₁ *
          ons_turnW omega d₁.2 d₂.2)
    else 0

Uses 5 · Used by 10

Statement usesDarts of the square-lattice torus · Decorated weight of a Kac-Ward transition · Boundary phase of a step in a direction · Neighbouring site in a given direction on the torus · Turn weight between two lattice directions

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · 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 · Closed-walk weight through a dart but not its reverse · Closed-walk weight avoiding a dart and its reverse · Onsager's formula · Augmented Kac-Ward matrix with two side states · Balanced augmented Kac-Ward matrix

DefinitionDecorated weights induced by torus edge weights#✓fully proved

Decorated weights induced by torus edge weights: external edges get the weight of their torus edge, internal edges get 1.

noncomputable def ons_decSpecializedWeight
    {L : ℕ} (weight : Sym2 (ZMod L × ZMod L) → ℂ)
    (edge : Sym2 (ons_Dart L)) : ℂ := by
  classical
  exact if ons_decIsExternal edge then
      weight (ons_decEdgeProjection edge)
    else 1

Uses 3 · Used by 3

Statement usesDarts of the square-lattice torus · Projection of a decorated edge to the torus · Externality of a decorated edge

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

DefinitionDecorated weights with internal edges weighted by t#✓fully proved

Decorated weights with external edges weighted by their torus edge and internal edges by t.

noncomputable def ons_decInterpolatedWeight
    {L : ℕ} (weight : Sym2 (ZMod L × ZMod L) → ℂ) (t : ℂ)
    (edge : Sym2 (ons_Dart L)) : ℂ := by
  classical
  exact if ons_decIsExternal edge then
      weight (ons_decEdgeProjection edge)
    else t

Uses 3

Statement usesDarts of the square-lattice torus · Projection of a decorated edge to the torus · Externality of a decorated edge

DefinitionDecorated character sum with weights on all edges#✓fully proved

The decorated character sum ∑_D χ_{a,b}(hom D) ∏_{e ∈ D} w_e with a weight on every decorated edge.

noncomputable def ons_decoratedFullWeightedSpinSum
    (L : ℕ) [Fact (2 < L)]
    (decWeight : Sym2 (ons_Dart L) → ℂ) (a b : Fin 2) : ℂ :=
  ∑ D : ons_DecoratedEvenSubgraph L,
    (ons_spinCharacter a b
      (ons_evenHomology L (ons_originalEdgesOfDecorated L D)) : ℂ) *
      ∏ edge ∈ D.1, decWeight edge

Uses 10 · Used by 3

Statement usesEven subgraphs of a graph · Darts of the square-lattice torus · Even subgraphs of the decorated torus graph · Reverse of a dart · Adjacency of the decorated torus graph · Decorated graph of the torus · Internal adjacency of the torus decoration · Mod 2 homology class of an edge set · Torus even subgraph of a decorated even subgraph · Spin-structure character of a mod 2 homology class

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

DefinitionSide of a direction at a site#✓fully proved

The side of a direction at a site: 0 for east and north, 1 for west and south.

def ons_decMiddleSide (mu : Fin 4) : Fin 2 :=
  if mu.val < 2 then 0 else 1

Used by 4

Used byOnsager's formula · Reversal-invariant internal factor of the augmented matrix · Column factor of the rank-two middle-edge term · Row factor of the rank-two middle-edge term

DefinitionRepresentative direction of a side#✓fully proved

The representative direction of a side: east for side 0, west for side 1.

def ons_decMiddleDir (side : Fin 2) : Fin 4 :=
  if side = 0 then 0 else 2

Used by 4

Used byOnsager's formula · Directions of augmented states · Column factor of the rank-two middle-edge term · Row factor of the rank-two middle-edge term

DefinitionDestination-side internal weight to a port#✓fully proved

The weight of the internal edges between the middle edge and the port of direction μ, on the destination side.

noncomputable def ons_decMiddleDestFactor
    {L : ℕ} (decWeight : ons_DecEdge L → ℂ)
    (site : ZMod L × ZMod L) (mu : Fin 4) : ℂ :=
  match mu with
  | 0 => decWeight (ons_decChainEdge site 0)
  | 1 => 1
  | 2 => 1
  | 3 => decWeight (ons_decChainEdge site 2)

Uses 2 · Used by 3

Statement usesDecorated edges as formal-series variables · Internal edge of the path at a site

Used byOnsager's formula · Reversal-invariant internal factor of the augmented matrix · Column factor of the rank-two middle-edge term

DefinitionSource-side internal weight from a port#✓fully proved

The weight of the internal edges between the port of direction μ and the middle edge, on the source side.

noncomputable def ons_decMiddleSourceFactor
    {L : ℕ} (decWeight : ons_DecEdge L → ℂ)
    (site : ZMod L × ZMod L) (mu : Fin 4) : ℂ :=
  match mu with
  | 0 => 1
  | 1 => decWeight (ons_decChainEdge site 2)
  | 2 => decWeight (ons_decChainEdge site 0)
  | 3 => 1

Uses 2 · Used by 3

Statement usesDecorated edges as formal-series variables · Internal edge of the path at a site

Used byOnsager's formula · Reversal-invariant internal factor of the augmented matrix · Row factor of the rank-two middle-edge term

DefinitionColumn factor of the rank-two middle-edge term#✓fully proved

The column factor of the rank-two term: from a side of site to the darts leaving site on that side.

noncomputable def ons_decMiddleU
    (L : ℕ) (decWeight : ons_DecEdge L → ℂ)
    (omega : ℂ) (site : ZMod L × ZMod L) :
    Matrix (ons_Dart L) (Fin 2) ℂ :=
  fun d side ↦
    if d.1 = site ∧ ons_decMiddleSide d.2 = side then
      ons_decMiddleDestFactor decWeight site d.2 *
        ons_turnW omega (ons_decMiddleDir side) d.2
    else 0

Uses 6 · Used by 4

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Destination-side internal weight to a port · Representative direction of a side · Side of a direction at a site · Turn weight between two lattice directions

Used byColumn-scaled augmented Kac-Ward matrix · Onsager's formula · Augmented Kac-Ward matrix with two side states · Balanced augmented Kac-Ward matrix

DefinitionRow factor of the rank-two middle-edge term#✓fully proved

The row factor of the rank-two term: from the darts entering site to the side on which they arrive.

noncomputable def ons_decMiddleV
    (L : ℕ) (decWeight : ons_DecEdge L → ℂ)
    (omega u v : ℂ) (site : ZMod L × ZMod L) :
    Matrix (Fin 2) (ons_Dart L) ℂ :=
  fun side d ↦
    if site = ons_dirStep L d.2 d.1 ∧
        ons_decMiddleSide d.2 = side then
      decWeight (ons_decChainEdge site 1) *
        ons_dirPhase u v d.2 *
        decWeight s(d, ons_dartRev L d) *
        ons_decMiddleSourceFactor decWeight site d.2 *
        ons_turnW omega d.2 (ons_decMiddleDir side)
    else 0

Uses 10 · Used by 4

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Reverse of a dart · Internal edge of the path at a site · Representative direction of a side · Side of a direction at a site · Source-side internal weight from a port · Boundary phase of a step in a direction · Neighbouring site in a given direction on the torus · Turn weight between two lattice directions

Used byColumn-scaled augmented Kac-Ward matrix · Onsager's formula · Augmented Kac-Ward matrix with two side states · Balanced augmented Kac-Ward matrix

DefinitionAugmented Kac-Ward matrix with two side states#✓fully proved

The augmented Kac-Ward matrix on darts and the two sides of site, with blocks Λ₀, U, t V and 0.

noncomputable def ons_decMiddleAugmented
    (L : ℕ) (decWeight : ons_DecEdge L → ℂ)
    (omega u v t : ℂ) (site : ZMod L × ZMod L) :
    Matrix (ons_Dart L ⊕ Fin 2) (ons_Dart L ⊕ Fin 2) ℂ :=
  Matrix.fromBlocks
    (ons_KWmatDecorationWeightedPhase L
      (ons_scaleDecEdgeWeight decWeight
        (ons_decChainEdge site 1) 0) omega u v)
    (ons_decMiddleU L decWeight omega site)
    (t • ons_decMiddleV L decWeight omega u v site)
    0

Uses 7 · Used by 1

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Twisted Kac-Ward matrix with decorated transition weights · Internal edge of the path at a site · Column factor of the rank-two middle-edge term · Row factor of the rank-two middle-edge term · Decorated weights with one edge weight scaled by t

Used byOnsager's formula

DefinitionBalanced augmented Kac-Ward matrix#✓fully proved

The augmented matrix with blocks Λ₀, (t λ) U, λ⁻¹ V and 0.

noncomputable def ons_decMiddleBalanced
    (L : ℕ) (decWeight : ons_DecEdge L → ℂ)
    (omega t lambda : ℂ) (site : ZMod L × ZMod L) :
    Matrix (ons_Dart L ⊕ Fin 2) (ons_Dart L ⊕ Fin 2) ℂ :=
  Matrix.fromBlocks
    (ons_KWmatDecorationWeightedPhase L
      (ons_scaleDecEdgeWeight decWeight
        (ons_decChainEdge site 1) 0) omega 1 1)
    ((t * lambda) • ons_decMiddleU L decWeight omega site)
    (lambda⁻¹ • ons_decMiddleV L decWeight omega 1 1 site)
    0

Uses 7 · Used by 1

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Twisted Kac-Ward matrix with decorated transition weights · Internal edge of the path at a site · Column factor of the rank-two middle-edge term · Row factor of the rank-two middle-edge term · Decorated weights with one edge weight scaled by t

Used byOnsager's formula

DefinitionRow weights of the balanced augmented matrix#✓fully proved

Row weights of the balanced augmented matrix.

noncomputable def ons_decMiddleBalancedRowWeight
    {L : ℕ} (decWeight : ons_DecEdge L → ℂ) (lambda : ℂ)
    (site : ZMod L × ZMod L) : ons_Dart L ⊕ Fin 2 → ℂ
  | .inl _ => 1
  | .inr _ => lambda⁻¹ * decWeight (ons_decChainEdge site 1)

Uses 3 · Used by 1

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Internal edge of the path at a site

Used byOnsager's formula

DefinitionColumn weights of the balanced augmented matrix#✓fully proved

Column weights of the balanced augmented matrix.

noncomputable def ons_decMiddleBalancedColWeight
    {L : ℕ} (decWeight : ons_DecEdge L → ℂ) (t lambda : ℂ) :
    ons_Dart L ⊕ Fin 2 → ℂ
  | .inl d => decWeight s(d, ons_dartRev L d)
  | .inr _ => t * lambda

Uses 3 · Used by 1

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Reverse of a dart

Used byOnsager's formula

DefinitionReversal on augmented states#✓fully proved

Reversal on augmented states: reverse darts and swap the two sides.

def ons_decMiddleAugRev (L : ℕ) :
    ons_Dart L ⊕ Fin 2 → ons_Dart L ⊕ Fin 2
  | .inl d => .inl (ons_dartRev L d)
  | .inr side => .inr (side + 1)

Uses 2 · Used by 1

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

Used byOnsager's formula

DefinitionDirections of augmented states#✓fully proved

Directions of augmented states: the direction of a dart, and east or west for the two sides.

def ons_decMiddleAugDir {L : ℕ} :
    ons_Dart L ⊕ Fin 2 → Fin 4
  | .inl d => d.2
  | .inr side => ons_decMiddleDir side

Uses 2 · Used by 1

Statement usesDarts of the square-lattice torus · Representative direction of a side

Used byOnsager's formula

DefinitionRow weights of the augmented Kac-Ward matrix#✓fully proved

Row weights of the augmented matrix: 1 on darts and t times the middle weight on side states.

noncomputable def ons_decMiddleRowWeight
    {L : ℕ} (decWeight : ons_DecEdge L → ℂ)
    (t : ℂ) (site : ZMod L × ZMod L) :
    ons_Dart L ⊕ Fin 2 → ℂ
  | .inl _ => 1
  | .inr _ => t * decWeight (ons_decChainEdge site 1)

Uses 3 · Used by 1

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Internal edge of the path at a site

Used byOnsager's formula

DefinitionColumn weights of the augmented Kac-Ward matrix#✓fully proved

Column weights of the augmented matrix: the external weight on darts and 1 on side states.

noncomputable def ons_decMiddleColWeight
    {L : ℕ} (decWeight : ons_DecEdge L → ℂ) :
    ons_Dart L ⊕ Fin 2 → ℂ
  | .inl d => decWeight s(d, ons_dartRev L d)
  | .inr _ => 1

Uses 3 · Used by 1

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Reverse of a dart

Used byOnsager's formula

DefinitionReversal-invariant internal factor of the augmented matrix#✓fully proved

The reversal-invariant internal factor of the augmented matrix.

StatMech.Onsager.ons_decMiddleInternalFactor · 20 lines

noncomputable def ons_decMiddleInternalFactor
    (L : ℕ) (decWeight : ons_DecEdge L → ℂ)
    (site : ZMod L × ZMod L) :
    (ons_Dart L ⊕ Fin 2) → (ons_Dart L ⊕ Fin 2) → ℂ
  | .inl d₂, .inl d₁ =>
      if d₂.1 = ons_dirStep L d₁.2 d₁.1 then
        ∏ i ∈ ons_decChainPathIndices (d₁.2 + 2) d₂.2,
          ons_scaleDecEdgeWeight decWeight
            (ons_decChainEdge site 1) 0 (ons_decChainEdge d₂.1 i)
      else 0
  | .inl d₂, .inr side =>
      if d₂.1 = site ∧ ons_decMiddleSide d₂.2 = side then
        ons_decMiddleDestFactor decWeight site d₂.2
      else 0
  | .inr side, .inl d₁ =>
      if site = ons_dirStep L d₁.2 d₁.1 ∧
          ons_decMiddleSide d₁.2 = side then
        ons_decMiddleSourceFactor decWeight site d₁.2
      else 0
  | .inr _, .inr _ => 0

Uses 9 · Used by 1

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Internal edge of the path at a site · Indices of internal edges between two ports · Destination-side internal weight to a port · Side of a direction at a site · Source-side internal weight from a port · Neighbouring site in a given direction on the torus · Decorated weights with one edge weight scaled by t

Used byOnsager's formula

DefinitionTest for a dart traversing an external edge#✓fully proved

Whether a dart of the decorated graph traverses an external edge (from a torus dart to its reverse).

def ons_decDartIsExternal {L : ℕ} (a : (ons_decGraph L).Dart) : Bool :=
  decide (a.snd = ons_dartRev L a.fst)

Uses 3 · Used by 2

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

Used byOnsager's formula · External darts of a decorated walk in order

DefinitionExternal darts of a decorated walk in order#✓fully proved

The torus darts at which a decorated walk traverses an external edge, in order.

def ons_decWalkExternalDarts {L : ℕ} {u v : ons_Dart L}
    (p : (ons_decGraph L).Walk u v) : List (ons_Dart L) :=
  (p.darts.filter ons_decDartIsExternal).map (fun a => a.fst)

Uses 3 · Used by 3

Statement usesDarts of the square-lattice torus · Test for a dart traversing an external edge · Decorated graph of the torus

Used byOnsager's formula · First-return loop of a rooted decorated cycle · Directions of the external darts of a decorated walk

DefinitionFirst-return loop of a rooted decorated cycle#✓fully proved

The first-return loop at d read off from a decorated cycle rooted at d: the root, the remaining external darts in reverse order, and the root again.

def ons_decCycleFirstReturn {L : ℕ} {d : ons_Dart L}
    (q : (ons_decGraph L).Walk d d) : List (ons_Dart L) :=
  d :: (ons_decWalkExternalDarts q).tail.reverse ++ [d]

Uses 3 · Used by 3

Statement usesDarts of the square-lattice torus · Decorated graph of the torus · External darts of a decorated walk in order

Used byCycle removal identity for decorated even subgraphs · Onsager's formula · Dart list of a rooted decorated cycle

DefinitionAdjacency of directions along the port line#✓fully proved

Two directions are adjacent in the order 0, 1, 2, 3 of the internal path at a site.

def ons_portLineAdj (a b : Fin 4) : Prop :=
  a.val + 1 = b.val ∨ b.val + 1 = a.val

Used by 5

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Onsager's formula · Internal path between two ports at a site · Internal walk between two ports at a site

DefinitionMicro directions along internal decorated edges at a site#✓fully proved

The micro directions of the routes along a sequence of internal decorated edges at one site.

def ons_internalMicroDirections : List (Fin 4) → List (Fin 4)
  | a :: b :: rest =>
      [b, b, a + 2, a + 2] ++ ons_internalMicroDirections (b :: rest)
  | _ => []

Used by 1

Used byOnsager's formula

DefinitionDirections of the expanded dart list of a decorated walk#✓fully proved

The directions of the expanded dart list of a decorated walk.

def ons_walkExpandedDirections
    (L : ℕ) [Fact (2 < L)] {u v : ons_Dart L}
    (p : (ons_decGraph L).Walk u v) : List (Fin 4) :=
  (ons_decExpandedDartList L p).map (fun a ↦ a.2)

Uses 3 · Used by 1

Statement usesDarts of the square-lattice torus · Expanded dart list of a decorated walk in the finer torus · Decorated graph of the torus

Used byOnsager's formula

DefinitionDirections of the external darts of a decorated walk#✓fully proved

The directions of the external darts of a decorated walk.

def ons_walkExternalDirections
    {L : ℕ} {u v : ons_Dart L}
  (p : (ons_decGraph L).Walk u v) : List (Fin 4) :=
  (ons_decWalkExternalDarts p).map (fun a ↦ a.2)

Uses 3 · Used by 1

Statement usesDarts of the square-lattice torus · Decorated graph of the torus · External darts of a decorated walk in order

Used byOnsager's formula

DefinitionInternal walk between two ports at a site#✓fully proved

A walk along the internal path from port a to port b at a site.

noncomputable def ons_decPortChainWalk
    (L : ℕ) (site : ZMod L × ZMod L) (a b : Fin 4) :
    (ons_decGraph L).Walk (site, a) (site, b) :=
  Classical.choose (ons_exists_decPortChainWalk L site a b)

Uses 8

Statement usesDarts of the square-lattice torus · Reverse of a dart · Internal edge of the path at a site · Internal edges between two ports at a site · Indices of internal edges between two ports · Decorated graph of the torus · Internal adjacency of the torus decoration · Adjacency of directions along the port line

DefinitionInternal path between two ports at a site#✓fully proved

The internal path from port a to port b at a site, as a path in the decorated graph.

noncomputable def ons_decPortChainPath
    (L : ℕ) (site : ZMod L × ZMod L) (a b : Fin 4) :
    (ons_decGraph L).Walk (site, a) (site, b) :=
  Classical.choose (ons_exists_decPortChainPath L site a b)

Uses 8 · Used by 4

Statement usesDarts of the square-lattice torus · Reverse of a dart · Internal edge of the path at a site · Internal edges between two ports at a site · Indices of internal edges between two ports · Decorated graph of the torus · Internal adjacency of the torus decoration · Adjacency of directions along the port line

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Onsager's formula · Decorated walk of a Kac-Ward transition

DefinitionDecorated walk of a Kac-Ward transition#✓fully proved

The decorated walk of the Kac-Ward transition from d₁ to d₂: the external edge at d₁ followed by the internal path to d₂.

noncomputable def ons_decTransitionWalk
    (L : ℕ) (d₂ d₁ : ons_Dart L)
    (hstep : d₂.1 = ons_dirStep L d₁.2 d₁.1) :
    (ons_decGraph L).Walk d₁ d₂ := by
  let ext : (ons_decGraph L).Walk d₁ (ons_dartRev L d₁) :=
    .cons (@id ((ons_decGraph L).Adj d₁ (ons_dartRev L d₁)) (Or.inl rfl)) .nil
  let chain₀ := ons_decPortChainPath L d₂.1 (d₁.2 + 2) d₂.2
  have hstart : (d₂.1, d₁.2 + 2) = ons_dartRev L d₁ := by
    apply Prod.ext
    · exact hstep.trans (ons_dartRev_fst_eq_step L d₁).symm
    · simp [ons_dartRev]
  let chain : (ons_decGraph L).Walk (ons_dartRev L d₁) d₂ :=
    chain₀.copy hstart rfl
  exact ext.append chain

Uses 6 · Used by 4

Statement usesDarts of the square-lattice torus · Reverse of a dart · Decorated graph of the torus · Internal adjacency of the torus decoration · Internal path between two ports at a site · Neighbouring site in a given direction on the torus

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Onsager's formula · Decorated walk of a chain of darts

DefinitionHead-to-tail relation between darts#✓fully proved

Dart target starts at the head of dart source.

def ons_decGeometricStep (L : ℕ) (source target : ons_Dart L) : Prop :=
  target.1 = ons_dirStep L source.2 source.1

Uses 2 · Used by 3

Statement usesDarts of the square-lattice torus · Neighbouring site in a given direction on the torus

Used byOnsager's formula · Closed decorated walk of a valid Kac-Ward loop · Decorated walk of a chain of darts

DefinitionEdge multiset of a decorated walk as an exponent#✓fully proved

The multiset of edges of a decorated walk, as an exponent.

noncomputable def ons_decWalkEdgeCount
    {L : ℕ} {u v : ons_Dart L}
    (p : (ons_decGraph L).Walk u v) : ons_DecEdge L →₀ ℕ := by
  classical
  exact Multiset.toFinsupp (p.edges : Multiset (ons_DecEdge L))

Uses 3 · Used by 1

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Decorated graph of the torus

Used byOnsager's formula

DefinitionTransition exponent sum along a dart chain#✓fully proved

The sum of the transition exponents along a chain of darts starting at start.

noncomputable def ons_decKWChainExponent
    (L : ℕ) (start : ons_Dart L) :
    List (ons_Dart L) → ons_DecEdge L →₀ ℕ
  | [] => 0
  | target :: rest =>
      ons_decTransitionExponent L target start +
        ons_decKWChainExponent L target rest

Uses 3 · Used by 1

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Exponent of a Kac-Ward transition

Used byOnsager's formula

DefinitionLast dart of a dart chain#✓fully proved

The last dart of a chain starting at start.

def ons_decKWChainLast {L : ℕ} (start : ons_Dart L) :
    List (ons_Dart L) → ons_Dart L
  | [] => start
  | target :: rest => ons_decKWChainLast target rest

Uses 1 · Used by 3

Statement usesDarts of the square-lattice torus

Used byOnsager's formula · Closed decorated walk of a valid Kac-Ward loop · Decorated walk of a chain of darts

DefinitionDecorated walk of a chain of darts#✓fully proved

The decorated walk obtained by concatenating the trails of the transitions along a chain of darts.

noncomputable def ons_decWalkOfKWChain
    (L : ℕ) (start : ons_Dart L) :
    (tail : List (ons_Dart L)) →
    List.IsChain (ons_decGeometricStep L) (start :: tail) →
    (ons_decGraph L).Walk start (ons_decKWChainLast start tail)
  | [], _ => .nil
  | target :: rest, hchain => by
      have hstep : target.1 = ons_dirStep L start.2 start.1 :=
        hchain.rel
      let first := ons_decTransitionWalk L target start hstep
      let remaining :=
        @id ((ons_decGraph L).Walk target (ons_decKWChainLast start (target :: rest)))
          (ons_decWalkOfKWChain L target rest hchain.tail)
      exact first.append remaining

Uses 6 · Used by 2

Statement usesDarts of the square-lattice torus · Head-to-tail relation between darts · Decorated graph of the torus · Last dart of a dart chain · Decorated walk of a Kac-Ward transition · Neighbouring site in a given direction on the torus

Used byOnsager's formula · Closed decorated walk of a valid Kac-Ward loop

DefinitionDarts of a Kac-Ward loop in walking order#✓fully proved

The darts of a Kac-Ward loop in walking order (reversed indexing).

def ons_decGeometricLoopStates
    {L n : ℕ} (d : Fin n → ons_Dart L) : Fin n → ons_Dart L :=
  fun k ↦ d (-k)

Uses 1 · Used by 2

Statement usesDarts of the square-lattice torus

Used byOnsager's formula · Closed decorated walk of a valid Kac-Ward loop

DefinitionClosed decorated walk of a valid Kac-Ward loop#✓fully proved

The closed decorated walk of a valid closed Kac-Ward walk, rooted at its first dart.

StatMech.Onsager.ons_decLoopWalk · 28 lines

noncomputable def ons_decLoopWalk
    (L : ℕ) {n : ℕ} [NeZero n] (d : Fin n → ons_Dart L)
    (hvalid : ∀ k : Fin n,
      (d k).1 = ons_dirStep L (d (k + 1)).2 (d (k + 1)).1) :
    (ons_decGraph L).Walk (d 0) (d 0) := by
  let states := List.ofFn (ons_decGeometricLoopStates d)
  have hstatesNonempty : states ≠ [] := by
    rw [List.ne_nil_iff_length_pos, List.length_ofFn]
    exact NeZero.pos n
  have hhead : states.head? = some (d 0) := by
    rw [List.head?_eq_some_head hstatesNonempty,
      List.head_ofFn hstatesNonempty]
    simp [ons_decGeometricLoopStates]
  have hstates : states = d 0 :: states.tail := by
    apply List.eq_cons_of_mem_head?
    simp [hhead]
  have hchain : List.IsChain (ons_decGeometricStep L)
      (states ++ [d 0]) := by
    simpa [states, ons_decGeometricLoopStates] using
      ons_isChain_closed_ofFn_mk (ons_decGeometricLoopStates d)
        (ons_decGeometricLoopStates_valid d hvalid)
  have hchain' : List.IsChain (ons_decGeometricStep L)
      (d 0 :: (states.tail ++ [d 0])) := by
    rw [← List.cons_append, ← hstates]
    exact hchain
  let walk := ons_decWalkOfKWChain L (d 0)
    (states.tail ++ [d 0]) hchain'
  exact walk.copy rfl (ons_decKWChainLast_append_singleton _ _ _)

Uses 7 · Used by 1

Statement usesDarts of the square-lattice torus · Darts of a Kac-Ward loop in walking order · Head-to-tail relation between darts · Decorated graph of the torus · Last dart of a dart chain · Decorated walk of a chain of darts · Neighbouring site in a given direction on the torus

Used byOnsager's formula

DefinitionDart list of a rooted decorated cycle#✓fully proved

The first-return loop of a rooted decorated cycle without its final repeated dart.

def ons_decCycleDartList {L : ℕ} {d : ons_Dart L}
    (q : (ons_decGraph L).Walk d d) : List (ons_Dart L) :=
  (ons_decCycleFirstReturn q).dropLast

Uses 3 · Used by 2

Statement usesDarts of the square-lattice torus · First-return loop of a rooted decorated cycle · Decorated graph of the torus

Used byOnsager's formula · Closed dart walk of a rooted decorated cycle

DefinitionClosed dart walk of a rooted decorated cycle#✓fully proved

The closed walk of darts of a rooted decorated cycle, indexed by Fin of its length.

def ons_decCycleDartLoop {L : ℕ} {d : ons_Dart L}
    (q : (ons_decGraph L).Walk d d) :
    Fin (ons_decCycleDartList q).length → ons_Dart L :=
  (ons_decCycleDartList q).get

Uses 3 · Used by 1

Statement usesDarts of the square-lattice torus · Dart list of a rooted decorated cycle · Decorated graph of the torus

Used byOnsager's formula

DefinitionSimple graph spanned by an edge set#✓fully proved

The simple graph on V whose edges are the non-loop elements of F; this is SimpleGraph.fromEdgeSet F.

def ons_edgeSubgraph (F : Finset (Sym2 V)) : SimpleGraph V :=
  SimpleGraph.fromEdgeSet (F : Set (Sym2 V))

Used by 2

Used byChosen split of a decorated even subgraph at an external edge · Onsager's formula

90 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.