reducedDensity_trace_eq_frobenius_complex
plain-language theorem explainer
For any 2×2 complex amplitude matrix, the trace of the first-qubit reduced density equals the Frobenius norm-squared of the amplitudes, viewed in ℂ. Workers on the pure two-qubit entropy–concurrence chain cite it to promote the real normalization identity into complex scalars. The proof is a one-line rewrite through the Fin-2 trace expansion and the real-valued sibling lemma.
Claim. For every $2\times 2$ matrix $A$ with complex entries, $\operatorname{tr}(\rho_1(A)) = \|A\|_F^2$ as elements of $\mathbb{C}$, where $\rho_1(A)$ is the reduced density matrix of the pure two-qubit state with amplitude matrix $A$ (partial trace over the second qubit) and $\|A\|_F^2 = \sum_{i,j} |A_{ij}|^2$.
background
Track 2.B of the pure two-qubit module links Wootters concurrence $C(A) = 2|\det A|$ of a normalized amplitude matrix to strict positivity of the von Neumann entanglement entropy of the reduced state. The reduced density $\rho_1(A)$ is the partial trace of $|\psi\rangle\langle\psi|$ over the second qubit; its eigenvalues are $(1 \pm \sqrt{1-C^2})/2$, so entropy is the binary entropy of that spectrum.
The Frobenius norm-squared $|A|F^2 = \sum{i,j}|A_{ij}|^2$ is the algebraic normalization of the pure state. A real-valued sibling already equates $\operatorname{tr}(\rho_1(A))$ (as a real) to that sum. The present statement lifts the equality into $\mathbb{C}$ so that later complex-trace goals typecheck without coercions.
Local setting: structural theorems only, no new Recognition Science assumptions; the module closes the algebraic core plus the reduced-density step of the entropy-positivity chain.
proof idea
One-line wrapper. Expand the $2\times 2$ matrix trace via Matrix.trace_fin_two, then rewrite by the real sibling reducedDensity_trace_eq_frobenius, which already identifies the diagonal sum of $\rho_1(A)$ with $|A|_F^2$. The coercion of the real Frobenius sum into $\mathbb{C}$ is implicit in the goal type.
why it matters
Immediate parent is reducedDensity_trace_eq_one_of_normalized_complex: under $|A|F^2 = 1$ the complex trace equals $1$, the density-matrix normalization needed before eigenvalue and entropy arguments. That step sits inside the reduced-density half of Track 2.B, which feeds the full identity $E{\mathrm{VN}}(\rho_1) = h((1+\sqrt{1-C^2})/2)$ and the strict positivity theorem for entangled pure two-qubit states.
In the broader Recognition Science quantum track this is bookkeeping, not a new physical claim: it keeps the pure-state partial-trace calculus aligned with the concurrence witness already tied to the algebraic entanglement fact in the BMV-positive channel work. No forcing-chain landmark (T5–T8, RCL, $\phi$-ladder) is touched; the lemma is infrastructure for the entropy–concurrence bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.