Provedads-cfthep-th-9802150near-boundary-expansionwitton
The x₀² coefficient of the massless near-boundary solution: 2a(2 − d) − k² = 0 iff a = −k²/(2(d − 2))
For all , if , then
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 : ℝ)) - ≠Not equal
- d and 2 are different. (
d ≠ 2) - ·Multiplication
- 2 times a. (
2 * a) - =Equality
- 2 · a · (2 − d) − k^2 and 0 are the same. (
2 * a * (2 - d) - k ^ 2 = 0) - ⟺If and only if
- 2 · a · (2 − d) − k^2 = 0 holds exactly when a = −(k^2)/(2 · (d − 2)) holds. (
2 * a * (2 - d) - k ^ 2 = 0 ↔ a = -(k ^…) - -Subtraction
- 2 minus d. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
2 - d) - aᵇPower
- k raised to the power 2. (
k ^ 2) - −xNegation
- The negative of k^2. (
-(k ^ 2)) - a/bDivision
- −(k^2) divided by 2 · (d − 2). In Lean, dividing by 0 gives 0. (
-(k ^ 2) / (2 * (d - 2)))
theorem near-boundary-second-order-coefficient (d k a : ℝ) (hd : d ≠ 2) :
2 * a * (2 - d) - k ^ 2 = 0 ↔ a = -(k ^ 2) / (2 * (d - 2))For a plane wave of wavenumber k, the massless radial equation on AdS_{d+1} applied to 1 + a x0^2 leaves the x0^2 coefficient 2a(2 - d) - k^2 (statement near-boundary-operator-on-quadratic-ansatz). It vanishes exactly for a = -k^2/(2(d - 2)), i.e. phi_2 = grad^2 phi_0/(2(d-2)): the solution has an x0^2 term, of lower order than the x0^d term for d > 2, which eq. (2.21) of hep-th/9802150 omits from its remainder. Decided in Alpha as wittonNearBoundaryCoefficientLaw and wittonRemainderClaimLaw.
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
- 18 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.