reducedDensity
plain-language theorem explainer
Defines the first-qubit reduced density matrix of a pure two-qubit amplitude matrix A as the partial trace over the second qubit: ρ₁ = A A† with entries Σⱼ Aᵢⱼ conj(Aₖⱼ). Anyone proving Wootters concurrence identities or von Neumann entanglement entropy for pure two-qubit states cites this. The body is a direct entrywise sum, not a derived theorem.
Claim. For a $2\times 2$ complex amplitude matrix $A$, the first-qubit reduced density matrix is the $2\times 2$ matrix $\rho_1$ with entries $\rho_1(i,k)=\sum_j A_{ij}\overline{A_{kj}}$. Equivalently $\rho_1=A A^\dagger$, the partial trace of $|\psi\rangle\langle\psi|$ over the second qubit when $|\psi\rangle=\sum_{ij}A_{ij}|ij\rangle$.
background
Track 2.B of the pure two-qubit module links Wootters concurrence of a pure amplitude matrix to strict positivity of von Neumann entanglement entropy. The concurrence convention is $C(A):=2|\det A|$ for normalized $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$. The reduced-density step is the bridge: eigenvalues of $\rho_1=\mathrm{tr}2|\psi\rangle\langle\psi|$ are $(1\pm\sqrt{1-C^2})/2$, so $E{\mathrm{VN}}(\rho_1)$ equals the binary entropy of that argument.
This definition supplies $\rho_1$ itself. Entrywise it is the Gram matrix of the rows of $A$ under the standard Hermitian product, i.e. $A A^\dagger$. Sibling objects include the Frobenius norm squared (normalization) and the concurrence functional; later lemmas relate $\det\rho_1$ to $|\det A|^2$ and to $C(A)^2/4$.
proof idea
Not a proof: a four-line definition. The matrix is specified entrywise by summing over the traced qubit index $j$, multiplying $A_{ij}$ by the complex conjugate of $A_{kj}$ via starRingEnd. That is exactly the $(i,k)$ entry of $A A^\dagger$ and of the partial trace of the pure projector.
why it matters
Every algebraic identity in the reduced-density half of Track 2.B is stated about this object: $\det\rho_1=|\det A|^2$, $\det\rho_1=C(A)^2/4$, nonvanishing of $\det\rho_1$ when $C>0$, the discriminant identity $\mathrm{tr}(\rho_1)^2-4\det\rho_1=1-C^2$ under unit Frobenius norm, hermiticity, and the certificate clause that the reduced-density trace equals the Frobenius norm. Those feed PureTwoQubitConcurrenceEntropyCert and the composition that yields $E_{\mathrm{VN}}(\rho_1)=h((1+\sqrt{1-C^2})/2)$ with strict positivity for $C\in(0,1]$. The module status is structural theorem, Track 2.B closed, no new RS assumptions; this def is the matrix-level substrate of that closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.