fairCoinEntropy
plain-language theorem explainer
The definition computes Shannon entropy for a fair coin flip using the standard formula with equal probabilities of one half. Information theorists cite it as the baseline case establishing the one-bit lower bound on lossless compression for unbiased binary symbols. Recognition Science researchers use it to illustrate minimum J-cost for faithful representation. The definition is a direct algebraic expression that applies the log base two function to each term.
Claim. $H = -0.5 log_2(0.5) - 0.5 log_2(0.5)$
background
Shannon entropy for a discrete source is the negative sum over probabilities times log base two of each probability. In the Recognition Science setting this quantity equals the minimum J-cost required for any faithful representation of the message. The module derives compression limits directly from J-cost minimization, with the fair-coin case serving as the simplest illustration that no scheme can compress below the entropy value. The upstream log2 definition supplies the base-two logarithm satisfying log2(2) = 1.
proof idea
The declaration is a direct definition that substitutes the two equal probabilities into the entropy formula and applies the log2 operation to each term.
why it matters
This definition supplies the concrete base case for the theorem that proves fair-coin entropy equals exactly one bit. That result anchors the broader claim that entropy is the J-cost minimum in the source-coding limit derived from Recognition Science. It directly supports the module's statement that compressed information has lower J-cost and that no lossless scheme can beat the entropy bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.