Definitions for Entanglement Entropy in the O(N) model

Definition

QAlgorithms_Papers_Independent_Intakethird100_P31

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

The objects the formalized statements of Entanglement Entropy in the O(N) model (arXiv:0904.4477) are stated in. Each was checked against the paper by a blind read-back and a moderator.

transverseHeatTerm: Summand of the shifted transverse heat trace, PDF p.30, (5.26).
transverseHeat: Shifted one-dimensional heat trace, PDF p.30, (5.26). Only positive heat times are used in the statements.
transverseIntegral: Heat-kernel continuation of the transverse reciprocal-square sum, PDF p.30, (5.25). Its convergent domain is 2 < D < 4 and nonzero twist.
squareHeat: The massless square torus has side 2*pi. Its heat kernel is defined spectrally, independently of the theta formula; PDF p.27, (5.13)--(5.14).
OffSquareLattice: Off the lattice of source points of the side-2*pi square torus.
squareGreen: Zero-mode-removed inverse Laplacian on the square torus, constructed by the heat kernel. The pointwise integral is used only off its source lattice; its logarithmic singularity is locally integrable. PDF p.27.
oddThetaAtI: Odd Jacobi theta function at modulus i, with argument of period one, using its convergent sine series, in the convention of PDF p.27, (5.14).
etaAtI: Positive real value of Dedekind eta at i. Mathlib defines eta by exp(pi*i*z/12) times the product of 1-exp(2*pi*i*(j+1)*z).
geometricProfile: Analytic coefficient profile on the right-hand side of (5.31), PDF p.30. This definition does not assert a physical entropy/partition-function identity; that calculation is the separately deferred node #5.31.
reducedGap: The reduced small-alpha gap equation, PDF p.37, (6.33). This is the specified asymptotic truncation, not the full integral gap equation (6.25).
reducedDiscriminant: Discriminant in PDF p.37, (6.34).
reducedRoot: The two explicit branches of the reduced equation (6.34); true selects the plus sign. Negative discriminants are excluded in its use.
reducedAmplitude: The retained small-alpha normalization from (6.7) as D tends to four. It is the leading reduced d amplitude, not an exact finite-epsilon value of the original Gamma-normalized saddle. PDF p.37, (6.35).

Definition code

import Mathlib

/-!
Analytic statements from Metlitski--Fuertes--Sachdev, arXiv:0904.4477v1.
The continuum entropy and interacting-field constructions that are not supplied
here are explicitly deferred in the assigned unit's HARD.md and GAPS.json.
All reduced quantities below are mathematical objects of the indicated
truncation; they are not definitions of the full physical entropy.
-/

noncomputable section

open Filter Set MeasureTheory
open scoped Topology BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P31

/-- Summand of the shifted transverse heat trace, PDF p.30, (5.26). -/
def transverseHeatTerm (s phi : ℝ) (j : ℤ) : ℝ :=
  Real.exp (-s * (2 * Real.pi * (j : ℝ) + phi) ^ 2)

/-- Shifted one-dimensional heat trace, PDF p.30, (5.26).
Only positive heat times are used in the statements. -/
def transverseHeat (s phi : ℝ) : ℝ :=
  ∑' j : ℤ, transverseHeatTerm s phi j

/-- Heat-kernel continuation of the transverse reciprocal-square sum,
PDF p.30, (5.25). Its convergent domain is `2 < D < 4` and nonzero twist. -/
def transverseIntegral (D phi : ℝ) : ℝ :=
  ∫ s in Ioi (0 : ℝ), (transverseHeat s phi) ^ (D - 2)

example (s phi : ℝ) : transverseHeatTerm s phi 0 = Real.exp (-s * phi ^ 2) := by
  simp [transverseHeatTerm]

example (s : ℝ) : transverseHeat s 0 =
    ∑' j : ℤ, Real.exp (-s * (2 * Real.pi * (j : ℝ)) ^ 2) := by
  simp [transverseHeat, transverseHeatTerm]

/-- The massless square torus has side `2*pi`. Its heat kernel is defined
spectrally, independently of the theta formula; PDF p.27, (5.13)--(5.14). -/
def squareHeat (s x y : ℝ) : ℝ :=
  (∑' k : ℤ × ℤ,
    Real.exp (-s * ((k.1 : ℝ) ^ 2 + (k.2 : ℝ) ^ 2)) *
      Real.cos ((k.1 : ℝ) * x + (k.2 : ℝ) * y)) / (4 * Real.pi ^ 2)

/-- Off the lattice of source points of the side-`2*pi` square torus. -/
def OffSquareLattice (x y : ℝ) : Prop :=
  ¬ ∃ k : ℤ × ℤ, x = 2 * Real.pi * (k.1 : ℝ) ∧
    y = 2 * Real.pi * (k.2 : ℝ)

/-- Zero-mode-removed inverse Laplacian on the square torus, constructed
by the heat kernel. The pointwise integral is used only off its source
lattice; its logarithmic singularity is locally integrable. PDF p.27. -/
def squareGreen (x y : ℝ) : ℝ :=
  ∫ s in Ioi (0 : ℝ), squareHeat s x y - 1 / (4 * Real.pi ^ 2)

/-- Odd Jacobi theta function at modulus `i`, with argument of period one,
using its convergent sine series, in the convention of PDF p.27, (5.14). -/
def oddThetaAtI (z : ℂ) : ℂ :=
  2 * ∑' j : ℕ, (-1 : ℂ) ^ j *
    (Real.exp (-Real.pi * ((j : ℝ) + 1 / 2) ^ 2) : ℂ) *
      Complex.sin (((2 * j + 1 : ℕ) : ℂ) * (Real.pi : ℂ) * z)

/-- Positive real value of Dedekind eta at `i`. Mathlib defines eta by
`exp(pi*i*z/12)` times the product of `1-exp(2*pi*i*(j+1)*z)`. -/
def etaAtI : ℝ := ‖ModularForm.eta Complex.I‖

example : ¬ OffSquareLattice 0 0 := by
  intro h
  exact h ⟨(0, 0), by simp⟩

example : oddThetaAtI 0 = 0 := by
  simp [oddThetaAtI]

example : 0 ≤ etaAtI := by
  exact norm_nonneg _

/-- Analytic coefficient profile on the right-hand side of (5.31), PDF
p.30. This definition does not assert a physical entropy/partition-function
identity; that calculation is the separately deferred node #5.31. -/
def geometricProfile (N : ℕ) (phi : ℝ) : ℝ :=
  Real.pi * (N : ℝ) * squareGreen phi phi / (3 * ((N : ℝ) + 8))

example (phi : ℝ) : geometricProfile 0 phi = 0 := by
  simp [geometricProfile]

/-- The reduced small-alpha gap equation, PDF p.37, (6.33). This is the
specified asymptotic truncation, not the full integral gap equation (6.25). -/
def reducedGap (eps n alpha : ℝ) : ℝ :=
  alpha / n + alpha ^ 2 / eps - (1 / n ^ 2 - 1) / 6

/-- Discriminant in PDF p.37, (6.34). -/
def reducedDiscriminant (eps n : ℝ) : ℝ :=
  eps ^ 2 + (2 / 3 : ℝ) * eps * (1 - n ^ 2)

/-- The two explicit branches of the reduced equation (6.34); `true`
selects the plus sign. Negative discriminants are excluded in its use. -/
def reducedRoot (eps n : ℝ) (plus : Bool) : ℝ :=
  -eps / (2 * n) + (if plus then 1 else -1) *
    Real.sqrt (reducedDiscriminant eps n) / (2 * n)

/-- The retained small-alpha normalization from (6.7) as D tends to four.
It is the leading reduced d amplitude, not an exact finite-epsilon value
of the original Gamma-normalized saddle. PDF p.37, (6.35). -/
def reducedAmplitude (N : ℕ) (eps alpha : ℝ) : ℝ :=
  (N : ℝ) * alpha ^ 2 / (8 * Real.pi ^ 2 * eps)

example (eps n : ℝ) : reducedGap eps n 0 = -(1 / n ^ 2 - 1) / 6 := by
  simp [reducedGap] <;> ring

example (eps : ℝ) : reducedDiscriminant eps 1 = eps ^ 2 := by
  simp [reducedDiscriminant]

example (eps : ℝ) : reducedAmplitude 0 eps 0 = 0 := by
  simp [reducedAmplitude]

end QAlgorithms.Papers.Independent.Intakethird100.P31

Source

Entanglement Entropy in the O(N) model, arXiv:0904.4477v1, https://arxiv.org/abs/0904.4477v1

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

`QAlgorithms.Papers.Independent.Intakethird100.P31.OffSquareLattice`

For real numbers $x,y$ , this defines the proposition that there is no pair of integers $(m,n)$ satisfying both $x=2\pi m$ and $y=2\pi n$ . Equivalently, $(x,y)\notin(2\pi\mathbb Z)\times(2\pi\mathbb Z)$ ; it is sufficient for either coordinate to fail to be an integer multiple of $2\pi$ .

`QAlgorithms.Papers.Independent.Intakethird100.P31.etaAtI`

This defines the real number $E=|\eta(i)|$ , the complex norm of the Dedekind eta function evaluated at the imaginary unit $i$ . The definition itself makes no positivity or nonvanishing assertion.

`QAlgorithms.Papers.Independent.Intakethird100.P31.geometricProfile`

For every natural number $N$ , including $N=0$ , and every real $\phi$ , this defines

P_N(\phi)= \frac{\pi N}{3(N+8)} \int_{(0,\infty)} \left( \frac{1}{4\pi^2} \sum_{(m,n)\in\mathbb Z^2} e^{-s(m^2+n^2)}\cos\bigl((m+n)\phi\bigr) -\frac{1}{4\pi^2} \right)\,ds.

Here $N$ is viewed as a real number, the sum is assigned $0$ when its family is not summable, and the Lebesgue integral is assigned $0$ when its integrand is not integrable. There is no restriction on $\phi$ , including integer multiples of $2\pi$ ; in particular, $P_0(\phi)=0$ for every $\phi$ .

`QAlgorithms.Papers.Independent.Intakethird100.P31.oddThetaAtI`

For every complex number $z$ , this defines the complex number

\Theta(z)=2\sum_{j=0}^{\infty} (-1)^j e^{-\pi(j+\frac12)^2} \sin\!\bigl((2j+1)\pi z\bigr),

where the sine is the complex sine and the real exponential coefficient is viewed as a complex number. The index includes $j=0$ . The sum is a totalized complex sum, assigned $0$ if the family is not summable; the definition itself assumes no summability or restriction on $z$ .

`QAlgorithms.Papers.Independent.Intakethird100.P31.reducedAmplitude`

For every natural number $N$ , including $N=0$ , and arbitrary real numbers $\varepsilon,\alpha$ , this defines the real number

\frac{N\alpha^2}{8\pi^2\varepsilon},

where $N$ is regarded as a real number. Division by zero is defined to give zero, so the value is zero if $\varepsilon=0$ ; it is also zero if $N=0$ .

`QAlgorithms.Papers.Independent.Intakethird100.P31.reducedDiscriminant`

For arbitrary real numbers $\varepsilon$ and $n$ , including zero and negative values, this defines the real number

\varepsilon^2+\frac23\varepsilon(1-n^2).

No assumption requires this number to be nonnegative.

`QAlgorithms.Papers.Independent.Intakethird100.P31.reducedGap`

For arbitrary real numbers $\varepsilon,n,\alpha$ , this defines the real number

\frac{\alpha}{n}+\frac{\alpha^2}{\varepsilon} -\frac{1/n^2-1}{6}.

There are no positivity or nonzero assumptions. Division by zero is defined to give zero, so the formula also assigns values when $n=0$ or $\varepsilon=0$ .

`QAlgorithms.Papers.Independent.Intakethird100.P31.reducedRoot`

For arbitrary real numbers $\varepsilon,n$ and a Boolean choice $b$ , this defines

-\frac{\varepsilon}{2n} +\frac{\sigma_b\sqrt{\varepsilon^2+\frac23\varepsilon(1-n^2)}}{2n}, \qquad \sigma_b= \begin{cases} 1,&b=\mathrm{true},\\ -1,&b=\mathrm{false}. \end{cases}

The real square root is defined to be zero for a negative input, and division by zero is defined to give zero; in particular, the defined value is zero whenever $n=0$ .

`QAlgorithms.Papers.Independent.Intakethird100.P31.squareGreen`

For any real numbers $x,y$ , this defines

G(x,y)=\int_{(0,\infty)} \left( \frac{1}{4\pi^2} \sum_{(m,n)\in\mathbb Z^2}e^{-s(m^2+n^2)}\cos(mx+ny) -\frac{1}{4\pi^2} \right)\,ds.

The sum is assigned $0$ if its family is not summable, and the Lebesgue integral is assigned $0$ if its integrand is not integrable. The definition applies to every pair $(x,y)$ , including lattice points $(2\pi m,2\pi n)$ , without any integrability hypothesis.

`QAlgorithms.Papers.Independent.Intakethird100.P31.squareHeat`

For any real numbers $s,x,y$ , this defines

K(s,x,y)=\frac{1}{4\pi^2} \sum_{(m,n)\in\mathbb Z^2} e^{-s(m^2+n^2)}\cos(mx+ny).

No positivity assumption on $s$ or restriction on $x,y$ is imposed. The sum is the totalized real sum, assigned $0$ if the indexed family is not summable.

`QAlgorithms.Papers.Independent.Intakethird100.P31.transverseHeat`

For any real numbers $s,\phi$ , this defines

H(s,\phi)=\sum_{j\in\mathbb Z}\exp\!\left(-s(2\pi j+\phi)^2\right).

The sum is a totalized real sum: it equals the sum when the family is summable, and equals $0$ otherwise. No summability hypothesis is imposed by this definition. In particular, for $s\leq0$ the family is not summable and $H(s,\phi)=0$ .

`QAlgorithms.Papers.Independent.Intakethird100.P31.transverseHeatTerm`

For any real numbers $s,\phi$ and any integer $j$ , this defines the real number

\exp\!\left(-s(2\pi j+\phi)^2\right).

There are no sign or nonzero assumptions on $s$ or $\phi$ ; in particular, the value at $s=0$ is $1$ .

`QAlgorithms.Papers.Independent.Intakethird100.P31.transverseIntegral`

For any real numbers $D,\phi$ , this defines

I(D,\phi)=\int_{(0,\infty)} \left(\sum_{j\in\mathbb Z}\exp\!\left(-s(2\pi j+\phi)^2\right)\right)^{D-2}\,ds,

where the exponent is a real power, the sum is assigned $0$ when its family is not summable, and the integral is the totalized real Lebesgue integral, assigned $0$ when its integrand is not integrable. There are no restrictions on $D$ or $\phi$ . In particular, at $D=2$ the integrand is constantly $1$ , so this convention gives $I(2,\phi)=0$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph