reducedDensity_eigenvalues_eq_lambda_or_swap
plain-language theorem explainer
For a Frobenius-normalized pure two-qubit amplitude matrix, the eigenvalues of the first-qubit reduced density are exactly the pair λ±(C)=(1±√(1−C²))/2 in either order, with C the Wootters concurrence. Spectral proofs of the entanglement-entropy identity E_VN=h((1+√(1−C²))/2) cite this. The argument matches each eigenvalue to a root of the quadratic fixed by the sum and product identities.
Claim. Let $A$ be a $2\times 2$ complex amplitude matrix with Frobenius norm squared equal to $1$, and let $C=2|\det A|$ be its Wootters concurrence. If $\rho$ is the Hermitian reduced density of the first qubit and $\lambda_\pm(C)=(1\pm\sqrt{1-C^2})/2$, then the ordered eigenvalues of $\rho$ are either $(\lambda_+(C),\lambda_-(C))$ or $(\lambda_-(C),\lambda_+(C))$.
background
Track 2.B of the pure two-qubit module links Wootters concurrence of a pure amplitude matrix $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$ to positivity of the von Neumann entanglement entropy of the reduced state. Concurrence is the pure-state formula $C(A):=2|\det A|$. Normalization is the Frobenius condition $\sum_{i,j}|A_{ij}|^2=1$.
The reduced density $\rho_1=\mathrm{tr}2|\psi\rangle\langle\psi|$ is Hermitian of trace one. Its spectrum is known classically to be $\lambda\pm=(1\pm\sqrt{1-C^2})/2$, so the binary entropy of either eigenvalue equals $E_{\mathrm{VN}}(\rho_1)$. The module packages that spectral claim as a Prop-shaped sub-target and composes it with the algebraic core on binary entropy.
Upstream facts used here are the sum of eigenvalues equaling one (from trace normalization), the product equaling $C^2/4$ (from the determinant identity $\det\rho_1=C^2/4$), nonnegativity and the bound $C\le 1$ under normalization, and the elementary root classification for the monic quadratic $x^2-x+C^2/4=0$.
proof idea
Introduce the Hermitian witness for the reduced density and the scalar $C$. From normalization obtain $C\le 1$, hence nonnegative discriminant $1-C^2$. Invoke the sum identity (eigenvalues add to 1) and the product identity (eigenvalues multiply to $C^2/4$). The sum-product lemma puts eigenvalue 0 on the quadratic $x^2-x+C^2/4=0$. The root-classification lemma yields the dichotomy: that eigenvalue is $\lambda_+(C)$ or $\lambda_-(C)$. In each branch, the complementary eigenvalue is recovered by linear arithmetic from the sum identity and $\lambda_++\lambda_-=1$.
why it matters
This is the spectral half of the reduced-density step in Track 2.B. Downstream, pureTwoQubitReducedEntropyTarget_holds applies it to identify the von Neumann entropy of $\rho_1$ with the binary entropy $h((1+\sqrt{1-C^2})/2)$, discharging the Prop-shaped target PureTwoQubitReducedEntropyTarget and closing the chain from concurrence positivity to strict positivity of entanglement entropy for pure two-qubit states.
Within the broader Recognition Science quantum track, the result is structural rather than RS-axiomatic: it uses only linear algebra of $2\times 2$ amplitude matrices and the pure-state Wootters formula, with no new ledger or forcing-chain hypotheses. It sits under the already-proved algebraic entanglement witness that $C>0$ iff $\det A\ne 0$, and feeds the entropy-positivity theorem that finishes Track 2.B.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.