module module high

`IndisputableMonolith.Information.Compression`

The Information.Compression module links data compression to J-cost minimization in Recognition Science. It defines the base-2 logarithm and establishes the source coding theorem that bounds achievable rates by Shannon entropy. Supporting definitions distinguish message J-cost, lossless compression, and lossy compression. Information theorists working inside the RS framework would cite these results for entropy-derived compression limits.

claimDefines the base-2 logarithm $log_2 x$ and states the source coding theorem: for a discrete source with Shannon entropy $H = -∑ p_i log_2 p_i$, the minimal average code length per symbol satisfies $L ≥ H$, with equality in the asymptotic limit for lossless schemes.

background

The module belongs to the Information domain and imports the RS time quantum τ₀ = 1 tick from Constants together with J-cost primitives from the Cost module. It extends the Shannon entropy construction (INFO-001) that derives H = -∑ p_i log p_i directly from J-cost structure. Core objects include sourceEntropy for an arbitrary probability distribution, fairCoinEntropy for the uniform binary case, and biasedCoinEntropy for nonuniform bits.

proof idea

This is a definition module containing supporting lemmas. Logarithmic identities (log2_two, log2_half) are established first from Mathlib properties. The source_coding_theorem is obtained by applying the entropy definition to average code lengths. The key equivalence compression_is_jcost_minimization follows by expressing code length as a J-cost sum, after which messageJCost, losslessCompression, and lossyCompression are introduced as definitions.

why it matters in Recognition Science

The module supplies the compression layer that converts Shannon entropy into concrete rate bounds inside Recognition Science. It aligns with J-uniqueness (T5) by casting compression as J-cost minimization and prepares the ground for efficiency measures that later connect to the phi-ladder. No downstream theorems are yet listed, so the module functions as a foundational block for the broader information framework.

scope and limits

Does not treat noisy channels or error-correcting codes.
Does not supply explicit compression algorithms.
Does not address continuous sources or differential entropy.
Does not relate compression rates to the phi-ladder or spatial dimension D=3.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Information.ShannonEntropy module_import

declarations in this module (23)

def log2 L39
lemma log2_two L42
lemma log2_half L45
theorem source_coding_theorem L60
def sourceEntropy L65
def fairCoinEntropy L76
theorem fair_coin_one_bit L79
def biasedCoinEntropy L93
theorem compression_is_jcost_minimization L105
def messageJCost L117
def losslessCompression L128
def lossyCompression L137
def rateDistortionTheory L148
def kolmogorovComplexity L162
theorem most_strings_incompressible L174
def huffmanCoding L184
def arithmeticCoding L191
def lempelZiv L199
def englishLetterEntropy L213
def englishEntropyRate L214
theorem english_is_redundant L216
def summary L229
structure CompressionFalsifier L243