Exact Complex Reference-Frame Tax and Optimal Span

Abstract

The finite exchange model has an exact complex-amplitude tax and an explicitly identified paired sine-mode optimum space.

Theorem 1.1 (The complex reference-frame tax and optimal span are 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{eigenspace}(J^2,\cos (\frac{\pi }{N+1}{)}^2)={\mathrm{span}}_{\mathbb{C}}(\{v_1,v_N\}),\\ {\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/ComplexReferenceFrameTaxExactSpan.complex_reference_frame_tax_exact_span (✓ 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 sharp cosine-squared optimum, so its complementary optimal tax is sine-squared. The normalized flat complex vector has tax three over two N.

The full squared path-average eigenspace at the sharp eigenvalue equals the complex span of the coerced low-edge and high-edge sine modes, and that space has complex dimension two.

The lower bound on N records the frozen one-level counterexample to the flat formula. The proof applies the existing exact complex clauses and reconstructs only the span equality that was previously private.

References

• Truth anchor: D5/S3/QuantumBounds/ReferenceFrame/ComplexReferenceFrameTaxExactSpan.complex_reference_frame_tax_exact_span
• Dependency: D5/S3/QuantumBounds/ReferenceFrame/ComplexReferenceFrameTaxExact