entanglement_entropy_nonneg
plain-language theorem explainer
Entanglement entropy for a bipartite quantum system is non-negative when evaluated from normalized non-negative eigenvalues of the reduced density matrix on subsystem A. Researchers deriving the Ryu-Takayanagi formula within Recognition Science cite this to confirm the entropy functional is well-defined before linking it to boundary area. The proof unfolds the definition, reduces via sum non-positivity, and handles each summand by case analysis on eigenvalue positivity together with the normalization constraint.
Claim. Let $S$ be a bipartite quantum system with subsystem dimensions $d_A>1$ and $d_B>1$. For eigenvalues $p_i$ ($i=1$ to $d_A$) satisfying $p_i>0$ or $p_i=0$, with $p_i=0$ by convention when the term vanishes, $p_i$ non-negative, and summing to 1, the entanglement entropy $S_A = -Tr(p_A log p_A) = -sum_i p_i log p_i$ (zero when $p_i=0$) satisfies $S_A >=0$.
background
The module QG-008 derives the Ryu-Takayanagi formula from Recognition Science ledger structure: ledger entries are 2D, entanglement counts shared entries across a boundary, and counting yields area proportionality. A BipartiteSystem is the structure with Hilbert-space dimensions dim_A and dim_B both strictly greater than 1. The entanglementEntropy function is the von Neumann entropy of the reduced density matrix on A, expressed as the negative sum over positive eigenvalues of lambda times log lambda. Upstream entropy definitions treat entropy as total defect (zero defect yields minimum entropy) or as k_B (log Z + beta average energy) in thermodynamic modules.
proof idea
Unfold the definition of entanglementEntropy. Apply simp on neg_nonneg to flip the sign. Invoke Finset.sum_nonpos to reduce the claim to each summand being non-positive. For each index i perform case analysis on whether the eigenvalue exceeds zero: when positive, invoke single_le_sum plus normalization to bound the eigenvalue by 1, apply Real.log_nonpos to obtain a non-positive logarithm, then multiply to conclude the product is non-positive; when zero the term vanishes by the if-then-else.
why it matters
The result supplies the basic non-negativity property required inside the QG-008 derivation of the Ryu-Takayanagi formula from ledger projections in Recognition Science. It precedes the maximum-entropy statement (log dim_A) and the area-law connection S_A proportional to boundary area over 4 G_N hbar. The declaration sits in the module whose target is the PRL paper deriving the RT formula from RS; it closes a consistency check before geometric interpretation via minimal surfaces and defect counting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.