binaryEntropy
plain-language theorem explainer
Binary entropy h(p) = −p log p − (1−p) log(1−p) on the reals, with Mathlib’s log 0 = 0 giving the continuous extension h(0) = h(1) = 0. Anyone proving von Neumann entanglement entropy for pure two-qubit states cites it as the scalar function of the reduced eigenvalues. The body is a one-line closed-form definition.
Claim. Define the binary entropy $h:\mathbb{R}\to\mathbb{R}$ by $h(p)=-p\log p-(1-p)\log(1-p)$. With the convention $\log 0=0$, one has $h(0)=h(1)=0$ by direct evaluation.
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 a reduced qubit. Concurrence is $C(A):=2|\det A|$. The reduced density matrix $\rho_1=\mathrm{tr}_2|\psi\rangle\langle\psi|$ has eigenvalues $(1\pm\sqrt{1-C^2})/2$, so the entanglement entropy is binary entropy of either eigenvalue.
Binary entropy is the classical Shannon entropy of a Bernoulli($p$) bit. It is symmetric about $p=1/2$, vanishes at the endpoints $0$ and $1$, and is strictly positive on $(0,1)$. Those three facts, together with the algebraic placement of the inner radius $(1+\sqrt{1-C^2})/2$ in $(1/2,1]$ for $C\in(0,1]$, close the entropy-positivity chain without new Recognition Science assumptions.
proof idea
Pure definition: the right-hand side is written directly as $-p\cdot\mathrm{Real.log},p-(1-p)\cdot\mathrm{Real.log}(1-p)$. No lemmas are applied. Endpoint values $h(0)=h(1)=0$ follow later from Mathlib’s $\mathrm{Real.log},0=0$ and $\mathrm{Real.log},1=0$, proved in the sibling zero lemmas by unfolding and simplifying.
why it matters
This is the scalar workhorse of the algebraic core of Track 2.B. Downstream results use it to prove symmetry about $1/2$, vanishing at endpoints, strict positivity on $(0,1)$, and positivity of $h$ at the concurrence inner radius for $0<C\le 1$. Those feed the identity equating pure two-qubit entanglement entropy to binary entropy of the inner radius, and the certificate PureTwoQubitConcurrenceEntropyCert. The module status is structural theorem: Track 2.B closed with no proof holes and no new RS assumptions. The definition itself is classical; its place in the framework is to turn the eigenvalue formula $(1\pm\sqrt{1-C^2})/2$ into a strictly positive entropy whenever concurrence is positive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.