reducedDensityVonNeumannEntropy
plain-language theorem explainer
Defines the von Neumann entanglement entropy of the first-qubit reduced density matrix of a pure two-qubit amplitude matrix A as −∑ λᵢ log λᵢ from the Hermitian spectral theorem. Cited by anyone proving E_VN(ρ₁) = h((1+√(1−C²))/2) or unconditional entropy positivity from concurrence. The body is a three-line definition that packages eigenvalues of the reduced density via the Hermitian witness.
Claim. For a $2\times 2$ complex amplitude matrix $A$, the von Neumann entropy of its first-qubit reduced density matrix is $S(\rho_1(A)) := -\sum_{i=1}^{2} \lambda_i \log \lambda_i$, where $\lambda_i$ are the eigenvalues of the Hermitian matrix $\rho_1(A) = \mathrm{tr}_2 |\psi_A\rangle\langle\psi_A|$.
background
Track 2.B of the pure two-qubit module links Wootters concurrence $C(A) := 2|\det A|$ of a normalized amplitude matrix to strict positivity of the entanglement entropy. The reduced density $\rho_1 = \mathrm{tr}_2 |\psi\rangle\langle\psi|$ is the partial trace over the second qubit; for pure two-qubit states its spectrum is known explicitly in terms of $C$.
Von Neumann entropy is the standard spectral functional $-\mathrm{Tr}(\rho\log\rho)$, here specialized to the two eigenvalues of $\rho_1$. The module already proves that $\rho_1$ is Hermitian (reducedDensity_isHermitian), so the Mathlib spectral theorem supplies real eigenvalues and the sum is well-typed as a real number.
The algebraic core of the track shows that those eigenvalues equal $(1\pm\sqrt{1-C^2})/2$, so this definition becomes the left-hand side of the identity $E_{\mathrm{VN}}(\rho_1)=h((1+\sqrt{1-C^2})/2)$ with binary entropy $h$.
proof idea
Definition, not a proof. Obtain the Hermitian structure certificate hρ := reducedDensity_isHermitian A, read off hρ.eigenvalues : Fin 2 → ℝ, and return the finite sum $-\sum_i \lambda_i \log\lambda_i$. No tactics beyond the let binding; the spectral data come entirely from Mathlib's Hermitian eigenvalue API once hermiticity is established by rewriting $\rho_1$ as $A A^\dagger$.
why it matters
This is the canonical spectral left-hand side for every entropy identity in Track 2.B. Downstream, pureTwoQubitReducedEntropyTarget_holds asserts that the definition equals binary entropy of the inner radius $(1+\sqrt{1-C^2})/2$; pure_two_qubit_entropy_eq_binaryEntropy_inner_radius and pure_two_qubit_entropy_positive_unconditional then give the full reduction and unconditional positivity whenever $C>0$ on a normalized state.
The Gravity master theorem carries the same positivity as bmv_positive_unconditional_carried_prop, witnessing BMV von Neumann entropy positivity without extra RS hypotheses. The certificate structure PureTwoQubitConcurrenceEntropyCert packages the definition among the five algebraic clauses that close Track 2.B. No new Recognition Science assumptions enter; the object is pure quantum information on $2\times 2$ amplitudes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.