KleinGordonEquation1D
A scalar field φ : ℝ × ℝ → ℝ satisfies the one-dimensional Klein-Gordon equation with mass parameter m and propagation speed c if for all (x, t), the second time derivative minus c^2 times the second spatial derivative plus m^2 * φ(x, t) equals zero.
Statement
def KleinGordonEquation1D (m c : ℝ) (φ : ℝ × ℝ → ℝ) : Prop
- Source
- Peskin & Schroeder, An Introduction to Quantum Field Theory, ch. 2
- Verified
- 11 Sep 2026
- Axioms
- none listed
- Used by 1
- klein_gordon_zero_mass_iff_wave_equationA scalar field φ : ℝ × ℝ → ℝ satisfies the one-dimensional Klein-Gordon equation with mass parameter 0 and speed c if and only if it…
Read back from the Lean
Given real parameters m, c : ℝ and a function φ : ℝ × ℝ → ℝ, KleinGordonEquation1D m c φ asserts that for all x, t : ℝ, the second derivative with respect to the second coordinate (evaluating deriv (deriv (fun s => φ (x, s))) at t) minus c^2 times the second derivative with respect to the first coordinate (evaluating deriv (deriv (fun y => φ (y, t))) at x) plus m^2 * φ (x, t) equals 0.
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- A real scalar field satisfies the 1D Klein-Gordon equation with mass m and speed c if d^2/dt^2 φ - c^2 d^2/dx^2 φ + m^2 φ = 0. -/ def KleinGordonEquation1D (m c : ℝ) (φ : ℝ × ℝ → ℝ) : Prop := ∀ x t : ℝ, deriv (deriv (fun s => φ (x, s))) t - c^2 * deriv (deriv (fun y => φ (y, t))) x + m^2 * φ (x, t) = 0