Lemma: Horizon occupation covariance

For positive-frequency tests supported in a compact subset of $(0,\infty )$, the horizon state has

The infinity input is independent and has

These statements define finite packet covariances without requiring the stationary state to be a density matrix in the outgoing vacuum Fock representation.

Proof. Comparing (eq:currentexpansion) with (eq:thermalspectral) identifies the coefficients of the positive and negative frequency terms. Stationarity excludes an anomalous covariance supported at $\omega +{\omega }^{\prime }=0$ on the strictly positive-frequency test domain. This gives (eq:Hnumber)–(eq:Hanomalous).

For an explicit realization on any compact positive-frequency band, take two independent vacuum oscillator fields $b_1,b_2$ and set

Its commutator is $\delta (\omega -{\omega }^{\prime })$, and its vacuum covariances are precisely (eq:Hnumber) and (eq:Hanomalous). All multiplication factors are bounded on the chosen band. A third independent vacuum oscillator field realizes $a_{\mathrm{I}}$ and (eq:Inumber). The horizon occupation function in this realization is the function already derived in Lemma lem:fourier, not an additional input.