lambdaMinus
plain-language theorem explainer
The lower reduced-density eigenvalue candidate is the closed form λ₋(C)=(1-√(1-C²))/2 in the Wootters concurrence C. Anyone proving the pure two-qubit entropy–concurrence identity cites this as the smaller spectral weight of ρ₁. It is a one-line algebraic definition, dual to the upper weight λ₊.
Claim. For $C \in \mathbb{R}$, define the lower concurrence spectral weight $\lambda_-(C) := \dfrac{1 - \sqrt{1 - C^2}}{2}$.
background
Track 2.B links Wootters concurrence of a pure two-qubit amplitude matrix to von Neumann entanglement entropy of the reduced state. For normalized $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$, concurrence is $C(A)=2|\det A|$. The reduced density $\rho_1=\mathrm{tr}_2|\psi\rangle\langle\psi|$ is a qubit state whose eigenvalues are the roots of $x^2-x+C^2/4=0$, namely $(1\pm\sqrt{1-C^2})/2$.
This declaration names the lower root. Its companion is the upper root $\lambda_+(C)=(1+\sqrt{1-C^2})/2$. Binary entropy is symmetric about $1/2$, so $E_{\mathrm{VN}}(\rho_1)=h(\lambda_+)=h(\lambda_-)$. The module status is structural: no new Recognition assumptions, only the pure-state concurrence convention.
proof idea
Definitional. The body is the closed-form expression $(1-\sqrt{1-C^2})/2$; no tactics or lemmas. Downstream lemmas unfold this def together with $\lambda_+$ and cancel by ring or sq_sqrt.
why it matters
Anchor for the algebraic core of Track 2.B. Immediate consumers prove $\lambda_++\lambda_-=1$, $\lambda_+\lambda_-=C^2/4$ (when $1-C^2\ge 0$), ordering $\lambda_-\le\lambda_+$, and that quadratic roots equal one of the two weights. Those identities feed lambdaPair_sum_product_of_concurrence_unit_interval and binaryEntropy_eq_neg_sum_lambda, which identify $E_{\mathrm{VN}}$ with binary entropy of $\lambda_+$. The certificate PureTwoQubitConcurrenceEntropyCert packages the full chain: $C\in(0,1]$ forces strict positivity of entanglement entropy. No open scaffolding; the track is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.