binaryEntropy_inner_radius_pos_of_concurrence
plain-language theorem explainer
For concurrence C in (0,1], the binary entropy of the larger reduced eigenvalue (1+√(1−C²))/2 is strictly positive. Quantum-information and RS Track 2.B arguments cite this as the algebraic half of entropy positivity from concurrence. The proof places that radius in (1/2,1) then applies open-interval positivity of binary entropy.
Claim. Let $C\in\mathbb{R}$ satisfy $0<C\le 1$. Write $p=(1+\sqrt{1-C^2})/2$ for the larger eigenvalue of a pure two-qubit reduced density matrix at concurrence $C$. Then the binary entropy $h(p)=-p\log p-(1-p)\log(1-p)$ obeys $h(p)>0$.
background
Track 2.B links Wootters concurrence of a pure two-qubit amplitude matrix to strict positivity of von Neumann entanglement entropy. For a normalized $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$, concurrence is $C(A)=2|\det A|$. The reduced state $\rho_1=\mathrm{tr}2|\psi\rangle\langle\psi|$ has eigenvalues $(1\pm\sqrt{1-C^2})/2$, so $E{\mathrm{VN}}(\rho_1)=h((1+\sqrt{1-C^2})/2)$ by symmetry of binary entropy about $1/2$.
Binary entropy $h$ vanishes only at the endpoints $0$ and $1$ and is strictly positive on $(0,1)$. The companion geometric fact is that for $C\in(0,1]$ the inner radius $p=(1+\sqrt{1-C^2})/2$ lies in $(1/2,1)$: at least $1/2$, and strictly less than $1$ whenever $C>0$. This lemma composes those two facts and is purely algebraic; it does not yet invoke a concrete von Neumann functional.
proof idea
Term-mode composition of two prior facts. First unpack inner_radius_in_unit_interval_of_pos_concurrence at the given bounds on $C$, obtaining lower and upper inequalities for $p=(1+\sqrt{1-C^2})/2$ (in particular $p>1/2$ and $p<1$). Then apply binaryEntropy_pos_of_open_unit_interval, which asserts $h>0$ on the open unit interval: discharge $0<p$ by linarith from the lower bound, and feed the strict upper bound $p<1$ directly. No expansion of $h$ or square roots is needed.
why it matters
This is the algebraic core of Track 2.B in the pure two-qubit entropy–concurrence module (status: structural theorem, no new RS assumptions). It feeds the conditional closure pure_two_qubit_entropy_positive_of_concurrence_positive, which, given any von Neumann functional satisfying the reduced-density-matrix sub-target, upgrades $C>0$ to $E_{\mathrm{VN}}(\rho_1)>0$.
In the module plan, the full identity $E_{\mathrm{VN}}(\rho_1)=h((1+\sqrt{1-C^2})/2)$ splits into (i) this positivity-of-$h$ on the inner radius and (ii) the spectral identification of reduced eigenvalues with that radius. Strict positivity of concurrence is already tied to nonzero determinant (the algebraic entanglement witness). The lemma therefore closes the pure-state half of the entropy-from-concurrence chain without touching mixed-state Wootters machinery or continuum field content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.