binaryEntropy_pos_of_open_unit_interval
plain-language theorem explainer
Binary entropy is strictly positive on the open unit interval: if 0 < p < 1 then h(p) = −p log p − (1−p) log(1−p) > 0. Cited by anyone closing the algebraic core of pure two-qubit entanglement entropy from Wootters concurrence. The proof unfolds the definition, uses Real.log_neg on both arguments, and finishes by linear arithmetic on one strictly positive term and one nonnegative term.
Claim. For every real $p$ with $0 < p < 1$, the binary entropy $h(p) = -p\log p - (1-p)\log(1-p)$ satisfies $h(p) > 0$.
background
Track 2.B of the pure two-qubit module links Wootters concurrence of a normalized amplitude matrix $A$ to strict positivity of the von Neumann entanglement entropy of the reduced state. The algebraic core needs two facts: for concurrence $C \in (0,1]$, the inner radius $(1+\sqrt{1-C^2})/2$ lies in $(1/2,1)$, and binary entropy is strictly positive on $(0,1)$ and zero at the endpoints.
Binary entropy is the Shannon entropy of a Bernoulli trial: $h(p)=-p\log p-(1-p)\log(1-p)$. On $(0,1)$ both logs are negative, so each summand $-x\log x$ is nonnegative; the claim is that their sum is strictly positive. The module already treats concurrence $C(A):=2|\det A|$ and the reduced-density eigenvalues $(1\pm\sqrt{1-C^2})/2$, so $E_{\mathrm{VN}}(\rho_1)=h$ of either eigenvalue by symmetry of $h$ about $1/2$.
proof idea
Unfold binaryEntropy. From $0<p<1$ get $0<1-p$ by linarith. Apply Real.log_neg to obtain $\log p<0$, then nlinarith yields the strict inequality $0<-p\log p$. For the second summand, case-split on whether $1-p=1$: if equal, $\log 1=0$; otherwise $\log(1-p)<0$ again by Real.log_neg, so in either case $\log(1-p)\le 0$. Another nlinarith gives $0\le-(1-p)\log(1-p)$. Add the two inequalities with linarith.
why it matters
This is the positivity half of the algebraic core that closes Track 2.B (structural theorem, no new RS assumptions, no proof holes). Downstream, binaryEntropy_inner_radius_pos_of_concurrence composes it with the inner-radius interval lemma: for $0<C\le 1$, $h((1+\sqrt{1-C^2})/2)>0$. That fact feeds the certificate pureTwoQubitConcurrenceEntropyCert, which packages concurrence nonnegativity, the det-zero characterization, reduced-trace and reduced-det identities into the full concurrence-to-entropy chain.
In the broader Recognition picture the result is classical information theory, not a forcing-chain step (T5–T8). It supplies the missing strict inequality that turns nonzero concurrence (equivalently nonzero det of the amplitude matrix) into strictly positive entanglement entropy for pure two-qubit states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.