Packing a wanted output's digits

The binary mask selects inner positions. At each remaining position, consume one digit from each compressed base-three offset and emit their row-major base-ten digit. All three numberings put the first coordinate in the least significant place.

Main definitions

• QueryDigits.pack: the arithmetic recurrence computed by the native query encoder.

Main results

• QueryDigits.pack_lt: the packed word occupies at most the original number of digits.

This recurrence and its elementary bounds are original implementation mathematics.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.QueryDigits.pack : ℕ → ℕ → ℕ → ℕ → ℕ

Pack a binary level mask and two compressed base-three offsets into output digits. Unused high bits and high offset digits are ignored after the specified depth.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.QueryDigits.pack_lt (L mask row col : ℕ) : pack L mask row col < 10 ^ L

Packing never needs a supplied bound on a partial accumulator or residual input.