coding_length
plain-language theorem explainer
This definition sets the coding length for a natural number of events equal to the J-cost of that count in real units. Researchers deriving minimum description length priors from the Recognition Science ledger would cite it to link event counts to the universal cost function. The implementation is a one-line wrapper that casts the input to reals and applies the Jcost abbreviation from the Cost module.
Claim. For a natural number $n$ of events the coding length is defined as $J(n)$, where $J$ is the cost function from the Recognition Science ledger quantity.
background
The module sets the compression prior by equating minimum description length to the ledger cost J, implementing the φ-prior as a built-in universal coding measure that ties directly to T5 J-uniqueness for encoding and decoding. J-cost is supplied by the Cost abbreviation, which stands for the quantity of type CostUnit. The upstream from theorem supplies the reduction from seven independent axioms to four structural conditions plus three definitional facts, while the as structure identifies the Laplacian action on the simplicial ledger with the continuum bridge via the weighted sum of squared differences.
proof idea
The definition is a one-line wrapper that applies the Jcost abbreviation from the Cost module after casting the natural-number input to reals.
why it matters
This definition supplies the explicit coding-length measure that realizes the φ-prior for MDL inside the information domain, directly filling the connection from T5 J-uniqueness to a universal prior. It anchors the claim that the φ-prior holds as the unique MDL derived from the J-cost. In the broader framework it supports the Recognition Composition Law and the self-similar fixed point at T6 while remaining silent on numerical evaluation or extension beyond natural-number event counts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.