maximalEntanglement_pos
plain-language theorem explainer
The theorem establishes positivity of the maximal entanglement logarithm in the RS framework. Physicists deriving quantum entanglement from J-cost would cite it when confirming that the D=3 case yields positive entropy. The proof is a one-line wrapper applying the mul_pos lemma to the factors 3 and log 2.
Claim. $0 < 3 log 2$
background
The module identifies entanglement entropy with the J-cost between subsystems in the recognition basis. For a maximally entangled state at three spatial dimensions, S equals log(2^D) which is 3 log 2. This builds directly on the upstream definition of maximalEntanglementLog as 3 times the real logarithm of 2, encoding the D equals 3 result from the forcing chain. The module defines five canonical entanglement structures with costs derived from the recognition composition law.
proof idea
The proof is a one-line wrapper applying the mul_pos lemma from the standard library to the product of 3 and the real logarithm of 2. Norm_num confirms both 3 and log 2 are positive.
why it matters
This positivity statement is referenced inside the entanglementEntropyCert definition to complete the certification of the five entanglement structures. It supports the RS claim that maximal entanglement entropy is positive and scales with spatial dimension D=3 in the eight-tick octave. The result anchors the derivation of entanglement entropy from the J-cost without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.