Prove2Me

Δ(Q/2+iP)=c−124+P2\Delta(Q/2 + iP) = \frac{c-1}{24} + P^2

Proved
LiouvilleFieldTheory.conformalDimension_momentum

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

conformal-field-theoryliouville-theorymathematical-physics

Let b∈Cb \in \mathbb{C}, Q=b+1/bQ = b + 1/b, c=1+6Q2c = 1 + 6Q^2, and Δ(α)=α(Q−α)\Delta(\alpha) = \alpha(Q - \alpha). For every P∈CP \in \mathbb{C},

Δ ⁣(Q2+iP)=c−124+P2.\Delta\!\left(\frac{Q}{2} + iP\right) = \frac{c - 1}{24} + P^2.

This expresses the conformal dimension of a state of the continuous spectrum in terms of its momentum PP; for real PP it shows Δ∈c−124+R+\Delta \in \frac{c-1}{24} + \mathbb{R}_+.

Formalization Note The identity is stated for all complex PP (the source uses P∈R+P \in \mathbb{R}_+) and all b∈Cb \in \mathbb{C}.

Preamble
import Mathlib
import Definitions.Def_LiouvilleFieldTheory_kinematics
open Complex
Formal statement
namespace LiouvilleFieldTheory

theorem conformalDimension_momentum (b P : ℂ) :
    conformalDimension b (backgroundCharge b / 2 + I * P) =
      (centralCharge b - 1) / 24 + P ^ 2 := 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): Δ ∈ (c−1)/24 + ℝ₊ ⟺ α ∈ Q/2 + iP, 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 all complex numbers bb and PP, with Q(b)=b+b−1Q(b) = b + b^{-1} (Q(0)=0Q(0)=0) and c(b)=1+6Q(b)2c(b) = 1 + 6Q(b)^2:

(Q(b)2+iP)(Q(b)−Q(b)2−iP)=c(b)−124+P2.\left(\tfrac{Q(b)}{2} + iP\right)\left(Q(b) - \tfrac{Q(b)}{2} - iP\right) = \frac{c(b) - 1}{24} + P^2.

No hypotheses; PP is complex, not restricted to reals or to P≥0P \ge 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