entanglementEntropy
plain-language theorem explainer
Entanglement entropy for subsystem A is defined via the von Neumann formula applied to the eigenvalues of the reduced density matrix. Researchers deriving the Ryu-Takayanagi area law from Recognition Science ledger projections would cite this when linking information measures to boundary geometry. The definition directly transcribes S = -sum lambda log lambda with a conditional that drops zero-eigenvalue terms.
Claim. For a bipartite system with subsystems A and B, the entanglement entropy of A is $S_A = -Tr(ρ_A log ρ_A) = -∑_i λ_i log λ_i$, where the λ_i are the eigenvalues of the reduced density matrix ρ_A on A, subject to ∑ λ_i = 1 and λ_i ≥ 0 for all i.
background
The module QG-008 targets the Ryu-Takayanagi formula S_A = Area(γ_A)/(4 G_N ℏ) by viewing ledger entries as fundamentally two-dimensional surfaces whose shared count across a boundary yields area-proportional entropy. A BipartiteSystem is a structure recording Hilbert-space dimensions dim_A > 1 and dim_B > 1 for the two subsystems. The supplied eigenvalues represent the spectrum of the reduced density matrix on A after tracing out B.
proof idea
Direct definition that evaluates the standard von Neumann entropy expression. It sums λ_i log λ_i over the positive eigenvalues (via an if-then guard) and negates the result, returning zero for any vanishing eigenvalue.
why it matters
Supplies the concrete information measure required by the downstream non-negativity theorem and by the module's goal of recovering the Ryu-Takayanagi area law from the two-dimensional character of ledger entries. It sits inside the Recognition Science derivation of holographic bounds from the eight-tick octave and defect counting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.