reducedDensity_trace_eq_one_of_normalized

In the pure two-qubit setting a state is encoded by an amplitude matrix $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$. The Frobenius norm squared of $A$ is the total Born weight $\sum_{ij}|A_{ij}|^2$. Normalization means this equals one, so $A$ represents a pure state $|\psi\rangle=\sum_{ij}A_{ij}|ij\rangle$.

The reduced density on the first qubit is the partial trace $\rho_1=\operatorname{tr}_2|\psi\rangle\langle\psi|$. Its diagonal sum is the ordinary matrix trace; for $\rho_1$ to be a physical density operator that trace must equal one.

This module closes Track 2.B: the chain from Wootters concurrence $C(A)=2|\det A|$ of a pure two-qubit amplitude matrix to strict positivity of the von Neumann entanglement entropy. A sibling identity already equates $\operatorname{tr}(\rho_1)$ with the Frobenius norm squared of $A$, so the present statement is the normalized special case.

One-line tactic proof. Rewrite the claimed diagonal sum by the sibling identity that the reduced-density trace equals the Frobenius norm squared of $A$. Substitute the normalization hypothesis (that norm squared equals $1$). Finish with norm_num, which discharges $1=1$.

Track 2.B needs $\rho_1$ to be a genuine density matrix before its eigenvalues $(1\pm\sqrt{1-C^2})/2$ can feed the binary-entropy formula $E_{\mathrm{VN}}(\rho_1)=h((1+\sqrt{1-C^2})/2)$. Unit trace is the first structural requirement on that path. The module is marked STRUCTURAL THEOREM (Track 2.B closed; no proof holes, no new RS assumptions). Sibling results then relate $\det\rho_1$ to $|\det A|^2$ and to $C^2/4$, converting the algebraic entanglement witness $\det A\neq 0$ into positive concurrence and hence positive entropy. No downstream edges are recorded yet; the lemma sits inside the reduced-density infrastructure that the entropy-positivity composition uses.