log2_two
plain-language theorem explainer
The lemma records that log base 2 of 2 equals 1. Researchers deriving entropy bounds inside the J-cost formulation of Shannon coding would invoke this identity when normalizing probabilities. The proof is a one-line application of the general logb self-equality lemma together with a numerical check that the base exceeds 1.
Claim. $log_2 2 = 1$
background
The module INFO-003 derives fundamental limits on lossless compression from J-cost, stating that average code length is at least the Shannon entropy H(X) = -sum p(x) log2 p(x) and that compression equals J-cost minimization. The local definition log2 (x : R) := Real.logb 2 x supplies the base-2 logarithm used throughout the entropy calculations. The upstream result is exactly this definition of log2 together with its statement that it computes the logarithm base 2.
proof idea
One-line wrapper that applies Real.logb_self_eq_one to the definition of log2, discharging the side condition 1 < 2 by norm_num.
why it matters
The identity is the elementary normalization step required before any entropy or J-cost calculation in the compression module can proceed. It sits inside the Shannon source-coding development that equates minimum code length with minimum J-cost. No downstream theorems are recorded yet, so its role remains preparatory for later sourceEntropy and compression_is_jcost_minimization results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.