`englishEntropyRate`

definition

show as: view math explainer →

module: IndisputableMonolith.Information.Compression
domain: Information
line: 214 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Information.Compression on GitHub at line 214.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

formal source

 211    - Single letter entropy: ~4.2 bits/letter
 212    - Entropy rate: ~1.0-1.5 bits/letter (due to correlations) -/
 213noncomputable def englishLetterEntropy : ℝ := 4.2  -- bits
 214noncomputable def englishEntropyRate : ℝ := 1.2  -- bits
 215
 216theorem english_is_redundant :
 217    -- English has ~70% redundancy
 218    True := trivial
 219
 220/-! ## Summary -/
 221
 222/-- RS perspective on compression:
 223
 224    1. **Shannon limit**: Can't compress below entropy
 225    2. **J-cost minimization**: Compression reduces J-cost
 226    3. **Entropy = minimum J-cost**: For faithful representation
 227    4. **Redundancy = excess J-cost**: Can be removed
 228    5. **Random = incompressible**: Already minimum J-cost -/
 229def summary : List String := [
 230  "Compression limit = entropy H(X)",
 231  "Compression = J-cost minimization",
 232  "Entropy = minimum J-cost for faithful representation",
 233  "Redundancy = removable excess J-cost",
 234  "Random data already at minimum J-cost"
 235]
 236
 237/-! ## Falsification Criteria -/
 238
 239/-- The derivation would be falsified if:
 240    1. Compression below entropy achieved
 241    2. J-cost doesn't decrease with compression
 242    3. Random data can be systematically compressed -/
 243structure CompressionFalsifier where
 244  below_entropy : Prop

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.