binaryEntropy_zero_left

This module closes Track 2.B: the chain from Wootters concurrence of a pure two-qubit amplitude matrix to strict positivity of von Neumann entanglement entropy. The algebraic core needs that binary entropy $h$ is strictly positive on $(0,1)$ and zero at the endpoints $0$ and $1$, so that $E_{\mathrm{VN}}(\rho_1) = h\bigl((1+\sqrt{1-C^2})/2\bigr)$ is positive precisely when concurrence $C>0$.

The binary entropy is defined by the usual formula $h(p)=-p\log p-(1-p)\log(1-p)$. Mathlib sets $\mathrm{Real.log},0=0$, so the expression evaluates continuously at the endpoints without a separate piecewise clause. The companion fact $h(1)=0$ sits immediately below this theorem.

One-line tactic proof: unfold the definition of binary entropy, then simp with Real.log_one. Substituting $p=0$ yields $-0\cdot\log 0-(1-0)\cdot\log 1$. The first summand is zero; the second is $-\log 1=0$.

Endpoint vanishing of $h$ is the boundary half of the algebraic core quoted in the module doc: for $C\in(0,1]$, the argument $(1+\sqrt{1-C^2})/2$ lies in $(1/2,1]$, and $h$ is zero only at $0,1$ while positive on $(0,1)$. Together with the reduced-density eigenvalue identification $\lambda_\pm=(1\pm\sqrt{1-C^2})/2$, this forces $E_{\mathrm{VN}}(\rho_1)>0$ exactly when the pure two-qubit state is entangled.

No downstream Lean users are recorded yet; the fact is infrastructure for the entropy-positivity theorem that closes Track 2.B. It carries no new Recognition Science assumptions (structural theorem only).