eigenvalues_fin_two_sum_eq_of_complex_sum
plain-language theorem explainer
If two reals, cast into ℂ, sum to a third real cast into ℂ, then the original reals sum to that third value. Anyone tracking eigenvalue sums of a 2×2 Hermitian reduced density matrix cites this when Mathlib returns the sum in ℂ. The proof rewrites the sum via the real embedding and applies injectivity of ℝ → ℂ.
Claim. Let $e_0, e_1, t \in \mathbb{R}$. If $(e_0 : \mathbb{C}) + (e_1 : \mathbb{C}) = (t : \mathbb{C})$, then $e_0 + e_1 = t$ as real numbers.
background
Track 2.B of the pure two-qubit module links Wootters concurrence $C(A) = 2|\det A|$ of a normalized amplitude matrix $A$ to strict positivity of the von Neumann entanglement entropy of the reduced state. The reduced density matrix $\rho_1 = \mathrm{tr}_2 |\psi\rangle\langle\psi|$ is Hermitian on $\mathbb{C}^2$; its eigenvalues are real and, for a pure normalized state, sum to one.
Mathlib's Hermitian eigenvalue API often states additive identities after the canonical embedding $\mathbb{R} \hookrightarrow \mathbb{C}$. This lemma is the one-line bridge that recovers the real identity $e_0 + e_1 = t$ from the complex equality of casts. It is local bookkeeping, not a physical assumption: the module status is structural theorem with no new Recognition Science hypotheses.
proof idea
Term-mode, two steps. Rewrite the hypothesis with Complex.ofReal_add so the left-hand side becomes the cast of the real sum $e_0 + e_1$. Then apply Complex.ofReal_injective to cancel the embedding and obtain $e_0 + e_1 = t$ in $\mathbb{R}$. No case splits and no spectral theory beyond the cast.
why it matters
Immediate parent is reducedDensity_eigenvalues_sum_eq_one, which asserts that the two eigenvalues of the reduced density of a Frobenius-normalized pure two-qubit amplitude sum to 1. That identity is required so the spectrum can be written $(1 \pm \sqrt{1 - C^2})/2$ and the entanglement entropy identified with binary entropy $h((1 + \sqrt{1 - C^2})/2)$. The module then composes this with the algebraic core (binary entropy strictly positive on $(0,1)$) to close Track 2.B: $C > 0$ implies $E_{\mathrm{VN}}(\rho_1) > 0$. The lemma itself is pure analysis; it carries none of the RS forcing chain (T5–T8) but keeps the eigenvalue bookkeeping honest inside the quantum track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.