reducedDensity_trace_eq_one_of_normalized_complex
plain-language theorem explainer
For a pure two-qubit amplitude matrix over ℂ with unit Frobenius norm-squared, the first-qubit reduced density has trace one. Anyone assembling the eigenvalue sum or von Neumann entropy chain in Track 2.B cites this. The argument is a short rewrite through the Frobenius-trace identity, then numerical cleanup of the constant.
Claim. Let $A$ be a $2\times 2$ matrix with complex entries. If $\sum_{i,j}\|A_{ij}\|^2=1$, then $\operatorname{tr}(\rho_1(A))=1$, where $\rho_1(A)$ is the first-qubit reduced density matrix of the pure bipartite state with amplitude matrix $A$ (partial trace over the second qubit).
background
Track 2.B of the pure two-qubit module links Wootters concurrence of a normalized amplitude matrix $A$ to strict positivity of the von Neumann entanglement entropy of the reduced state. The state is $|\psi\rangle=\sum_{ij}A_{ij}|ij\rangle$; the reduced density $\rho_1=\operatorname{tr}_2|\psi\rangle\langle\psi|$ is the object whose spectrum feeds binary entropy.
Normalization is algebraic: the Frobenius norm-squared $\sum_{i,j}|A_{ij}|^2$ (via Complex.normSq) equals one. An upstream identity in the same module equates $\operatorname{tr}(\rho_1(A))$ to that Frobenius quantity (complex version). Unit trace is the density-matrix sanity check needed before eigenvalues can be treated as a probability pair.
The module status is structural: no new Recognition Science assumptions; the chain is pure linear algebra on $2\times 2$ complex amplitudes.
proof idea
Term-mode proof in three short steps. Rewrite the goal with the complex Frobenius-trace identity (reducedDensity_trace_eq_frobenius_complex), which replaces $\operatorname{tr}(\rho_1(A))$ by the Frobenius norm-squared of $A$. Substitute the normalization hypothesis that this equals $1$. Finish with norm_num to close the resulting numeral equality. No case splits and no spectral theory.
why it matters
Unit trace of $\rho_1$ is the bridge from normalization of $|\psi\rangle$ to the spectral picture used for entanglement entropy. The sole recorded consumer is reducedDensity_eigenvalues_sum_eq_one, which states that the two Hermitian eigenvalues of $\rho_1$ sum to one under the same hypothesis; that fact is required so the eigenvalues can be written $(1\pm\sqrt{1-C^2})/2$ and fed into binary entropy.
In the module plan this sits inside the reduced-density-matrix step of Track 2.B: concurrence $C=2|\det A|$ controls the eigenvalue gap, and entropy positivity follows once the spectrum is a normalized pair in $(0,1)$. The result is ordinary QM bookkeeping, not an RS forcing step (T0–T8), but it closes a necessary lemma in the structural entropy-concurrence theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.