PureTwoQubitReducedEntropyTargetDef
plain-language theorem explainer
Namespace alias for the reduced-density-matrix sub-target already discharged in §3b of this module. It names the Prop that the reduced state of a pure two-qubit amplitude has eigenvalues fixed by the Wootters concurrence, so von Neumann entropy equals binary entropy of that spectrum. Downstream composite positivity cites this anchor rather than reopening the RDM algebra. Pure abbreviation: no proof content.
Claim. Abbreviation for the reduced-density-matrix sub-target: for a pure two-qubit amplitude matrix $A$ of a normalized state $|\psi\rangle=\sum_{ij} A_{ij}|ij\rangle$, the reduced density $\rho_1=\mathrm{tr}_2|\psi\rangle\langle\psi|$ has eigenvalues $(1\pm\sqrt{1-C(A)^2})/2$ with Wootters concurrence $C(A)=2|\det A|$, hence $E_{\mathrm{VN}}(\rho_1)=h\bigl((1+\sqrt{1-C(A)^2})/2\bigr)$ where $h$ is binary entropy.
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. The module status is structural theorem: no proof holes and no new Recognition Science assumptions.
Concurrence is the pure-state formula $C(A):=2|\det A|$ on a normalized $2\times 2$ complex amplitude matrix. The algebraic core shows that for $C\in(0,1]$ the value $(1+\sqrt{1-C^2})/2$ lies in $(1/2,1]$, and binary entropy $h(p)=-p\log p-(1-p)\log(1-p)$ is strictly positive on $(0,1)$.
The reduced-density-matrix step supplies the spectral identification: eigenvalues of $\rho_1$ are exactly $(1\pm\sqrt{1-C^2})/2$, so $E_{\mathrm{VN}}(\rho_1)=h$ of either eigenvalue (binary entropy is symmetric about $1/2$). That step is packaged as a Prop-shaped sub-target already defined and discharged in §3b; this abbrev is only the namespace anchor for that Prop.
proof idea
One-line abbreviation. The body is the already-defined reduced-density-matrix sub-target from §3b; there is no tactic proof, no lemma application, and no new obligation. Downstream composite statements simply refer to this name when they assume the RDM spectral relation and compose it with the algebraic binary-entropy core.
why it matters
Gives a stable citation handle for the RDM half of Track 2.B so the composite section (§5) can state conditional closure: an abstract von Neumann functional meeting the reduced-density sub-target, plus strict concurrence positivity, yields strict positivity of entanglement entropy. The full chain is $E_{\mathrm{VN}}(\rho_1)=h((1+\sqrt{1-C^2})/2)$, combining algebraic core with this spectral identification.
Module doc records Track 2.B closed as a structural theorem. Concurrence positivity matches the algebraic entanglement witness already available from the det-branch amplitude factorization in the quantum-channel development. No new RS forcing-chain hypotheses (T5–T8, RCL, phi ladder) enter; the content is pure two-qubit linear algebra and entropy calculus inside the Recognition quantum track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.