concurrence_eq_zero_iff_det_zero
plain-language theorem explainer
Wootters concurrence of a pure two-qubit amplitude matrix vanishes exactly when that matrix has zero determinant. Anyone citing the algebraic entanglement witness for pure bipartite states, or the Track 2.B entropy-positivity chain, needs this equivalence. The proof unfolds C(A)=2‖det A‖ and uses nonnegativity of the complex modulus in both directions.
Claim. For every $2\times 2$ complex amplitude matrix $A$, the Wootters concurrence $C(A):=2\|\det A\|$ satisfies $C(A)=0$ if and only if $\det A=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. For a pure state $|\psi\rangle=\sum_{ij}A_{ij}|ij\rangle$, the pure-state Wootters formula collapses to $C(A)=2|\det A|$. That is the local definition of concurrence used throughout.
The reduced density matrix $\rho_1=\mathrm{tr}_2|\psi\rangle\langle\psi|$ has eigenvalues $(1\pm\sqrt{1-C^2})/2$, so entanglement entropy is the binary entropy of those eigenvalues. Vanishing concurrence is therefore the algebraic marker of a product (separable) pure state. The module already records nonnegativity of concurrence; the present statement is the zero-set characterization that matches the earlier algebraic entanglement witness via nonzero determinant.
proof idea
One short tactic proof. Unfold the definition $C(A)=2|\det A|$. Left-to-right: if the product is zero then $|\det A|=0$ by nonnegativity of the norm (via linarith with norm_nonneg), hence $\det A=0$ by norm_eq_zero. Right-to-left: substitute $\det A=0$ and simplify $2|0|$ to zero. No external lemmas beyond the norm API.
why it matters
This is the zero-set half of the pure-state concurrence dictionary. Downstream, concurrence_pos_iff_det_ne_zero rewrites positivity of $C$ as nonzero determinant by combining this iff with nonnegativity. The certificate bundle pureTwoQubitConcurrenceEntropyCert packages the same fact as concurrence_zero_iff_det_zero, feeding the structural theorem that $E_{\mathrm{VN}}(\rho_1)>0$ precisely when $C>0$.
In the broader Recognition plan this discharges the algebraic core of Track 2.B with no new RS assumptions: concurrence zero iff det zero is the pure-state simplification of Wootters, aligned with the determinant branch-amplitude witness already used elsewhere in the quantum-channel development. 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-positivity reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.