reducedDensity_trace_eq_frobenius
plain-language theorem explainer
For any 2×2 complex amplitude matrix, the sum of the diagonal entries of its single-qubit reduced density equals the squared Frobenius norm of that matrix (as a complex scalar). Anyone showing that a normalized pure two-qubit state has unit-trace reduced density cites this identity. The proof unfolds both sides, expands the three Fin-2 sums, and closes by conjugate multiplication.
Claim. For every $2\times 2$ complex matrix $A$, $$\rho(A)_{00}+\rho(A)_{11}=\|A\|_F^2$$ holds in $\mathbb{C}$, where $\rho(A)$ is the reduced density matrix of the pure bipartite state with amplitude matrix $A$, and $\|A\|_F^2=\sum_{i,j}|A_{ij}|^2$.
background
Track 2.B works with pure two-qubit states written through an amplitude matrix $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$, so $|\psi\rangle=\sum_{ij}A_{ij}|ij\rangle$. The reduced density on the first factor is $\rho_1=\mathrm{tr}_2|\psi\rangle\langle\psi|$; its diagonal sum is the ordinary matrix trace of $\rho_1$.
The squared Frobenius norm $|A|F^2=\sum{i,j}|A_{ij}|^2$ is the $L^2$ mass of the amplitude matrix. Normalization $|A|_F=1$ means $|\psi\rangle$ is a unit vector, and one then expects $\mathrm{tr}(\rho_1)=1$. This lemma is the bare algebraic identity linking that diagonal sum to $|A|_F^2$ before any normalization hypothesis is imposed.
The surrounding module closes the chain from Wootters concurrence $C(A)=2|\det A|$ to strict positivity of von Neumann entanglement entropy, as a structural theorem with no new Recognition Science assumptions.
proof idea
Direct term-mode expansion. Unfold the definitions of the reduced density and of the squared Frobenius norm. Expand every sum over $\mathrm{Fin},2$ with the two-point universe rewrite (applied three times). The resulting four-term expressions agree after simplification with the complex identity $z\cdot\overline{z}=|z|^2$. No external domain lemmas are needed beyond Fin-sum rewriting and conjugate arithmetic.
why it matters
This is the trace half of the reduced-density step inside Track 2.B. Downstream, the normalized specialization reads off unit trace whenever $|A|_F^2=1$, and a thin wrapper restates the same fact as an equality of matrix traces. Both are packaged into the pure two-qubit concurrence-entropy certificate, which also carries concurrence nonnegativity, the det-zero characterization, and the relation of $\det A$ to $C^2/4$.
With the eigenvalue formula $\lambda_\pm=(1\pm\sqrt{1-C^2})/2$ already in the module plan, unit trace underwrites $E_{\mathrm{VN}}(\rho_1)=h((1+\sqrt{1-C^2})/2)$ and therefore strict positivity of entanglement entropy for $C>0$. Module status: structural theorem, Track 2.B closed, no proof holes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.