Binary words for power-of-two residue matrices

A rectangular matrix over ZMod (2 ^ w) is represented row by row, with w low-order-first bits per entry. The dimensions are external parameters. Decoding arbitrary words pads missing bits with false and ignores excess bits, including when a dimension or the width is zero.

Main definitions

• Cslib.Matrix.toBinary, Cslib.Matrix.ofBinary: fixed-width row-major encoding and total decoding.
• Cslib.Matrix.binaryEntry: the number read from the entry bits at an arbitrary row and column of a word, with missing bits false.
• Cslib.Matrix.encBinary: the injective encoding of matrices with fixed dimensions and width.

Main results

• Cslib.Matrix.ofBinary_toBinary: decoding a matrix's word recovers the matrix.
• Cslib.Matrix.length_toBinary: the exact complete output length is rows * cols * w.

def Cslib.Matrix.toBinary {rows cols w : ℕ} (A : Matrix (Fin rows) (Fin cols) (ZMod (2 ^ w))) : List Bool

Fixed-width row-major encoding; the digits of each residue are least significant first.

def Cslib.Matrix.ofBinary (rows cols w : ℕ) (word : List Bool) : Matrix (Fin rows) (Fin cols) (ZMod (2 ^ w))

Read the declared matrix dimensions, padding missing bits with false and ignoring excess bits. Zero-width entries are the unique residue modulo one.

def Cslib.Matrix.binaryEntry (cols w : ℕ) (word : List Bool) (i j : ℕ) : ℕ

Read one low-order-first residue word at an arbitrary row and column. Missing bits are false; the declared column count determines the stride.

theorem Cslib.Matrix.ofBinary_apply (rows cols w : ℕ) (word : List Bool) (i : Fin rows) (j : Fin cols) : ofBinary rows cols w word i j = ↑(binaryEntry cols w word ↑i ↑j)

List slicing and the finite matrix decoder use the same coordinates.

@[simp]

theorem Cslib.Matrix.length_toBinary {rows cols w : ℕ} (A : Matrix (Fin rows) (Fin cols) (ZMod (2 ^ w))) : (toBinary A).length = rows * cols * w

Encoding writes every entry's declared width, including leading zero digits.

theorem Cslib.Matrix.toBinary_eq {rows cols w : ℕ} (A : Matrix (Fin rows) (Fin cols) (ZMod (2 ^ w))) : toBinary A = (List.ofFn fun (i : Fin rows) => (List.ofFn fun (j : Fin cols) => List.ofFn fun (k : Fin w) => (A i j).val.testBit ↑k).flatten).flatten

The row-major representation is the concatenation of each row's low-order-first words.

@[simp]

theorem Cslib.Matrix.ofBinary_toBinary {rows cols w : ℕ} (A : Matrix (Fin rows) (Fin cols) (ZMod (2 ^ w))) : ofBinary rows cols w (toBinary A) = A

Canonical fixed-width words decode exactly, including empty dimensions and width zero.

def Cslib.Matrix.encBinary (rows cols w : ℕ) : Matrix (Fin rows) (Fin cols) (ZMod (2 ^ w)) ↪ List Bool

Fixed-dimensional matrices inject into their complete binary words. This fixed-type embedding alone makes no claim of uniform computational efficiency in the dimensions.