pureTwoQubitReducedEntropyTarget_holds
plain-language theorem explainer
For any normalized pure two-qubit amplitude matrix, the von Neumann entropy of the single-qubit reduced density equals the binary entropy of (1 + √(1 − C²))/2, with C the Wootters concurrence. Anyone citing the pure-state entropy–concurrence identity or Track 2.B positivity will use this. The proof cases on the two eigenvalue orderings of the reduced density and matches each to the binary-entropy expansion via the λ± identities.
Claim. Let $A$ be a $2\times 2$ complex amplitude matrix with $\sum_{i,j}|A_{ij}|^2=1$, and let $C(A)=2\|\det A\|$ be its Wootters concurrence. Then the von Neumann entropy of the reduced density of $A$ equals the binary entropy $h\bigl((1+\sqrt{1-C(A)^2})/2\bigr)$, where $h(p)=-p\log p-(1-p)\log(1-p)$.
background
Track 2.B of the pure two-qubit module closes the chain from Wootters concurrence of a pure amplitude matrix to strict positivity of entanglement entropy. The module records the standard pure-state simplification $C(A)=2|\det A|$ and builds the reduced density $\rho_1=\mathrm{tr}_2|\psi\rangle\langle\psi|$ from $A$.
The Prop-shaped sub-target PureTwoQubitReducedEntropyTarget asserts that a chosen von Neumann functional on $2\times 2$ matrices equals binary entropy of the larger Schmidt eigenvalue $(1+\sqrt{1-C^2})/2$ whenever $A$ is Frobenius-normalized. The canonical spectral definition sums $-\lambda\log\lambda$ over the two eigenvalues of the reduced density.
Upstream, concurrence is nonnegative and at most one on normalized states; the reduced-density eigenvalues are exactly $\lambda_\pm(C)=(1\pm\sqrt{1-C^2})/2$ up to order; and binary entropy at $\lambda_+$ equals the negative sum of $\lambda_\pm\log\lambda_\pm$. Binary entropy is symmetric about $1/2$, so either eigenvalue ordering yields the same value.
proof idea
Tactic proof. Normalize the hypothesis to Frobenius squared norm one, then invoke concurrence $\le 1$ on normalized states. Case-split on the eigenvalue lemma that places the reduced spectrum at $(\lambda_+(C),\lambda_-(C))$ or the swap.
In the matching order: unfold the spectral entropy, rewrite the two-term Fin sum by the eigenvalue equalities, and apply the private identity that binary entropy of $\lambda_+$ equals $-(\lambda_+\log\lambda_++\lambda_-\log\lambda_-)$; unfold $\lambda_+$ and finish by reflexivity.
In the swapped order: the same rewrite produces the sum with $\lambda_-$ first; an ac_rfl commutativity step restores the order required by the binary-entropy identity, then the same unfold closes. No external analytic estimates beyond those lemmas.
why it matters
This is the reduced-density-matrix half of Track 2.B. The module status line marks the track closed with no new Recognition Science assumptions: once this target holds at the canonical spectral entropy, the algebraic core (binary entropy strictly positive on $(0,1)$ and $\lambda_+\in(1/2,1]$ for $C\in(0,1]$) yields unconditional entropy positivity from concurrence positivity.
Immediate consumers are the one-line restatement equating reduced entropy to binary entropy of the inner radius, the unconditional positivity theorem for pure two-qubit states with $C>0$, and the certificate bundle that packages concurrence nonnegativity, det-zero equivalence, reduced trace, and reduced det identities. The concurrence witness also aligns with the algebraic entanglement fact already used on the gravity/quantum-channel side (nonzero det of branch amplitudes).
Within the broader framework this is structural quantum bookkeeping rather than a forcing-chain step (T5–T8); it supplies the entropy side of pure bipartite entanglement once amplitudes are normalized on the two-qubit sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.