Theorem: Exact finite Page curve

Under Definition def:haar, for every fixed pure input independent of $U$,

The value is independent of that fixed input and of the code embedding $J$. It satisfies

It increases strictly up to the middle and decreases strictly afterward. For odd $N$, the two central cuts have equal maximal mean entropy. For even $N$, the unique maximal mean occurs at $k=N/2$.

Proof. Haar invariance makes $UJ|\psi ⟩$ a uniform unit vector. The two reductions of a bipartite pure state have the same nonzero spectrum. The calculation in Appendix app:page therefore applies with $m=m_k$, $n=n_k$, and gives (eq:page). This is the Page–Sen average, rederived there with normalization explicit PageAverage,Sen.

The endpoint and symmetry statements follow immediately. To verify monotonicity, consider consecutive cuts lying on the early half, so $m^{\prime }=sm$, $n^{\prime }=n/s$, with $m^{\prime }\le n^{\prime }$. Their difference, in natural entropy units, is

The first term is at least $1-1/s$. Since $n\ge s^{2}m$, the difference is at least

Symmetry proves the decreasing half and the central statements.