Prove2Me

Duality b→1/bb \to 1/b preserves cc and Δ\Delta

Proved
LiouvilleFieldTheory.centralCharge_conformalDimension_duality

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

conformal-field-theoryliouville-theorymathematical-physics

Let c(b)=1+6(b+1/b)2c(b) = 1 + 6(b + 1/b)^2 and Δb(α)=α(b+1/b−α)\Delta_b(\alpha) = \alpha(b + 1/b - \alpha). For every b∈Cb \in \mathbb{C} and every momentum α∈C\alpha \in \mathbb{C},

c(1/b)=c(b)andΔ1/b(α)=Δb(α).c(1/b) = c(b) \qquad\text{and}\qquad \Delta_{1/b}(\alpha) = \Delta_b(\alpha).

The central charge and the conformal dimensions are invariant under the duality b→1/bb \to 1/b; correlation functions are covariant under it, although the exponential potential of the Lagrangian is not invariant.

Formalization Note 1/b1/b is Lean's inverse b−1b^{-1}, with 0−1=00^{-1} = 0, so b=0b = 0 is a trivial case.

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

theorem centralCharge_conformalDimension_duality (b α : ℂ) :
    centralCharge b⁻¹ = centralCharge b ∧
      conformalDimension b⁻¹ α = conformalDimension b α := 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 Introduction (p. 2): "The central charge and conformal dimensions are invariant under the duality b → 1/b".
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 bb and α\alpha, two equalities hold simultaneously:

1+6(b−1+(b−1)−1)2=1+6(b+b−1)21 + 6\bigl(b^{-1} + (b^{-1})^{-1}\bigr)^2 = 1 + 6\bigl(b + b^{-1}\bigr)^2

and

α(b−1+(b−1)−1−α)=α(b+b−1−α),\alpha\bigl(b^{-1} + (b^{-1})^{-1} - \alpha\bigr) = \alpha\bigl(b + b^{-1} - \alpha\bigr),

i.e. c(b−1)=c(b)c(b^{-1}) = c(b) and Δ(b−1,α)=Δ(b,α)\Delta(b^{-1}, \alpha) = \Delta(b, \alpha), with the convention 0−1=00^{-1} = 0. No hypotheses.

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