concurrence_le_one_of_normalized
plain-language theorem explainer
For a pure two-qubit amplitude matrix with unit Frobenius norm, the Wootters concurrence is at most 1. Anyone citing the pure-state bound C ∈ [0,1] or the entropy formula E = h((1+√(1−C²))/2) needs this. The proof is a short nonlinear arithmetic step from nonnegativity and the already-proved C² ≤ 1 bound.
Claim. Let $A$ be a $2\times 2$ complex matrix with Frobenius norm squared equal to $1$, i.e. $\sum_{i,j}|A_{ij}|^2 = 1$. Then the Wootters concurrence $C(A) := 2\|\det A\|$ satisfies $C(A) \le 1$.
background
Track 2.B of the Recognition Science quantum layer links pure two-qubit entanglement to von Neumann entropy positivity. For a pure state $|\psi\rangle = \sum_{ij} A_{ij}|ij\rangle$, the Wootters concurrence collapses to $C(A) = 2|\det A|$. Normalization is expressed as unit Frobenius squared norm of the amplitude matrix $A$.
The module already records $C(A)\ge 0$ and the squared bound $C(A)^2\le 1$ under the same normalization. The reduced density matrix $\rho_1 = \mathrm{tr}2|\psi\rangle\langle\psi|$ then has eigenvalues $(1\pm\sqrt{1-C^2})/2$, so the binary-entropy formula for $E{\mathrm{VN}}(\rho_1)$ is well-defined only when $C\in[0,1]$.
This lemma supplies the missing upper endpoint: under unit Frobenius norm, $C\le 1$.
proof idea
Term-mode nonlinear arithmetic. From concurrence_nonneg one has $0\le C(A)$, so $C(A)^2$ is a square of a nonnegative real. From concurrence_sq_le_one_of_normalized one has $C(A)^2\le 1$ under the Frobenius hypothesis. nlinarith closes $C(A)\le 1$ from those two facts together with nonnegativity of the square.
why it matters
Closes the interval $C\in[0,1]$ required by 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\le 1$. Downstream, pureTwoQubitReducedEntropyTarget_holds invokes it to discharge the reduced-density sub-target, and pure_two_qubit_entropy_positive_unconditional uses that target for unconditional entropy positivity from $C>0$. The private spectral lemma reducedDensity_eigenvalues_eq_lambda_or_swap likewise assumes the normalized setting where $C\le 1$. No new RS assumptions; pure structural quantum information inside the already-closed Track 2.B chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.