Positive energy of a one-parameter unitary group

The positive-energy (spectrum) condition for a strongly continuous one-parameter unitary group on a Hilbert space, in the bounded-generator scaffold form: the group is t ↦ exp(i t P) for a positive bounded operator P. This is spacetime-agnostic — it is shared by the Minkowski (translation) and curved (Killing-flow) spectrum conditions.

The generator of a physical translation/Killing flow is unbounded, so requiring P bounded is a genuine restriction; the faithful unbounded form needs Stone's theorem and unbounded self-adjoint operators, which Mathlib does not yet provide.

Main results

• Physicslib4.AQFT.IsPositiveEnergy — the bounded-generator positive-energy condition.
• isPositiveEnergy_const_refl — the trivial group has positive energy.
• exp_generator_unique — the generator is unique.
• IsPositiveEnergy.conj — positive energy is a unitary invariant.
• IsPositiveEnergy.strongContinuous — a positive-energy group is strongly continuous.

def Physicslib4.AQFT.IsPositiveEnergy {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (V : ℝ → H ≃ₗᵢ[ℂ] H) : Prop

Positive-energy condition (bounded-generator scaffold). A one-parameter unitary group V : ℝ → (H ≃ₗᵢ[ℂ] H) has positive energy when its generator is a positive bounded operator: there is P : H →L[ℂ] H with P.IsPositive (hence self-adjoint, with non-negative spectrum) such that V t = exp(i t P) for every t.

The generator of a physical translation is unbounded, so requiring P bounded is a restriction; the faithful unbounded form needs Stone's theorem and unbounded self-adjoint operators, absent from Mathlib. The positivity P.IsPositive is the energy-positivity that the spectrum condition asserts.

Equations

• Physicslib4.AQFT.IsPositiveEnergy V = ∃ (P : H →L[ℂ] H), P.IsPositive ∧ ∀ (t : ℝ) (x : H), (V t) x = (NormedSpace.exp ((↑t * Complex.I) • P)) x

theorem Physicslib4.AQFT.isPositiveEnergy_const_refl {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] : IsPositiveEnergy fun (x : ℝ) => LinearIsometryEquiv.refl ℂ H

The constant (trivial) unitary group t ↦ id has positive energy, with zero generator P = 0: exp(0) = 1 = id, and 0 is a positive operator.

theorem Physicslib4.AQFT.exp_generator_unique {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P Q : H →L[ℂ] H} (h : ∀ (t : ℝ) (x : H), (NormedSpace.exp ((↑t * Complex.I) • P)) x = (NormedSpace.exp ((↑t * Complex.I) • Q)) x) : P = Q

Uniqueness of the positive-energy generator. If two bounded generators induce the same one-parameter unitary group — exp(i t P) = exp(i t Q) for all t — they are equal. Differentiating at t = 0 gives i \cdot P = i \cdot Q, hence P = Q; positivity is not needed. So the generator witnessing IsPositiveEnergy is unique.

theorem Physicslib4.AQFT.IsPositiveEnergy.conj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (W : H ≃ₗᵢ[ℂ] H) {V : ℝ → H ≃ₗᵢ[ℂ] H} (hV : IsPositiveEnergy V) : IsPositiveEnergy fun (t : ℝ) => (W.symm.trans (V t)).trans W

Positive energy is a unitary invariant. If a one-parameter unitary group V has positive energy, so does its conjugate t ↦ W ∘ V t ∘ W⁻¹ by a unitary W, with generator W P W⁻¹ (positive, being the unitary conjugate of the positive generator P). Physically: the spectrum condition does not depend on the choice of unitary frame.

theorem Physicslib4.AQFT.IsPositiveEnergy.strongContinuous {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {V : ℝ → H ≃ₗᵢ[ℂ] H} (hV : IsPositiveEnergy V) (x : H) : Continuous fun (t : ℝ) => (V t) x

A positive-energy group is strongly continuous. The bounded-generator scaffold V t = exp(i t P) is automatically strongly continuous: t ↦ V t x is continuous for every x, since t ↦ (i t) • P is continuous and the operator exponential is continuous. This justifies describing a positive-energy group as a strongly continuous one-parameter unitary group.