Information Compression Prior Mdl Prior

The compression prior

Minimum description length (MDL) is a principle from information theory: among competing explanations for a set of observations, prefer the one that compresses the data to the shortest message. The idea, developed by Jorma Rissanen in the 1970s and 1980s, treats learning as a form of data compression. A model that captures real regularities lets you describe the data briefly; a model that merely memorizes noise requires a long description. MDL gives a concrete way to balance model complexity against goodness of fit.

The classical MDL framework measures description length in bits, using a code length function. For a model class and data, the total description length is the cost of encoding the model plus the cost of encoding the data given the model. The best model minimizes that sum. This is a definitional choice, not a theorem: different coding schemes yield different MDL criteria, and the principle itself does not single out one universal cost function.

In Recognition Science, the framework's library defines mdl_prior as the recognition cost J, the unique cost function forced by five plain conditions (reciprocal symmetry, zero cost at unity, a composition law, calibration, continuity). The library proves, as a machine-checked theorem, that this prior equals J for every model. In plain terms: within the framework, the shortest description length is not chosen from a menu of coding schemes; it is the same function that governs recognition events generally. The framework models MDL as a special case of its universal ledger cost.

The library also defines coding_length for a number of events as J applied to that count. This gives a concrete formula: for n events, the coding length is (n + 1/n)/2 - 1. The theorem prior_holds states that mdl_prior equals J for all models, which the library proves by unfolding the definition.

What the declaration does not claim is important. It does not prove that MDL is correct in any empirical sense; it defines a specific prior and shows it coincides with J. It does not claim that Rissanen's original MDL principle uniquely determines this cost; that uniqueness is a separate theorem about J under its five conditions. The declaration also does not claim that this prior outperforms other coding schemes on real data; that would be an empirical question the library does not address.

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]

noncomputable def coding_length (events : ℕ) : ℝ := Cost.Jcost (events : ℝ)

What this page does not claim

The declaration does not prove MDL is the correct learning principle in general. It does not claim Rissanen's MDL uniquely determines this cost without the five conditions. It does not claim empirical superiority over other coding schemes on real data.

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: