Reflection relation consistency $R_P\,R_{-P} = 1$

Proved

LiouvilleFieldTheory.reflectionCoefficient_mul_neg

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, $\lambda \in \mathbb{C}\setminus\{0\}$ the normalization parameter, and $P \in \mathbb{C}$ a momentum such that neither $2ibP$ nor $2ib^{-1}P$ is an integer. With the reflection coefficient

R_P = \pm\,\lambda^{-2iP}\,\frac{\Gamma(2ibP)\,\Gamma(2ib^{-1}P)}{\Gamma(-2ibP)\,\Gamma(-2ib^{-1}P)}

(sign $+1$ if $c \in (-\infty,1)$ , $-1$ otherwise), one has

R_P\,R_{-P} = 1.

The primary fields $V_P$ and $V_{-P}$ correspond to the same state and are related by the reflection relation $V_P = R_P V_{-P}$ ; applying it to both $P$ and $-P$ is consistent precisely because $R_P R_{-P} = 1$ .

Formalization Note The non-integrality hypothesis keeps all four Gamma factors away from their poles (where Lean's $\Gamma$ returns a junk value); it also forces $b \neq 0$ and $P \neq 0$ . $\lambda \neq 0$ is needed because the principal-branch power $0^{w}$ vanishes for $w \neq 0$ . This consistency identity is implied by, but not printed in, the source.

Preamble

import Mathlib
import Definitions.Def_LiouvilleFieldTheory_kinematics
open Complex

Formal statement

namespace LiouvilleFieldTheory

theorem reflectionCoefficient_mul_neg (b lam P : ℂ) (hlam : lam ≠ 0)
    (hP : ∀ n : ℤ, 2 * I * b * P ≠ n ∧ 2 * I * b⁻¹ * P ≠ n) :
    reflectionCoefficient b lam P * reflectionCoefficient b lam (-P) = 1 := 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 Fields and reflection relation (p. 2–3): V_P(z) = R_P V_{−P}(z), formula for R_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 $b$ , $\lambda$ , $P$ such that (1) $\lambda \neq 0$ , and (2) for every integer $n$ , $2ibP \neq n$ and $2ib^{-1}P \neq n$ (with $0^{-1} = 0$ ): the product $R(b,\lambda,P)\cdot R(b,\lambda,-P)$ equals $1$ , where

R(b,\lambda,P) = \frac{s(b)\,\lambda^{-2iP}\,\Gamma(2ibP)\,\Gamma(2ib^{-1}P)}{\Gamma(-2ibP)\,\Gamma(-2ib^{-1}P)},

$s(b) = 1$ if $c(b) = 1 + 6(b + b^{-1})^2$ is a real number $< 1$ and $s(b) = -1$ otherwise, $\lambda^{w}$ is the principal-branch complex power, and $\Gamma$ is the complex Gamma function. Hypothesis (2) with $n = 0$ excludes $b = 0$ and $P = 0$ ; it is satisfiable (e.g. $b = 1$ , $P$ a non-zero real number).

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

Reflection relation consistency RP R−P=1R_P\,R_{-P} = 1RP​R−P​=1

Reflection relation consistency $R_P\,R_{-P} = 1$