Scope, dependencies, and the release boundary

The finite-mode Gaussian construction is standard in structure Weedbrook. The supplied companion account attributes a general version to En02-E, at :gaussian, :outcov, and :K En02EAccount. The full En02-E source is not supplied. We therefore give the needed specialization and its proof explicitly rather than importing an unseen theorem or claiming novelty for Gaussian diagonalization.

The remaining constructions are ordinary channel calculations. Landmark I is optional semantic input for calling finite destructive readout $\mathsf{Enter}$; it is not a field-state or apparatus premise.

boundary. The source supplies analytical arguments. No compilation, machine checking, numerical experiment, statistical calibration, or physical realization is asserted. The term “certified” refers to explicit mathematical estimates under stated model data.

. We use $c=\hslash =k_B=1$, $G,M>0$, and

Channels are normal CPTP maps on trace-class operators. A finite spectator is denoted $S$; an arbitrary finite-dimensional external reference is denoted $R$. Their tensor placements are retained throughout. The normal state identities also hold with separable references.

We write $\Gamma (U)$ for bosonic second quantization of a one-particle unitary. This notation is distinct from the greybody probability ${\Gamma }_{\ell }(\omega )$.