log2
plain-language theorem explainer
This definition supplies the base-2 logarithm on the reals via the standard logb operation. Researchers deriving entropy bounds or octant subdivision counts in the Recognition Science framework cite it when expressing Shannon entropy or Morton-index levels. It is realized as a direct noncomputable wrapper around Mathlib's Real.logb.
Claim. The base-two logarithm is defined by $log_2(x) = logb(2, x)$ for real $x$.
background
The Information.Compression module derives data-compression limits from J-cost minimization under the Recognition Composition Law. Shannon entropy appears as $H(X) = -sum p(x) log_2 p(x)$, and the module equates this entropy to the minimum J-cost of a faithful representation; compression is therefore J-cost reduction. The log2 definition supplies the explicit base-2 measure required by these statements and by the sibling definitions fairCoinEntropy and biasedCoinEntropy.
proof idea
The definition is a one-line wrapper that applies Real.logb 2 to the input real number.
why it matters
It is invoked by twelve downstream declarations, including maxOctantLevel and log2_succ_le in SAT.GeoFamily (which compute subdivision levels via log2(n.succ)/3) and log25_eq_5 in QuantumMolecularBound. The definition therefore supplies the logarithmic scale that lets the INFO-003 section translate Shannon's source-coding theorem into the J-cost language of the Recognition framework, linking information measures to the eight-tick octave and phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.