Twist dependence of the explicit leading geometric coefficient

Open

QAlgorithms.Papers.Independent.Intakethird100.P31.geometric_profile_twist

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

prove2quantum

Let $N\ge1$ be an integer, and let $G_T$ denote the independently constructed zero-mean square-torus Green function. Consider the explicit coefficient profile on the right-hand side of (5.31),

g_N(\phi)=\frac{\pi N}{3(N+8)}G_T(\phi,\phi).

For every such $N$ , its antiperiodic value is

g_N(\pi)=-\frac{N\log2}{12(N+8)}<0.

For even $N$ , so that arbitrary twists are allowed, $g_N$ is nonincreasing on $0<\phi<\pi$ , and

\lim_{\phi\downarrow0}\frac{g_N(\phi)}{\log\phi}=-\frac{N}{6(N+8)}.

In particular, this coefficient is positive for all sufficiently small positive twists. These statements analyze the explicit epsilon coefficient first; they do not assert a joint small-twist/epsilon expansion or a value of the physical entropy at zero twist.

This describes the sign and twist dependence of the analytic profile; the derivation identifying it with the Wilson–Fisher entropy coefficient is the separately inventoried node (5.31).

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P31

Formal statement

noncomputable section

open Filter Set MeasureTheory

open scoped Topology BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P31

/-- PDF pp.30--31, Fig.10 and (5.32)--(5.33): twist dependence of the
explicit leading coefficient profile, after epsilon-coefficient extraction.
Arbitrary twists use even N. The antiperiodic value is available for every
positive N. No assertion is made about the physical zero-twist entropy. -/
theorem geometric_profile_twist (N : ℕ) (hN : 0 < N) :
    geometricProfile N Real.pi =
      -(N : ℝ) * Real.log 2 / (12 * ((N : ℝ) + 8)) ∧
    geometricProfile N Real.pi < 0 ∧
    (Even N →
      AntitoneOn (geometricProfile N) (Ioo (0 : ℝ) Real.pi) ∧
      Tendsto (fun phi : ℝ => geometricProfile N phi / Real.log phi)
        (𝓝[>] (0 : ℝ)) (𝓝 (-(N : ℝ) / (6 * ((N : ℝ) + 8)))) ∧
      (∀ᶠ phi : ℝ in 𝓝[>] (0 : ℝ), 0 < geometricProfile N phi)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P31

end

Source

Entanglement Entropy in the O(N) model, arXiv:0904.4477v1, PDF p. 30, §V C (5.32)–(5.33): twist dependence of the leading geometric coefficient

Read-back

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

For every natural number $N$ satisfying $N>0$ , define, for every real $\phi$ ,

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,

where $N$ is viewed as real, nonsummable families have totalized sum $0$ , and nonintegrable integrands have totalized Lebesgue integral $0$ . The statement asserts

P_N(\pi)=-\frac{N\log2}{12(N+8)} \qquad\text{and}\qquad P_N(\pi)<0.

If $N$ is even, it additionally asserts all three of the following: for any real $a,b$ with $0<a<\pi$ , $0<b<\pi$ , and $a\leq b$ , one has $P_N(b)\leq P_N(a)$ ;

\lim_{\phi\to0^+}\frac{P_N(\phi)}{\log\phi} =-\frac{N}{6(N+8)};

and there exists a real $\delta>0$ such that $P_N(\phi)>0$ for every real $\phi$ with $0<\phi<\delta$ .

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