lambdaPlus_sub_lambdaMinus
plain-language theorem explainer
For any real concurrence parameter C, the gap between the upper and lower reduced-density eigenvalue candidates equals √(1−C²). Anyone deriving the pure two-qubit spectrum or binary-entropy formula from Wootters concurrence cites this identity. The proof is a one-line algebraic reduction: unfold the two definitions and cancel by ring.
Claim. For every real number $C$, if $\lambda_+(C) = (1 + \sqrt{1 - C^2})/2$ and $\lambda_-(C) = (1 - \sqrt{1 - C^2})/2$, then $\lambda_+(C) - \lambda_-(C) = \sqrt{1 - C^2}$.
background
Track 2.B of the Recognition Science quantum plan links Wootters concurrence of a pure two-qubit amplitude matrix to strict positivity of von Neumann entanglement entropy. For a normalized pure state with amplitude matrix $A$, concurrence is $C(A) := 2|\det A|$. The reduced density matrix $\rho_1 = \mathrm{tr}_2|\psi\rangle\langle\psi|$ is claimed to have eigenvalues $(1 \pm \sqrt{1 - C^2})/2$, so the entanglement entropy is the binary entropy of either weight.
The two candidate eigenvalues are defined pointwise on the real line: the upper weight $\lambda_+(C) = (1 + \sqrt{1 - C^2})/2$ and the lower weight $\lambda_-(C) = (1 - \sqrt{1 - C^2})/2$. Their sum is identically one; the present identity isolates their difference. Both definitions are pure algebraic abbreviations with no domain side-conditions at the definition site; reality of the square root is handled by later lemmas that restrict $C$ to $[0,1]$.
proof idea
Term-mode proof by direct expansion. Unfold $\lambda_+$ and $\lambda_-$ to their fractional definitions, then apply ring to the difference:
$$\frac{1+\sqrt{1-C^2}}{2} - \frac{1-\sqrt{1-C^2}}{2} = \frac{2\sqrt{1-C^2}}{2} = \sqrt{1-C^2}.$$
No external lemmas are required beyond the two local definitions.
why it matters
This gap identity is the elementary spectral arithmetic behind the pure two-qubit eigenvalue formula $\lambda_\pm = (1 \pm \sqrt{1-C^2})/2$ that the module uses to equate entanglement entropy with binary entropy of a concurrence-dependent argument. The module status is STRUCTURAL THEOREM (Track 2.B closed): the full reduction $E_{\mathrm{VN}}(\rho_1) = h((1+\sqrt{1-C^2})/2)$ rests on having $\lambda_+ - \lambda_- = \sqrt{1-C^2}$ so that the two eigenvalues sit symmetrically about $1/2$.
No downstream declarations currently list this private theorem as a direct edge, but it is the natural intermediate for any proof that reconstructs the spectrum gap from the two weight definitions before feeding the algebraic core (positivity of binary entropy on $(0,1)$). It does not invoke RS forcing landmarks (T5–T8, RCL, $\phi$-ladder); it is pure two-qubit linear algebra supporting the entropy-concurrence bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.