pith. sign in
module module high

IndisputableMonolith.Information.Compression

show as:
view Lean formalization →

The Information.Compression module defines base-2 logarithms and establishes that data compression minimizes J-cost within the Recognition Science framework. Information theorists and RS foundation researchers would cite it when connecting Shannon entropy to practical compression bounds. The module proceeds via successive definitions of entropy measures followed by direct algebraic reductions to J-cost equalities from the Cost and ShannonEntropy imports.

claim$H = -∑ p_i log_2 p_i$ with the source coding theorem bounding achievable compression rates; compression processes are characterized as minimizers of message J-cost.

background

The module resides in the Information domain and imports Constants (τ₀ = 1 tick), Cost (J-cost primitives), and ShannonEntropy. The latter derives Shannon entropy via the core insight that H = -Σ p_i log(p_i) quantifies uncertainty from the J-cost structure. It introduces log base 2 as the natural information unit and applies it to message costs and compression types.

proof idea

This is a definition module with theorems. It defines log2 via Mathlib, proves the two and half identities, defines sourceEntropy and coin-specific entropies, then establishes the source coding theorem and compression_is_jcost_minimization by reduction to entropy identities imported from ShannonEntropy.

why it matters in Recognition Science

The module extends the Shannon entropy derivation (INFO-001) by applying it to compression limits and J-cost minimization. It supplies the information-theoretic layer that supports higher Recognition Science results on data processing, though the dependency graph lists no immediate used_by targets. It fills the step from entropy to operational compression bounds in RS-native units.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (23)