The Lee–Yang circle property for a single edge and for matchings

4 fully proved

A. The single edge

DefinitionSingle-edge graph on two vertices#✓fully proved

The graph on two vertices joined by one edge.

def twoVertexEdge : SimpleGraph (Fin 2) := ⊤

Used by 1

Used byPerfect matching with n edges

B. The Lee–Yang circle property

DefinitionLee–Yang circle property of a graph#✓fully proved

The Lee–Yang circle property: every complex zero of the Lee–Yang polynomial of G at inverse temperature β has modulus one.

def HasLeeYangCircle {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (beta : ℝ) : Prop :=
  ∀ z : ℂ, (leeYangComplexPolynomial G beta).eval z = 0 → ‖z‖ = 1

Uses 1 · Used by 1

Statement usesLee–Yang polynomial with complex coefficients

Used byLee–Yang circle theorem

C. Finite matchings

DefinitionVertex type of the perfect matching with n edges#✓fully proved

The vertex type of the perfect matching with n edges: n disjoint copies of Fin 2.

def MatchingVertex : ℕ → Type
  | 0 => Empty
  | n + 1 => Fin 2 ⊕ MatchingVertex n

Used by 1

Used byPerfect matching with n edges

DefinitionPerfect matching with n edges#✓fully proved

The perfect matching with n edges, the disjoint union of n single edges.

def finiteMatching : (n : ℕ) → SimpleGraph (MatchingVertex n)
  | 0 => ⊥
  | n + 1 => twoVertexEdge ⊕g finiteMatching n

Uses 2

Statement usesVertex type of the perfect matching with n edges · Single-edge graph on two vertices

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.