Existence of the high-rate code and complete source-bit placement

The monomial construction supplies the exact information dimension. Its positivity then gives an offline placement for any source table, using the quotient-plus-one number of code copies from the finite packing bound.

theorem Algebraic.MassProduction.HighRate.retainedDimension_positive (alphabet blocks : ℕ) (alphabetPositive : 0 < alphabet) (blocksPositive : 0 < blocks) : 0 < retainedDimension alphabet blocks

Retaining at least one digit block gives a nonempty information space.

theorem Algebraic.MassProduction.HighRate.existsBinaryCodeAndPlacement (blockWidth blocks dimension prefixWidth : ℕ) (blockPositive : 0 < blockWidth) (blocksPositive : 0 < blocks) (dimensionPositive : 0 < dimension) (dimensionFits : dimension ≤ 2 ^ blockWidth) : ∃ (code : LineCode (BinaryExtension (blockWidth * blocks)) (Fin dimension)), Nat.card ↑code.information = retainedDimension (2 ^ (blockWidth * dimension)) blocks ∧ Nonempty (Fin (2 ^ prefixWidth) ↪ InformationBit code (packingCopies (2 ^ prefixWidth) (retainedDimension (2 ^ (blockWidth * dimension)) blocks) (blockWidth * blocks)))

A systematic binary-extension line code and a placement of every source bit exist with exactly the prescribed information dimension and copy count.