prior_holds
plain-language theorem explainer
The φ-prior equates minimum description length to the ledger cost J for any recognition model. Researchers deriving universal coding measures from Recognition Science cite this when linking MDL directly to the T5 J-function. The proof is a one-line wrapper that introduces the model and simplifies the prior definition.
Claim. For every model $m$, the minimum description length prior function equals the J-cost: $MDL(m) = J$.
background
The Compression Prior module implements the φ-prior for minimum description length as the universal ledger cost J, tying directly to T5 J-uniqueness for encoding and decoding events. J-cost is the function $J(x) = (x + x^{-1})/2 - 1$ that supplies the built-in coding measure in RS-native units. The upstream model construction assembles a CPM Model from a hypothesis bundle containing defect mass, ortho mass, and energy gap data. Cost is the Quantity type over CostUnit that carries these ledger values.
proof idea
The proof introduces an arbitrary model and applies simplification on the mdl_prior definition, which expands directly to the J-cost constant.
why it matters
This theorem confirms the φ-prior holds as the unique MDL derived from T5 J-uniqueness, anchoring the information domain within the Recognition framework. It supplies the compression prior that feeds universal coding lengths for recognition events and aligns with the eight-tick octave structure. No downstream uses are recorded yet, leaving open its integration into explicit hypothesis compression calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.