reducedDensity_eigenvalues_sum_eq_one
plain-language theorem explainer
For a Frobenius-normalized pure two-qubit amplitude matrix, the two eigenvalues of the first-qubit reduced density sum to one. Anyone bounding concurrence or matching the reduced spectrum to the Wootters lambdas cites this. The proof rewrites the Hermitian trace-equals-sum-of-eigenvalues identity against the unit-trace lemma, then injects the complex sum back to the reals.
Claim. Let $A$ be a $2\times 2$ complex amplitude matrix with Frobenius norm-squared equal to $1$. Writing $\rho$ for the first-qubit reduced density matrix of the pure state with amplitudes $A$ (which is Hermitian), the two eigenvalues of $\rho$ satisfy $\lambda_0(\rho)+\lambda_1(\rho)=1$.
background
This module closes Track 2.B: the chain from Wootters concurrence of a pure two-qubit amplitude matrix to strict positivity of von Neumann entanglement entropy. For a pure state $|\psi\rangle=\sum_{ij} A_{ij}|ij\rangle$, the reduced density is $\rho_1=\mathrm{tr}2|\psi\rangle\langle\psi|$, and the target spectrum is $(\lambda\pm)=(1\pm\sqrt{1-C^2})/2$ with $C=2|\det A|$.
The Frobenius norm-squared is $\sum_{ij}|A_{ij}|^2$, so $h\mathrm{Norm}$ is the algebraic pure-state normalization. The reduced density is proved Hermitian in-module; Mathlib then supplies that the trace of a Hermitian matrix equals the sum of its eigenvalues (as complex numbers). An upstream in-module lemma already shows that normalization forces $\mathrm{tr},\rho_1=1$.
A tiny companion lemma converts a complex sum-of-reals equality back to a real equality by injectivity of the real embedding into $\mathbb{C}$.
proof idea
Introduce the Hermitian witness $h\rho$ for the reduced density of $A$. Apply Mathlib's trace_eq_sum_eigenvalues to get $\mathrm{tr},\rho=\sum_i\lambda_i$ as a complex identity. Rewrite the left side by the unit-trace lemma reducedDensity_trace_eq_one_of_normalized_complex (using $h\mathrm{Norm}$) and expand the finite sum over Fin 2. The resulting complex equality $(\lambda_0:\mathbb{C})+(\lambda_1:\mathbb{C})=1$ is discharged by eigenvalues_fin_two_sum_eq_of_complex_sum, which injects through Complex.ofReal.
why it matters
This is the trace half of the reduced-spectrum identification needed for Track 2.B. Downstream, concurrence_sq_le_one_of_normalized uses the eigenvalue sum (with nonnegativity and the det-concurrence link) to prove $C^2\le 1$ for normalized amplitudes. The sibling reducedDensity_eigenvalues_eq_lambda_or_swap then pins the ordered pair of eigenvalues to $(\lambda_+(C),\lambda_-(C))$ up to swap, which is exactly the reduced-density step in the module doc: $E_{\mathrm{VN}}(\rho_1)=h((1\pm\sqrt{1-C^2})/2)$.
Together these close the pure two-qubit bridge from algebraic concurrence to binary-entropy positivity, with no new Recognition Science assumptions. The result is local linear algebra inside the quantum track; it does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.