Hankel Bogoliubov Lift

Abstract

A finite contractive singular-value family has a canonical Bogoliubov lift.

Theorem 1.1 (Finite contractive singular values have a Bogoliubov lift).

$$\forall n\in \mathbb{N},\sigma \in \mathrm{Fin}(n)to\mathbb{R},\forall j\in \mathrm{Fin}(n),0\le {\sigma }_j\wedge {\sigma }_j<1\Rightarrow let{\alpha }_j=\cosh (\mathrm{artanh}({\sigma }_j));let{\beta }_j=\sinh (\mathrm{artanh}({\sigma }_j));\forall j\in \mathrm{Fin}(n),{\alpha }_j^2-{\beta }_j^2=1\wedge \forall j\in \mathrm{Fin}(n),\left|{\alpha }_j\right|=\frac{1}{\mathrm{sqrt}(1-{\sigma }_j^2)}\wedge \forall j\in \mathrm{Fin}(n),\left|{\beta }_j\right|=\frac{{\sigma }_j}{\mathrm{sqrt}(1-{\sigma }_j^2)}\wedge \forall j\in \mathrm{Fin}(n),{\beta }_j^2=\frac{{\sigma }_j^2}{1-{\sigma }_j^2}.$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Bogoliubov/HankelBogoliubovLift.hankel_bogoliubov_lift (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a finite indexed family of Hankel singular values with 0 <= sigma_j < 1, define r_j = artanh(sigma_j), alpha_j = cosh(r_j), and beta_j = sinh(r_j).

The diagonal coefficient operators satisfy the canonical CCR identity pointwise. The strict interval hypothesis makes the square-root denominator positive and yields the displayed amplitude and particle-number formulas.

The pointwise CCR is the finite diagonal form of alpha_H^* alpha_H - beta_H^* beta_H = I; no infinite-dimensional operator is assumed.

References

• Truth anchor: D5/S3/Quantum/Bogoliubov/HankelBogoliubovLift.hankel_bogoliubov_lift
• Dependency: D5/S3/Quantum/Bogoliubov/BogoliubovNormConservation