Spin Kac–Ward identities

DefinitionOne-edge decorated walk along an external edge#✓fully proved

The one-edge decorated walk along the external edge from d to its reverse.

def ons_decExternalStepWalk (L : ℕ) (d : ons_Dart L) :
    (ons_decGraph L).Walk d (ons_dartRev L d) :=
  .cons (@id ((ons_decGraph L).Adj d (ons_dartRev L d)) (Or.inl rfl)) .nil

Uses 4 · Used by 1

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

Used byOnsager's formula

DefinitionValue of a monomial at weights#✓fully proved

The value ∏_e w_e ^ {m e} of the monomial with exponent m at weights w.

noncomputable def ons_mvMonomialValue
    {E : Type*} (weight : E → ℂ) (m : E →₀ ℕ) : ℂ :=
  m.prod fun edge n ↦ weight edge ^ n

Used by 7

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Degree-\(n\) part of a power series evaluated at a point · Sum of absolute values of the degree-\(n\) terms at a point · Onsager's formula · Sum of absolute values of an evaluated power series · Absolute summability of a power series evaluated at weights

DefinitionAbsolute summability of a power series evaluated at weights#✓fully proved

Absolute summability of ∑_m coeff_m · w^m.

def ons_MvSeriesEvalSummable
    {E : Type*} (series : MvPowerSeries E ℂ) (weight : E → ℂ) : Prop :=
  Summable fun m : E →₀ ℕ ↦
    ‖MvPowerSeries.coeff m series * ons_mvMonomialValue weight m‖

Uses 1 · Used by 3

Statement usesValue of a monomial at weights

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

DefinitionSum of absolute values of an evaluated power series#✓fully proved

The sum ∑_m ‖coeff_m · w^m‖ of absolute values.

noncomputable def ons_mvSeriesEvalNorm
    {E : Type*} (series : MvPowerSeries E ℂ) (weight : E → ℂ) : ℝ :=
  ∑' m : E →₀ ℕ,
    ‖MvPowerSeries.coeff m series * ons_mvMonomialValue weight m‖

Uses 1 · Used by 3

Statement usesValue of a monomial at weights

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

AbbreviationEven subgraphs of the L × L torus#✓fully proved

Even subgraphs of the L × L torus.

abbrev ons_TorusEvenSubgraph (L : ℕ) [Fact (2 < L)] :=
  {F : Finset (Sym2 (ZMod L × ZMod L)) //
    F ∈ evenSubgraphs (onsTorusGraph L)}

Uses 3

Statement usesEven subgraphs of a graph · Nearest-neighbor adjacency on the discrete torus · The \(L \times L\) square-lattice torus graph

AbbreviationEven subgraphs of the decorated torus graph#✓fully proved

Even subgraphs of the decorated graph of the torus.

abbrev ons_DecoratedEvenSubgraph (L : ℕ) [Fact (2 < L)] :=
  {D : Finset (Sym2 (ons_Dart L)) //
    D ∈ evenSubgraphs (ons_decGraph L)}

Uses 6 · Used by 12

Statement usesEven subgraphs of a graph · Darts of the square-lattice torus · Reverse of a dart · Adjacency of the decorated torus graph · Decorated graph of the torus · 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 · Decorated spin polynomial · Spin weight of a decorated even subgraph · Edge-weighted spin weight of a decorated even subgraph · Onsager's formula · Torus even subgraph of a decorated even subgraph · Decorated character sum with weights on all edges

DefinitionTorus even subgraph of a decorated even subgraph#✓fully proved

The torus even subgraph corresponding to a decorated even subgraph under the decoration bijection.

noncomputable def ons_originalEdgesOfDecorated
    (L : ℕ) [Fact (2 < L)]
    (D : ons_DecoratedEvenSubgraph L) :
    Finset (Sym2 (ZMod L × ZMod L)) :=
  ((ons_decorationEquiv L).symm D).1

Uses 10 · Used by 7

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 · 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 · Equivalence between even subgraphs of the torus and its decoration

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Decorated spin polynomial · Spin weight of a decorated even subgraph · Edge-weighted spin weight of a decorated even subgraph · Onsager's formula · Decorated character sum with weights on all edges

DefinitionExternality of a decorated edge#✓fully proved

An edge of the decorated graph is external if it joins a dart to its reverse.

def ons_decIsExternal {L : ℕ} (edge : Sym2 (ons_Dart L)) : Prop :=
  ∃ d : ons_Dart L, edge = s(d, ons_dartRev L d)

Uses 2 · Used by 7

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 · External edges of a decorated edge set · Onsager's formula · Decorated weights with internal edges weighted by t · Decorated weights induced by torus edge weights · Decorated weights twisted by seam signs

DefinitionExternal edges of a decorated edge set#✓fully proved

The external edges of a decorated edge set.

noncomputable def ons_decoratedExternalEdges {L : ℕ}
    (D : Finset (Sym2 (ons_Dart L))) : Finset (Sym2 (ons_Dart L)) := by
  classical
  exact D.filter ons_decIsExternal

Uses 2 · Used by 4

Statement usesDarts of the square-lattice 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 · External edges used by a decorated walk

DefinitionProjection of a decorated edge to the torus#✓fully proved

The projection of a decorated edge to the torus, taking each dart to its starting site.

def ons_decEdgeProjection {L : ℕ}
    (edge : Sym2 (ons_Dart L)) : Sym2 (ZMod L × ZMod L) :=
  Sym2.map Prod.fst edge

Uses 1 · Used by 6

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 · Onsager's formula · Torus edges underlying a decorated walk · Decorated weights with internal edges weighted by t · Decorated weights induced by torus edge weights

DefinitionSpin weight of a decorated even subgraph#✓fully proved

The weight χ_{a,b}(hom F) x^|F| of the torus even subgraph F corresponding to a decorated even subgraph.

noncomputable def ons_decoratedSpinWeight
    (L : ℕ) [Fact (2 < L)] (x : ℝ) (a b : Fin 2)
    (D : ons_DecoratedEvenSubgraph L) : ℝ :=
  let F := ons_originalEdgesOfDecorated L D
  ons_spinCharacter a b (ons_evenHomology L F) * x ^ F.card

Uses 4

Statement usesEven subgraphs of the decorated torus graph · 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

DefinitionExternal edges used by a decorated walk#✓fully proved

The external edges used by a walk in the decorated graph.

noncomputable def ons_walkExternalEdges {L : ℕ} {u v : ons_Dart L}
    (p : (ons_decGraph L).Walk u v) : Finset (Sym2 (ons_Dart L)) :=
  ons_decoratedExternalEdges p.edges.toFinset

Uses 3 · Used by 2

Statement usesDarts of the square-lattice torus · Decorated graph of the torus · External edges of a decorated edge set

Used byOnsager's formula · Torus edges underlying a decorated walk

DefinitionTorus edges underlying a decorated walk#✓fully proved

The torus edges underlying the external edges of a decorated walk.

noncomputable def ons_walkOriginalEdges {L : ℕ} {u v : ons_Dart L}
    (p : (ons_decGraph L).Walk u v) :
    Finset (Sym2 (ZMod L × ZMod L)) :=
  (ons_walkExternalEdges p).image ons_decEdgeProjection

Uses 4 · Used by 2

Statement usesDarts of the square-lattice torus · Projection of a decorated edge to the torus · Decorated graph of the torus · External edges used by a decorated walk

Used byLog-coefficient polynomial over the cycles of a decomposition · Onsager's formula

AbbreviationDecorated edges as formal-series variables#✓fully proved

Decorated edges, used as the variables of the formal series.

abbrev ons_DecEdge (L : ℕ) := Sym2 (ons_Dart L)

Uses 1 · Used by 40

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 · Log-coefficient polynomial over the cycles of a decomposition · Formal-logarithm term from closed walks of given length and exponent · Formal logarithm of the Kac-Ward root · Coefficient of the formal Kac-Ward logarithm · Vanishing of repeated-edge coefficients of the formal Kac-Ward root · Formal Kac-Ward root · Second difference of a formal series in one variable · Monomial of a Kac-Ward transition · Exponent of a closed Kac-Ward walk · External part of a loop exponent · Internal part of a loop exponent · Masked closed-walk weight through a dart but not its reverse · Masked closed-walk weight avoiding a dart and its reverse · Column-scaled augmented Kac-Ward matrix · Column weights of the column-scaled augmented matrix · Row weights of the column-scaled augmented matrix · Closed-walk weight through a dart but not its reverse · Closed-walk weight avoiding a dart and its reverse · Kac-Ward loops with a given squarefree exponent and nonzero scalar · Exponent of a Kac-Ward transition · Formal Kac-Ward identity on the torus · Decorated spin polynomial · Onsager's formula · Decorated weights with one edge weight scaled by t · Transition exponent sum along a dart chain · Augmented Kac-Ward matrix with two side states · Balanced augmented Kac-Ward matrix · Column weights of the balanced augmented matrix · Row weights of the balanced augmented matrix · Column weights of the augmented Kac-Ward matrix · 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 · Column factor of the rank-two middle-edge term · Row factor of the rank-two middle-edge term · Edge multiset of a decorated walk as an exponent · Decorated weights twisted by seam signs

DefinitionExponent of a Kac-Ward transition#✓fully proved

The exponent of a transition: one for the external edge at d₁ and one for each internal edge on the path at the site of d₂.

noncomputable def ons_decTransitionExponent
    (L : ℕ) (d₂ d₁ : ons_Dart L) : ons_DecEdge L →₀ ℕ := by
  classical
  exact Finsupp.single s(d₁, ons_dartRev L d₁) 1 +
    ∑ i ∈ ons_decChainPathIndices (d₁.2 + 2) d₂.2,
      Finsupp.single (ons_decChainEdge d₂.1 i) 1

Uses 5 · Used by 6

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 · 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 · Monomial of a Kac-Ward transition · Exponent of a closed Kac-Ward walk · Onsager's formula · Transition exponent sum along a dart chain

DefinitionScalar of a Kac-Ward transition#✓fully proved

The scalar of a transition: its boundary phase times its turn weight, or 0 if d₂ does not start at the head of d₁.

noncomputable def ons_decTransitionScalar
    (L : ℕ) (omega u v : ℂ) (d₂ d₁ : ons_Dart L) : ℂ :=
  if d₂.1 = ons_dirStep L d₁.2 d₁.1 then
    ons_dirPhase u v d₁.2 * ons_turnW omega d₁.2 d₂.2
  else 0

Uses 4 · Used by 5

Statement usesDarts of the square-lattice torus · 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 · Monomial of a Kac-Ward transition · Scalar of a closed Kac-Ward walk · Onsager's formula

DefinitionMonomial of a Kac-Ward transition#✓fully proved

The monomial of the transition from d₁ to d₂.

noncomputable def ons_decFormalTransition
    (L : ℕ) (omega u v : ℂ) (d₂ d₁ : ons_Dart L) :
    MvPowerSeries (ons_DecEdge L) ℂ :=
  MvPowerSeries.monomial (ons_decTransitionExponent L d₂ d₁)
    (ons_decTransitionScalar L omega u v d₂ d₁)

Uses 4

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

DefinitionExponent of a closed Kac-Ward walk#✓fully proved

The exponent of a closed walk: the sum of the exponents of its transitions.

noncomputable def ons_decLoopExponent
    (L : ℕ) {n : ℕ} [NeZero n] (d : Fin n → ons_Dart L) :
    ons_DecEdge L →₀ ℕ :=
  ∑ k, ons_decTransitionExponent L (d k) (d (k + 1))

Uses 3 · Used by 6

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

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Formal-logarithm term from closed walks of given length and exponent · Coefficient of the formal Kac-Ward logarithm · Kac-Ward loops with a given squarefree exponent and nonzero scalar · Onsager's formula

DefinitionScalar of a closed Kac-Ward walk#✓fully proved

The scalar of a closed walk: the product of the scalars of its transitions.

noncomputable def ons_decLoopScalar
    (L : ℕ) (omega u v : ℂ) {n : ℕ} [NeZero n]
    (d : Fin n → ons_Dart L) : ℂ :=
  ∏ k, ons_decTransitionScalar L omega u v (d k) (d (k + 1))

Uses 2 · Used by 6

Statement usesDarts of the square-lattice torus · Scalar of a Kac-Ward transition

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Formal-logarithm term from closed walks of given length and exponent · Coefficient of the formal Kac-Ward logarithm · Kac-Ward loops with a given squarefree exponent and nonzero scalar · Onsager's formula

DefinitionTotal degree of an exponent#✓fully proved

The total degree ∑ m e of an exponent; this is Finsupp.degree.

def ons_finsuppTotalDegree {E : Type*} (m : E →₀ ℕ) : ℕ :=
  m.sum fun _ n ↦ n

Used by 5

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Coefficient of the formal Kac-Ward logarithm · Total degree of an exponent agrees with Mathlib's degree · Onsager's formula

LemmaTotal degree of an exponent agrees with Mathlib's degree#✓fully proved

ons_finsuppTotalDegree agrees with Mathlib's Finsupp.degree.

lemma ons_finsuppTotalDegree_eq_degree {E : Type*} (m : E →₀ ℕ) :
    ons_finsuppTotalDegree m = m.degree

Uses 1

Statement usesTotal degree of an exponent

DefinitionCoefficient of the formal Kac-Ward logarithm#✓fully proved

The coefficient of x^m in the formal logarithm: minus one half of the sum over closed walks of length r + 1 ≤ deg m with exponent m of their scalars divided by r + 1.

noncomputable def ons_decFormalLogCoeff
    (L : ℕ) [NeZero L] (omega u v : ℂ)
    (m : ons_DecEdge L →₀ ℕ) : ℂ :=
  -(∑ r ∈ Finset.range (ons_finsuppTotalDegree m),
      (∑ d : Fin (r + 1) → ons_Dart L,
        if ons_decLoopExponent L d = m then
          ons_decLoopScalar L omega u v d
        else 0) / ((r : ℂ) + 1)) / 2

Uses 5 · Used by 4

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Exponent of a closed Kac-Ward walk · Scalar of a closed Kac-Ward walk · Total degree of an exponent

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

DefinitionFormal logarithm of the Kac-Ward root#✓fully proved

The formal logarithm of the Kac-Ward root.

noncomputable def ons_decFormalLog
    (L : ℕ) [NeZero L] (omega u v : ℂ) :
    MvPowerSeries (ons_DecEdge L) ℂ :=
  ons_decFormalLogCoeff L omega u v

Uses 2 · Used by 4

Statement usesDecorated edges as formal-series variables · Coefficient of the formal Kac-Ward logarithm

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

DefinitionFormal Kac-Ward root#✓fully proved

The formal Kac-Ward root: the formal exponential of ons_decFormalLog.

noncomputable def ons_decFormalRoot
    (L : ℕ) [NeZero L] (omega u v : ℂ) :
    MvPowerSeries (ons_DecEdge L) ℂ :=
  PowerSeries.subst (ons_decFormalLog L omega u v)
    (PowerSeries.exp ℂ)

Uses 2 · Used by 5

Statement usesDecorated edges as formal-series variables · Formal logarithm of the Kac-Ward root

Used bySpin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Vanishing of repeated-edge coefficients of the formal Kac-Ward root · Formal Kac-Ward identity on the torus · Onsager's formula

DefinitionSquarefree exponent of a set of variables#✓fully proved

The squarefree exponent ∑_{e ∈ S} single e 1 of a set of variables.

noncomputable def ons_finsetExponent
    {E : Type*} [DecidableEq E] (S : Finset E) : E →₀ ℕ :=
  ∑ edge ∈ S, Finsupp.single edge 1

Used by 6

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 · Kac-Ward loops with a given squarefree exponent and nonzero scalar · Decorated spin polynomial · Onsager's formula

DefinitionDecorated spin polynomial#✓fully proved

The decorated spin polynomial ∑_D χ_{a,b}(hom D) ∏_{e ∈ D} x_e over decorated even subgraphs.

noncomputable def ons_decoratedSpinPolynomial
    (L : ℕ) [Fact (2 < L)] (a b : Fin 2) :
    MvPolynomial (ons_DecEdge L) ℂ :=
  ∑ D : ons_DecoratedEvenSubgraph L,
    MvPolynomial.monomial (ons_finsetExponent D.1)
      (ons_spinCharacter a b
        (ons_evenHomology L (ons_originalEdgesOfDecorated L D)) : ℂ)

Uses 12 · Used by 4

Statement usesEven subgraphs of a graph · Darts of the square-lattice torus · Decorated edges as formal-series variables · 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 · Squarefree exponent of a set of variables · 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 · Formal Kac-Ward identity on the torus · Onsager's formula

DefinitionEvaluation of a multivariate power series at weights#✓fully proved

Evaluation of a multivariate formal power series at weights, as the sum ∑_m coeff_m · weight^m.

noncomputable def ons_mvSeriesEval
    {E : Type*} (series : MvPowerSeries E ℂ) (weight : E → ℂ) : ℂ :=
  ∑' m : E →₀ ℕ,
    MvPowerSeries.coeff m series *
      m.prod (fun edge n ↦ weight edge ^ n)

Used by 3

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

DefinitionFormal Kac-Ward identity on the torus#✓fully proved

The formal Kac-Ward identity on the L × L torus: for every spin structure, the formal Kac-Ward root equals the decorated spin polynomial.

def ons_decoratedFormalKacWardIdentity
    (L : ℕ) [Fact (2 < L)] : Prop :=
  ∀ a b : Fin 2,
    ons_decFormalRoot L ons_turnRoot
        (ons_spinPhase L a) (ons_spinPhase L b) =
      (ons_decoratedSpinPolynomial L a b :
        MvPowerSeries (ons_DecEdge L) ℂ)

Uses 5 · Used by 3

Statement usesDecorated edges as formal-series variables · Formal Kac-Ward root · Decorated spin polynomial · Boundary phase \(e^{i\pi a/L}\) · Turning phase \(\omega = e^{i\pi/4}\)

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

DefinitionClosed-walk weight through a dart but not its reverse#✓fully proved

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

noncomputable def ons_decPhaseBucketE
    (L : ℕ) [NeZero L] (decWeight : ons_DecEdge L → ℂ)
    (a b : Fin 2) (e : ons_Dart L) (n : ℕ) : ℂ :=
  ∑ loop ∈ Finset.univ.filter
      (fun loop : Fin (n + 1) → ons_Dart L =>
        (∃ i, loop i = e) ∧
          ¬ ∃ j, loop j = ons_dartRev L e),
    ons_loopWeight
      (ons_KWmatDecorationWeightedPhase L decWeight ons_turnRoot
        (ons_spinPhase L a) (ons_spinPhase L b)) loop

Uses 7

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Twisted Kac-Ward matrix with decorated transition weights · Reverse of a dart · Weight of a cyclic sequence · Boundary phase \(e^{i\pi a/L}\) · Turning phase \(\omega = e^{i\pi/4}\)

DefinitionClosed-walk weight avoiding a dart and its reverse#✓fully proved

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

noncomputable def ons_decPhaseBucketN
    (L : ℕ) [NeZero L] (decWeight : ons_DecEdge L → ℂ)
    (a b : Fin 2) (e : ons_Dart L) (n : ℕ) : ℂ :=
  ∑ loop ∈ Finset.univ.filter
      (fun loop : Fin (n + 1) → ons_Dart L =>
        ¬ (∃ i, loop i = e) ∧
          ¬ ∃ j, loop j = ons_dartRev L e),
    ons_loopWeight
      (ons_KWmatDecorationWeightedPhase L decWeight ons_turnRoot
        (ons_spinPhase L a) (ons_spinPhase L b)) loop

Uses 7

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Twisted Kac-Ward matrix with decorated transition weights · Reverse of a dart · Weight of a cyclic sequence · Boundary phase \(e^{i\pi a/L}\) · Turning phase \(\omega = e^{i\pi/4}\)

DefinitionMasked closed-walk weight through a dart but not its reverse#✓fully proved

As ons_decPhaseBucketE, with the darts of forbidden masked.

noncomputable def ons_decMaskPhaseBucketE
    (L : ℕ) [NeZero L] (decWeight : ons_DecEdge L → ℂ)
    (a b : Fin 2) (forbidden : Finset (ons_Dart L))
    (e : ons_Dart L) (n : ℕ) : ℂ :=
  ∑ loop ∈ Finset.univ.filter
      (fun loop : Fin (n + 1) → ons_Dart L =>
        (∃ i, loop i = e) ∧
          ¬ ∃ j, loop j = ons_dartRev L e),
    ons_loopWeight
      (ons_maskMatrix forbidden
        (ons_KWmatDecorationWeightedPhase L decWeight ons_turnRoot
          (ons_spinPhase L a) (ons_spinPhase L b))) loop

Uses 8 · Used by 1

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Twisted Kac-Ward matrix with decorated transition weights · Reverse of a dart · Weight of a cyclic sequence · Matrix with forbidden rows and columns set to zero · Boundary phase \(e^{i\pi a/L}\) · Turning phase \(\omega = e^{i\pi/4}\)

Used byOnsager's formula

DefinitionMasked closed-walk weight avoiding a dart and its reverse#✓fully proved

As ons_decPhaseBucketN, with the darts of forbidden masked.

noncomputable def ons_decMaskPhaseBucketN
    (L : ℕ) [NeZero L] (decWeight : ons_DecEdge L → ℂ)
    (a b : Fin 2) (forbidden : Finset (ons_Dart L))
    (e : ons_Dart L) (n : ℕ) : ℂ :=
  ∑ loop ∈ Finset.univ.filter
      (fun loop : Fin (n + 1) → ons_Dart L =>
        ¬ (∃ i, loop i = e) ∧
          ¬ ∃ j, loop j = ons_dartRev L e),
    ons_loopWeight
      (ons_maskMatrix forbidden
      (ons_KWmatDecorationWeightedPhase L decWeight ons_turnRoot
          (ons_spinPhase L a) (ons_spinPhase L b))) loop

Uses 8 · Used by 1

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Twisted Kac-Ward matrix with decorated transition weights · Reverse of a dart · Weight of a cyclic sequence · Matrix with forbidden rows and columns set to zero · Boundary phase \(e^{i\pi a/L}\) · Turning phase \(\omega = e^{i\pi/4}\)

Used byOnsager's formula

DefinitionDecorated weights with one edge weight scaled by t#✓fully proved

Decorated weights with the weight of edge multiplied by t.

def ons_scaleDecEdgeWeight
    {L : ℕ} (decWeight : ons_DecEdge L → ℂ)
    (edge : ons_DecEdge L) (t : ℂ) : ons_DecEdge L → ℂ :=
  fun f => if f = edge then t * decWeight f else decWeight f

Uses 2 · Used by 5

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

Used byColumn-scaled augmented Kac-Ward matrix · Onsager's formula · Augmented Kac-Ward matrix with two side states · Balanced augmented Kac-Ward matrix · Reversal-invariant internal factor of the augmented matrix

DefinitionLog-coefficient polynomial over the cycles of a decomposition#✓fully proved

The polynomial ∑_C log-coefficient(C) x^{E(C)} over the cycles C of a fixed decomposition of an even subgraph.

noncomputable def ons_decComponentSeries
    (L : ℕ) [Fact (2 < L)] (a b : Fin 2)
    {I : Type*} [Fintype I]
    (base : I → ons_Dart L)
    (p : (i : I) → (ons_decGraph L).Walk (base i) (base i)) :
    MvPowerSeries (ons_DecEdge L) ℂ :=
  ∑ i : I, MvPowerSeries.monomial
    (ons_finsetExponent (p i).edges.toFinset)
    (ons_spinCharacter a b
      (ons_evenHomology L (ons_walkOriginalEdges (p i))) : ℂ)

Uses 7 · Used by 1

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Decorated graph of the torus · Mod 2 homology class of an edge set · Squarefree exponent of a set of variables · Spin-structure character of a mod 2 homology class · Torus edges underlying a decorated walk

Used byOnsager's formula

DefinitionSquarefree exponent#✓fully proved

An exponent is squarefree if every variable occurs with exponent at most 1.

def ons_IsSquarefreeExponent {E : Type*} (m : E →₀ ℕ) : Prop :=
  ∀ edge, m edge ≤ 1

Used by 1

Used byOnsager's formula

DefinitionFormal-logarithm term from closed walks of given length and exponent#✓fully proved

The term of the evaluated formal logarithm from closed walks of length r + 1 with exponent m, divided by r + 1 and multiplied by w^m.

noncomputable def ons_decFormalBucketTerm
    (L : ℕ) [NeZero L] (omega u v : ℂ) (decWeight : ons_DecEdge L → ℂ)
    (r : ℕ) (m : ons_DecEdge L →₀ ℕ) : ℂ :=
  ((∑ d : Fin (r + 1) → ons_Dart L,
      if ons_decLoopExponent L d = m then
        ons_decLoopScalar L omega u v d
      else 0) / ((r : ℂ) + 1)) *
    m.prod (fun edge n ↦ decWeight edge ^ n)

Uses 4 · Used by 3

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

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

DefinitionExternal part of a loop exponent#✓fully proved

The external part of a loop exponent: one for the external edge at each dart of the loop.

noncomputable def ons_decLoopExternalExponent
    (L : ℕ) {n : ℕ} [NeZero n] (d : Fin n → ons_Dart L) :
    ons_DecEdge L →₀ ℕ :=
  ∑ k, Finsupp.single s(d k, ons_dartRev L (d k)) 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

DefinitionInternal part of a loop exponent#✓fully proved

The internal part of a loop exponent: the internal edges on the paths between consecutive ports.

noncomputable def ons_decLoopInternalExponent
    (L : ℕ) {n : ℕ} [NeZero n] (d : Fin n → ons_Dart L) :
    ons_DecEdge L →₀ ℕ :=
  ∑ k, ∑ i ∈ ons_decChainPathIndices ((d (k + 1)).2 + 2) (d k).2,
    Finsupp.single (ons_decChainEdge (d k).1 i) 1

Uses 4 · 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

Used byOnsager's formula

DefinitionKac-Ward loops with a given squarefree exponent and nonzero scalar#✓fully proved

The closed Kac-Ward walks of length n with exponent the squarefree exponent of S and nonzero scalar.

noncomputable def ons_decSquarefreeLoopFinset
    (L : ℕ) [Fact (2 < L)] (a b : Fin 2)
    {n : ℕ} [NeZero n] (S : Finset (ons_DecEdge L)) :
    Finset (Fin n → ons_Dart L) :=
  Finset.univ.filter fun d ↦
    ons_decLoopExponent L d = ons_finsetExponent S ∧
      ons_decLoopScalar L ons_turnRoot
        (ons_spinPhase L a) (ons_spinPhase L b) d ≠ 0

Uses 7 · Used by 1

Statement usesDarts of the square-lattice torus · Decorated edges as formal-series variables · Exponent of a closed Kac-Ward walk · Scalar of a closed Kac-Ward walk · Squarefree exponent of a set of variables · Boundary phase \(e^{i\pi a/L}\) · Turning phase \(\omega = e^{i\pi/4}\)

Used byOnsager's formula

DefinitionDarts of a loop with their reverses#✓fully proved

The darts of a loop together with their reverses.

noncomputable def ons_decLoopRootFinset
    (L : ℕ) {n : ℕ} [NeZero n] (d : Fin n → ons_Dart L) :
    Finset (ons_Dart L) :=
  Finset.univ.image d ∪
    Finset.univ.image (fun k ↦ ons_dartRev L (d k))

Uses 2 · Used by 1

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

Used byOnsager's formula

DefinitionRotations of a loop and of its reversal#✓fully proved

The 2n rotations of a loop and of its reversal, indexed by Fin n ⊕ Fin n.

def ons_decLoopOrientation
    (L : ℕ) {n : ℕ} [NeZero n] (d : Fin n → ons_Dart L) :
    Fin n ⊕ Fin n → (Fin n → ons_Dart L)
  | Sum.inl k => ons_rotate k d
  | Sum.inr k => ons_rotate k (ons_loopRev L d)

Uses 3 · Used by 1

Statement usesDarts of the square-lattice torus · Reverse of a closed walk · Rotation of a cyclic sequence by \(k\) steps

Used byOnsager's formula

DefinitionColumn-scaled augmented Kac-Ward matrix#✓fully proved

The augmented matrix with blocks Λ₀, t U, V and 0 (scaling on the column factor).

noncomputable def ons_decMiddleAugmentedCol
    (L : ℕ) (decWeight : ons_DecEdge L → ℂ)
    (omega 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 1 1)
    (t • ons_decMiddleU L decWeight omega site)
    (ons_decMiddleV L decWeight omega 1 1 site)
    0

Uses 7

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

DefinitionRow weights of the column-scaled augmented matrix#✓fully proved

Row weights of the column-scaled augmented matrix.

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

Uses 3

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

DefinitionColumn weights of the column-scaled augmented matrix#✓fully proved

Column weights of the column-scaled augmented matrix.

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

Uses 3

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

DefinitionVanishing of repeated-edge coefficients of the formal Kac-Ward root#✓fully proved

On every L × L torus with L > 2 and for every spin structure, the coefficient of the formal Kac-Ward root at any exponent that uses some decorated edge at least twice is zero.

def ons_DecFormalRepeatedEdgeVanishes : Prop :=
  ∀ (L : ℕ) (hL : 2 < L),
    letI : Fact (2 < L) := ⟨hL⟩
    ∀ (a b : Fin 2) (m : ons_DecEdge L →₀ ℕ)
      (edge : ons_DecEdge L), 2 ≤ m edge →
      MvPowerSeries.coeff m
        (ons_decFormalRoot L ons_turnRoot
          (ons_spinPhase L a) (ons_spinPhase L b)) = 0

Uses 4 · Used by 1

Statement usesDecorated edges as formal-series variables · Formal Kac-Ward root · Boundary phase \(e^{i\pi a/L}\) · Turning phase \(\omega = e^{i\pi/4}\)

Used byOnsager's formula

DefinitionEdge-weighted spin weight of a decorated even subgraph#✓fully proved

The edge-weighted spin weight χ_{a,b}(hom F) ∏_{e ∈ F} w_e of the torus even subgraph F corresponding to a decorated even subgraph.

noncomputable def ons_decoratedWeightedSpinWeight
    (L : ℕ) [Fact (2 < L)]
    (weight : Sym2 (ZMod L × ZMod L) → ℂ) (a b : Fin 2)
    (D : ons_DecoratedEvenSubgraph L) : ℂ :=
  (ons_spinCharacter a b
      (ons_evenHomology L (ons_originalEdgesOfDecorated L D)) : ℂ) *
    ∏ edge ∈ ons_originalEdgesOfDecorated L D, weight edge

Uses 4 · Used by 4

Statement usesEven subgraphs of the decorated torus graph · 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 · Cycle removal identity for decorated even subgraphs · Onsager's formula

AbbreviationDecorated even subgraphs containing a given external edge#✓fully proved

Decorated even subgraphs that contain the external edge at d.

abbrev ons_DecoratedContainingEdge
    (L : ℕ) [Fact (2 < L)] (d : ons_Dart L) :=
  {D : ons_DecoratedEvenSubgraph L //
    s(d, ons_dartRev L d) ∈ D.1}

Uses 7 · 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

Used byCycle 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

StructureSplit of a decorated even subgraph into a rooted cycle and remainder#✓fully proved

A split of a decorated even subgraph containing the external edge at d into a simple cycle rooted at d (starting along that edge) and an even remainder disjoint from the cycle.

structure ons_DecoratedEdgeSplit
    (L : ℕ) [Fact (2 < L)] (d : ons_Dart L)
    (D : ons_DecoratedContainingEdge L d) where
  cycle : (ons_decGraph L).Walk d d
  remainder : ons_DecoratedEvenSubgraph L
  cycle_isCycle : cycle.IsCycle
  cycle_snd : cycle.snd = ons_dartRev L d
  edge_split : D.1.1 = cycle.edges.toFinset ∪ remainder.1
  edge_disjoint : Disjoint cycle.edges.toFinset remainder.1
  remainder_zero : ∀ v ∈ cycle.support, incCount remainder.1 v = 0
  remainder_zero_root : incCount remainder.1 d = 0
  remainder_zero_rev : incCount remainder.1 (ons_dartRev L d) = 0

Uses 9 · Used by 2

Statement usesEven subgraphs of a graph · Number of edges of an edge set incident to a vertex · Darts of the square-lattice torus · Decorated even subgraphs containing a given external edge · 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

Used byCycle removal identity for decorated even subgraphs · Chosen split of a decorated even subgraph at an external edge

DefinitionChosen split of a decorated even subgraph at an external edge#✓fully proved

A chosen split of a decorated even subgraph at the external edge of d.

noncomputable def ons_decoratedEdgeSplit
    (L : ℕ) [Fact (2 < L)] (d : ons_Dart L)
    (D : ons_DecoratedContainingEdge L d) :
    ons_DecoratedEdgeSplit L d D := by
  let hex := ons_decorated_split_cycle_at_external L D.1 d D.2
  let q := Classical.choose hex
  let hexR := Classical.choose_spec hex
  let R := Classical.choose hexR
  have hs := Classical.choose_spec hexR
  exact ⟨q, R, hs.1, hs.2.1, hs.2.2.1, hs.2.2.2.1,
    hs.2.2.2.2.1, hs.2.2.2.2.2.1, hs.2.2.2.2.2.2⟩

Uses 13 · 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 · Decorated even subgraphs containing a given external edge · Split of a decorated even subgraph into a rooted cycle and remainder · 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 · Internal neighbors of a dart in the decoration · Simple graph spanned by an edge set

Used byCycle removal identity for decorated even subgraphs

DefinitionCycle removal identity for decorated even subgraphs#✓fully proved

The cycle removal identity: the Kac-Ward root with d and its reverse masked, times the total first-return weight at d, equals the sum over decorated even subgraphs through d of the first-return weight of the split-off cycle times the spin weight of the remainder.

StatMech.Onsager.ons_decoratedCycleRemovalIdentity · 19 lines

def ons_decoratedCycleRemovalIdentity (L : ℕ) [Fact (2 < L)] : Prop :=
  ∀ (a b : Fin 2)
    (weight : Sym2 (ZMod L × ZMod L) → ℂ) (d : ons_Dart L),
    ons_detWalkRoot
        (ons_maskMatrix ({d, ons_dartRev L d} : Finset (ons_Dart L))
          (ons_KWmatWeightedPhase L weight ons_turnRoot
            (ons_spinPhase L a) (ons_spinPhase L b))) *
      (∑' s, ons_firstReturnWeight
        (ons_KWmatWeightedPhase L weight ons_turnRoot
          (ons_spinPhase L a) (ons_spinPhase L b))
        d (ons_dartRev L d) s) =
      ∑ D : ons_DecoratedContainingEdge L d,
        ons_edgeWeight
            (ons_KWmatWeightedPhase L weight ons_turnRoot
              (ons_spinPhase L a) (ons_spinPhase L b))
            (ons_decCycleFirstReturn
              (ons_decoratedEdgeSplit L d D).cycle) *
          ons_decoratedWeightedSpinWeight L weight a b
            (ons_decoratedEdgeSplit L d D).remainder

Uses 19

Statement usesEven subgraphs of a graph · Darts of the square-lattice torus · Decorated even subgraphs containing a given external edge · Split of a decorated even subgraph into a rooted cycle and remainder · Even subgraphs of the decorated torus graph · Edge-weighted Kac-Ward matrix with direction phases · Reverse of a dart · Adjacency of the decorated torus graph · First-return loop of a rooted decorated cycle · Decorated graph of the torus · Internal adjacency of the torus decoration · Chosen split of a decorated even subgraph at an external edge · Edge-weighted spin weight of a decorated even subgraph · Walk-series square root of det(1 − Λ) · Edge weight of a walk · Weight of a first-return segment avoiding a state · Matrix with forbidden rows and columns set to zero · Boundary phase \(e^{i\pi a/L}\) · Turning phase \(\omega = e^{i\pi/4}\)

DefinitionDegree-\(n\) part of a power series evaluated at a point#✓fully proved

The sum of the terms of total degree n of a series evaluated at w.

noncomputable def ons_degreeFiberCoeff
    {E : Type*} (series : MvPowerSeries E ℂ)
    (weight : E → ℂ) (n : ℕ) : ℂ :=
  ∑' m : {m : E →₀ ℕ // Finsupp.degree m = n},
    MvPowerSeries.coeff m.1 series * ons_mvMonomialValue weight m.1

Uses 1 · Used by 1

Statement usesValue of a monomial at weights

Used byOnsager's formula

DefinitionSum of absolute values of the degree-\(n\) terms at a point#✓fully proved

The sum of the absolute values of the terms of total degree n evaluated at w.

noncomputable def ons_degreeFiberNorm
    {E : Type*} (series : MvPowerSeries E ℂ)
    (weight : E → ℂ) (n : ℕ) : ℝ :=
  ∑' m : {m : E →₀ ℕ // Finsupp.degree m = n},
    ‖MvPowerSeries.coeff m.1 series * ons_mvMonomialValue weight m.1‖

Uses 1 · Used by 1

Statement usesValue of a monomial at weights

Used byOnsager's formula

DefinitionHomogeneous degree-\(n\) part of a power series as a polynomial#✓fully proved

The homogeneous degree-n part of a series as a polynomial (finitely many variables).

noncomputable def ons_degreeFiberPolynomial
    {E : Type*} [Fintype E] [DecidableEq E]
    (series : MvPowerSeries E ℂ) (n : ℕ) : MvPolynomial E ℂ :=
  ∑ m ∈ (Finsupp.finite_of_degree_le (σ := E) n).toFinset.filter
      (fun m ↦ Finsupp.degree m = n),
    MvPolynomial.monomial m (MvPowerSeries.coeff m series)

Used by 1

Used byOnsager's formula

DefinitionSpin-character sums squared as twisted determinants at activity \(x\)#✓fully proved

For every spin structure (a, b), the square of the spin-character sum equals the twisted Kac-Ward determinant det (1 - Λ_{ab}) at activity x.

def ons_spinCoefficientIdentity (L : ℕ) [Fact (2 < L)] (x : ℝ) : Prop :=
  ∀ a b : Fin 2,
    (ons_spinCharacterSum L x a b : ℂ) ^ 2 =
      (1 - ons_KWmatPhase L (x : ℂ) ons_turnRoot
        (ons_spinPhase L a) (ons_spinPhase L b)).det

Uses 5 · Used by 3

Statement usesDarts of the square-lattice torus · Twisted Kac-Ward matrix with direction phases · Spin-character sum over even subgraphs of the torus · Boundary phase \(e^{i\pi a/L}\) · Turning phase \(\omega = e^{i\pi/4}\)

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

DefinitionSector weight of a homology class as a polynomial#✓fully proved

The sector weight of the homology class h as a real polynomial in x.

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

Uses 4 · Used by 7

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 bySpin Kac-Ward identities from the decorated-torus formal identity · Spin Kac-Ward identities from the edge-weighted root identity · Onsager's formula · Signed sector polynomial with the \((1,1)\) sector negated · Signed sector polynomial with the \((0,1)\) sector negated · Signed sector polynomial with the \((1,0)\) sector negated · Signed sector polynomial with only the \((0,0)\) sector positive

DefinitionSigned sector polynomial with the \((1,1)\) sector negated#✓fully proved

The signed sector sum ons_spin00 as a polynomial.

noncomputable def ons_spinPoly00 (L : ℕ) [Fact (2 < L)] : Polynomial ℝ :=
  ons_sectorPoly L (0, 0) + ons_sectorPoly L (1, 0) +
    ons_sectorPoly L (0, 1) - ons_sectorPoly L (1, 1)

Uses 1 · Used by 3

Statement usesSector weight of a homology class as a polynomial

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

DefinitionSigned sector polynomial with the \((1,0)\) sector negated#✓fully proved

The signed sector sum ons_spin10 as a polynomial.

noncomputable def ons_spinPoly10 (L : ℕ) [Fact (2 < L)] : Polynomial ℝ :=
  ons_sectorPoly L (0, 0) - ons_sectorPoly L (1, 0) +
    ons_sectorPoly L (0, 1) + ons_sectorPoly L (1, 1)

Uses 1 · Used by 3

Statement usesSector weight of a homology class as a polynomial

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

DefinitionSigned sector polynomial with the \((0,1)\) sector negated#✓fully proved

The signed sector sum ons_spin01 as a polynomial.

noncomputable def ons_spinPoly01 (L : ℕ) [Fact (2 < L)] : Polynomial ℝ :=
  ons_sectorPoly L (0, 0) + ons_sectorPoly L (1, 0) -
    ons_sectorPoly L (0, 1) + ons_sectorPoly L (1, 1)

Uses 1 · Used by 3

Statement usesSector weight of a homology class as a polynomial

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

DefinitionSigned sector polynomial with only the \((0,0)\) sector positive#✓fully proved

The signed sector sum ons_spin11 as a polynomial.

noncomputable def ons_spinPoly11 (L : ℕ) [Fact (2 < L)] : Polynomial ℝ :=
  ons_sectorPoly L (0, 0) - ons_sectorPoly L (1, 0) -
    ons_sectorPoly L (0, 1) - ons_sectorPoly L (1, 1)

Uses 1 · Used by 3

Statement usesSector weight of a homology class as a polynomial

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

DefinitionSector determinant as a function of \(x\)#✓fully proved

The sector determinant as a function of x: the product over shifted momenta of (1 + x²)² - 2x(1 - x²)(cos k₁ + cos k₂).

noncomputable def ons_spinDetX (L : ℕ) (x : ℝ) (a b : Fin 2) : ℝ :=
  ∏ i ∈ Finset.range L, ∏ j ∈ Finset.range L,
    ((1 + x ^ 2) ^ 2 - 2 * x * (1 - x ^ 2) *
      (Real.cos (2 * Real.pi * (i + (a.val : ℝ) / 2) / L) +
        Real.cos (2 * Real.pi * (j + (b.val : ℝ) / 2) / L)))

Used by 4

Used bySpin 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\)

DefinitionSector determinant as a real polynomial#✓fully proved

The sector determinant as a real polynomial in x.

noncomputable def ons_spinDetPoly (L : ℕ) (a b : Fin 2) : Polynomial ℝ :=
  ∏ i ∈ Finset.range L, ∏ j ∈ Finset.range L,
    ((1 + X ^ 2) ^ 2 -
      C (2 * (Real.cos (2 * Real.pi * (i + (a.val : ℝ) / 2) / L) +
        Real.cos (2 * Real.pi * (j + (b.val : ℝ) / 2) / L))) * X * (1 - X ^ 2))

Used by 3

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

DefinitionFour spin Kac-Ward identities on the torus at activity \(x\)#✓fully proved

The four spin Kac-Ward identities spin_{ab}(x)² = det_{ab}(x) on the L × L torus at activity x.

def ons_spinKacWardAt (L : ℕ) [Fact (2 < L)] (x : ℝ) : Prop :=
  ons_spin11 L x ^ 2 = ons_spinDetX L x 0 0 ∧
  ons_spin01 L x ^ 2 = ons_spinDetX L x 1 0 ∧
  ons_spin10 L x ^ 2 = ons_spinDetX L x 0 1 ∧
  ons_spin00 L x ^ 2 = ons_spinDetX L x 1 1

Uses 5 · Used by 3

Statement usesSigned sector sum \(Z_{00} + Z_{10} + Z_{01} - Z_{11}\) · Signed sector sum \(Z_{00} + Z_{10} - Z_{01} + Z_{11}\) · Signed sector sum \(Z_{00} - Z_{10} + Z_{01} + Z_{11}\) · Signed sector sum \(Z_{00} - Z_{10} - Z_{01} - Z_{11}\) · Sector determinant as a function of \(x\)

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

DefinitionWeighted character sum over even subgraphs containing an edge#✓fully proved

The part of the edge-weighted character sum coming from even subgraphs that contain edge.

noncomputable def ons_weightedSpinEdgeCoefficient
    (L : ℕ) [Fact (2 < L)]
    (weight : Sym2 (ZMod L × ZMod L) → ℂ)
    (a b : Fin 2) (edge : Sym2 (ZMod L × ZMod L)) : ℂ :=
  ∑ F ∈ (evenSubgraphs (onsTorusGraph L)).filter (edge ∈ ·),
    (ons_spinCharacter a b (ons_evenHomology L F) : ℂ) *
      ∏ f ∈ F, weight f

Uses 5 · Used by 1

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 byEdge coefficient identity on the \(L \times L\) torus

DefinitionEdge weights restricted to a set of edges#✓fully proved

The edge weights restricted to S: equal to weight on S and 0 elsewhere.

def ons_restrictEdgeWeight
    {L : ℕ} (weight : Sym2 (ZMod L × ZMod L) → ℂ)
    (S : Finset (Sym2 (ZMod L × ZMod L))) :
    Sym2 (ZMod L × ZMod L) → ℂ :=
  fun edge => if edge ∈ S then weight edge else 0

DefinitionEdge coefficient identity on the \(L \times L\) torus#✓fully proved

The edge coefficient identity on the L × L torus: for small weights, the part of the edge-weighted character sum from even subgraphs through the edge of e equals minus the Kac-Ward root with e and its reverse masked, times the total first-return weight at e.

StatMech.Onsager.ons_weightedEdgeCoefficientIdentity · 16 lines

def ons_weightedEdgeCoefficientIdentity (L : ℕ) [Fact (2 < L)] : Prop :=
  ∀ (a b : Fin 2)
    (weight : Sym2 (ZMod L × ZMod L) → ℂ) (q : ℝ),
    0 ≤ q →
    (∀ edge, ‖weight edge‖ ≤ q) →
    q < (2 * (Fintype.card (ons_Dart L) : ℝ) ^ 2)⁻¹ →
    ∀ e : ons_Dart L,
    ons_weightedSpinEdgeCoefficient L weight a b (ons_portEdge L e) =
      -ons_detWalkRoot
          (ons_maskMatrix ({e, ons_dartRev L e} : Finset (ons_Dart L))
            (ons_KWmatWeightedPhase L weight ons_turnRoot
              (ons_spinPhase L a) (ons_spinPhase L b))) *
        (∑' s, ons_firstReturnWeight
          (ons_KWmatWeightedPhase L weight ons_turnRoot
            (ons_spinPhase L a) (ons_spinPhase L b))
          e (ons_dartRev L e) s)

Uses 10

Statement usesDarts of the square-lattice torus · Edge-weighted Kac-Ward matrix with direction phases · Reverse of a dart · Walk-series square root of det(1 − Λ) · Weight of a first-return segment avoiding a state · Matrix with forbidden rows and columns set to zero · Torus edge underlying a dart · Boundary phase \(e^{i\pi a/L}\) · Turning phase \(\omega = e^{i\pi/4}\) · Weighted character sum over even subgraphs containing an edge

DefinitionEdge-weighted spin-character sum over even subgraphs#✓fully proved

The edge-weighted spin-character sum ∑_F χ_{a,b}(hom F) ∏_{e ∈ F} w_e over even subgraphs of the torus.

noncomputable def ons_weightedSpinCharacterSum
    (L : ℕ) [Fact (2 < L)]
    (weight : Sym2 (ZMod L × ZMod L) → ℂ)
    (a b : Fin 2) : ℂ :=
  ∑ F ∈ evenSubgraphs (onsTorusGraph L),
    (ons_spinCharacter a b (ons_evenHomology L F) : ℂ) *
      ∏ edge ∈ F, weight edge

Uses 5 · Used by 5

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 · Edge-weighted root identity from the decorated-torus formal identity · Onsager's formula · Edge-weighted root identity on the torus

DefinitionEdge-weighted root identity on the torus#✓fully proved

The edge-weighted root identity on the L × L torus: for every spin structure and every edge weight bounded by q below Sherman's radius, the walk-series square root of the twisted edge-weighted Kac-Ward determinant equals the edge-weighted character sum.

def ons_weightedRootIdentity (L : ℕ) [Fact (2 < L)] : Prop :=
  ∀ (a b : Fin 2)
    (weight : Sym2 (ZMod L × ZMod L) → ℂ) (q : ℝ),
    0 ≤ q →
    (∀ edge, ‖weight edge‖ ≤ q) →
    q < (2 * (Fintype.card (ons_Dart L) : ℝ) ^ 2)⁻¹ →
    ons_detWalkRoot
        (ons_KWmatWeightedPhase L weight ons_turnRoot
          (ons_spinPhase L a) (ons_spinPhase L b)) =
      ons_weightedSpinCharacterSum L weight a b

Uses 6 · Used by 4

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

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

DefinitionSherman's radius for \(L > 2\), with value 1 otherwise#✓fully proved

Sherman's radius for L > 2, and 1 otherwise.

noncomputable def ons_spinShermanRadius (L : ℕ) : ℝ :=
  if h : 2 < L then
    letI : NeZero L := ⟨by omega⟩
    ons_ShermanRadius L
  else 1

Uses 1 · Used by 3

Statement usesSherman's convergence radius for the torus Kac-Ward matrix

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

DefinitionSecond-difference factor for a monomial of degree k#✓fully proved

The factor 2^k - 2 + 0^k by which a second difference multiplies a monomial of degree k in one variable.

def ons_secondDifferenceFactor (k : ℕ) : ℂ :=
  (2 : ℂ) ^ k - 2 + (0 : ℂ) ^ k

Used by 2

Used bySecond difference of a formal series in one variable · Onsager's formula

DefinitionSecond difference of a formal series in one variable#✓fully proved

The second difference of a formal series in the variable edge: the coefficient at m is multiplied by 2^{m edge} - 2 + 0^{m edge}.

noncomputable def ons_decFormalSecondDifference
    {L : ℕ} (series : MvPowerSeries (ons_DecEdge L) ℂ)
    (edge : ons_DecEdge L) : MvPowerSeries (ons_DecEdge L) ℂ :=
  fun m ↦ ons_secondDifferenceFactor (m edge) *
    MvPowerSeries.coeff m series

Uses 2 · Used by 1

Statement usesDecorated edges as formal-series variables · Second-difference factor for a monomial of degree k

Used byOnsager's formula

TheoremOnsager's formula#✓fully proved

Onsager's formula for the zero-field square-lattice Ising model, in the form torus pressure → ons_pressure β for β ≥ 0 (L. Onsager, Crystal statistics. I, 1944). See main_free_energy for the explicit integral.

theorem ons_free_energy
    (beta : ℝ) (hbeta : 0 ≤ beta) :
    Filter.Tendsto (ons_torusPressureSeq beta)
      Filter.atTop (nhds (ons_pressure beta))

Uses 283 · Used by 1

Statement usesOnsager's pressure of the square-lattice Ising model · Torus pressure sequence of the zero-field Ising model

Proof usesConfiguration space of a statistical-mechanics model · Even subgraph condition on an edge set · Partition function of a finite system · Bond variable of an unordered pair · Even subgraphs of a graph · Ising Hamiltonian on a finite graph · Number of edges of an edge set incident to a vertex · Spin of a configuration at a site · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Hopf's Umlaufsatz · Forward vertex recursion of a closed lattice walk · Closed lattice walk starts at the origin · Nearest-neighbor adjacency on the discrete torus · The \(L \times L\) square-lattice torus graph · Darts of the square-lattice torus · Decorated edges as formal-series variables · Vanishing of repeated-edge coefficients of the formal Kac-Ward root · Micro point of the finer torus as a cell and an offset · Even subgraphs of the decorated torus graph · Squarefree exponent · Block of the twisted Kac-Ward matrix between a site and the origin · Kac–Ward matrix of the square-lattice torus · Twisted Kac-Ward matrix with decorated transition weights · Twisted Kac-Ward matrix with direction phases · Edge-weighted Kac-Ward matrix · Edge-weighted Kac-Ward matrix with direction phases · Fourier symbol of one minus the Kac-Ward matrix · Limit statement for \(\log X_L(\tanh\beta)/L^2\) on the torus · Absolute summability of a power series evaluated at weights · Port pattern on the darts of the torus · Sherman's convergence radius for the torus Kac-Ward matrix · Even-subgraph generating function of a graph · Zero-field Ising partition function with unit couplings · States of the first \(N + 1\) periods of a periodic walk · Periodic lift anchored at the base point · Critical inverse temperature ½ log(1 + √2) of the square lattice · Kramers-Wannier critical point · β_c is the unique positive solution of sinh 2β = 1 · Two-dimensional block-circulant matrix on the torus · Fourier symbol of a two-dimensional block-circulant matrix · Uniform bound constant for the inner integrals near β_c · Integrable dominating function for log g near the critical point · Rotation of a cyclic sequence by one step · Cyclic turning sum of a direction list · Edge set of a closed walk of darts · Reverse of a dart · Adjacency of the decorated torus graph · Internal edge of the path at a site · Internal edges between two ports at a site · Indices of internal edges between two ports · Log-coefficient polynomial over the cycles of a decomposition · 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 · Interior points of the route of a decorated edge · Four finer-torus darts along the route of a decorated edge · Projection of a decorated edge to the torus · Four-step route of a decorated edge in the finer torus · Step directions of the route of a decorated edge · Five points of the route of a decorated edge · 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 · 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 · One-edge decorated walk along an external edge · Formal-logarithm term from closed walks of given length and exponent · Formal logarithm of the Kac-Ward root · Coefficient of the formal Kac-Ward logarithm · Formal Kac-Ward root · Second difference of a formal series in one variable · Darts of a Kac-Ward loop in walking order · Head-to-tail relation between darts · Decorated graph of the torus · Cell offsets used by interior route points · Internal adjacency of the torus decoration · Internal neighbors of a dart in the decoration · Externality of a decorated edge · Transition exponent sum along a dart chain · Last dart of a dart chain · Exponent of a closed Kac-Ward walk · External part of a loop exponent · Internal part of a loop exponent · Rotations of a loop and of its reversal · Darts of a loop with their reverses · Scalar of a closed Kac-Ward walk · Closed decorated walk of a valid Kac-Ward loop · Masked closed-walk weight through a dart but not its reverse · Masked closed-walk weight avoiding a dart and its reverse · Decorated edge whose route passes through an interior micro point · Point of the finer torus represented by a micro point · Directions of augmented states · Reversal on augmented states · Augmented Kac-Ward matrix with two side states · Balanced augmented Kac-Ward matrix · Column weights of the balanced augmented matrix · Row weights of the balanced augmented matrix · Column weights of the augmented Kac-Ward matrix · Destination-side internal weight to a port · Representative direction of a side · Reversal-invariant internal factor of the augmented matrix · Row weights of the augmented Kac-Ward matrix · Side of a direction at a site · Source-side internal weight from a port · Column factor of the rank-two middle-edge term · Row factor of the rank-two middle-edge term · Internal path between two ports at a site · Micro point at which a dart is placed · Decorated weights induced by torus edge weights · Kac-Ward loops with a given squarefree exponent and nonzero scalar · Exponent of a Kac-Ward transition · Scalar of a Kac-Ward transition · Decorated walk of a Kac-Ward transition · Decorated weight of a Kac-Ward transition · Edge multiset of a decorated walk as an exponent · External darts of a decorated walk in order · Decorated walk of a chain of darts · External edges of a decorated edge set · Formal Kac-Ward identity on the torus · Decorated character sum with weights on all edges · Port bit of a dart in a decorated edge set · Decorated spin polynomial · Edge-weighted spin weight of a decorated even subgraph · Equivalence between even subgraphs of the torus and its decoration · Degree-\(n\) part of a power series evaluated at a point · Sum of absolute values of the degree-\(n\) terms at a point · Homogeneous degree-\(n\) part of a power series as a polynomial · Walk-series square root of det(1 − Λ) · Diagonal gauge conjugation of a matrix · Horizontal displacement of a step in a direction · Vertical displacement of a step in a direction · Boundary phase of a step in a direction · Neighbouring site in a given direction on the torus · \(N\) repetitions of a direction sequence · Indicator bit of an edge in an edge set · Mod 2 intersection number of two torus edge sets · Intersection number of torus edge sets in the field \(\mathbb{Z}/2\) · Simple graph spanned by an edge set · Edge weight of a walk · Mod 2 homology class of an edge set · Majorant \(q^{|s|-1}\) for the weight of a walk · Squarefree exponent of a set of variables · Total degree of an exponent · First-return segments of a closed walk · Splitting a list at the occurrences of a root · Weight of a first-return segment avoiding a state · Torus walk of four lattice steps · Endpoint of four lattice steps · Onsager's free-energy double integral · Onsager integrand of the square-lattice Ising model · Gluing of walk segments at a root · Positions where a sequence meets an edge or its reverse · Intersection form on the mod 2 homology of the torus · Horizontal edge bit of an edge set at a site · Horizontal edge bit as an element of \(\mathbb{Z}/2\) · High-temperature expansion · Parity of an integer as a bit · Micro directions along internal decorated edges at a site · Reversal of a cyclic sequence of states · First-return segment at a state · First position meeting an edge or its reverse · Last element of \(\{0, \ldots, n - 1\}\) · Sherman's Lemma 5 · Base point in \(\mathbb{Z}^2\) over the start of a torus loop · Direction sequence of the lift of a closed torus walk · Sites of a closed torus walk in lift order · Term of the list series: product of weights over length · Signed boundary coefficient along a torus loop · Reverse of a closed walk · Cyclic sequences visiting two given states · Weight of a cyclic sequence · Last position meeting the reverse of the first hit · Positions meeting the reverse of the first hit · Matrix with forbidden rows and columns set to zero · Matrix bucket: walks through one state avoiding another · Matrix bucket: walks avoiding two given states · Mirror position within a segment · Value of a monomial at weights · Evaluation of a multivariate power series at weights · Sum of absolute values of an evaluated power series · \(1 - z \neq 0\) for \(|z| < 1\) · Open turning sum of a direction list · Torus even subgraph of a decorated even subgraph · Signed boundary coefficient on an outgoing edge · Outside connector around the bounding box of a periodic arc · Lattice points visited by the outside connector · Total displacement of a list of lattice directions · Lattice points visited by a path from the origin · Lattice point of a period state · States of one period of a periodic walk · Directions along a periodic arc · States of a periodic arc across \(N\) periods · Points of the periodic lift of a torus loop · Torus edge underlying a dart · Adjacency of directions along the port line · Torus edge set of a port pattern · Port pattern of an even decorated subgraph · Finite-volume pressure · Reduction of a lattice site to the torus · Reversal of a segment of a cyclic sequence · Rooted closed walks as lists of first-return segments · Rooted term: walk weight over its number of first-return factors · Rotation of a cyclic sequence by \(k\) steps · Rotation by \(k\) as an equivalence of sequences · Rotation of a lattice point by quarter turns · Matrix with selected columns scaled · Decorated weights with one edge weight scaled by t · Second-difference factor for a monomial of degree k · Sector 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)\) · Sector weight of a homology class as a polynomial · Sector weight of a homology class · Translation of a dart by a lattice vector · Signed potential difference across a horizontal edge · Signed potential difference across a vertical edge · Primitive L-th root of unity \(e^{2\pi i/L}\) · Signed sector sum \(Z_{00} + Z_{10} + Z_{01} - Z_{11}\) · Signed sector sum \(Z_{00} + Z_{10} - Z_{01} + Z_{11}\) · Signed sector sum \(Z_{00} - Z_{10} + Z_{01} + Z_{11}\) · Signed sector sum \(Z_{00} - Z_{10} - Z_{01} - Z_{11}\) · Spin-structure character of a mod 2 homology class · Spin-character sum over even subgraphs of the torus · Spin-character sums squared as twisted determinants at activity \(x\) · Seam sign of a dart · Sector determinant with boundary phases · Sector determinant as a real polynomial · Sector determinant as a function of \(x\) · Four spin Kac-Ward identities on the torus at activity \(x\) · Spin Kac-Ward identities at inverse temperature \(\beta\) · Linear character of the boundary phases · Boundary phase \(e^{i\pi a/L}\) · Signed sector polynomial with the \((1,1)\) sector negated · Signed sector polynomial with the \((0,1)\) sector negated · Signed sector polynomial with the \((1,0)\) sector negated · Signed sector polynomial with only the \((0,0)\) sector positive · Decorated weights twisted by seam signs · Sherman's radius for \(L > 2\), with value 1 otherwise · Spin boundary-phase gauge at a site · State-weighted reversible turn matrix · Sherman's segment-reversal surgery · Kac-Ward symbol determinant at t = tanh β · Integer turn exponent between two directions · Turning phase \(\omega = e^{i\pi/4}\) · Turn weight between two lattice directions · Turn between two directions as an element of \(\mathbb{Z}/4\) · List of first-return segments avoiding a state · Rooted closed walk at a state avoiding another · Vertical edge bit of an edge set at a site · Vertical edge bit as an element of \(\mathbb{Z}/2\) · Number of visits of a sequence to a state · Directions of the expanded dart list of a decorated walk · Directions of the external darts of a decorated walk · External edges used by a decorated walk · Torus edges underlying a decorated walk · Edge-weighted root identity on the torus · Edge-weighted spin-character sum over even subgraphs · Mod 2 homology class of a winding · Translation of \(\mathbb{Z}^2\) for a winding around the torus · Horizontal flux of an edge set through a column · Edges crossing the vertical seam of the torus · Vertical-seam edge in a given row · Crossing of the vertical seam by a dart · Signed crossing of the vertical seam by a dart · Vertical flux of an edge set through a row · Edges crossing the horizontal seam of the torus · Horizontal-seam edge in a given column · Crossing of the horizontal seam by a dart · Signed crossing of the horizontal seam by a dart · Horizontal part of the zero-flux potential construction · Face potential of an even subgraph of zero homology · Vertical part of the zero-flux potential construction · Prefix sum of a function on \(\mathbb{Z}/L\) · Trace of a power as a power sum of characteristic roots

Used byOnsager's formula

71 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.