{"fqn":"KLean.Atoms.Info.EntropyAtHalfIsLogTwo.entropy_at_half","short":"entropy_at_half","module":"KLean.Atoms.Info.EntropyAtHalfIsLogTwo","path":"KLean/Atoms/Info/EntropyAtHalfIsLogTwo.lean","claim":"At p = 1/2, binary entropy = ln 2","verified":true,"axiom_level":"kernel-standard","olean_sha256":"710ae64dc9e66f5b46b28c71415c172154220ba15726a31873b15809d6e431a4","quarantined":false,"statement":"theorem entropy_at_half : binaryEntropy (1 / 2) = Real.log 2","topics":["information"],"refs":[],"depends_on":["KLean.Atoms.Info.EntropySurpriseDefs"],"used_by":["KLean.Atoms.Info.EntropyMaxAtHalf"],"compute":"/api/v1/klean/compute/shannon_entropy","seal":{"receipt_id":"d017cc7dffff572a7adc3c1d","digest":"ff9469cecfb2bfdf74174682d2499bf3dcc86c0d62e7197d6640fab11f61bd22","sealed_at":"2026-08-10T03:30:24.740384+00:00","time_source":"roughtime_chain"},"commit":"4b8413e1b8"}