binaryEntropy_symm

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. For a normalized pure state with amplitude matrix $A$, concurrence is $C(A) := 2|\det A|$. The reduced density $\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 real function $h(p) = -p\log p - (1-p)\log(1-p)$. The module records that $h$ vanishes at the endpoints $0,1$ and is strictly positive on $(0,1)$. Symmetry about $p=1/2$ is the algebraic fact that lets one write $E_{\mathrm{VN}}(\rho_1) = h((1-\sqrt{1-C^2})/2) = h((1+\sqrt{1-C^2})/2)$ without choosing a branch.

One-line algebraic identity. Unfold the definition of binary entropy, then apply ring_nf. After expansion, the two summands swap under $p \mapsto 1-p$, so the expressions are identical as polynomials in $p$ and the logs. No analytic lemmas or domain side-conditions are required for the equality itself.

Track 2.B's reduced-density step needs both eigenvalue forms of $\rho_1$ to yield the same entropy. The module doc states explicitly that $E_{\mathrm{VN}}(\rho_1) = h((1-\sqrt{1-C^2})/2) = h((1+\sqrt{1-C^2})/2)$ because binary entropy is symmetric about $p=1/2$. This theorem is that symmetry lemma.

It sits in the algebraic core of the concurrence-to-entropy reduction: once $C\in(0,1]$ forces the larger eigenvalue into $(1/2,1)$, positivity of $h$ on $(0,1)$ gives strict positivity of entanglement entropy. No new Recognition Science assumptions enter; the result is pure real analysis supporting the pure two-qubit structural theorem. Downstream graph edges are empty here, but the identity is the bridge named in the module composition plan.