lambdaPlus
plain-language theorem explainer
Defines the larger spectral weight of a pure two-qubit reduced density matrix as a function of Wootters concurrence: λ₊(C) = (1 + √(1−C²))/2. Anyone proving the entropy–concurrence identity or the algebraic core of Track 2.B cites it. The body is a one-line closed form; no proof obligations.
Claim. For a real parameter $C$, set $\lambda_+(C) := \dfrac{1 + \sqrt{1 - C^2}}{2}$. This is the upper candidate eigenvalue of the single-qubit reduced density matrix of a pure two-qubit state whose Wootters concurrence equals $C$.
background
Track 2.B links Wootters concurrence of a pure two-qubit amplitude matrix $A$ to von Neumann entanglement entropy of the reduced state. Concurrence is $C(A) := 2|\det A|$ for a normalized $2\times 2$ complex amplitude matrix. The reduced density $\rho_1 = \mathrm{tr}_2|\psi\rangle\langle\psi|$ is a qubit state whose eigenvalues are forced by the characteristic polynomial $x^2 - x + C^2/4 = 0$.
Those roots are exactly $\lambda_\pm(C) = (1 \pm \sqrt{1-C^2})/2$. Binary entropy is symmetric about $1/2$, so $E_{\mathrm{VN}}(\rho_1) = h(\lambda_+(C)) = h(\lambda_-(C))$. The module status is structural: no new Recognition Science assumptions, only this algebraic identification plus positivity of binary entropy on $(0,1)$.
Sibling material already records $C \ge 0$, $C=0$ iff $\det A = 0$, and $\det\rho_1 = C^2/4$. The present definition packages the larger root for reuse.
proof idea
Pure definitional abbreviation. The right-hand side is the closed-form larger root of the monic quadratic $x^2 - x + C^2/4 = 0$ under the discriminant condition $1-C^2 \ge 0$. No tactics, no lemmas applied at the definition site; downstream lemmas unfold it and apply ring, Real.sq_sqrt, or linarith.
why it matters
This is the named upper weight in the full reduction $E_{\mathrm{VN}}(\rho_1) = h((1+\sqrt{1-C^2})/2)$ that closes Track 2.B. Downstream facts built on it include: the pair sums to 1 and multiplies to $C^2/4$ (matching $\mathrm{tr},\rho_1$ and $\det\rho_1$); $\lambda_+ \ge \lambda_-$; any root of the reduced characteristic polynomial equals $\lambda_+$ or $\lambda_-$; and binary entropy of $\lambda_+$ equals $-(\lambda_+\log\lambda_+ + \lambda_-\log\lambda_-)$. The certificate PureTwoQubitConcurrenceEntropyCert also consumes it. In the broader RS quantum track it converts the algebraic entanglement witness (nonzero det) into strict positivity of entanglement entropy for pure two-qubit states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.