pure_two_qubit_entropy_positive_of_concurrence_positive
plain-language theorem explainer
Strict positivity of Wootters concurrence on a normalized pure two-qubit amplitude matrix forces strict positivity of any von Neumann entropy that matches the reduced-density binary-entropy formula. Cite this when closing the pure-state entanglement chain under an abstract entropy interface. The proof rewrites through the reduced-entropy target and applies the algebraic binary-entropy positivity lemma on the concurrence radius.
Claim. Let $S$ be a real-valued map on $2\times 2$ complex matrices such that, whenever $A$ is Frobenius-normalized ($\sum_{i,j}|A_{ij}|^2=1$), one has $S(A)=h\bigl((1+\sqrt{1-C(A)^2})/2\bigr)$, where $h$ is binary entropy and $C(A)=2|\det A|$ is the Wootters concurrence. If $0<C(A)\le 1$, then $S(A)>0$.
background
Track 2.B treats pure two-qubit entanglement for an amplitude matrix $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$. The Wootters concurrence is the pure-state simplification $C(A):=2|\det A|$; nonnegativity and $C=0\Leftrightarrow\det=0$ are already in-module. Normalization is the Frobenius condition $\sum_{i,j}|A_{ij}|^2=1$.
The reduced state $\rho_1=\mathrm{tr}_2|\psi\rangle\langle\psi|$ of a pure bipartite qubit has eigenvalues $(1\pm\sqrt{1-C^2})/2$. Von Neumann entropy of a qubit is therefore binary entropy of either eigenvalue. The module packages that identification as a Prop-shaped sub-target: any candidate entropy functional must equal $h((1+\sqrt{1-C(A)^2})/2)$ on normalized $A$.
The algebraic core already shows that for $C\in(0,1]$ the argument of $h$ lies in $(1/2,1)$, hence strictly inside $(0,1)$, where binary entropy is strictly positive. This theorem only composes that core with the sub-target interface.
proof idea
Term-mode, two steps. First rewrite the goal $0<S(A)$ by the sub-target hypothesis at the given normalized $A$, replacing $S(A)$ by binary entropy of the concurrence radius $(1+\sqrt{1-C(A)^2})/2$. Second, discharge the rewritten inequality by the existing algebraic lemma that binary entropy of that radius is strictly positive whenever $0<C(A)\le 1$. No matrix spectral work happens here; all reduced-density content is abstracted into the hypothesis.
why it matters
This is the conditional half of Track 2.B closure: concurrence positivity implies entanglement-entropy positivity once the reduced-density formula is assumed. Downstream, the unconditional theorem instantiates the same argument at the canonical spectral entropy, and the concurrence-entropy certificate bundles the supporting algebraic and reduced-density facts for export.
In the broader Recognition layout the result sits in the quantum channel / entanglement witness layer rather than the T0–T8 forcing chain. It connects the pure-state determinant witness (nonzero $\det A$) to a thermodynamic-style entropy positivity statement, matching the module claim that Track 2.B is structurally closed with no new RS assumptions. Open work, if any, lives outside this file: mixed-state concurrence and multipartite extensions are not addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.