Liouville field theory: background charge, central charge, conformal dimension, reflection coefficient

Definition

LiouvilleFieldTheory_kinematics

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

conformal-field-theoryliouville-theorymathematical-physics

Kinematic data of Liouville field theory as functions of the complex coupling constant $b$ .

The background charge is $Q = b + \dfrac{1}{b}$ .
The central charge is $c = 1 + 6Q^2$ .
The conformal dimension of the primary field with momentum $\alpha \in \mathbb{C}$ is

\Delta(\alpha) = \alpha\,(Q - \alpha).

The reflection coefficient with normalization parameter $\lambda$ and momentum $P$ is

R_P = \pm\,\lambda^{-2iP}\,\frac{\Gamma(2ibP)\,\Gamma(2ib^{-1}P)}{\Gamma(-2ibP)\,\Gamma(-2ib^{-1}P)},

where the sign is $+1$ if $c \in (-\infty, 1)$ and $-1$ otherwise.

These are the objects in terms of which the spectrum, the reflection relation $\alpha \to Q - \alpha$ and the duality $b \to 1/b$ of Liouville theory are stated.

Formalization Note All quantities are complex-valued functions of $b \in \mathbb{C}$ . Lean's inverse satisfies $0^{-1} = 0$ , so at $b = 0$ the definitions return junk values ( $Q = 0$ , $c = 1$ ); statements that need $b \neq 0$ assume it. The power $\lambda^{-2iP}$ is the principal-branch complex power, and $\Gamma$ is Mathlib's complex Gamma function. The condition " $c \in (-\infty,1)$ " is encoded as $\operatorname{Im} c = 0$ and $\operatorname{Re} c < 1$ .

Definition code

import Mathlib

/-!
# Liouville field theory: kinematic definitions

Source: Wikipedia, "Liouville field theory" (oldid 1376996606): sections
"Introduction", "Spectrum", "Fields and reflection relation".
-/

namespace LiouvilleFieldTheory

open Complex

/-- The background charge `Q = b + 1/b` of Liouville theory with coupling constant `b`. -/
noncomputable def backgroundCharge (b : ℂ) : ℂ := b + b⁻¹

/-- The central charge `c = 1 + 6 Q²` of Liouville theory with coupling constant `b`. -/
noncomputable def centralCharge (b : ℂ) : ℂ := 1 + 6 * backgroundCharge b ^ 2

/-- The conformal dimension `Δ = α (Q - α)` of the primary field with momentum `α`. -/
noncomputable def conformalDimension (b α : ℂ) : ℂ := α * (backgroundCharge b - α)

/-- The sign in the reflection coefficient: `+1` if `c ∈ (-∞, 1)`, and `-1` otherwise. -/
noncomputable def reflectionSign (b : ℂ) : ℂ :=
  if (centralCharge b).im = 0 ∧ (centralCharge b).re < 1 then 1 else -1

/-- The reflection coefficient
`R_P = ± λ^{-2iP} Γ(2ibP) Γ(2ib⁻¹P) / (Γ(-2ibP) Γ(-2ib⁻¹P))`,
with the sign given by `reflectionSign` and normalization parameter `λ`. -/
noncomputable def reflectionCoefficient (b lam P : ℂ) : ℂ :=
  reflectionSign b * lam ^ (-2 * I * P) *
    (Gamma (2 * I * b * P) * Gamma (2 * I * b⁻¹ * P)) /
    (Gamma (-2 * I * b * P) * Gamma (-2 * I * b⁻¹ * P))

end LiouvilleFieldTheory

Source

Wikipedia, "Liouville field theory", revision oldid=1376996606 (https://en.wikipedia.org/w/index.php?title=Liouville_field_theory&oldid=1376996606); sections Introduction (p. 1–2), Spectrum (p. 2), Fields and reflection relation (p. 2–3).

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 file declares five functions in the namespace LiouvilleFieldTheory, all with complex inputs and complex outputs; no theorems are asserted.

Background charge. For $b \in \mathbb{C}$ , $Q(b) = b + b^{-1}$ , where $b^{-1}$ is the field inverse with the convention $0^{-1} = 0$ ; hence $Q(0) = 0$ .
Central charge. $c(b) = 1 + 6\,Q(b)^2$ ; in particular $c(0) = 1$ .
Conformal dimension. For $b, \alpha \in \mathbb{C}$ , $\Delta(b,\alpha) = \alpha\,(Q(b) - \alpha)$ .
Sign. $s(b) = 1$ if the imaginary part of $c(b)$ is $0$ and the real part of $c(b)$ is strictly less than $1$ ; otherwise $s(b) = -1$ . (So $c(b) = 1$ gives $s = -1$ .)
Reflection coefficient. For $b, \lambda, P \in \mathbb{C}$ ,

R(b,\lambda,P) = \frac{s(b)\,\lambda^{-2iP}\,\Gamma(2ibP)\,\Gamma(2ib^{-1}P)}{\Gamma(-2ibP)\,\Gamma(-2ib^{-1}P)},

where $\lambda^{w}$ is the principal-branch complex power $\exp(w \log \lambda)$ (with $0^{w} = 0$ for $w \neq 0$ and $0^0 = 1$ ), $\Gamma$ is the complex Gamma function (which takes the value $0$ at $0, -1, -2, \dots$ in this library), and division by $0$ yields $0$ . Consequently $R = 0$ whenever a denominator Gamma factor is evaluated at a non-positive integer, or a numerator factor is, or $\lambda = 0$ with $P \neq 0$ .

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