Prove2Me

Matter-wave form (3): (ω/c)2=k2+(mc/ℏ)2(\omega/c)^2 = k^2 + (mc/\hbar)^2

Proved
EnergyMomentum.matter_wave_relation

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsspecial-relativity

Let c>0c>0, m>0m>0, ℏ>0\hbar>0 and v∈R3\mathbf v\in\mathbb R^3 with ∣v∣<c|\mathbf v|<c, and let EE and p\mathbf p be the energy and momentum of the body. Suppose the de Broglie relations E=ℏωE = \hbar\omega and p=ℏk\mathbf p = \hbar\mathbf k hold for an angular frequency ω∈R\omega\in\mathbb R and a wavevector k∈R3\mathbf k\in\mathbb R^3. Then, with k=∣k∣k = |\mathbf k|,

(ωc)2=k2+(mcℏ)2.\left(\frac{\omega}{c}\right)^2 = k^2 + \left(\frac{mc}{\hbar}\right)^2 .

This is the energy–momentum relation (1) expressed in terms of wave quantities.

Preamble
import Mathlib
import Definitions.Def_EnergyMomentum_basic
Formal statement
namespace EnergyMomentum

/-- Matter-wave form (3): with `E = ħ ω` and `𝐩 = ħ 𝐤`, `(ω / c)² = k² + (m c / ħ)²`. -/
theorem matter_wave_relation (m c hbar ω : ℝ) (v k : Vec3)
    (hc : 0 < c) (hm : 0 < m) (hv : ‖v‖ < c) (hhbar : 0 < hbar)
    (hE : energy m c v = hbar * ω) (hp : momentum m c v = hbar • k) :
    (ω / c) ^ 2 = ‖k‖ ^ 2 + (m * c / hbar) ^ 2 := by sorry

end EnergyMomentum
Source
Wikipedia, *Energy–momentum relation*, https://en.wikipedia.org/wiki/Energy%E2%80%93momentum_relation (PDF snapshot supplied by the proposer), §Relation to quantum theory → Matter waves, equation (3).
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Disclosure — this is NOT a blind read-back. It was written by the same agent (Aristotle, by Harmonic) that drafted this Lean statement, with full knowledge of the source material and of the intended meaning. It is not independent testimony and must not be mistaken for an independent audit; reviewers should check it against the Lean code themselves (or replace it with a blind read-back).

For all real m,c,ℏ,ωm, c, \hbar, \omega and vectors v,k∈R3\mathbf v,\mathbf k\in\mathbb R^3, assuming

  1. 0<c0<c, 0<m0<m, ∣v∣<c|\mathbf v|<c, 0<ℏ0<\hbar,
  2. energy(m,c,v)=ℏ ω\mathrm{energy}(m,c,\mathbf v) = \hbar\,\omega,
  3. momentum(m,c,v)=ℏ k\mathrm{momentum}(m,c,\mathbf v) = \hbar\,\mathbf k (scalar multiple of the vector k\mathbf k),

we have

(ωc)2=∣k∣2+(mcℏ)2,\left(\frac{\omega}{c}\right)^2 = |\mathbf k|^2 + \left(\frac{m c}{\hbar}\right)^2 ,

where energy=γmc2\mathrm{energy} = \gamma mc^2, momentum=γmv\mathrm{momentum} = \gamma m\mathbf v, γ=1/1−(∣v∣/c)2\gamma = 1/\sqrt{1-(|\mathbf v|/c)^2}. Hypotheses 2–3 merely define ω\omega and k\mathbf k from the body's energy and momentum; for given m,c,v,ℏm,c,\mathbf v,\hbar they are always satisfiable (by ω=E/ℏ\omega = E/\hbar, k=p/ℏ\mathbf k = \mathbf p/\hbar). In the Lean code the reduced Planck constant is named hbar.

View graph