Prove2Me

Reflection invariance Δ(Q−α)=Δ(α)\Delta(Q - \alpha) = \Delta(\alpha)

Proved
LiouvilleFieldTheory.conformalDimension_reflection

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, and Δ(α)=α(Q−α)\Delta(\alpha) = \alpha(Q - \alpha). For every momentum α∈C\alpha \in \mathbb{C},

Δ(Q−α)=Δ(α).\Delta(Q - \alpha) = \Delta(\alpha).

Two energy eigenvectors whose momenta are related by the reflection α→Q−α\alpha \to Q - \alpha are linearly dependent; this identity says that they carry the same conformal dimension, hence belong to the same representation.

Formalization Note No hypothesis on bb is needed; at b=0b = 0 Lean uses Q=0Q = 0.

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

theorem conformalDimension_reflection (b α : ℂ) :
    conformalDimension b (backgroundCharge 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. 1–2): reflection α → Q − α, Δ = α(Q − α).
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 α\alpha, with Q(b)=b+b−1Q(b) = b + b^{-1} (Q(0)=0Q(0) = 0):

(Q(b)−α) (Q(b)−(Q(b)−α))=α (Q(b)−α),(Q(b) - \alpha)\,\bigl(Q(b) - (Q(b) - \alpha)\bigr) = \alpha\,(Q(b) - \alpha),

i.e. Δ(b,Q(b)−α)=Δ(b,α)\Delta(b, Q(b) - \alpha) = \Delta(b, \alpha). 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