reducedDensity_det_ne_zero_of_concurrence_pos
plain-language theorem explainer
Positive Wootters concurrence of a pure two-qubit amplitude matrix forces the first-qubit reduced density matrix to be invertible (nonzero determinant). Anyone linking concurrence to Schmidt rank or von Neumann entropy positivity on Track 2.B would cite this. The proof is a short algebraic rewrite: det(ρ₁) equals C²/4, which is nonzero once C > 0.
Claim. Let $A$ be a $2\times 2$ complex amplitude matrix. If its Wootters concurrence satisfies $C(A) > 0$, then $\det(\rho_1(A)) \neq 0$, where $\rho_1(A)$ is the first-qubit reduced density matrix obtained by partial trace of $|\psi_A\rangle\langle\psi_A|$.
background
Track 2.B of the pure two-qubit module closes the chain from Wootters concurrence of a pure amplitude matrix $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$ to strict positivity of the von Neumann entanglement entropy of the reduced state. Concurrence is the pure-state formula $C(A):=2|\det A|$; it is nonnegative, and $C(A)=0$ iff $\det A=0$.
The reduced density $\rho_1(A)=\mathrm{tr}_2|\psi\rangle\langle\psi|$ is the $2\times 2$ Hermitian matrix obtained by tracing out the second qubit. A sibling identity records the exact relation $\det(\rho_1)=C(A)^2/4$. Eigenvalues of a trace-one qubit state are then $(1\pm\sqrt{1-4\det\rho_1})/2=(1\pm\sqrt{1-C^2})/2$, which is the bridge to binary entropy.
This lemma is the nondegeneracy half of that bridge: positive concurrence rules out a singular reduced density, so the Schmidt spectrum is nondegenerate at the endpoints $0$ and $1$.
proof idea
One algebraic rewrite. Apply the sibling identity $\det(\rho_1(A))=C(A)^2/4$. From $C(A)>0$ deduce $C(A)\neq 0$, hence $C(A)^2\neq 0$ by pow_ne_zero. Since the denominator $4$ is nonzero in $\mathbb{R}$, the quotient is nonzero (div_ne_zero), and exact_mod_cast aligns the real equality with the complex determinant type.
why it matters
Track 2.B needs $\det(\rho_1)\neq 0$ whenever $C>0$ so that the eigenvalues $(1\pm\sqrt{1-C^2})/2$ lie strictly inside $(0,1)$ rather than at the binary-entropy zeros ${0,1}$. Combined with the algebraic core (binary entropy strictly positive on $(0,1)$) and the eigenvalue identification, this yields $E_{\mathrm{VN}}(\rho_1)>0$ for every entangled pure two-qubit state.
The module status is structural theorem: no new Recognition Science assumptions, no proof holes. The concurrence convention matches the algebraic entanglement witness already used elsewhere ($C>0$ iff $\det A\neq 0$). No downstream consumers are wired yet in the graph; the immediate parent is the Prop-shaped reduced-entropy target that composes this nondegeneracy with the binary-entropy core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.