The massless d = 3 on-shell kernel k²/(ε(1 + kε)) splits into the contact part k²/(ε(1 − k²ε²)) and the odd part −k³/(1 − k²ε²)
For all , if , and , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- k, ε range over real numbers: the statement must hold for every choice. (
(k ε : ℝ)) - ≠Not equal
- ε and 0 are different. (
ε ≠ 0) - +Addition
- 1 plus k · ε. (
1 + k * ε) - -Subtraction
- 1 minus k · ε. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - k * ε) - =Equality
- (k^2/(ε · (1 + k · ε)) + −k^2/(ε · (1 + −k · ε)))/2 and k^2/(ε · (1 − k^2 · ε^2)) are the same. (
(k ^ 2 / (ε * (1 + k * ε)) + (-k) ^ 2 /…) - ∧And
- Both hold: (k^2/(ε · (1 + k · ε)) + −k^2/(ε · (1 + −k · ε)))/2 = k^2/…, and (k^2/(ε · (1 + k · ε)) − −k^2/(ε · (1 + −k · ε)))/2 = −(k^…. (
(k ^ 2 / (ε * (1 + k * ε)) + (-k) ^ 2 /…) - aᵇPower
- k raised to the power 2. (
k ^ 2) - a/bDivision
- k^2 divided by ε · (1 + k · ε). In Lean, dividing by 0 gives 0. (
k ^ 2 / (ε * (1 + k * ε))) - ·Multiplication
- k times ε. (
k * ε) - −xNegation
- The negative of k. (
-k)
theorem massless-d3-on-shell-kernel-even-odd-split (k ε : ℝ) (hε : ε ≠ 0) (h1 : 1 + k * ε ≠ 0) (h2 : 1 - k * ε ≠ 0) :
(k ^ 2 / (ε * (1 + k * ε)) + (-k) ^ 2 / (ε * (1 + -k * ε))) / 2 = k ^ 2 / (ε * (1 - k ^ 2 * ε ^ 2)) ∧ (k ^ 2 / (ε * (1 + k * ε)) - (-k) ^ 2 / (ε * (1 + -k * ε))) / 2 = -(k ^ 3 / (1 - k ^ 2 * ε ^ 2))The on-shell action of a massless scalar on the half space x0 >= eps in d = 3, with the Dirichlet condition imposed at eps, is (1/2) int d^3k/(2pi)^3 |phi0(k)|^2 W(k, eps) with W = k^2/(eps(1 + k eps)) (from the exact solution x0^{3/2} K_{3/2}(k x0) = e^{-k x0}(1 + k x0)). Its even part in k is the divergent contact term eps^{-1} k^2 + ..., which hep-th/9802150 drops in (2.21)-(2.23); its odd part -k^3/(1 - k^2 eps^2) -> -k^3 is the non-local two-point function, whose Fourier transform gives the NEGATIVE position-space kernel, so the sign printed in (2.23) is wrong. This statement is the algebraic split; the Bessel-function origin of W and the Fourier transform are not part of it. Decided in Alpha as wittonOddPartLaw and wittonContactTermLaw.
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
- 31 lines of Lean