log2
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove any identities or inequalities for log2.
- Does not restrict the domain to positive reals.
- Does not relate log2 to J-cost or defectDist.
- Does not address numerical evaluation or approximation.
formal statement (Lean)
39noncomputable def log2 (x : ℝ) : ℝ := Real.logb 2 x
proof body
Definition body.
40
41/-- log₂(2) = 1 -/