log2_two
plain-language theorem explainer
The lemma establishes that the base-2 logarithm of 2 equals 1. Researchers deriving Shannon entropy bounds from J-cost minimization in Recognition Science cite this identity when anchoring calculations for binary messages or fair-coin entropy. The proof is a direct term application of the general log_b b = 1 property, with the base condition discharged by norm_num.
Claim. $log_2 2 = 1$
background
In the Information.Compression module the function log2 is introduced as the real logarithm base 2 via Real.logb 2 x. This definition supports the module's target of deriving compression limits from J-cost, where entropy H(X) equals minus the sum of p(x) log2 p(x) and the minimum J-cost for faithful representation coincides with the entropy bound.
proof idea
The proof is a one-line term wrapper that applies Real.logb_self_eq_one to the specific base 2. The side condition 1 < 2 is discharged inline by norm_num.
why it matters
This identity anchors the entropy calculations that feed the source coding theorem and fair-coin entropy results in the same module. It thereby supports the Recognition Science claim that compression equals J-cost minimization and that the entropy limit is the minimum J-cost for lossless representation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.