PureTwoQubitReducedEntropyTarget
plain-language theorem explainer
Packages the reduced-density-matrix identity for pure two-qubit states: any von Neumann entropy functional on 2×2 amplitude matrices must equal binary entropy of (1+√(1−C²))/2 whenever the Frobenius norm is one. Cited by the conditional and unconditional entropy-positivity closures in Track 2.B. Definitional Prop, not a proved equality; the equality is discharged later for the spectral entropy.
Claim. A real-valued functional $S$ on $2\times 2$ complex matrices satisfies the reduced-entropy target if, for every amplitude matrix $A$ with $\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.
background
Track 2.B links Wootters concurrence of a pure two-qubit amplitude matrix to strict positivity of von Neumann entanglement entropy. For normalized $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$, concurrence is $C(A):=2|\det A|$. The reduced state $\rho_1=\mathrm{tr}2|\psi\rangle\langle\psi|$ has eigenvalues $(1\pm\sqrt{1-C^2})/2$, so $E{\mathrm{VN}}(\rho_1)$ equals binary entropy of either eigenvalue.
Binary entropy is $h(p)=-p\log p-(1-p)\log(1-p)$, continuous with $h(0)=h(1)=0$. The algebraic core already shows $h((1+\sqrt{1-C^2})/2)>0$ whenever $C\in(0,1]$. This definition isolates the remaining reduced-density step as a Prop on an abstract entropy functional, so the positivity argument can be stated once and instantiated at the spectral definition.
proof idea
No proof body: this is a Prop-valued definition. It quantifies over all $2\times 2$ complex matrices $A$ with unit Frobenius norm (sum of squared moduli of entries equal to 1) and asserts equality of the supplied entropy map with binaryEntropy evaluated at $(1+\sqrt{1-(\mathrm{concurrence},A)^2})/2$. Downstream, pureTwoQubitReducedEntropyTarget_holds discharges the Prop at reducedDensityVonNeumannEntropy by relating eigenvalues of the partial trace to concurrence.
why it matters
Closes the interface between the algebraic core of Track 2.B and the spectral entropy definition. The conditional theorem pure_two_qubit_entropy_positive_of_concurrence_positive takes this Prop as hypothesis and concludes $0<S(A)$ from $0<C(A)$. The unconditional theorem instantiates that argument after pureTwoQubitReducedEntropyTarget_holds proves the Prop for the canonical reduced-density von Neumann entropy. The certificate structure PureTwoQubitConcurrenceEntropyCert and the alias PureTwoQubitReducedEntropyTargetDef also reference it. Module status is structural theorem, Track 2.B closed, no new RS assumptions; this sub-target is the named hinge that makes the composition modular.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.