binaryEntropy_zero_right
plain-language theorem explainer
Binary entropy vanishes at the right endpoint: h(1) = 0. Anyone closing the algebraic core of the pure two-qubit entanglement-entropy identity cites this, since von Neumann entropy is written as binary entropy of the concurrence eigenvalues and must be zero when the state is product. The proof unfolds the definition and simplifies with log 1 = 0.
Claim. The binary entropy function satisfies $h(1) = 0$, where $h(p) = -p \log p - (1-p)\log(1-p)$ (with the continuous extension $h(0) = h(1) = 0$ at the endpoints).
background
Track 2.B of the master plan links 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)$ vanishes exactly when $C=0$.
Binary entropy is defined by $h(p) = -p\log p - (1-p)\log(1-p)$. Mathlib sets $\log 0 = 0$, so the same formula evaluates to zero at both endpoints without a separate case split. The companion fact $h(0)=0$ sits immediately above this theorem in the module.
Concurrence for a normalized pure two-qubit amplitude matrix $A$ is $C(A) := 2|\det A|$. The reduced density matrix has eigenvalues $(1\pm\sqrt{1-C^2})/2$, and binary entropy's symmetry about $1/2$ equates the two eigenvalue presentations.
proof idea
One-line tactic proof. Unfold the definition of binary entropy to $-1\cdot\log 1 - (1-1)\cdot\log(1-1)$. Then simp with Real.log_one (and the arithmetic of the zero coefficient on the second term) reduces both summands to zero.
why it matters
Closes the right-endpoint half of the algebraic core stated in the module doc: $h$ vanishes at $0$ and $1$, and is strictly positive on $(0,1)$. Together with the left-endpoint lemma and positivity on the open interval, this lets the full reduction $E_{\mathrm{VN}}(\rho_1) = h\bigl((1+\sqrt{1-C^2})/2\bigr)$ conclude that entanglement entropy is zero precisely when concurrence vanishes (product states) and positive when $C\in(0,1]$.
The module is marked STRUCTURAL THEOREM: Track 2.B closed, no proof holes, no new Recognition Science assumptions. No downstream consumers are wired yet in the graph; the lemma is infrastructure for the entropy-positivity composition with PureTwoQubitReducedEntropyTarget. It does not touch the forcing chain (T0–T8), RCL, or the mass ladder; it is pure quantum-information algebra inside the RS mirror.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.