reducedDensity_discriminant_eq_one_sub_concurrence_sq
plain-language theorem explainer
For a Frobenius-normalized pure two-qubit amplitude matrix, the characteristic discriminant of the reduced density equals one minus the squared Wootters concurrence. Anyone extracting Schmidt eigenvalues (1 ± √(1−C²))/2 from the partial trace cites this identity. The proof rewrites the reduced determinant as C²/4 and closes by ring arithmetic.
Claim. Let $A$ be a $2\times 2$ complex amplitude matrix with Frobenius norm squared equal to $1$. Write $\rho_1(A)$ for the single-qubit reduced density (partial trace of $|\psi\rangle\langle\psi|$ over the second factor) and $C(A)=2|\det A|$ for the pure-state Wootters concurrence. Then $1-4\det(\rho_1(A))=1-C(A)^2$ as an equality in $\mathbb{C}$.
background
Track 2.B of the pure two-qubit module links Wootters concurrence of a normalized amplitude matrix $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$ to strict positivity of the von Neumann entanglement entropy of the reduced state. Concurrence is the pure-state simplification $C(A):=2|\det A|$; vanishing $C$ is equivalent to vanishing determinant.
The reduced density $\rho_1$ is the partial trace of $|\psi\rangle\langle\psi|$ over the second qubit. For a pure bipartite state its eigenvalues are the Schmidt weights. The characteristic discriminant of a trace-one $2\times 2$ Hermitian matrix is $\mathrm{tr}(\rho)^2-4\det(\rho)$; under normalization this collapses to $1-4\det(\rho_1)$.
An upstream sibling already records $\det(\rho_1)=C(A)^2/4$. The present identity converts that determinant formula into the discriminant form that feeds the standard eigenvalue radicals $(1\pm\sqrt{1-C^2})/2$.
proof idea
Term-mode wrapper, three tactics. Rewrite the left-hand side with the sibling identity that $\det(\rho_1(A))=C(A)^2/4$. After substitution one has $1-4\cdot(C^2/4)$. norm_num clears the rational coefficient; ring finishes $1-C^2$. The Frobenius-normalization hypothesis is carried for interface consistency with the reduced-density API (trace one) but is not invoked in the algebraic steps.
why it matters
Algebraic bridge named in the module plan: once the discriminant equals $1-C^2$, the characteristic polynomial of $\rho_1$ yields eigenvalues $(1\pm\sqrt{1-C^2})/2$. The next section of the same file introduces the upper weight $\lambda_+(C)=(1+\sqrt{1-C^2})/2$ and routes it into binary entropy, closing $E_{\mathrm{VN}}(\rho_1)=h((1+\sqrt{1-C^2})/2)$.
Module status marks Track 2.B as a structural theorem with no new Recognition Science assumptions and no proof holes. The identity therefore sits inside the pure-state half of the entanglement-entropy positivity chain, matching the algebraic entanglement witness already available from the determinant branch of the amplitude matrix. No external used-by edges are recorded yet; consumption is local to the spectral-weight and entropy lemmas that follow in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.