Packing many high-rate code copies without rounding loss

Take one plus the quotient of the desired source-bit count by the message capacity of one code. This fits all source bits and loses at most one whole codeword to rounding. The integer rate inequality transfers directly to the total physical storage. The actual placement can be chosen offline and used as a single batched prefix lookup table.

def Algebraic.MassProduction.HighRate.packingCopies (sourceBits messageSymbols symbolBits : ℕ) : ℕ

A sufficient number of code copies, including one final partial copy.

Equations

• Algebraic.MassProduction.HighRate.packingCopies sourceBits messageSymbols symbolBits = sourceBits / (messageSymbols * symbolBits) + 1

theorem Algebraic.MassProduction.HighRate.packingCopies_capacity (sourceBits messageSymbols symbolBits : ℕ) (messagePositive : 0 < messageSymbols) (symbolPositive : 0 < symbolBits) : sourceBits ≤ packingCopies sourceBits messageSymbols symbolBits * messageSymbols * symbolBits

All source bits fit in the chosen copies' information positions.

theorem Algebraic.MassProduction.HighRate.packingCopies_storage (sourceBits messageSymbols codeSymbols symbolBits precision : ℕ) (rate : precision * codeSymbols ≤ (precision + 1) * messageSymbols) : precision * (packingCopies sourceBits messageSymbols symbolBits * codeSymbols * symbolBits) ≤ (precision + 1) * sourceBits + precision * (codeSymbols * symbolBits)

The storage expansion is the code-rate expansion plus at most one codeword's worth of rounding.

theorem Algebraic.MassProduction.HighRate.existsPackingPlacement {Information : Type u_1} [Fintype Information] (sourceBits symbolBits : ℕ) (informationPositive : 0 < Fintype.card Information) (symbolPositive : 0 < symbolBits) : Nonempty (Fin sourceBits ↪ Fin (packingCopies sourceBits (Fintype.card Information) symbolBits) × Information × Fin symbolBits)

An offline injection assigns every source bit to a distinct code, information symbol, and binary coordinate.