The canonical code of a finite model: the Encodable code of its sorted element list. Sorted lists are used rather than Finset itself because the decoder that reads a model back has to be primitive recursive, and List ℕ is Primcodable while Finset ℕ is not. @audit:ok

The description length of a finite model: the prefix complexity of its canonical code. Using prefix complexity rather than the literal length of modelCode keeps the quantity insensitive to the redundancy of the canonical code. @audit:ok

The length of the two-part description built from the model S: the model part plus the index part. The coefficient 4 on the index part is built into the definition rather than recovered by the argument (see the implementation notes); the coefficient on the model part is exactly 1. @audit:ok

The shortest two-part description length of x, minimized over all finite models containing x. The singleton model always competes, so the infimum is attained (mdlComplexity_spec). @audit:ok

The structure function of x: the least index part ⌈log₂ |S|⌉ over models S ∋ x whose description length is within the budget k. The value is ℕ∞ because the constraint set is empty for small budgets, where the value has to be ⊤ rather than 0 (structureFunction_zero); over ℕ the empty infimum would collapse to 0 and contradict structureFunction_antitone. @audit:ok

A model S is a sufficient statistic for x at slack c when it contains x and its two-part description is no longer than prefixComplexity x + c. The slack is an explicit argument so that minimality statements can quantify over it. @audit:ok

One step of the little-endian bit expansion: peel off the lowest bit of the remaining value and append it to the accumulated bit string.

The payload decoder presented as a code together with its input: the literal mode uses the identity code, and the interpret mode the code named by the unary index. The empty payload has no dispatch, which is how decodePayload diverges on it.

The index part packed into N: the self-delimited prefix of the bit string of N.

The payload part packed into N: what follows the self-delimited index, with the terminating sentinel bit removed.

The bit string packing an index i together with a payload d: the index in self-delimited form, then the payload, then a sentinel bit making the string a canonical binary expansion.

The unpacking machine: read the index and the payload out of N, run the payload through the machine's own payload decoder, and feed the result together with the index to A.

Feeding a partial recursive A a value y and an index i costs, in payload complexity, no more than the payload complexity of y plus the self-delimited index, up to a constant depending only on A. The hypothesis Partrec₂ A is what puts A on the machine at all: it is discharged into a Code and never supplies the bound. @audit:ok

The two-part decoder: read y as a list of naturals and return its i-th entry.

Every two-part description of x bounds its prefix complexity, up to an additive constant independent of x and of the model. The index part carries the machine-specific coefficient 4 built into twoPartLength, so this is not the textbook inequality K(x) ≤ K(S) + log |S| + O(1); the model part does carry coefficient 1. @audit:ok

The shortest two-part description length agrees with the prefix complexity up to an additive constant. As with prefixComplexity_le_twoPartLength, the index part of twoPartLength carries the machine-specific coefficient 4, so this is a statement about that quantity and not the textbook minimum description length principle. @audit:ok