Information Compression Prior

The compression prior

Information compression is the task of describing data with fewer bits than the raw stream would take. The central question is how to price a description: what does it cost to encode an event or a model? In the 1960s, Jorma Rissanen and others developed minimum description length (MDL), the principle that the best model is the one that minimizes the combined cost of describing the model and the data given the model. The framework of Recognition Science takes this principle further: it does not merely recommend a compression measure, it derives a unique one from five plain conditions on any cost function.

Those conditions are reciprocal symmetry, zero cost at unity, a forced composition law, calibration, and continuity. The framework proves that any cost function satisfying all five must equal J(x) = (x + 1/x)/2 - 1. This is a proved theorem in a machine-checked library of formal theorems, with no hidden assumptions beyond the standard three axioms of the underlying type theory. The result is called the unique cost, and it is the same function that appears throughout the framework as the cost of recognition, the price of encoding, and the measure of description length.

In Recognition Science, the compression prior is the claim that this unique cost J is the correct MDL measure. The module defines mdl_prior as exactly this function, and coding_length as J applied to the number of events. The theorem prior_holds states that for any model, the prior equals the unique cost. In plain language: the framework identifies the best compression measure with the forced cost function, so that encoding and decoding are priced by the same law that governs recognition itself.

The practical consequence is that the framework does not leave compression as a modeling choice. If you accept the five conditions, the cost of a description is fixed. The golden ratio appears as the natural scale: J(x) is minimized at x = 1, and the self-similar scaling that emerges from the framework is the golden ratio φ. This ties compression to the same structural constants that appear elsewhere in the framework, such as the reduced Planck constant ħ = φ⁻⁵ and the gravitational constant G = φ⁵/π.

What this establishes is a bridge between information theory and the framework's core cost function. The MDL principle, which in conventional statistics is a heuristic with many possible coding schemes, becomes here a single derived law. The module does not claim that all compression problems reduce to J, only that the prior for MDL is uniquely determined once the five conditions are accepted.

/-- Theorem: φ-prior holds as unique MDL from T5 J-unique. -/
theorem prior_holds : ∀ model, mdl_prior model = Cost.Jcost := by
  intro model
  simp [mdl_prior]

noncomputable def mdl_prior (_model : Cost.SymmUnit (fun x => x)) : ℝ → ℝ := Cost.Jcost

-- Universal coding: length = J( complexity ) for recognition events

/-- Theorem: φ-prior holds as unique MDL from T5 J-unique. -/
theorem prior_holds : ∀ model, mdl_prior model = Cost.Jcost := by
  intro model
  simp [mdl_prior]

/-- Theorem: φ-prior holds as unique MDL from T5 J-unique. -/
theorem prior_holds : ∀ model, mdl_prior model = Cost.Jcost := by
  intro model
  simp [mdl_prior]

What this page does not claim

The framework does not claim that all compression problems reduce to J. The module does not prove that MDL is the only valid principle of model selection. The five conditions are accepted as premises, not derived from more basic principles.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/CompressionPrior.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: