concurrence_nonneg
plain-language theorem explainer
Wootters concurrence of any pure two-qubit amplitude matrix is nonnegative. Anyone working the Track 2.B chain from concurrence to von Neumann entropy positivity cites this as the first algebraic bound. The proof unfolds C(A) = 2|det A| and applies nonnegativity of the complex modulus.
Claim. For every $2\times 2$ complex amplitude matrix $A$, the Wootters concurrence satisfies $C(A)\ge 0$, where $C(A):=2|\det A|$.
background
Track 2.B of the Recognition Science quantum stack links pure two-qubit entanglement to strict positivity of reduced von Neumann entropy. The amplitude matrix $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$ encodes a pure bipartite state $|\psi\rangle=\sum_{ij}A_{ij}|ij\rangle$. Its Wootters concurrence is the pure-state simplification $C(A):=2|\det A|$; the mixed-state formula collapses to this when the global state is pure.
Nonnegativity is the first structural fact needed before relating $C$ to the spectrum of the reduced density matrix $\rho_1=\mathrm{tr}2|\psi\rangle\langle\psi|$. Later identities give eigenvalues $(1\pm\sqrt{1-C^2})/2$ and $E{\mathrm{VN}}(\rho_1)=h((1+\sqrt{1-C^2})/2)$ with binary entropy $h$, so the sign of $C$ controls whether entropy can leave zero.
The module status is structural theorem: no new RS assumptions, Track 2.B closed once the algebraic core and reduced-density step are assembled.
proof idea
One-line algebraic argument. Unfold the definition $C(A)=2|\det A|$. Complex modulus is nonnegative by norm_nonneg, so $0\le|\det A|$. Scaling by the positive constant 2 and a short linear-arithmetic close yields $0\le C(A)$. No spectral theory or normalization hypothesis is used.
why it matters
Clause (1) of the pure two-qubit concurrence-entropy certificate PureTwoQubitConcurrenceEntropyCert, which packages the algebraic core of Track 2.B. Downstream, concurrence_pos_iff_det_ne_zero turns nonnegativity into the equivalence $C>0\Leftrightarrow\det A\ne 0$; concurrence_le_one_of_normalized uses it with the squared bound to get $C\le 1$ under Frobenius normalization; and the unconditional entropy-positivity theorem pure_two_qubit_entropy_positive_unconditional needs $C\ge 0$ to place the binary-entropy argument in $(1/2,1]$.
In the broader RS picture this is the pure-state entanglement witness that matches the already-proved determinant factorization on branch amplitudes. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is ordinary complex-linear algebra sitting under the entropy certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.