CV-14: boost covariance of the mass shell

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

CV/Dispersion.lean proved the mass shell ω² − p² = m² and read the Lorentz content off its shape. This module makes that content a theorem: the 1+1D boost acts on energy–momentum pairs, and the shell is its invariant.

• boostE / boostP — the 1+1D boost at rapidity χ: E ↦ E cosh χ − p sinh χ, p ↦ p cosh χ − E sinh χ.
• boostE_zero / boostP_zero, boostE_add / boostP_add — the boosts form a one-parameter group: rapidities add (cosh/sinh addition formulas). So "boost" is earned, not a name for an arbitrary map.
• ★ boost_invariant — E'² − p'² = E² − p² for every rapidity: the quadratic form is preserved (cosh² − sinh² = 1).
• ★★ boost_mass_shell — the boosted dispersion pair satisfies the SAME shell: (ω')² − (p')² = m². ⚠️ Boost covariance of a posited (E, p)-plane cone, not Lorentz content derived (name check 2026-09-05, CR-8). The two-dimensional (ω, p) plane and its cone are set up, not deduced; what is proved is that the boost family preserves the shell on them. Nothing here derives the Lorentz group, four-dimensional spacetime, or the signature.
• boost_forward — the forward shell is preserved (0 ≤ ω'), using abs_le_omega and |sinh| ≤ cosh: boosts cannot turn a physical mode into a negative-energy one.
• ★ boost_omega — the sharp form: the boosted energy IS the dispersion evaluated at the boosted momentum, ω' = ω(m, p'). The dispersion relation is boost-covariant on the nose.

⚠️ Honest scope: this is one-particle kinematic covariance, at the level of the dispersion relation. There is no claim of a boost action on the mode lattice — a finite lattice of modes is not boost-invariant, and that asymmetry is the standard cutoff honesty rather than an oversight (the mode structure is a cutoff artefact; the dispersion is what survives the limit). No continuum claims (ApproxCCR.no_exact_finite_ccr stands).

References

CV/Dispersion.lean (omega, omega_sq_sub_sq, abs_le_omega); specs/eft-stage4-plan.md (row CV-14); specs/future-work.md.

The 1+1D boost

noncomputable def CSD.CV.boostE (χ E p : ℝ) : ℝ

The boosted energy at rapidity χ.

Equations

• CSD.CV.boostE χ E p = E * Real.cosh χ - p * Real.sinh χ

noncomputable def CSD.CV.boostP (χ E p : ℝ) : ℝ

The boosted momentum at rapidity χ.

Equations

• CSD.CV.boostP χ E p = p * Real.cosh χ - E * Real.sinh χ

@[simp]

theorem CSD.CV.boostE_zero (E p : ℝ) : boostE 0 E p = E

@[simp]

theorem CSD.CV.boostP_zero (E p : ℝ) : boostP 0 E p = p

theorem CSD.CV.boostE_add (χ₁ χ₂ E p : ℝ) : boostE χ₂ (boostE χ₁ E p) (boostP χ₁ E p) = boostE (χ₁ + χ₂) E p

Rapidities add on the energy component.

theorem CSD.CV.boostP_add (χ₁ χ₂ E p : ℝ) : boostP χ₂ (boostE χ₁ E p) (boostP χ₁ E p) = boostP (χ₁ + χ₂) E p

Rapidities add on the momentum component.

The invariant

theorem CSD.CV.boost_invariant (χ E p : ℝ) : boostE χ E p ^ 2 - boostP χ E p ^ 2 = E ^ 2 - p ^ 2

★ The boost preserves the quadratic form E² − p².

theorem CSD.CV.boost_mass_shell (m p χ : ℝ) : boostE χ (omega m p) p ^ 2 - boostP χ (omega m p) p ^ 2 = m ^ 2

★★ Boost covariance of the mass shell: the boosted energy–momentum pair of a mode satisfies the same shell, with the same mass. ⚠️ Boost covariance of a posited (E, p)-plane cone — not a derivation of Lorentz structure; see the module header.

The forward shell

theorem CSD.CV.abs_sinh_le_cosh (χ : ℝ) : |Real.sinh χ| ≤ Real.cosh χ

|sinh χ| ≤ cosh χ.

theorem CSD.CV.boost_forward (m p χ : ℝ) : 0 ≤ boostE χ (omega m p) p

The forward shell is preserved: a boost never turns a physical mode into a negative-energy one.

theorem CSD.CV.boost_omega (m p χ : ℝ) : boostE χ (omega m p) p = omega m (boostP χ (omega m p) p)

★ The dispersion relation is boost-covariant on the nose: the boosted energy IS the dispersion evaluated at the boosted momentum.