reducedDensity_eigenvalues_prod_eq_concurrence_sq_div_four
plain-language theorem explainer
For any pure two-qubit amplitude matrix A, the product of the two eigenvalues of the reduced density matrix equals C(A)^2/4, with C the Wootters concurrence. Anyone deriving the Schmidt spectrum or entanglement entropy from concurrence cites this identity. The proof rewrites the Hermitian determinant-as-product-of-eigenvalues fact through the already-proved det(ρ₁)=C²/4 and injects the complex product back to reals.
Claim. Let $A$ be a $2\times 2$ complex matrix and let $\rho_1$ be its reduced density matrix (partial trace of $|\psi\rangle\langle\psi|$ over the second qubit). Write $\lambda_0,\lambda_1$ for the eigenvalues of $\rho_1$ as a Hermitian matrix. Then $\lambda_0\lambda_1 = C(A)^2/4$, where $C(A)=2\|\det A\|$ is the Wootters concurrence.
background
Track 2.B of the Recognition Science quantum program links Wootters concurrence of a pure two-qubit amplitude matrix to strict positivity of von Neumann entanglement entropy. The amplitude matrix $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$ encodes $|\psi\rangle=\sum_{ij}A_{ij}|ij\rangle$. Concurrence is the pure-state simplification $C(A):=2|\det A|$.
The reduced density $\rho_1=\mathrm{tr}_2|\psi\rangle\langle\psi|$ is Hermitian (proved as reducedDensity_isHermitian). For any Hermitian matrix the determinant equals the product of eigenvalues. An upstream algebraic identity already gives $\det(\rho_1)=C(A)^2/4$. The present lemma simply transfers that identity from the determinant to the ordered eigenvalue pair.
Downstream work needs the product $\lambda_0\lambda_1$ (together with the trace constraint $\lambda_0+\lambda_1=1$ under normalization) to pin the spectrum to the closed form $(1\pm\sqrt{1-C^2})/2$.
proof idea
Short tactic proof. Introduce the Hermitian witness $h_\rho$. Invoke Mathlib's det_eq_prod_eigenvalues for Hermitian matrices, obtaining $\det(\rho_1)=\prod_i\lambda_i$ as a complex equality. Rewrite the left side by the upstream theorem reducedDensity_det_eq_concurrence_sq_div_four and expand the finite product over Fin 2. The resulting complex product of two real eigenvalues equals the real scalar $C^2/4$; apply the local casting lemma eigenvalues_fin_two_prod_eq_of_complex_prod (injectivity of Complex.ofReal on products) to recover the real identity.
why it matters
This is a necessary bridge inside the reduced-density-matrix half of Track 2.B. The module goal is the full identity $E_{\mathrm{VN}}(\rho_1)=h((1+\sqrt{1-C^2})/2)$ with binary entropy $h$, which forces $E_{\mathrm{VN}}>0$ whenever $C>0$.
Two immediate parents consume the product formula: concurrence_sq_le_one_of_normalized (with the eigenvalue sum equal to one, the product bound yields $C^2\le 1$) and reducedDensity_eigenvalues_eq_lambda_or_swap (the quadratic $t^2-t+C^2/4=0$ has roots $\lambda_\pm=(1\pm\sqrt{1-C^2})/2$, so the spectrum is exactly that pair up to order). Those lemmas close the structural chain from concurrence to entropy positivity with no new RS assumptions.
The result is pure linear algebra on $2\times 2$ Hermitian matrices; it does not invoke the forcing chain T0–T8, RCL, or the phi-ladder, but it supplies the quantum-information side of the entanglement witness already linked to the det-branch amplitude fact in the gravity/quantum-channel track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.