eq_lambdaPlus_or_lambdaMinus_of_quadratic
plain-language theorem explainer
Any real root of the monic quadratic x² − x + C²/4 = 0, under the discriminant hypothesis 1 − C² ≥ 0, equals one of the two concurrence spectral weights λ₊(C) or λ₋(C). Downstream eigenvalue identification for the pure two-qubit reduced density matrix cites this. The proof factors the quadratic against the closed-form roots and applies the no-zero-divisors rule.
Claim. Let $C, x \in \mathbb{R}$ with $1 - C^2 \ge 0$. If $x^2 - x + C^2/4 = 0$, then $x = (1 + \sqrt{1 - C^2})/2$ or $x = (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 amplitude matrix to the von Neumann entanglement entropy of the reduced density matrix $\rho_1 = \mathrm{tr}_2 |\psi\rangle\langle\psi|$. The algebraic core identifies the eigenvalues of $\rho_1$ with the closed forms
$$\lambda_+(C) = \frac{1 + \sqrt{1 - C^2}}{2}, \qquad \lambda_-(C) = \frac{1 - \sqrt{1 - C^2}}{2}.$$
These are the two roots of the characteristic quadratic $t^2 - (\mathrm{tr},\rho_1)t + \det\rho_1 = 0$. Under unit trace one has $\mathrm{tr},\rho_1 = 1$ and $\det\rho_1 = C^2/4$, so the equation collapses to $x^2 - x + C^2/4 = 0$. The discriminant hypothesis $1 - C^2 \ge 0$ is exactly the condition that $\sqrt{1 - C^2}$ is real, which holds for physical concurrence $C \in [0, 1]$.
proof idea
Unfold the definitions of $\lambda_+$ and $\lambda_-$. From $1 - C^2 \ge 0$ one has $(\sqrt{1 - C^2})^2 = 1 - C^2$. Nonlinear arithmetic then shows that the quadratic factors as
$$\bigl(x - \tfrac{1 + \sqrt{1 - C^2}}{2}\bigr)\bigl(x - \tfrac{1 - \sqrt{1 - C^2}}{2}\bigr) = 0.$$
Apply mul_eq_zero to split into cases; each case is discharged by linear arithmetic, yielding $x = \lambda_+(C)$ or $x = \lambda_-(C)$.
why it matters
This is the pure algebraic root-identification step inside the reduced-density eigenvalue theorem reducedDensity_eigenvalues_eq_lambda_or_swap, which asserts that the Hermitian eigenvalues of $\rho_1$ are exactly ${\lambda_+(C), \lambda_-(C)}$ up to order. That identification is the bridge from concurrence to binary entropy: once the spectrum is known, $E_{\mathrm{VN}}(\rho_1) = h(\lambda_+(C))$, and the algebraic core of Track 2.B shows this is strictly positive for $C \in (0, 1]$. The module status is STRUCTURAL THEOREM (Track 2.B closed; no new RS assumptions). No forcing-chain landmark (T0–T8) is touched directly; the result is quantum-information infrastructure feeding the entropy-positivity claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.