Multilinear polynomials and Asano contraction

Multilinear polynomials

MultilinPoly ι is a function Finset ι → ℂ giving the coefficient of each monomial ∏_{i ∈ X} z_i. Used here and in LeeYang.lean.

Asano contraction

The Asano contraction merges two variables of a multilinear polynomial by keeping only the "both present" and "both absent" parts. The main result asanoContraction_nonvanishing shows that contraction preserves non-vanishing on the unit polydisk.

Reference: Friedli–Velenik, Proposition 3.44, §3.7, pp. 122–127.

Multilinear polynomials

@[reducible, inline]

abbrev IsingModel.MultilinPoly (ι : Type u_2) [Fintype ι] : Type u_2

A multilinear polynomial over ℂ with variables indexed by ι. The coefficient p X corresponds to the monomial ∏_{i ∈ X} z_i.

Equations

• IsingModel.MultilinPoly ι = (Finset ι → ℂ)

noncomputable def IsingModel.MultilinPoly.eval {ι : Type u_1} [Fintype ι] (p : MultilinPoly ι) (z : ι → ℂ) : ℂ

Evaluate a multilinear polynomial at z : ι → ℂ.

Equations

• p.eval z = ∑ X : Finset ι, p X * ∏ i ∈ X, z i

Asano contraction

def IsingModel.MultilinPoly.asanoContract {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : MultilinPoly ι) (i j : ι) (_hij : i ≠ j) : MultilinPoly ι

Asano contraction: given a polynomial p on ι and two distinct variables i, j : ι, contract j into i. The result is a polynomial on ι that does not depend on j.

Mathematically: write P = P_{--} z_i z_j + P_{+-} z_j + P_{-+} z_i + P_{++}. The contraction is P_{--} z_i + P_{++}.

In terms of coefficients:

• For X with i ∈ X: (contract p i j)(X) = p(X ∪ {j}) (the P_{--} part)
• For X with i ∉ X: (contract p i j)(X) = p(X) (the P_{++} part)
• For X with j ∈ X: (contract p i j)(X) = 0 (contracted variable is eliminated)

Reference: Friedli–Velenik, pp. 123–124.

Equations

• p.asanoContract i j _hij X = if j ∈ X then 0 else if i ∈ X then p (insert j X) else p X

Asano contraction preserves non-vanishing

theorem IsingModel.bilinear_nonvanishing (a b c d : ℂ) (hf : ∀ (z w : ℂ), ‖z‖ < 1 → ‖w‖ < 1 → a * z * w + b * w + c * z + d ≠ 0) (z : ℂ) (hz : ‖z‖ < 1) : a * z + d ≠ 0

Bilinear non-vanishing lemma: if f(z,w) = azw + bw + cz + d does not vanish on the open unit bidisk |z|,|w| < 1, then az + d does not vanish on |z| < 1. This is the algebraic core of Asano contraction.

The proof shows normSq d ≥ normSq a by combining norm bounds from the z- and w-directions via the parallelogram law. Then az₀ + d = 0 would require ‖z₀‖ = ‖d/a‖ ≥ 1, contradicting ‖z₀‖ < 1.

Reference: Friedli–Velenik, Proposition 3.44 (algebraic core).

theorem IsingModel.MultilinPoly.asanoContract_nonvanishing {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : MultilinPoly ι) (i j : ι) (hij : i ≠ j) (hp : ∀ (z : ι → ℂ), (∀ (k : ι), ‖z k‖ < 1) → p.eval z ≠ 0) (z : ι → ℂ) : (∀ (k : ι), ‖z k‖ < 1) → (p.asanoContract i j hij).eval z ≠ 0

Key property: Asano contraction preserves non-vanishing on the open unit polydisk.

Write P = P_{--} z_i z_j + P_{+-} z_j + P_{-+} z_i + P_{++}. The contraction is Q(z) = P_{--}(z) z_i + P_{++}(z). If Q(z₀) = 0 for some z₀ with |z₀_k| < 1 ∀k, then z₀_i = -P_{++}/P_{--}. But P(z₀_with_j=w) = P_{--} z₀_i w + P_{+-} w + P_{-+} z₀_i + P_{++} is linear in w, and vanishes at w = -(P_{-+} z₀_i + P_{++})/(P_{--} z₀_i + P_{+-}). The hypothesis says this w must have |w| ≥ 1. But by algebraic manipulation, |w| < 1 leads to a contradiction.

Base case: single edge

def IsingModel.singleEdgePoly {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i j : ι) (t : ℝ) : MultilinPoly ι

The partition polynomial for a single edge {i, j} with coupling t = e^{-2β}: P(z_i, z_j) = z_i z_j + t(z_i + z_j) + 1 where 0 ≤ t < 1.

Equations

• IsingModel.singleEdgePoly i j t X = if X = {i, j} then 1 else if X = {i} then ↑t else if X = {j} then ↑t else if X = ∅ then 1 else 0

theorem IsingModel.norm_tz_add_one_gt (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t < 1) (z : ℂ) (hz : ‖z‖ < 1) : ‖z + ↑t‖ < ‖↑t * z + 1‖

‖tz + 1‖ > ‖z + t‖ when 0 ≤ t < 1 and ‖z‖ < 1. This is the norm inequality underlying the Möbius transformation property.

theorem IsingModel.singleEdgePoly_nonvanishing {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i j : ι) (hij : i ≠ j) (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t < 1) (z : ι → ℂ) (hz : ∀ (k : ι), ‖z k‖ < 1) : (singleEdgePoly i j t).eval z ≠ 0

The single-edge polynomial does not vanish on the open unit polydisk. If P(z_i, z_j) = 0, then z_i = -(tz_j+1)/(z_j+t), but the Möbius transformation maps |z_j| < 1 to |z_i| > 1, contradiction.