Exact Complex Reference-Frame Tax

Abstract

The finite exchange model has an exact complex-amplitude fidelity, tax, and paired top eigenspace.

Theorem 1.1 (The complex 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{C}}^N,F_e(c)=|Jc{|}_2^2,\\ F_e^{\mathrm{opt}}(N):=\underset{c\in {\mathbb{C}}^N,|c{|}_2=1}{\max }{F}_e(c)=\cos (\frac{\pi }{N+1}{)}^2,\\ 1-F_e^{\mathrm{opt}}(N)=\sin (\frac{\pi }{N+1}{)}^2,\\ 1-F_e(m\mapsto 1/\sqrt{N})=\frac{3}{2N},\\ {\mathrm{finrank}}_{\mathbb{C}}(\mathrm{eigenspace}(J^2,\cos (\frac{\pi }{N+1}{)}^2))=2\end{array}$$

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

Source. Repository-derived.

Commentary.

For ladders of length at least two, the exchange permutation is unitary and conserves total excitation. For every complex reference vector, the channel entanglement fidelity is exactly the squared norm of zero-boundary nearest-neighbour averaging.

The complex unit sphere has the same sharp cosine-squared optimum as the real sphere, so the complementary optimal tax is sine-squared. The normalized flat complex vector has tax three over two N.

The squared complex path-average eigenspace at the sharp eigenvalue has complex dimension two. The lower bound on N is necessary because the one-level flat tax is one rather than three halves.

Repository search found exact declarations for all four complex-amplitude clauses in the frozen complexification module; this declaration applies them directly and adds no replacement proof.

References

• Truth anchor: D5/S3/QuantumBounds/ReferenceFrame/ComplexReferenceFrameTaxExact.complex_reference_frame_tax_exact
• Dependency: D5/S3/QuantumBounds/ReferenceFrame/Complexification