concurrence_sq_le_one_of_normalized
plain-language theorem explainer
For a normalized pure two-qubit amplitude matrix, the square of the Wootters concurrence is at most one. Anyone bounding pure bipartite entanglement or feeding the entropy-positivity chain would cite this bound. The argument is a short nlinarith on the reduced-density eigenvalues: their sum is one, their product is C²/4, and (λ₀−λ₁)²≥0 forces C²≤1.
Claim. Let $A$ be a $2\times 2$ complex amplitude matrix with Frobenius norm squared equal to $1$. Writing $C(A)=2|\det A|$ for the Wootters concurrence, one has $C(A)^2\le 1$.
background
This module closes Track 2.B: the chain from Wootters concurrence of a pure two-qubit amplitude matrix to strict positivity of von Neumann entanglement entropy. For a pure state $|\psi\rangle=\sum_{ij}A_{ij}|ij\rangle$, the concurrence is the pure-state simplification $C(A)=2|\det A|$. Normalization is algebraic: the Frobenius norm-squared $\sum_{ij}|A_{ij}|^2$ equals one.
The first-qubit reduced density $\rho_1=\mathrm{tr}2|\psi\rangle\langle\psi|$ is Hermitian. Under normalization its eigenvalues sum to one. A sibling identity equates their product to $C(A)^2/4$, matching the classical formula $\lambda\pm=(1\pm\sqrt{1-C^2})/2$.
Those two spectral facts are the only inputs needed for the quadratic bound on $C$.
proof idea
Term-mode proof. Bind the Hermitian structure of the reduced density via reducedDensity_isHermitian. Invoke reducedDensity_eigenvalues_sum_eq_one (uses the Frobenius-normalization hypothesis) and reducedDensity_eigenvalues_prod_eq_concurrence_sq_div_four. Feed into nlinarith the nonnegativity of $(\lambda_0-\lambda_1)^2$ together with the sum and product identities. Expanding $(\lambda_0-\lambda_1)^2\ge 0$ yields $(\lambda_0+\lambda_1)^2-4\lambda_0\lambda_1\ge 0$, hence $1-C^2\ge 0$.
why it matters
Immediate parent is concurrence_le_one_of_normalized, which lifts the squared bound to $C\le 1$ by nonnegativity of concurrence. That unit upper bound is required for the algebraic core of Track 2.B: the map $C\mapsto(1+\sqrt{1-C^2})/2$ lands in $(1/2,1]$ only when $C\in(0,1]$, so binary entropy is strictly positive precisely when concurrence is positive. The module status is structural theorem, no new RS assumptions; the result is pure linear-algebraic support for the entropy-positivity discharge, not a forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.