pure_two_qubit_entropy_eq_binaryEntropy_inner_radius
plain-language theorem explainer
For a normalized pure two-qubit amplitude matrix, the von Neumann entropy of one reduced density matrix equals the binary entropy of (1 + √(1 − C²))/2, with C the Wootters concurrence. Quantum-information and Recognition Science readers of Track 2.B cite this closed-form identity. The proof is a one-line discharge of the module's reduced-density entropy target under the unit-Frobenius hypothesis.
Claim. Let $A$ be a $2\times 2$ complex amplitude matrix with Frobenius norm one, $\sum_{i,j}|A_{ij}|^2=1$. Write $C(A)=2|\det A|$ for the pure-state Wootters concurrence. Then the von Neumann entropy of the single-qubit reduced density matrix of the pure state with amplitudes $A$ equals the binary entropy $h\bigl((1+\sqrt{1-C(A)^2})/2\bigr)$.
background
The module treats pure two-qubit states as amplitude matrices $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$ with unit Frobenius norm. The Wootters concurrence is the pure-state simplification $C(A):=2|\det A|$; vanishing concurrence is equivalent to vanishing determinant and is the algebraic separability witness already used elsewhere in the monolith.
Partial trace over the second factor yields a single-qubit reduced density matrix $\rho_1$. For pure two-qubit states its eigenvalues are $(1\pm\sqrt{1-C^2})/2$. Von Neumann entropy of a qubit is therefore the binary entropy $h(p)=-p\log p-(1-p)\log(1-p)$ of either eigenvalue; binary entropy is symmetric about $1/2$, so the two choices agree.
Track 2.B packages the eigenvalue computation as a Prop-shaped sub-target (the reduced-density entropy target) and composes it with the elementary algebraic fact that $h$ is strictly positive on $(0,1)$. The present theorem is the equality half of that package.
proof idea
Term-mode one-liner: the statement is exactly the content of the already-proved reduced-density entropy target, applied to $A$ and the unit-Frobenius hypothesis. No extra algebraic rewriting occurs at this declaration; the heavy lifting (eigenvalues of $\rho_1$, relation of $\det A$ to concurrence, and identification with binary entropy) lives inside that target.
why it matters
This identity is the quantitative heart of Track 2.B: it converts the algebraic concurrence of a pure two-qubit amplitude matrix into the exact entanglement entropy of either reduced qubit. The module status line records Track 2.B as closed with no new Recognition Science assumptions and no proof holes; the present theorem is the named equality that the algebraic core and the reduced-density step jointly deliver.
Downstream the equality feeds the strict-positivity corollary: whenever $C>0$ the argument of $h$ lies in $(1/2,1)$, so $E_{\mathrm{VN}}(\rho_1)>0$. That positivity links the pure-state concurrence witness to genuine entanglement entropy, matching the master-plan goal of the module. No further used-by edges are recorded yet; the result stands as the reference form of the entropy-concurrence relation inside the quantum track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.