PureTwoQubitConcurrenceEntropyCert
plain-language theorem explainer
A certificate structure packaging the algebraic core of pure two-qubit entanglement: Wootters concurrence nonnegativity and det-equivalence, reduced-density trace and det identities, spectral pair sum/product, binary-entropy positivity, and both unconditional and conditional entropy positivity. Anyone citing Track 2.B (concurrence implies strict von Neumann entropy) uses this bundle. It is a pure structure definition; the inhabited instance wires the sibling lemmas into the fields.
Claim. A certificate is a record of ten facts for pure two-qubit amplitude matrices $A\in M_2(\mathbb{C})$: (1) concurrence $C(A)\ge 0$; (2) $C(A)=0$ iff $\det A=0$; (3) $\mathrm{tr}\,\rho_1(A)=\|A\|_F^2$; (4) $\det\rho_1(A)=C(A)^2/4$; (5) for $C\in[0,1]$, the spectral candidates $\lambda_\pm(C)$ satisfy $\lambda_++\lambda_-=1$ and $\lambda_+\lambda_-=C^2/4$; (6) binary entropy $h(p)>0$ on $(0,1)$; (7) for $0<C\le 1$, the inner radius $(1+\sqrt{1-C^2})/2$ lies in $[1/2,1)$; (8) if $\|A\|_F=1$ and $C(A)>0$ then the canonical reduced von Neumann entropy is strictly positive; (9) that canonical functional meets the reduced-entropy target $E_{\mathrm{VN}}(A)=h((1+\sqrt{1-C(A)^2})/2)$; (10) any functional meeting the target is strictly positive under the same hypotheses with $C(A)\le 1$.
background
Track 2.B links the Wootters concurrence of a pure two-qubit amplitude matrix to strict positivity of the reduced 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{\mathrm{VN}}(\rho_1)=h((1+\sqrt{1-C^2})/2)$ with binary entropy $h(p)=-p\log p-(1-p)\log(1-p)$.
The module status is structural: no new Recognition Science assumptions, no proof holes. Sibling definitions supply concurrence, Frobenius norm squared, the reduced density matrix, and the spectral entropy functional. The Prop-shaped sub-target PureTwoQubitReducedEntropyTarget asserts that a candidate entropy equals binary entropy of the inner radius whenever the Frobenius norm is one.
Upstream foundation material (finite Hilbert displays, amplitude norm-squared, configuration entropy as total defect) supplies the Born-weight and minimum-entropy language, but the certificate itself is pure $2\times 2$ linear algebra plus real analysis of $h$ and $\sqrt{1-C^2}$.
proof idea
No proof body: the declaration is a structure whose fields are named propositions. Inhabitation is separate. The companion definition pureTwoQubitConcurrenceEntropyCert fills each field by a sibling lemma: nonnegativity and zero-iff-det from the concurrence API; reduced trace from the Frobenius identity; reduced det from the $C^2/4$ identity; spectral sum/product, binary-entropy positivity, and inner-radius interval from the algebraic core; unconditional positivity and the reduced-entropy target from the spectral entropy construction; conditional positivity by composing any functional meeting the target with that core. The inhabited theorem is then a one-line Nonempty witness wrapping that value.
why it matters
This certificate is the single package that closes Track 2.B: concurrence positivity forces strict entanglement entropy for pure two-qubit states. Downstream, pureTwoQubitConcurrenceEntropyCert is the concrete inhabitant, and pureTwoQubitConcurrenceEntropyCert_inhabited records Nonempty so later modules can assume the bundle without re-proving each clause.
In the Recognition framework it sits on the quantum side of the forcing chain rather than on T5–T8 directly: it converts the algebraic entanglement witness (nonzero determinant of the amplitude matrix, already used in gravity/quantum-channel work) into a thermodynamic statement (strictly positive reduced entropy). The full reduction $E_{\mathrm{VN}}=h((1+\sqrt{1-C^2})/2)$ is the composition of the reduced-density target with the algebraic core packaged here. No open scaffolding remains in this module; the structure is the closed interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.