lambdaPlus_mul_lambdaMinus
plain-language theorem explainer
When the discriminant 1−C² is nonnegative, the product of the two concurrence spectral weights equals C²/4. That identity is the determinant half of the reduced-density eigenvalue pair for pure two-qubit states. Anyone assembling Wootters concurrence into von Neumann entropy cites it. The proof unfolds the ± square-root definitions, applies sq_sqrt, and finishes by nonlinear arithmetic.
Claim. Let $C\in\mathbb{R}$ satisfy $0\le 1-C^2$. Write $\lambda_\pm(C)=(1\pm\sqrt{1-C^2})/2$ for the concurrence spectral weights. Then $\lambda_+(C)\,\lambda_-(C)=C^2/4$.
background
Track 2.B links pure two-qubit Wootters concurrence to strict positivity of von Neumann entanglement entropy. For a normalized amplitude matrix $A$, concurrence is $C(A)=2|\det A|$. The reduced density $\rho_1=\mathrm{tr}_2|\psi\rangle\langle\psi|$ has eigenvalues $(1\pm\sqrt{1-C^2})/2$, so entropy is the binary entropy of either weight.
The spectral weights $\lambda_\pm(C)=(1\pm\sqrt{1-C^2})/2$ are the algebraic stand-ins for those eigenvalues. Their sum and product must match the trace and determinant of a normalized qubit density matrix (trace $1$, determinant $C^2/4$). The sibling reduced-density lemmas already identify $\det\rho_1$ with $C^2/4$; this theorem supplies the matching product identity on the spectral side.
The hypothesis $0\le 1-C^2$ is exactly the domain where the real square root is defined, so both weights are real.
proof idea
Unfold $\lambda_+$ and $\lambda_-$ to $(1\pm\sqrt{1-C^2})/2$. Their product is $(1-(\sqrt{1-C^2})^2)/4$. Discharge $(\sqrt{1-C^2})^2=1-C^2$ by Real.sq_sqrt on the discriminant hypothesis, then finish with nlinarith, which reduces the remaining rational identity to $C^2/4$.
why it matters
This is the product half of the spectral-pair bookkeeping that lets concurrence control entanglement entropy. Downstream, lambdaPair_sum_product_of_concurrence_unit_interval packages sum $=1$ and product $=C^2/4$ for $C\in[0,1]$, quoting this theorem for the product conjunct. That pair is the algebraic core feeding the full reduction $E_{\mathrm{VN}}(\rho_1)=h((1+\sqrt{1-C^2})/2)$ that closes Track 2.B.
In the module's chain, once the reduced density is known to have these eigenvalues, binary-entropy positivity on $(0,1)$ yields strict entropy positivity whenever $C>0$. No new Recognition Science assumptions enter; the result is pure two-qubit linear algebra inside the already-closed structural track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.