Imaginary coupling $\beta = ib \in \mathbb{R}$ gives exactly $c \le 1$

Proved

LiouvilleFieldTheory.centralCharge_imaginary_coupling

by Lucas · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

conformal-field-theoryliouville-theorymathematical-physics

Write the coupling constant as $b = -i\beta$ , i.e. $\beta = ib$ . As $\beta$ ranges over the nonzero real numbers, the central charge $c = 1 + 6(b + 1/b)^2$ ranges exactly over the real numbers $c \le 1$ :

\left\{\, 1 + 6\left(b + \tfrac1b\right)^2 \;:\; b = -i\beta,\ \beta \in \mathbb{R}\setminus\{0\} \right\} \;=\; (-\infty, 1] \subset \mathbb{C}.

In the source, the three-point structure constant for $c \in (-\infty, 1)$ is written in terms of $\beta = ib \in \mathbb{R}$ ; this statement records that real $\beta$ covers that range of central charges, and in fact produces exactly $c \in (-\infty, 1]$ (the value $c = 1$ occurs at $\beta = \pm 1$ ).

Formalization Note Real numbers $c \le 1$ are encoded as complex numbers with zero imaginary part and real part at most $1$ .

Preamble

import Mathlib
import Definitions.Def_LiouvilleFieldTheory_kinematics
open Complex

Formal statement

namespace LiouvilleFieldTheory

theorem centralCharge_imaginary_coupling :
    {c : ℂ | ∃ β : ℝ, β ≠ 0 ∧ centralCharge (-I * β) = c} =
      {c : ℂ | c.im = 0 ∧ c.re ≤ 1} := by
  sorry

end LiouvilleFieldTheory

Source

Wikipedia, "Liouville field theory", revision oldid=1376996606 (https://en.wikipedia.org/w/index.php?title=Liouville_field_theory&oldid=1376996606); section Correlation functions and DOZZ formula (p. 3): "For c ∈ (−∞, 1), the three-point structure constant is ... where β = ib ∈ ℝ".

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, at the explicit request of the proposal owner. It was not produced by an independent, blind auditor, and the author knew the intended meaning while writing it. Reviewers must not treat it as independent confirmation of faithfulness; compare it against the Lean code directly.

The set of complex numbers of the form $c(-i\beta) = 1 + 6\bigl(-i\beta + (-i\beta)^{-1}\bigr)^2$ with $\beta$ a real number, $\beta \neq 0$ , is asserted to be equal to the set of complex numbers $z$ with $\operatorname{Im} z = 0$ and $\operatorname{Re} z \le 1$ (non-strict inequality). Both inclusions are claimed: every such $c(-i\beta)$ is real and at most $1$ , and every real number $\le 1$ arises from some nonzero real $\beta$ .

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Imaginary coupling β=ib∈R\beta = ib \in \mathbb{R}β=ib∈R gives exactly c≤1c \le 1c≤1

Imaginary coupling $\beta = ib \in \mathbb{R}$ gives exactly $c \le 1$