eigenvalues_fin_two_prod_eq_of_complex_prod
plain-language theorem explainer
If two reals, cast to complexes, multiply to a third real cast to complex, then the real product equals that third real. Used when eigenvalue products of a Hermitian reduced density matrix are computed in ℂ and must be returned to ℝ. Proof is a two-line rewrite via ofReal_mul plus injectivity of the real-to-complex embedding.
Claim. Let $e_0, e_1, p \in \mathbb{R}$. If $(e_0 : \mathbb{C}) \cdot (e_1 : \mathbb{C}) = (p : \mathbb{C})$, then $e_0 \cdot e_1 = p$.
background
Track 2.B of the Recognition Science quantum program links Wootters concurrence of a pure two-qubit amplitude matrix $A$ to strict positivity of the von Neumann entanglement entropy of the reduced density matrix $\rho_1 = \mathrm{tr}_2 |\psi\rangle\langle\psi|$. Concurrence is $C(A) := 2|\det A|$, and the eigenvalues of $\rho_1$ are $(1 \pm \sqrt{1-C^2})/2$.
Hermitian eigenvalue APIs in Mathlib return real eigenvalues, but determinant and product identities are often stated over $\mathbb{C}$. The embedding $\mathbb{R}\to\mathbb{C}$ is a ring homomorphism and is injective, so equalities of products proved in $\mathbb{C}$ transfer back to $\mathbb{R}$. This private lemma is the exact transfer step for a two-eigenvalue product.
proof idea
Rewrite the complex product hypothesis with Complex.ofReal_mul, so the left-hand side becomes the complexification of the real product $e_0 e_1$. Then apply Complex.ofReal_injective to conclude $e_0 e_1 = p$ in $\mathbb{R}$. No case splits or analysis; pure embedding injectivity.
why it matters
Feeds the private theorem reducedDensity_eigenvalues_prod_eq_concurrence_sq_div_four, which asserts that the product of the two eigenvalues of the reduced density matrix equals $C(A)^2/4$. That identity is the bridge from the algebraic concurrence formula to the spectral data of $\rho_1$, and thence to $E_{\mathrm{VN}}(\rho_1)=h((1+\sqrt{1-C^2})/2)$ in the Track 2.B closure.
Without the real-complex product transfer, the determinant-as-product-of-eigenvalues step stays stuck in $\mathbb{C}$. The lemma is scaffolding-free and introduces no new RS assumptions; it is pure Mathlib hygiene inside an otherwise structural quantum theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.