klein_gordon_zero_mass_iff_wave_equation
theoremverifiedoriginal
A scalar field φ : ℝ × ℝ → ℝ satisfies the one-dimensional Klein-Gordon equation with mass parameter 0 and speed c if and only if it satisfies the one-dimensional wave equation with speed c.
Statement
theorem klein_gordon_zero_mass_iff_wave_equation (c : ℝ) (φ : ℝ × ℝ → ℝ) :
KleinGordonEquation1D 0 c φ ↔ WaveEquation1D c φ- Source
- Peskin & Schroeder, An Introduction to Quantum Field Theory, ch. 2
- Verified
- 11 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Built on 2
- WaveEquation1DA scalar field u : ℝ × ℝ → ℝ satisfies the one-dimensional wave equation with wave speed c if for all (x, t), the second partial…
- KleinGordonEquation1DA scalar field φ : ℝ × ℝ → ℝ satisfies the one-dimensional Klein-Gordon equation with mass parameter m and propagation speed c if for all…
Read back from the Lean
For every real number $c$ and every function $\phi : \mathbb{R} \times \mathbb{R} \to \mathbb{R}$, $\phi$ satisfies the 1D Klein-Gordon equation with mass parameter $0$ and parameter $c$ if and only if $\phi$ satisfies the 1D wave equation with speed parameter $c$.
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
/-- In the massless limit m = 0, the 1D Klein-Gordon equation is equivalent to the 1D wave equation. -/ theorem klein_gordon_zero_mass_iff_wave_equation (c : ℝ) (φ : ℝ × ℝ → ℝ) : KleinGordonEquation1D 0 c φ ↔ WaveEquation1D c φ := by dsimp [KleinGordonEquation1D, WaveEquation1D] simp [sub_eq_zero]