mdl_prior
plain-language theorem explainer
mdl_prior supplies the minimum description length prior by identifying it with the J-cost ledger function for models satisfying the symmetric unit axioms. Information theorists working on compression bounds in Recognition Science cite this when connecting MDL to the T5 uniqueness property. The definition is a direct one-line alias to Cost.Jcost that uses the model parameter only for type-level enforcement of symmetry.
Claim. For any model satisfying the symmetric unit property (i.e., $F(x)=F(x^{-1})$ for $x>0$ and $F(1)=0$), the MDL prior is defined by $mdl_prior(model) := J$, where $J$ is the J-cost function.
background
The SymmUnit class requires a function F to obey symmetry $F(x)=F(x^{-1})$ for positive x together with normalization $F(1)=0$. This module implements the φ-prior for minimum description length as the universal ledger cost J, directly tying to T5 unique cost for encoding and decoding events. Upstream, Cost is the abbrev for Quantity in the CostUnit, while the for structure records meta-realization properties needed for self-reference coherence.
proof idea
The definition is a direct alias that sets mdl_prior equal to Cost.Jcost. The model parameter is discarded after type-checking the SymmUnit hypothesis; no reduction or tactic steps are required beyond the equality.
why it matters
This definition supplies the concrete MDL prior invoked by the downstream prior_holds theorem, which states that the φ-prior holds as the unique MDL from T5 J-uniqueness. It anchors compression in the Recognition Science framework at the T5 step of the forcing chain, where J is the unique cost satisfying the symmetry and unit conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.