reducedDensity_det_eq_concurrence_sq_div_four
plain-language theorem explainer
For any pure two-qubit amplitude matrix A, the determinant of the first-qubit reduced density equals the square of the Wootters concurrence divided by four: det(ρ₁) = C(A)²/4. Anyone deriving the Schmidt eigenvalues or von Neumann entropy from concurrence cites this identity. The proof is a short algebraic rewrite: reduce det(ρ₁) to |det A|², unfold C(A) = 2|det A|, and clear the factor of four.
Claim. Let $A$ be a $2\times 2$ complex amplitude matrix for a pure two-qubit state. Write $\rho_1$ for the reduced density matrix of the first qubit (partial trace over the second factor) and $C(A)=2|\det A|$ for the Wootters concurrence. Then $\det(\rho_1)=C(A)^2/4$ as a real equality.
background
Track 2.B of the pure two-qubit module links Wootters concurrence of a pure amplitude matrix to strict positivity of the von Neumann entanglement entropy. The state is encoded as $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$ with $|\psi\rangle=\sum_{ij}A_{ij}|ij\rangle$. The reduced density is $\rho_1=\mathrm{tr}2|\psi\rangle\langle\psi|$, a $2\times 2$ Hermitian matrix whose eigenvalues determine $E{\mathrm{VN}}(\rho_1)$.
Concurrence is the pure-state simplification $C(A):=2|\det A|$. An earlier sibling already shows $\det(\rho_1)=|\det A|^2$ (equivalently the squared modulus of the complex determinant). The present identity rewrites that fact in concurrence units so later steps can quote the standard eigenvalue pair $(1\pm\sqrt{1-C^2})/2$.
The module status is structural: no new Recognition Science assumptions, only linear algebra on $2\times 2$ complex matrices.
proof idea
Term-mode proof in four steps. First rewrite with the sibling reducedDensity_det_eq_norm_det_sq, which supplies $\det(\rho_1)=|\det A|^2$. Unfold the definition of concurrence, so $C(A)=2|\det A|$ and the right-hand side becomes $(2|\det A|)^2/4$. Then norm_num and ring clear the constant factor and finish the real equality. No case splits and no analysis beyond field arithmetic.
why it matters
This is the algebraic hinge between the partial-trace determinant and the concurrence form used throughout Track 2.B. Downstream, reducedDensity_discriminant_eq_one_sub_concurrence_sq rewrites $\mathrm{tr}(\rho_1)^2-4\det(\rho_1)=1-C^2$, which is the bridge to eigenvalues $(1\pm\sqrt{1-C^2})/2$. The private product-of-eigenvalues lemma and the non-vanishing lemma reducedDensity_det_ne_zero_of_concurrence_pos both rewrite through this identity. The certificate bundle pureTwoQubitConcurrenceEntropyCert records it as the reduced_det field.
Together these close the reduced-density half of the master reduction $E_{\mathrm{VN}}(\rho_1)=h((1+\sqrt{1-C^2})/2)$, so positive concurrence forces positive binary entropy. The result is pure quantum information algebra; it does not invoke the RS forcing chain (T5–T8) or the Recognition Composition Law, but it supplies the entanglement witness used when RS channels meet two-qubit structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.