Liouville spectrum: $\alpha = Q/2 + iP$ , $P \in \mathbb{R}_+$ , parametrizes $\Delta \in \frac{c-1}{24} + \mathbb{R}_+$

Proved

LiouvilleFieldTheory.spectrum_momentum_bijOn

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

conformal-field-theoryliouville-theorymathematical-physics

Let $b \in \mathbb{C}$ be the coupling constant of Liouville theory, $Q = b + 1/b$ the background charge, $c = 1 + 6Q^2$ the central charge, and $\Delta(\alpha) = \alpha(Q - \alpha)$ the conformal dimension of the primary field of momentum $\alpha$ .

The spectrum of Liouville theory consists of the conformal dimensions $\Delta \in \frac{c-1}{24} + \mathbb{R}_+$ , which in terms of the momentum amounts to $\alpha \in \frac{Q}{2} + i\,\mathbb{R}_+$ . Precisely, the map

P \;\longmapsto\; \Delta\!\left(\tfrac{Q}{2} + iP\right)

is a bijection from $\mathbb{R}_+ = [0, \infty)$ onto

\frac{c-1}{24} + \mathbb{R}_+ = \left\{\tfrac{c-1}{24} + t \;:\; t \in \mathbb{R},\ t \ge 0\right\} \subset \mathbb{C}.

This is the statement that the half-line of momenta $P \ge 0$ labels each representation of the continuous spectrum exactly once; the reflection $\alpha \to Q - \alpha$ is responsible for the momentum taking values on a half-line rather than a full line.

Formalization Note $b$ ranges over all of $\mathbb{C}$ (the identity also holds with Lean's junk value at $b = 0$ ), and $\mathbb{R}_+$ is taken to include $0$ , i.e. $P = 0$ corresponds to the bottom $\Delta = \frac{c-1}{24}$ of the spectrum.

Preamble

import Mathlib
import Definitions.Def_LiouvilleFieldTheory_kinematics
open Complex

Formal statement

namespace LiouvilleFieldTheory

theorem spectrum_momentum_bijOn (b : ℂ) :
    Set.BijOn (fun P : ℝ => conformalDimension b (backgroundCharge b / 2 + I * P))
      (Set.Ici 0)
      {Δ : ℂ | ∃ t : ℝ, 0 ≤ t ∧ Δ = (centralCharge b - 1) / 24 + t} := 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 Spectrum (p. 2): "The conformal dimension takes values Δ ∈ (c−1)/24 + ℝ₊, which in terms of the momentum α amounts to α ∈ Q/2 + iP with P ∈ ℝ₊".

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.

For every complex number $b$ : consider the function $f_b : \mathbb{R} \to \mathbb{C}$ ,

f_b(P) = \Delta\!\left(b,\ \tfrac{Q(b)}{2} + iP\right) = \left(\tfrac{Q(b)}{2} + iP\right)\left(Q(b) - \tfrac{Q(b)}{2} - iP\right),

with $Q(b) = b + b^{-1}$ (and $Q(0) = 0$ ). The theorem asserts that $f_b$ is a bijection from the closed half-line $\{P \in \mathbb{R} : P \ge 0\}$ onto the set

S_b = \left\{\Delta \in \mathbb{C} \;:\; \exists\, t \in \mathbb{R},\ t \ge 0,\ \Delta = \tfrac{c(b) - 1}{24} + t\right\}, \qquad c(b) = 1 + 6Q(b)^2,

meaning all three of: (i) $f_b$ maps every $P \ge 0$ into $S_b$ ; (ii) $f_b$ is injective on $P \ge 0$ ; (iii) every element of $S_b$ equals $f_b(P)$ for some $P \ge 0$ . There are no hypotheses on $b$ ; the case $b = 0$ is included with $Q = 0$ , $c = 1$ .

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

Liouville spectrum: α=Q/2+iP\alpha = Q/2 + iPα=Q/2+iP, P∈R+P \in \mathbb{R}_+P∈R+​, parametrizes Δ∈c−124+R+\Delta \in \frac{c-1}{24} + \mathbb{R}_+Δ∈24c−1​+R+​

Liouville spectrum: $\alpha = Q/2 + iP$ , $P \in \mathbb{R}_+$ , parametrizes $\Delta \in \frac{c-1}{24} + \mathbb{R}_+$