maximalEntanglementLog
plain-language theorem explainer
This definition supplies the numerical value of maximal entanglement entropy in three spatial dimensions as three times the logarithm of two. Quantum information researchers working within Recognition Science would cite it when bounding bipartite entanglement or certifying entropy structures. The definition is a direct transcription of log(2^D) with D fixed at three.
Claim. The maximal entanglement entropy satisfies $S = 3 log 2$, which equals $log(2^D)$ at $D=3$.
background
The module treats entanglement entropy as the J-cost of the reduced density matrix for a bipartite system, with S = J(ρ_A). Product states give Jcost(1) = 0 while entangled states satisfy positive Jcost for r ≠ 1. The maximal case uses dimension d = 2^D, so S = log(d) = D log(2) when D = 3.
proof idea
The definition is a direct one-line assignment of the expression 3 * Real.log 2.
why it matters
This definition anchors the max_entanglement_pos field inside the EntanglementEntropyCert structure, which also records five entanglement structures and Jcost positivity. It realizes the module prediction S = log(d) for d = 8 at D = 3, consistent with the framework result fixing three spatial dimensions. The downstream theorem maximalEntanglement_pos invokes it to obtain strict positivity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.