P4: the dispersion earned — covariance selects ω = √(p² + m²)

Category: CV (continuous variables — relativistic structure forced, not defined; eft-pillars-plan.md P4).

CV/Dispersion.lean defines omega m p := √(p² + m²); CV/Boost.lean proves the forward direction (boost_omega: the definition is covariant). specs/necessity-audit.md records the gap: the converse — that covariance selects this dispersion — was proved nowhere. This module is the converse, in two independent selections chained into a characterisation, with the mass gap shown sharp. Scoped first in specs/dispersion-earned-plan.md.

• ★ cone_preserving_is_boost — the light cone selects the boost group: any linear map of the (E, p) plane preserving the two light rays forward, with unit determinant, IS boostE χ/boostP χ at some rapidity. The cosh/sinh form is derived, not posited: the rays are eigendirections, the eigenvalues are reciprocal and positive, and χ = −arsinh b does the rest.
• ★ boost_covariance_selects_omega — the boosts select the dispersion: if ω 0 = m > 0 and the graph of ω is boost-covariant (the exact law boost_omega establishes for omega m), then ω = omega m. The single orbit through the rest point (m, 0) covers every momentum, and single-valuedness pins ω on it — no continuity, evenness, or measurability assumed.
• omega_cone_covariant — non-vacuity from the corpus's own theorem: omega m satisfies the full cone-symmetry covariance (via cone_preserving_is_boost + the existing boost_omega).
• ★★ cone_symmetry_characterises_omega — P4's characterisation: for m > 0, ω = omega m iff ω has rest energy m and its graph is covariant under every ray-preserving unimodular linear symmetry. Relativity at the shell level, forced rather than written down.
• massless_covariance_not_selecting — the mass gap is sharp: at m = 0 selection fails — ω = id (the right-moving light ray) is boost-covariant with rest energy 0 yet differs from omega 0 = |p|. So 0 < m above is necessary, not a convenience.

⚠️ Honest scope: kinematic level, inherited from CV/Boost.lean. No boost action on the finite mode lattice is claimed (a lattice is not boost-invariant; standard cutoff honesty), and the identification of the (E, p) light rays with the dynamical Lieb-Robinson cone is not claimed here — the LR cone is an upper bound with a model-dependent velocity, not an exact invariant set.

References

specs/eft-pillars-plan.md (P4); specs/dispersion-earned-plan.md (scoping); specs/necessity-audit.md (the recorded overstatement this closes); specs/future-work.md; CV/Dispersion.lean (omega, omega_massless); CV/Boost.lean (boostE, boostP, boost_omega).

The rest-orbit helper

theorem CSD.CV.mul_cosh_arsinh_div {m : ℝ} (hm : 0 < m) (p : ℝ) : m * Real.cosh (Real.arsinh (p / m)) = omega m p

The rest-point orbit parametrisation: m · cosh (arsinh (p/m)) = ω(m, p). This is the algebraic heart of the selection — the boost orbit through the rest point (m, 0) traces out exactly the mass shell.

The boosts select the dispersion

theorem CSD.CV.boost_covariance_selects_omega {ω : ℝ → ℝ} {m : ℝ} (hm : 0 < m) (h0 : ω 0 = m) (hcov : ∀ (χ p : ℝ), boostE χ (ω p) p = ω (boostP χ (ω p) p)) : ω = omega m

★ Boost covariance selects the dispersion. If ω has rest energy m > 0 and its graph is boost-covariant — the exact law boost_omega proves for omega m — then ω IS omega m. The single orbit through the rest point (m, 0) covers every momentum (χ = −arsinh (p/m)), and single-valuedness of the graph pins ω on it. No continuity, evenness, or measurability is assumed.

The cone selects the boosts

theorem CSD.CV.cone_preserving_is_boost {a b c d : ℝ} (hR : a + b = c + d) (hRpos : 0 < a + b) (hL : a - b = d - c) (hLpos : 0 < a - b) (hdet : a * d - b * c = 1) : ∃ (χ : ℝ), ∀ (E p : ℝ), a * E + b * p = boostE χ E p ∧ c * E + d * p = boostP χ E p

★ The light cone selects the boost group. A linear map (E, p) ↦ (aE + bp, cE + dp) that preserves the right light ray forward (a + b = c + d > 0), preserves the left light ray forward (a − b = d − c > 0), and is unimodular (ad − bc = 1) is the boost at rapidity χ = −arsinh b. The cosh/sinh form is derived: the rays are eigendirections with reciprocal positive eigenvalues.

Non-vacuity: the corpus's dispersion satisfies the full covariance

theorem CSD.CV.omega_cone_covariant (m : ℝ) {a b c d : ℝ} (hR : a + b = c + d) (hRpos : 0 < a + b) (hL : a - b = d - c) (hLpos : 0 < a - b) (hdet : a * d - b * c = 1) (p : ℝ) : a * omega m p + b * p = omega m (c * omega m p + d * p)

omega m is covariant under EVERY ray-preserving unimodular linear symmetry — non-vacuity of the characterisation below, assembled from cone_preserving_is_boost and the corpus's own boost_omega.

The characterisation

theorem CSD.CV.cone_symmetry_characterises_omega {ω : ℝ → ℝ} {m : ℝ} (hm : 0 < m) : (ω 0 = m ∧ ∀ (a b c d : ℝ), a + b = c + d → 0 < a + b → a - b = d - c → 0 < a - b → a * d - b * c = 1 → ∀ (p : ℝ), a * ω p + b * p = ω (c * ω p + d * p)) ↔ ω = omega m

★★ P4's characterisation: relativity at the shell level, forced. For m > 0: ω = omega m iff ω has rest energy m and its graph is covariant under every linear symmetry of the (E, p) plane that preserves the two light rays forward and is unimodular. The forward direction chains the two selections (cone → boosts → dispersion); the backward direction is omega_cone_covariant, i.e. the corpus's own boost_omega.

Sharpness: the mass gap is necessary

theorem CSD.CV.massless_covariance_not_selecting : ∃ (ω : ℝ → ℝ), ω 0 = 0 ∧ (∀ (χ p : ℝ), boostE χ (ω p) p = ω (boostP χ (ω p) p)) ∧ ω ≠ omega 0

The mass gap is sharp. At m = 0 the selection fails: ω = id — the right-moving light ray as a graph — is boost-covariant with rest energy 0, yet is not omega 0 = |p|. So 0 < m in the selection theorems is necessary, not a convenience: the massless shell degenerates onto the cone, where covariant graphs are unions of half-rays and no longer unique.