fair_coin_one_bit
plain-language theorem explainer
The theorem establishes that the Shannon entropy of a fair coin equals exactly one bit. Information theorists applying Recognition Science to compression limits would cite this as the baseline case confirming the entropy bound for unbiased binary sources. The short term-mode proof reduces the entropy expression by unfolding its definition, normalizing the probability, rewriting the logarithm via a dedicated lemma, and closing with ring arithmetic.
Claim. For a binary random variable with equal probabilities $1/2$ for each outcome, the Shannon entropy $H = -p_0 log_2 p_0 - p_1 log_2 p_1$ equals 1.
background
The Information.Compression module derives fundamental limits on data compression from J-cost, where entropy is the minimum J-cost for faithful representation and compression equals J-cost minimization. Shannon entropy is given by $H(X) = -∑ p(x) log₂ p(x)$, matching the source coding theorem statement that average code length is at least this value. This setting rests on the shifted cost function H(x) = J(x) + 1, which converts the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y).
proof idea
The proof is a direct term-mode reduction. It unfolds the fair-coin entropy definition, normalizes 0.5 to 1/2 via norm_num, rewrites the logarithm using the log2_half lemma, and finishes with the ring tactic to obtain equality to 1.
why it matters
This result supplies the canonical base case for the source-coding limit in the Recognition Science treatment of information as J-cost. It confirms that a fair coin cannot be losslessly compressed below one bit per symbol, aligning with the module's claim that entropy equals minimum J-cost. The declaration sits inside the INFO-003 derivation of compression bounds and indirectly supports the framework's view of organized information lowering J-cost along the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.