Exact Finite Reference-Frame Tax

Abstract

The finite exchange model has an exact fidelity bridge, sharp tax, restricted flat tax, and paired top eigenspace.

Theorem 1.1 (The finite reference-frame tax is exact).

$$\begin{array}{c}N\in \mathbb{N},2\le N⟶\\ U_N^{\ast }{U}_N=I,n(exchange(x))=n(x),\\ \forall c\in {\mathbb{R}}^N,{\mathcal{E}}_c(\rho )=\sum _{r\in \mathrm{Fin}(N)}{K}_r\rho K_r^{\ast },\\ \forall c\in {\mathbb{R}}^N,F_e(c)=Q_N(c)=|Jc{|}_2^2,\\ F_e^{\mathrm{opt}}(N):=\underset{c\in {\mathbb{R}}^N,{\sum }_i{c}_i^2=1}{\max }{F}_e(c)=\cos (\frac{\pi }{N+1}{)}^2,\\ 1-F_e^{\mathrm{opt}}(N)=\sin (\frac{\pi }{N+1}{)}^2,\\ 2\le N⟶1-Q_N((\frac{1}{\sqrt{N}}{)}_{m\in \mathrm{Fin}(N)})=\frac{3}{2N},\\ {\mathrm{squaredTopEigenspace}}_{\mathbb{R}}(N)={\mathrm{topModeSpace}}_{\mathbb{R}}(N),{\mathrm{finrank}}_{\mathbb{R}}({\mathrm{squaredTopEigenspace}}_{\mathbb{R}}(N))=2\end{array}$$

Proof. Machine-checked in Lean as D5/S3/QuantumBounds/ReferenceFrame/ReferenceFrameTaxExact.reference_frame_tax_exact (✓ std3). ∎

Source. Repository-derived.

Commentary.

The declaration packages the concrete exchange permutation, its conservation law, the finite Kraus representation, and both exact fidelity forms. It then applies the frozen sharp quadratic bound, the sine identity, the flat identity for ladders of length at least two, and the imported paired top-eigenspace characterization.

The lower bound on the ladder length is explicit because the one-level flat calculation has tax one rather than the displayed three-halves formula.

References

• Truth anchor: D5/S3/QuantumBounds/ReferenceFrame/ReferenceFrameTaxExact.reference_frame_tax_exact
• Dependency: D5/S3/QuantumBounds/ReferenceFrame/ChannelFidelityBridge
• Dependency: D5/S3/QuantumBounds/ReferenceFrame/TopEigenspace