concurrence_pos_iff_det_ne_zero
plain-language theorem explainer
For a pure two-qubit amplitude matrix, Wootters concurrence is strictly positive exactly when the determinant is nonzero. Cite this when converting the algebraic entanglement witness (nonzero det) into a strict-positivity statement on C, or when feeding the Track 2.B entropy chain. The proof is a short rewrite: nonnegativity turns 0 < C into C ≠ 0, then the zero-iff-det-zero lemma finishes it.
Claim. For every $2\times 2$ complex matrix $A$, writing $C(A)=2|\det A|$ for the pure-state Wootters concurrence, one has $0 < C(A)$ if and only if $\det A \neq 0$.
background
This module closes Track 2.B: the chain from Wootters concurrence of a pure two-qubit amplitude matrix to strict positivity of von Neumann entanglement entropy. A pure two-qubit state is written $|\psi\rangle=\sum_{ij} A_{ij}|ij\rangle$ with $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$. The pure-state concurrence is the standard simplification $C(A):=2|\det A|$; the mixed-state Wootters formula reduces to this when the state is pure.
Sibling facts already record $C(A)\ge 0$ and $C(A)=0\Leftrightarrow\det A=0$. Strict positivity of $C$ is the algebraic entanglement witness used later for the reduced density matrix $\rho_1=\mathrm{tr}_2|\psi\rangle\langle\psi|$, whose eigenvalues are $(1\pm\sqrt{1-C^2})/2$, so entanglement entropy is the binary entropy of that spectrum.
proof idea
Term-mode rewrite, not a long tactic script. First replace the goal $0<C(A)$ by $C(A)\neq 0$: the forward direction is ne' of a strict inequality; the reverse uses lt_of_le_of_ne with the sibling nonnegativity lemma and Ne.symm. Then rewrite with Ne and the sibling concurrence_eq_zero_iff_det_zero, which already equates vanishing concurrence to vanishing determinant. No further matrix algebra is needed.
why it matters
Track 2.B is marked structurally closed: no proof holes and no new Recognition Science assumptions. This biconditional is the positivity half of the concurrence convention stated in the module: strict positivity of $C$ matches nonzero determinant, aligning with the algebraic entanglement witness already proved for branch amplitudes elsewhere in the monolith.
Downstream the reduced-density step needs $C>0$ to force the spectrum of $\rho_1$ off ${0,1}$, so binary entropy is strictly positive. The full reduction $E_{\mathrm{VN}}(\rho_1)=h((1+\sqrt{1-C^2})/2)$ then follows from the algebraic core on binary entropy. Even with no direct used_by edges recorded yet, the sibling reducedDensity_det_ne_zero_of_concurrence_pos and the Prop-shaped entropy target sit on this same spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.