reducedDensity_eq_mul_conjTranspose
plain-language theorem explainer
The partial-trace formula for a pure two-qubit amplitude matrix A coincides with the matrix product A A†. Anyone working the reduced-density step of the concurrence-to-entropy chain cites this identity. The proof is a one-line entrywise expansion: both sides are Σⱼ Aᵢⱼ conj(Aₖⱼ).
Claim. For every complex $2\times 2$ matrix $A$, the first-qubit reduced density matrix defined by the partial trace $\rho_1(i,k)=\sum_j A_{ij}\overline{A_{kj}}$ equals the ordinary matrix product $A A^\dagger$.
background
Track 2.B of the Recognition Science quantum plan links Wootters concurrence of a pure two-qubit amplitude matrix to strict positivity of von Neumann entanglement entropy. The amplitude matrix $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$ encodes $|\psi\rangle=\sum_{ij}A_{ij}|ij\rangle$. Concurrence is $C(A):=2|\det A|$.
The reduced density on the first qubit is the partial trace $\rho_1=\mathrm{tr}2|\psi\rangle\langle\psi|$. In coordinates the module defines it entrywise as $\rho_1(i,k)=\sum_j A{ij}\overline{A_{kj}}$. The same object is classically $A A^\dagger$ in matrix notation; the definition's doc-comment already records that equivalence.
This lemma makes the equivalence a proved identity rather than a comment, so later Hermitian and spectral arguments can rewrite through the Mathlib matrix API.
proof idea
Entrywise extensionality on the $2\times 2$ index type, then simp unfolds reducedDensity, matrix multiplication, conjugate transpose, and the star endomorphism on $\mathbb{C}$. Both sides reduce to the same finite sum $\sum_j A_{ij}\overline{A_{kj}}$, so the equality is definitional after unfolding.
why it matters
Immediate parent is reducedDensity_isHermitian, which rewrites through this identity and applies Mathlib's Matrix.isHermitian_mul_conjTranspose_self. Hermitianness is required before eigenvalues, determinant identities, and the binary-entropy formula $E_{\mathrm{VN}}(\rho_1)=h((1\pm\sqrt{1-C^2})/2)$ can be stated.
In the module's reduction chain this sits in the reduced-density-matrix step that feeds PureTwoQubitReducedEntropyTarget and closes Track 2.B (structural theorem, no new RS assumptions). It is ordinary linear algebra supporting the RS quantum track, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.