reducedDensity_det_eq_normSq_det
plain-language theorem explainer
For any complex 2×2 amplitude matrix A, the determinant of the first-qubit reduced density equals the squared modulus of det A (as a complex number). Entanglement theorists cite it as the pure-state bridge from Wootters concurrence to the spectrum of ρ₁. The proof expands both 2×2 determinants, unfolds the partial-trace sums, and finishes by ring after rewriting normSq via conjugate multiplication.
Claim. For every complex $2\times 2$ matrix $A$, if $\rho_1$ denotes the first-qubit reduced density matrix obtained by partial-tracing the pure bipartite state with amplitude matrix $A$, then $\det(\rho_1)=|\det A|^2$ (embedded $\mathbb{R}\to\mathbb{C}$).
background
Track 2.B of the Recognition Science quantum stack treats pure two-qubit states written as amplitude matrices $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$. The Wootters concurrence is the pure-state simplification $C(A):=2|\det A|$; vanishing determinant is exactly the product (separable) case.
The reduced density $\rho_1$ is the partial trace of $|\psi\rangle\langle\psi|$ over the second qubit. Its eigenvalues are $(1\pm\sqrt{1-4|\det A|^2})/2$, so $\det(\rho_1)$ controls the gap that feeds binary entropy and hence von Neumann entanglement entropy.
Complex squared modulus $\mathrm{normSq}(z)=z\overline{z}$ is the standard Born weight used throughout the finite Hilbert-display calculus; here it appears only as the scalar $|\det A|^2$.
proof idea
Expand $\det$ on both sides with the $2\times 2$ determinant formula. Unfold the definition of the reduced density and evaluate the four $\mathrm{Fin},2$ sums that build its entries. Rewrite the goal as an equality of explicit bilinear expressions in the entries of $A$ and their conjugates. Replace $\mathrm{normSq}$ by conjugate-self multiplication, push conjugation through subtraction and products, and close by the ring tactic.
why it matters
This identity is the algebraic core of the reduced-density step in Track 2.B: nonzero $\det A$ (equivalently positive concurrence) forces $\det(\rho_1)>0$, hence a nontrivial eigenvalue gap and strictly positive entanglement entropy. The immediate parent rephrases the right-hand side as $|\det A|^2$, after which the chain reaches $\det(\rho_1)=C^2/4$ and the positivity lemmas for concurrence. Module status is structural theorem with no new RS assumptions; the result sits entirely inside ordinary $2\times 2$ linear algebra supporting the Wootters formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.