inner_radius_in_unit_interval_of_pos_concurrence
plain-language theorem explainer
For concurrence C in (0,1], the Schmidt eigenvalue (1+√(1−C²))/2 sits in [1/2,1). Equality to 1/2 holds only at C=1; the upper bound is strict whenever C>0. Cited by the binary-entropy positivity step that closes the pure two-qubit entropy–concurrence chain. Proof splits into a lower-bound linarith from nonnegativity of the square root and a one-line call to the strict upper-bound lemma.
Claim. Let $C\in\mathbb{R}$ satisfy $0<C\le 1$. Then $$\frac12 \le \frac{1+\sqrt{1-C^2}}{2} < 1.$$ The lower bound is non-strict (equality at $C=1$); the upper bound is strict for every positive $C$.
background
Track 2.B of the pure two-qubit module links Wootters concurrence of a normalized amplitude matrix $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$ to strict positivity of the von Neumann entanglement entropy of the reduced state. Concurrence is $C(A):=2|\det A|$, so $C\in[0,1]$ on normalized pure states, with $C>0$ exactly when $\det A\ne 0$.
For a pure bipartite state the reduced density matrix $\rho_1=\mathrm{tr}_2|\psi\rangle\langle\psi|$ has eigenvalues $(1\pm\sqrt{1-C^2})/2$. Binary entropy is symmetric about $1/2$, so the entanglement entropy equals $h\bigl((1+\sqrt{1-C^2})/2\bigr)$. The algebraic core therefore needs this “inner radius” inside the open unit interval where $h$ is strictly positive.
The module already records nonnegativity of concurrence, the equivalence $C=0\Leftrightarrow\det A=0$, and the identity $\det\rho_1=C^2/4$. The present lemma is the interval membership step that feeds the binary-entropy positivity argument.
proof idea
Split the conjunction with refine. The strict upper bound is discharged by the sibling lemma inner_radius_lt_one_of_pos_concurrence (already proved for $0<C\le 1$).
For the lower bound, first obtain $C^2\le 1$ from $0<C\le 1$ via sq_le_sq' and linarith, hence $1-C^2\ge 0$. Nonnegativity of the real square root then gives $\sqrt{1-C^2}\ge 0$, so $(1+\sqrt{1-C^2})/2\ge 1/2$ by a final linarith. No external analytic machinery is required beyond Mathlib’s square-root API.
why it matters
This is the interval gate in the algebraic core of Track 2.B. Downstream, binaryEntropy_inner_radius_pos_of_concurrence unpacks the two bounds and applies binary-entropy positivity on the open unit interval, yielding $h\bigl((1+\sqrt{1-C^2})/2\bigr)>0$ whenever $0<C\le 1$. That positivity is packaged into the certificate pureTwoQubitConcurrenceEntropyCert, which closes the structural theorem: nonzero concurrence implies strictly positive entanglement entropy for pure two-qubit states.
The module status is “STRUCTURAL THEOREM (Track 2.B closed; no proof holes, no new RS assumptions).” The result is classical quantum information (Wootters concurrence, Schmidt eigenvalues) rather than a forcing-chain step, but it supplies the entropy witness that Recognition Science uses when linking algebraic entanglement (nonzero determinant of the amplitude matrix) to thermodynamic content of the reduced state. No open scaffolding remains on this edge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.