A partial recursive type-class decoder for the entropy-rate upper bound #

The method-of-types upper half of kolmogorov_entropy_rate encodes a length-n block by the pair ⟨type descriptor, index in its type class⟩. To turn this into a condComplexity bound through invariance, the corresponding decoder — the map that recovers a block from such a pair — must be a single partial recursive function, uniform in the block length n (a per-n code would make the additive constant of invariance_code diverge with n).

This file builds that decoder over a finite alphabet α and certifies it as Partrec₂. The decoder A(m, n) splits m by division and remainder against K = (n + 1) ^ card α: the type descriptor is the remainder m % K (the base-(n + 1) numeral of the occurrence signature, whose letter counts each lie in [0, n]), and the index is the quotient m / K. It enumerates every length-n word (a value-level List α, not the length-indexed Fin n → α), keeps those whose signature re-encodes to m % K, and returns the m / K-th such word as its base-card α numeral. This div/mod packing is length-additive (natLen m ≈ natLen index + card α · log (n + 1)), unlike Nat.pair, and the base-card α output matches the block encoder used by the upper bound.

Main definitions #

• typeDecoder — the decoder as a function ℕ → ℕ → Part ℕ.
• enumWords / typeSig — the length-n word enumerator and the occurrence signature.

Main statements #

• typeDecoder_partrec — typeDecoder is Partrec₂.

Primitive-recursive certification of the pieces #