binaryEntropy_eq_neg_sum_lambda
plain-language theorem explainer
Binary entropy of the larger Schmidt eigenvalue equals the two-term von Neumann sum −∑ λᵢ log λᵢ for a pure two-qubit reduced state. Anyone equating E_VN(ρ₁) to h(λ₊) cites this identity. The proof is a short algebraic rewrite: λ₋ = 1 − λ₊ from the eigenvalue sum, then unfold binary entropy and ring.
Claim. For $C \in [0,1]$, writing $\lambda_+(C)$ and $\lambda_-(C)$ for the two eigenvalues of the reduced density (so $\lambda_+ + \lambda_- = 1$), one has $h(\lambda_+(C)) = -(\lambda_+(C)\,\log\lambda_+(C) + \lambda_-(C)\,\log\lambda_-(C))$, where $h(p) = -p\log p - (1-p)\log(1-p)$ is binary entropy.
background
Track 2.B links Wootters concurrence of a pure two-qubit amplitude matrix to positivity of von Neumann entanglement entropy. For a normalized pure state $|\psi\rangle = \sum_{ij} A_{ij}|ij\rangle$, the reduced density $\rho_1 = \mathrm{tr}2|\psi\rangle\langle\psi|$ has eigenvalues $\lambda\pm = (1 \pm \sqrt{1-C^2})/2$ with $C = 2|\det A|$, and $E_{\mathrm{VN}}(\rho_1) = -\sum_i \lambda_i \log \lambda_i$.
Binary entropy is $h(p) = -p\log p - (1-p)\log(1-p)$. Because $\lambda_+ + \lambda_- = 1$ and $h$ is symmetric about $1/2$, the two-eigenvalue von Neumann sum collapses to $h(\lambda_+)$ (equivalently $h(\lambda_-)$). This lemma records that collapse as an equality of real expressions, under the standing bounds $0 \le C \le 1$ that keep both eigenvalues in $[0,1]$.
The local module already proves the concurrence algebra ($C = 2|\det A|$, nonnegativity, zero iff det zero) and the reduced-density determinant identities that identify $\lambda_\pm$ with the concurrence formula.
proof idea
From the eigenvalue sum lemma $\lambda_+(C) + \lambda_-(C) = 1$, linear arithmetic gives $\lambda_-(C) = 1 - \lambda_+(C)$. Unfold the definition of binary entropy (the standard $-p\log p - (1-p)\log(1-p)$ form). Substitute the rewritten $\lambda_-$ and finish by ring, matching the two-term sum $-(\lambda_+\log\lambda_+ + \lambda_-\log\lambda_-)$. The hypotheses $0 \le C \le 1$ are unused in the algebra; they only fix the physical domain.
why it matters
This is the bridge between the spectral definition of reduced von Neumann entropy and the binary-entropy expression used in the algebraic core of Track 2.B. Downstream, pureTwoQubitReducedEntropyTarget_holds applies it to discharge the Prop-shaped sub-target PureTwoQubitReducedEntropyTarget for the canonical spectral definition reducedDensityVonNeumannEntropy, so that $E_{\mathrm{VN}}(\rho_1) = h((1+\sqrt{1-C^2})/2)$ holds on normalized pure two-qubit states.
Together with the algebraic core (binary entropy strictly positive on $(0,1)$ and $\lambda_+ \in (1/2,1]$ when $C \in (0,1]$), that sub-target closes the full chain from concurrence positivity to entanglement-entropy positivity. The module status is structural theorem: Track 2.B closed with no new Recognition Science assumptions. No forcing-chain landmark (T5–T8) is touched; the result is ordinary finite-dimensional quantum information inside the RS quantum track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.