log2
plain-language theorem explainer
Definition log2 supplies the base-two logarithm on the reals via the standard library primitive. Workers deriving entropy bounds or Morton octant depths in geometric SAT encodings cite it to convert between real and natural-log forms. The definition is a direct one-line wrapper around Real.logb.
Claim. The function $xmapsto log_2 x$ for $x in mathbb{R}$, realized as the logarithm base 2.
background
The module INFO-003 derives data-compression limits from J-cost. Shannon entropy appears as $H(X)=-sum p(x)log_2 p(x)$, and the source-coding theorem states that average code length is at least this entropy. In the Recognition Science setting, entropy equals the minimum J-cost of a faithful representation, so compression is J-cost minimization. The definition imports from Mathlib and from the sibling ShannonEntropy module; no upstream lemmas are required.
proof idea
One-line wrapper that applies Real.logb 2.
why it matters
The definition is invoked by inOctant, maxOctantLevel, log2_succ_le and succ_le_two_pow inside GeoFamily to bound subdivision levels, and by log25_eq_5 and QuantumMolecularBoundCert to certify concrete bit counts. It therefore supplies the concrete logarithm needed for the J-cost lower bound on lossless compression stated in the module doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.