Binary digits of integer matrices

Finite binary expansions and their products, using Mathlib's pointwise positive and negative parts. These are algebraic identities, with no algorithm or running-time assertion.

Main definitions

• Matrix.bit: the binary digit matrix of a given weight.

Main results

• Matrix.eq_sum_two_pow_smul_bit: expansion of a nonnegative bounded matrix.
• Matrix.mul_eq_sum_two_pow_smul_bit_mul_bit: expansion of a product into digit products.
• Matrix.eq_map_posPart_sub_map_negPart: reconstruction from pointwise signed parts.
• Matrix.map_posPart_lt_and_map_negPart_lt: bounds for both pointwise signed parts.

References

Adapted from Anthropic's MatrixLanguage.lean, matBit and Footnote8.binary/product. The adaptation permits general index types and uses Mathlib's existing pointwise signed parts.

def Cslib.Matrix.bit {m : Type u_1} {n : Type u_2} (X : Matrix m n ℤ) (i : ℕ) : Matrix m n ℤ

The binary digit of weight 2^i, entry by entry. For negative entries this is the Euclidean remainder of the quotient; reconstruction below assumes nonnegative entries.

theorem Cslib.Matrix.eq_sum_two_pow_smul_bit {m : Type u_1} {n : Type u_2} (X : Matrix m n ℤ) (β : ℕ) (hX : ∀ (a : m) (j : n), 0 ≤ X a j ∧ X a j < 2 ^ β) : X = ∑ i ∈ Finset.range β, 2 ^ i • bit X i

A matrix with entries in [0, 2^β) is the weighted sum of its first β digit matrices.

theorem Cslib.Matrix.bit_eq_zero_or_one {m : Type u_1} {n : Type u_2} (X : Matrix m n ℤ) (i : ℕ) (a : m) (j : n) : bit X i a j = 0 ∨ bit X i a j = 1

Every digit matrix has entries zero or one, even for signed input.

theorem Cslib.Matrix.mul_eq_sum_two_pow_smul_bit_mul_bit {m : Type u_1} {d : Type u_2} {n : Type u_3} [Fintype d] (X : Matrix m d ℤ) (Y : Matrix d n ℤ) (β : ℕ) (hX : ∀ (a : m) (j : d), 0 ≤ X a j ∧ X a j < 2 ^ β) (hY : ∀ (j : d) (b : n), 0 ≤ Y j b ∧ Y j b < 2 ^ β) : X * Y = ∑ i ∈ Finset.range β, ∑ j ∈ Finset.range β, 2 ^ (i + j) • (bit X i * bit Y j)

Expand a product of nonnegative bounded matrices into products of binary digits.

theorem Cslib.Matrix.eq_map_posPart_sub_map_negPart {m : Type u_1} {n : Type u_2} (X : Matrix m n ℤ) : X = X.map posPart - X.map negPart

Entrywise positive and negative parts reconstruct an integer matrix. Matrix.map reuses scalar signed parts without adding an ordering instance to matrices.

theorem Cslib.Matrix.map_posPart_lt_and_map_negPart_lt {m : Type u_1} {n : Type u_2} (X : Matrix m n ℤ) {β : ℕ} (hX : ∀ (a : m) (j : n), |X a j| < 2 ^ β) : (∀ (a : m) (j : n), 0 ≤ X.map posPart a j ∧ X.map posPart a j < 2 ^ β) ∧ ∀ (a : m) (j : n), 0 ≤ X.map negPart a j ∧ X.map negPart a j < 2 ^ β

Both pointwise signed parts of an absolutely bounded matrix satisfy the same nonnegative bound. This uses the existing ordered-group operations, without introducing matrix variants.