inner_radius_lt_one_of_pos_concurrence

Track 2.B links pure two-qubit Wootters concurrence to strict positivity of von Neumann entanglement entropy. For a normalized amplitude matrix $A$, concurrence is $C(A) := 2|\det A|$. The reduced density matrix on one qubit has eigenvalues $(1 \pm \sqrt{1-C^2})/2$, so the entanglement entropy equals the binary entropy $h(p)$ of either eigenvalue.

Binary entropy $h(p) = -p\log p - (1-p)\log(1-p)$ vanishes at the endpoints $p\in{0,1}$ and is strictly positive on $(0,1)$. Thus any argument that $C>0$ forces $E_{\mathrm{VN}}>0$ needs the larger eigenvalue (the "inner radius") to lie strictly below 1. The companion lower bound $\ge 1/2$ is handled separately; together they place the radius in $[1/2,1)$.

This lemma isolates only the strict upper bound under the standing hypotheses $0<C\le 1$ that arise once concurrence is positive and at most one (the pure-state maximum).

Goal reduces to $\sqrt{1-C^2}<1$. From $C>0$, positivity gives $C^2>0$, so $1-C^2<1$. Nonnegativity of the radicand uses $C\le 1$ via $C^2\le 1^2$ (from sq_le_sq') and rearranging. Then Real.sqrt_lt_sqrt yields $\sqrt{1-C^2}<\sqrt{1}=1$. One linarith step lifts that to $(1+\sqrt{\cdot})/2<1$. Pure real-arithmetic tactics; no quantum lemmas.

Feeds directly into inner_radius_in_unit_interval_of_pos_concurrence, which packages the full interval membership $[1/2,1)$ needed before binary entropy can be applied. That interval lemma is the algebraic half of Track 2.B: once the reduced-state eigenvalues sit in $(0,1)$, $h$ is strictly positive, so $C>0$ implies $E_{\mathrm{VN}}(\rho_1)>0$.

Module status is structural theorem with no new Recognition Science assumptions: the chain is pure quantum information (concurrence $\to$ Schmidt spectrum $\to$ binary entropy). The strict upper bound is the piece entropy positivity actually needs; equality at $C=0$ would collapse $h$ to zero and break the entanglement witness. Closes the algebraic core cited in the module plan before composition with the reduced-density target.