Provedads-cfthep-th-9802150near-boundary-expansionwitton

The massless radial operator x²f″ + (1 − d)xf′ − k²x²f on f = 1 + ax² equals (2a(2 − d) − k²)x² − k²ax⁴

For all $\htmlData{mx=1}{d, k, a \in \htmlData{mx=0}{\mathbb{R}}}$ :

\begin{aligned} & \htmlData{mx=48}{\htmlData{mx=47}{\htmlData{mx=31}{\htmlData{mx=14}{\htmlData{mx=2}{\htmlData{mx=1}{\operatorname{X}}^{2}} \cdot \htmlData{mx=13}{\htmlData{mx=3}{\operatorname{derivative}}(\htmlData{mx=12}{\htmlData{mx=4}{\operatorname{derivative}}(\htmlData{mx=11}{1 + \htmlData{mx=10}{\htmlData{mx=7}{\htmlData{mx=5}{\operatorname{C}}\,\htmlData{mx=6}{a}} \cdot \htmlData{mx=9}{\htmlData{mx=8}{\operatorname{X}}^{2}}}})})}} + \htmlData{mx=30}{\htmlData{mx=20}{\htmlData{mx=18}{\htmlData{mx=15}{\operatorname{C}}\,\htmlData{mx=17}{1 - \htmlData{mx=16}{d}}} \cdot \htmlData{mx=19}{\operatorname{X}}} \cdot \htmlData{mx=29}{\htmlData{mx=21}{\operatorname{derivative}}(\htmlData{mx=28}{1 + \htmlData{mx=27}{\htmlData{mx=24}{\htmlData{mx=22}{\operatorname{C}}\,\htmlData{mx=23}{a}} \cdot \htmlData{mx=26}{\htmlData{mx=25}{\operatorname{X}}^{2}}}})}}} - \htmlData{mx=46}{\htmlData{mx=38}{\htmlData{mx=35}{\htmlData{mx=32}{\operatorname{C}}\,\htmlData{mx=34}{\htmlData{mx=33}{k}^{2}}} \cdot \htmlData{mx=37}{\htmlData{mx=36}{\operatorname{X}}^{2}}} \cdot (\htmlData{mx=45}{1 + \htmlData{mx=44}{\htmlData{mx=41}{\htmlData{mx=39}{\operatorname{C}}\,\htmlData{mx=40}{a}} \cdot \htmlData{mx=43}{\htmlData{mx=42}{\operatorname{X}}^{2}}}})}}} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=71}{\htmlData{mx=61}{\htmlData{mx=58}{\htmlData{mx=49}{\operatorname{C}}\,\htmlData{mx=57}{\htmlData{mx=54}{\htmlData{mx=51}{2\htmlData{mx=50}{a}} \cdot (\htmlData{mx=53}{2 - \htmlData{mx=52}{d}})} - \htmlData{mx=56}{\htmlData{mx=55}{k}^{2}}}} \cdot \htmlData{mx=60}{\htmlData{mx=59}{\operatorname{X}}^{2}}} - \htmlData{mx=70}{\htmlData{mx=67}{\htmlData{mx=62}{\operatorname{C}}\,\htmlData{mx=66}{\htmlData{mx=64}{\htmlData{mx=63}{k}^{2}} \cdot \htmlData{mx=65}{a}}} \cdot \htmlData{mx=69}{\htmlData{mx=68}{\operatorname{X}}^{4}}}} \end{aligned}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: d, k, a range over real numbers: the statement must hold for every choice. ((d k a : ℝ))
(x : T)Type ascription: X^2 · derivative(derivative(1 + C(a) · X^2)) + C(1 − d) · … read as a Polynomial(ℝ). Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((Polynomial.X ^ 2 * Polynomial.derivati…)
=Equality: X^2 · derivative(derivative(1 + C(a) · X^2)) + C(1 − d) · … and C(2 · a · (2 − d) − k^2) · X^2 − C(k^2 · a) · X^4 are the same. ((Polynomial.X ^ 2 * Polynomial.derivati…)
X: Polynomial.X: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Polynomial.X)
aᵇPower: X raised to the power 2. (Polynomial.X ^ 2)
derivative: Polynomial.derivative: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Polynomial.derivative)
+Addition: 1 plus C(a) · X^2. (1 + Polynomial.C a * Polynomial.X ^ 2)
C: Polynomial.C: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Polynomial.C)
f(x)Function application: Polynomial.C applied to a. Lean writes f x; papers write f(x). (Polynomial.C a)
·Multiplication: C(a) times X^2. (Polynomial.C a * Polynomial.X ^ 2)
-Subtraction: 1 minus d. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 - d)

theorem near-boundary-operator-on-quadratic-ansatz (d k a : ℝ) :
    (Polynomial.X ^ 2 * Polynomial.derivative (Polynomial.derivative (1 + Polynomial.C a * Polynomial.X ^ 2)) + Polynomial.C (1 - d) * Polynomial.X * Polynomial.derivative (1 + Polynomial.C a * Polynomial.X ^ 2) - Polynomial.C (k ^ 2) * Polynomial.X ^ 2 * (1 + Polynomial.C a * Polynomial.X ^ 2) : Polynomial ℝ) = Polynomial.C (2 * a * (2 - d) - k ^ 2) * Polynomial.X ^ 2 - Polynomial.C (k ^ 2 * a) * Polynomial.X ^ 4

The massless radial equation x0^{d+1} d/dx0 (x0^{1-d} dphi/dx0) + x0^2 grad^2 phi = 0 of hep-th/9802150 section 2.4, for a plane wave (grad^2 -> -k^2) and a polynomial in x0, is the polynomial operator x^2 f'' + (1-d) x f' - k^2 x^2 f. On the ansatz 1 + a x^2 it gives (2a(2-d) - k^2) x^2 - k^2 a x^4, as a polynomial identity over the reals. Decided in Alpha as wittonSecondOrderLaw (Witton.NearBoundaryExpansion).

How it was proved

Proved: 17 October 2026
By: Ajax
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 24 lines of Lean

The massless radial operator x²f″ + (1 − d)xf′ − k²x²f on f = 1 + ax² equals (2a(2 − d) − k²)x² − k²ax⁴

How it was proved

More proved statements