pure_two_qubit_entropy_positive_unconditional
plain-language theorem explainer
For a normalized pure two-qubit amplitude matrix with strictly positive Wootters concurrence, the von Neumann entropy of the reduced one-qubit density is strictly positive. Gravity and quantum-channel arguments cite this as the unconditional entropy-positivity closure of Track 2.B. The proof is a short wrapper: rename the Frobenius-norm hypothesis, invoke the discharged reduced-entropy target, and apply the conditional positivity lemma with the bound C ≤ 1.
Claim. Let $A$ be a $2\times 2$ complex amplitude matrix with Frobenius norm $\sum_{i,j}|A_{ij}|^2=1$ and Wootters concurrence $C(A)=2|\det A|>0$. Then the von Neumann entropy of the reduced density matrix $\rho_1=\mathrm{tr}_2|A\rangle\langle A|$ is strictly positive: $S(\rho_1)>0$.
background
Track 2.B links the Wootters concurrence of a pure two-qubit amplitude matrix to strict positivity of the entanglement entropy. For a normalized $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$, concurrence is the pure-state simplification $C(A):=2|\det A|$. Strict positivity of $C$ is equivalent to nonzero determinant and matches the algebraic entanglement witness used elsewhere in the gravity/quantum-channel stack.
The reduced density $\rho_1=\mathrm{tr}_2|\psi\rangle\langle\psi|$ has eigenvalues $(1\pm\sqrt{1-C^2})/2$. Hence the von Neumann entropy equals the binary entropy $h((1+\sqrt{1-C^2})/2)$, with $h(p)=-p\log p-(1-p)\log(1-p)$. For $C\in(0,1]$ that argument lies in $[1/2,1)$, so $h$ is strictly positive. The spectral identification is packaged as the Prop-shaped sub-target PureTwoQubitReducedEntropyTarget; the module discharges it at the canonical spectral definition and composes it with the algebraic core.
This declaration is the unconditional closure: concurrence positivity alone (plus normalization) yields $S(\rho_1)>0$, with no residual hypothesis on the reduced-entropy target.
proof idea
One-line wrapper around the conditional lemma. First rewrite the double-sum normalization hypothesis as equality of the Frobenius-norm-squared to $1$ (definitional simpa). Then apply pure_two_qubit_entropy_positive_of_concurrence_positive, feeding four ingredients: the discharged certificate pureTwoQubitReducedEntropyTarget_holds (canonical spectral entropy matches the binary-entropy formula), the matrix $A$, the original normalization and concurrence-positivity hypotheses, and concurrence_le_one_of_normalized (so $0<C\le 1$). The conditional lemma already knows that binary entropy is positive on $(0,1)$ and that the inner radius lies in $[1/2,1)$ whenever $C\in(0,1]$.
why it matters
Closes Track 2.B of the master plan: the full chain from Wootters concurrence of a pure two-qubit amplitude to strict positivity of reduced von Neumann entropy, with no proof holes and no new Recognition Science assumptions. The module certificate pureTwoQubitConcurrenceEntropyCert records this as clause entropy_pos_unconditional alongside nonnegativity of $C$, the det-zero equivalence, reduced-trace/det identities, and the spectral sum-product laws.
Downstream, Gravity.MasterTheorem.bmv_positive_unconditional_proven is literally this theorem, so the BMV-positivity clause of the gravity master theorem inherits unconditional status from Track 2.B. That feeds the broader master-theorem assembly (Hawking-temperature positivity, Page-curve content, and related continuum clauses). The concurrence-determinant link also aligns with the algebraic entanglement witness already used in the det-factored branch-amplitude facts.
Within the RS forcing picture this is structural quantum bookkeeping rather than a new T0–T8 step: it certifies that nonzero pure-state entanglement (nonzero det on the two-qubit block) forces positive entanglement entropy, which gravity-side positivity statements then quote by name.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.