pureTwoQubitConcurrenceEntropyCert
plain-language theorem explainer
Packages the full pure two-qubit concurrence-to-entropy certificate: nonnegativity and det-vanishing of Wootters C, reduced-density trace and det identities, spectral sum/product, binary-entropy positivity, and both conditional and unconditional entropy positivity. Anyone citing Track 2.B closure uses this bundle. Construction is a pure structure instance wiring already-proved lemmas.
Claim. There exists a certificate assembling: (i) $C(A)\ge 0$ and $C(A)=0\Leftrightarrow\det A=0$ for pure two-qubit amplitude matrices $A$; (ii) reduced-density trace equals the Frobenius norm and $\det\rho_1=C^2/4$; (iii) the spectral pair $(\lambda_+,\lambda_-)$ has sum $1$ and product $C^2/4$ for $C\in[0,1]$; (iv) binary entropy is strictly positive on $(0,1)$; (v) the inner radius $(1+\sqrt{1-C^2})/2$ lies in $[1/2,1)$ when $0<C\le 1$; and (vi) reduced von Neumann entropy is positive whenever $C>0$, and unconditionally under the reduced-entropy target.
background
Track 2.B of the master plan links Wootters concurrence of a pure two-qubit amplitude matrix to strict positivity of von Neumann entanglement entropy. For a normalized pure state $|\psi\rangle=\sum_{ij}A_{ij}|ij\rangle$, concurrence is the pure-state simplification $C(A):=2|\det A|$. The reduced density $\rho_1=\mathrm{tr}2|\psi\rangle\langle\psi|$ has eigenvalues $(1\pm\sqrt{1-C^2})/2$, so $E{VN}(\rho_1)=h((1+\sqrt{1-C^2})/2)$ where $h$ is binary entropy (symmetric about $1/2$).
The structure PureTwoQubitConcurrenceEntropyCert is the Prop-level bundle of the algebraic core plus the reduced-density and entropy-positivity clauses. Upstream lemmas already establish each field: concurrence nonnegativity and the zero-iff-det criterion; reduced trace equal to Frobenius norm; $\det\rho_1=C^2/4$; lambda-pair sum/product identities on $[0,1]$; binary entropy strictly positive on $(0,1)$; the inner-radius interval statement for $0<C\le 1$; and both the unconditional and concurrence-conditional entropy positivity theorems.
proof idea
One-line structure instance: each field of the certificate is filled by the corresponding already-proved theorem. Nonnegativity and zero-iff-det come from concurrence_nonneg and concurrence_eq_zero_iff_det_zero. Trace and determinant identities use reducedDensity_trace_eq_frobenius and reducedDensity_det_eq_concurrence_sq_div_four. Spectral invariants use lambdaPair_sum_product_of_concurrence_unit_interval. Binary-entropy positivity and the inner-radius interval use binaryEntropy_pos_of_open_unit_interval and inner_radius_in_unit_interval_of_pos_concurrence. Entropy positivity clauses are pure_two_qubit_entropy_positive_unconditional, the reduced-entropy target holder, and pure_two_qubit_entropy_positive_of_concurrence_positive. No new reasoning.
why it matters
This is the inhabiting witness that closes Track 2.B as a structural theorem: no proof holes and no new Recognition Science assumptions. Downstream, pureTwoQubitConcurrenceEntropyCert_inhabited simply wraps it as Nonempty PureTwoQubitConcurrenceEntropyCert, giving a single named object that later quantum-channel or entanglement-witness developments can require. The module status line records the full reduction $E_{VN}(\rho_1)=h((1+\sqrt{1-C^2})/2)$ as discharged. Strict positivity of $C$ matches the algebraic entanglement witness already available from the det-factored branch-amplitude work, so the certificate sits at the pure-state interface between concurrence geometry and entropy positivity without touching the forcing chain (T0–T8) or the Recognition Composition Law directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.