Marginality $\Delta(b) = 1 \iff Q = b + 1/b$

Proved

LiouvilleFieldTheory.marginality_iff

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

conformal-field-theoryliouville-theorymathematical-physics

Let $b \in \mathbb{C}$ with $b \neq 0$ and let $Q \in \mathbb{C}$ be an arbitrary background charge. With the conformal dimension $\Delta(\alpha) = \alpha(Q - \alpha)$ of the field $e^{2\alpha\varphi}$ , the field $e^{2b\varphi}$ in the action is marginal exactly when $Q$ is the Liouville background charge:

\Delta(b) = b\,(Q - b) = 1 \quad\Longleftrightarrow\quad Q = b + \frac{1}{b}.

This is the condition for conformal invariance of the Lagrangian formulation, which fixes the relation between the background charge and the coupling constant.

Formalization Note Here $Q$ is a free complex parameter (not the defined background charge), so the statement is the derivation of the relation $Q = b + 1/b$ from marginality.

Preamble

import Mathlib
import Definitions.Def_LiouvilleFieldTheory_kinematics
open Complex

Formal statement

namespace LiouvilleFieldTheory

theorem marginality_iff (b Q : ℂ) (hb : b ≠ 0) :
    b * (Q - b) = 1 ↔ Q = b + 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 Conformal symmetry (p. 5): "the field e^{2bφ} ... must be marginal, i.e. have the conformal dimension Δ(b) = 1. This leads to the relation Q = 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 numbers $b$ and $Q$ with $b \neq 0$ :

b\,(Q - b) = 1 \iff Q = b + b^{-1}.

$Q$ here is an arbitrary complex number (a bound variable of the statement), not the function $Q(b)$ of the definition file; the statement does not use any definition from the definition file. The hypothesis $b \neq 0$ is explicit.

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

Marginality Δ(b)=1 ⟺ Q=b+1/b\Delta(b) = 1 \iff Q = b + 1/bΔ(b)=1⟺Q=b+1/b

Marginality $\Delta(b) = 1 \iff Q = b + 1/b$