lambdaPlus_ge_lambdaMinus
plain-language theorem explainer
Whenever the discriminant $1-C^2$ is nonnegative, the upper reduced-density eigenvalue candidate is at least the lower one. Anyone assembling the pure two-qubit entropy-from-concurrence identity needs this ordering of $\lambda_\pm(C)$. The proof unfolds the two definitions and closes by linear arithmetic from nonnegativity of the square root.
Claim. For every real $C$ with $0 \le 1 - C^2$, one has $\lambda_-(C) \le \lambda_+(C)$, where $\lambda_+(C) = (1 + \sqrt{1-C^2})/2$ and $\lambda_-(C) = (1 - \sqrt{1-C^2})/2$.
background
Track 2.B of the pure two-qubit module links Wootters concurrence $C(A) := 2|\det A|$ of a normalized $2\times 2$ amplitude matrix to strict positivity of the von Neumann entanglement entropy of the reduced state. The reduced density matrix has candidate eigenvalues $\lambda_\pm(C) = (1 \pm \sqrt{1-C^2})/2$, and the entropy is the binary entropy of either weight.
The upper weight is defined by $\lambda_+(C) = (1 + \sqrt{1-C^2})/2$ and the lower by $\lambda_-(C) = (1 - \sqrt{1-C^2})/2$. The hypothesis $0 \le 1-C^2$ is exactly the condition that the square root is real, so both candidates are well-defined as reals. Ordering them is the elementary comparison needed before identifying the spectrum and feeding it into binary entropy.
proof idea
Unfold both definitions, reducing the claim to $(1 - \sqrt{1-C^2})/2 \le (1 + \sqrt{1-C^2})/2$. The only nontrivial input is $\sqrt{1-C^2} \ge 0$ (Mathlib's Real.sqrt_nonneg under the discriminant hypothesis). Linear arithmetic then finishes the inequality in one step.
why it matters
This is a private ordering lemma inside the algebraic core of Track 2.B: the chain from pure-state concurrence to $E_{\mathrm{VN}}(\rho_1) = h((1+\sqrt{1-C^2})/2)$ with $h$ the binary entropy. Without $\lambda_- \le \lambda_+$, one cannot cleanly treat the pair as ordered spectral weights on $[0,1]$ or invoke symmetry of $h$ about $1/2$. The module status is structural theorem (Track 2.B closed; no new RS assumptions). No external used-by edges are recorded; the lemma is consumed locally when assembling the eigenvalue pair and the entropy identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.