lambdaPlus_add_lambdaMinus
plain-language theorem explainer
For any real concurrence parameter C, the two spectral weights λ₊(C) and λ₋(C) sum to 1. Anyone deriving the reduced-density spectrum or binary-entropy form of two-qubit entanglement entropy cites this identity. The proof is a one-line algebraic cancellation after unfolding the closed forms.
Claim. For every real number $C$, $$\lambda_+(C) + \lambda_-(C) = 1,$$ where $\lambda_+(C) = \frac{1 + \sqrt{1 - C^2}}{2}$ and $\lambda_-(C) = \frac{1 - \sqrt{1 - C^2}}{2}$.
background
Track 2.B of the pure two-qubit module links Wootters concurrence of a normalized amplitude matrix $A$ to von Neumann entanglement entropy of the reduced state. Concurrence is $C(A) = 2|\det A|$. The candidate eigenvalues of the single-qubit reduced density matrix are written in closed form as the concurrence spectral weights $\lambda_\pm(C) = (1 \pm \sqrt{1-C^2})/2$.
These weights are the algebraic stand-ins for the spectrum of $\rho_1 = \mathrm{tr}2|\psi\rangle\langle\psi|$. The module proves the full reduction $E{\mathrm{VN}}(\rho_1) = h((1+\sqrt{1-C^2})/2)$ by combining the algebraic core (interval membership and strict positivity of binary entropy) with the reduced-density eigenvalue identification. The sum-to-one identity is the trace half of that spectral package: any normalized $2\times 2$ density matrix has eigenvalues adding to 1.
proof idea
Term-mode proof: unfold the definitions of $\lambda_+$ and $\lambda_-$, then apply ring. The square-root terms cancel and the remaining constants give $(1+1)/2 = 1$. No side conditions on $C$ are required; the identity is purely algebraic in the closed forms.
why it matters
This is the trace half of the spectral invariants used throughout Track 2.B. Downstream, lambdaPair_sum_product_of_concurrence_unit_interval packages it with the product identity $\lambda_+\lambda_- = C^2/4$ (matching $\det\rho_1$). binaryEntropy_eq_neg_sum_lambda rewrites binary entropy of $\lambda_+$ as $-(\lambda_+\log\lambda_+ + \lambda_-\log\lambda_-)$ via $\lambda_- = 1-\lambda_+$. reducedDensity_eigenvalues_eq_lambda_or_swap identifies the actual Hermitian eigenvalues of the reduced density with ${\lambda_+,\lambda_}$ up to order.
Together these close the chain from concurrence to strict positivity of entanglement entropy for pure two-qubit states, with no new Recognition Science assumptions. The module status is structural theorem: Track 2.B closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.