CV/Dispersion: relativistic dispersion ω_k = √(k² + m²) (EFT Stage 2a)

Category: CV (continuous variables — the multi-mode field).

Stage 1 (CV/FieldModes.lean) built the free field at a cutoff as a product of unit-frequency oscillators. Stage 2a gives the modes their relativistic frequencies: mode k carries momentum p k and oscillates at

ω(m, p) = √(p² + m²),

so the field's quanta are relativistic particles of mass m. This is what makes the mode sum a relativistic field rather than a generic collection of oscillators; spacetime itself is taken as given (the EFT posture — cutoff-independence, not the continuum limit).

What this file proves

The dispersion relation itself.

• omega_sq_sub_sq — the mass shell ω² − p² = m²: the Lorentz-invariant content of the dispersion relation, and the reason m deserves the name "mass".
• abs_le_omega — |p| ≤ ω: no mode carries energy below its momentum, the dispersion-level statement that excitations do not outrun the light cone.
• abs_mass_le_omega / omega_zero — the mass gap |m| ≤ ω, attained at p = 0: the rest energy is the floor.
• omega_massless — ω(0, p) = |p|, the light cone exactly.
• omega_le_newtonian — ω ≤ m + p²/(2m) for m > 0: the relativistic energy never exceeds the Newtonian rest-plus-kinetic energy. The non-relativistic limit stated as a clean inequality rather than an asymptotic expansion.
• omega_mono — higher momentum costs more energy.

The relativistic field.

• relFieldEnergy / relFieldHamiltonian — the free-field Hamiltonian with relativistic mode frequencies, ∑ₖ ω(m, pₖ)·(cₖ + ½); still diagonal in the configuration basis (relFieldHamiltonian_mulVec_single, relFieldHamiltonian_isHermitian), so the whole record-layer measurement account of CV/OscillatorBorn.lean applies verbatim — only the eigenvalues change.
• relFieldEnergy_quantum — the headline: adding one quantum to mode k₀ raises the field energy by exactly ω(m, p k₀). So the excitations are relativistic particles of mass m and momentum p k₀; the dispersion is a statement about the particle content, not a parameter choice.
• relFieldEnergy_vacuum — the zero-point energy ½∑ₖ ω(m, pₖ).
• relFieldEnergy_cutoff_independent — unchanged under raising the truncation, the Stage-1 cutoff-independence carried to relativistic frequencies.

What this file does NOT claim

Microcausality in its continuum form ([φ(x), φ(y)] = 0 at spacelike separation) is not proved here and does not hold exactly at a finite cutoff. The honest finite-cutoff locality statement — the Haag–Kastler one, that observables supported on disjoint mode sets commute — is CV/ModeLocality.lean. The continuum limit is deliberately deferred (CV/ApproxCCR.lean no_exact_finite_ccr).

References

CV/FieldModes.lean (Stage 1, the mode product); CV/OscillatorSpectrum.lean (oscEnergy, oscEnergy_cutoff_independent); CV/Position.lean (the spatial lattice); CV/ModeLocality.lean (Stage 2b, locality); specs/BACKLOG.md (the CV-chain row); specs/future-work.md.

The dispersion relation

noncomputable def CSD.CV.omega (m p : ℝ) : ℝ

The relativistic dispersion ω(m, p) = √(p² + m²): the frequency of the field mode of momentum p for a field of mass m.

Equations

• CSD.CV.omega m p = √(p ^ 2 + m ^ 2)

theorem CSD.CV.omega_nonneg (m p : ℝ) : 0 ≤ omega m p

theorem CSD.CV.omega_sq (m p : ℝ) : omega m p ^ 2 = p ^ 2 + m ^ 2

ω² = p² + m².

theorem CSD.CV.omega_sq_sub_sq (m p : ℝ) : omega m p ^ 2 - p ^ 2 = m ^ 2

The mass shell ω² − p² = m². The Lorentz-invariant content of the dispersion relation: the energy–momentum pair of a mode lies on the hyperboloid of invariant mass m.

theorem CSD.CV.abs_le_omega (m p : ℝ) : |p| ≤ omega m p

|p| ≤ ω — a mode's energy is never less than its momentum. At the level of the dispersion relation this is the statement that excitations stay inside the light cone.

theorem CSD.CV.abs_mass_le_omega (m p : ℝ) : |m| ≤ omega m p

The mass gap |m| ≤ ω — the rest energy is the floor of the spectrum.

theorem CSD.CV.omega_zero (m : ℝ) : omega m 0 = |m|

The mass gap is attained: a mode at rest has energy exactly |m|.

theorem CSD.CV.omega_massless (p : ℝ) : omega 0 p = |p|

The massless case is the light cone: ω(0, p) = |p|.

theorem CSD.CV.omega_pos {m : ℝ} (hm : m ≠ 0) (p : ℝ) : 0 < omega m p

A massive mode has strictly positive frequency.

theorem CSD.CV.omega_le_newtonian {m : ℝ} (hm : 0 < m) (p : ℝ) : omega m p ≤ m + p ^ 2 / (2 * m)

The non-relativistic bound ω ≤ m + p²/(2m). The relativistic energy never exceeds the Newtonian rest-plus-kinetic energy — the non-relativistic limit as an inequality, with no asymptotic expansion. The gap is exactly the p⁴/(4m²) term.

theorem CSD.CV.omega_mono (m : ℝ) {p q : ℝ} (h : |p| ≤ |q|) : omega m p ≤ omega m q

Higher momentum costs more energy.

The relativistic free field

noncomputable def CSD.CV.relFieldEnergy {K N : ℕ} (m : ℝ) (p : Fin K → ℝ) (c : FieldConfig K N) : ℝ

The relativistic field energy of a configuration: each mode k contributes ω(m, pₖ)·(cₖ + ½). Stage 1's fieldEnergy is the unit-frequency case.

Equations

• CSD.CV.relFieldEnergy m p c = ∑ k : Fin K, CSD.CV.omega m (p k) * CSD.CV.oscEnergy ↑(c k)

noncomputable def CSD.CV.relFieldHamiltonian (K N : ℕ) (m : ℝ) (p : Fin K → ℝ) : Matrix (FieldConfig K N) (FieldConfig K N) ℂ

The relativistic free-field Hamiltonian: diagonal in the configuration basis with the relativistic field energy on the diagonal.

Equations

• CSD.CV.relFieldHamiltonian K N m p = Matrix.diagonal fun (c : CSD.CV.FieldConfig K N) => ↑(CSD.CV.relFieldEnergy m p c)

theorem CSD.CV.relFieldHamiltonian_mulVec_single {K N : ℕ} (m : ℝ) (p : Fin K → ℝ) (c : FieldConfig K N) : (relFieldHamiltonian K N m p).mulVec (Pi.single c 1) = ↑(relFieldEnergy m p c) • Pi.single c 1

Configurations are energy eigenstates, now with relativistic eigenvalues. The Hamiltonian stays diagonal in the configuration basis, so the record-layer measurement account carries over verbatim from CV/OscillatorBorn.lean — only the eigenvalues change.

theorem CSD.CV.relFieldHamiltonian_isHermitian {K N : ℕ} (m : ℝ) (p : Fin K → ℝ) : (relFieldHamiltonian K N m p).IsHermitian

The relativistic Hamiltonian is Hermitian (diagonal with real entries).

theorem CSD.CV.relFieldEnergy_nonneg {K N : ℕ} (m : ℝ) (p : Fin K → ℝ) (c : FieldConfig K N) : 0 ≤ relFieldEnergy m p c

The field energy is non-negative (each mode contributes ω ≥ 0 times cₖ + ½ > 0).

theorem CSD.CV.relFieldEnergy_vacuum {K : ℕ} (m : ℝ) (p : Fin K → ℝ) {N : ℕ} [NeZero N] : (relFieldEnergy m p fun (x : Fin K) => 0) = (∑ k : Fin K, omega m (p k)) / 2

The zero-point energy. The empty configuration has energy ½∑ₖ ω(m, pₖ).

theorem CSD.CV.relFieldEnergy_quantum {K N : ℕ} (m : ℝ) (p : Fin K → ℝ) {c d : FieldConfig K N} (k₀ : Fin K) (hk₀ : ↑(d k₀) = ↑(c k₀) + 1) (hrest : ∀ (k : Fin K), k ≠ k₀ → ↑(d k) = ↑(c k)) : relFieldEnergy m p d - relFieldEnergy m p c = omega m (p k₀)

The headline: one quantum in mode k₀ costs exactly ω(m, p k₀).

If d has one more quantum in mode k₀ than c, and agrees with c elsewhere, the field energy rises by exactly the relativistic frequency of that mode. So the field's excitations are relativistic particles of mass m and momentum p k₀ — the dispersion relation is a statement about the particle content, not a parameter choice.

theorem CSD.CV.relFieldEnergy_cutoff_independent {K N M : ℕ} (m : ℝ) (p : Fin K → ℝ) (c : FieldConfig K N) (d : FieldConfig K M) (h : ∀ (k : Fin K), ↑(c k) = ↑(d k)) : relFieldEnergy m p c = relFieldEnergy m p d

Cutoff-independence. Configurations with the same per-mode occupation have the same relativistic field energy, regardless of the truncation — the Stage-1 statement carried to relativistic frequencies.