Deterministic mask tables for matrix bands

Size-m level sets are ordered by their binary masks. The first K0² masks are assigned in row-major order to block pairs. This specifies a deterministic instance of the existing Layout; a native scan can compute the table without receiving indexing data as an input.

Main definitions

• MaskTable.maskSet, MaskTable.maskCode: explicit binary masks and level sets.
• MaskTable.population: the truncated binary population count computed by division loops.
• MaskTable.validMasks: the masks with the required cardinality.

Main results

• MaskTable.card_validMasks: exactly L.choose m valid masks exist.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.maskSet {L : ℕ} (a : Fin (2 ^ L)) : Finset (Fin L)

The set of levels whose binary digit is one.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.maskCode {L : ℕ} (Q : Finset (Fin L)) : Fin (2 ^ L)

The integer mask of a finite level set, with level zero least significant.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.maskSet_maskCode {L : ℕ} (Q : Finset (Fin L)) : maskSet (maskCode Q) = Q

Decoding the explicitly numbered mask recovers the original set.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.maskCode_maskSet {L : ℕ} (a : Fin (2 ^ L)) : maskCode (maskSet a) = a

Encoding a decoded bounded mask recovers the original integer.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.maskEquiv (L : ℕ) : Fin (2 ^ L) ≃ Finset (Fin L)

Binary-mask numbering is an explicit bijection, not a chosen enumeration.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.population (L a : ℕ) : ℕ

Number of one digits among exactly the first L binary digits.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.population_zero (a : ℕ) : population 0 a = 0

A zero-depth scan has population zero.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.population_succ (L a : ℕ) : population (L + 1) a = a % 2 + population L (a / 2)

One native remainder/division step removes the lowest digit.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.population_le (L a : ℕ) : population L a ≤ L

There are at most L one digits, even for an unbounded natural argument.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.population_eq_card {L : ℕ} (a : Fin (2 ^ L)) : population L ↑a = (maskSet a).card

The loop's digit sum is the cardinality of the represented level set.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.validMasks (L m : ℕ) : Finset (Fin (2 ^ L))

All valid masks, in the ordinary linear order on bounded naturals.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.card_validMasks (L m : ℕ) : (validMasks L m).card = K L m

Every size-m subset occurs once in the bounded mask scan.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.prefixCount (L m t : ℕ) : ℕ

Number of valid masks strictly below the scan counter.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.prefixCount_zero (L m : ℕ) : prefixCount L m 0 = 0

The scan begins without any accepted mask.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.prefixCount_le (L m t : ℕ) : prefixCount L m t ≤ t

A scan accepts at most one mask in each iteration.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.prefixCount_succ (L m t : ℕ) : prefixCount L m (t + 1) = prefixCount L m t + if population L t = m then 1 else 0

The actual scalar counter update for one mask.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.prefixCount_mono (L m : ℕ) {a b : ℕ} (h : a ≤ b) : prefixCount L m a ≤ prefixCount L m b

Extending a scan cannot decrease the accepted-mask counter.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.prefixCount_lt {L m a b : ℕ} (ha : population L a = m) (hab : a < b) : prefixCount L m a < prefixCount L m b

Earlier valid masks have strictly smaller accepted-mask ranks.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.prefixCount_full (L m : ℕ) : prefixCount L m (2 ^ L) = K L m

The finite complete scan has exactly the binomial count.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.prefixCount_eq_bounded (L m t : ℕ) (ht : t ≤ 2 ^ L) : prefixCount L m t = {a ∈ validMasks L m | ↑a < t}.card

The scalar scan count equals the rank among the bounded valid masks.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.pairRank {L m : ℕ} (gh : Fin (K0 L m) × Fin (K0 L m)) : Fin (K L m)

Row-major block-pair rank in the full list of size-m masks.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.selectedMask {L m : ℕ} (gh : Fin (K0 L m) × Fin (K0 L m)) : Fin (2 ^ L)

The selected mask at a block pair is the corresponding mask in increasing order.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.prefixCount_selectedMask {L m : ℕ} (gh : Fin (K0 L m) × Fin (K0 L m)) : prefixCount L m ↑(selectedMask gh) = ↑(pairRank gh)

The computed prefix counter at a selected mask is its row-major block-pair rank.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.lookup (L m a : ℕ) : ℕ

The dense inverse-table word: zero for an unselected mask, otherwise rank plus one.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.lookup_ne_zero_iff (L m a : ℕ) : lookup L m a ≠ 0 ↔ a < 2 ^ L ∧ population L a = m ∧ prefixCount L m a < K0 L m * K0 L m

Exactly the selected valid masks have nonzero inverse-table words.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.lookup_le (L m a : ℕ) : lookup L m a ≤ a + 1

Every inverse-table word is bounded by its original mask plus one.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.lookup_selectedMask {L m : ℕ} (gh : Fin (K0 L m) × Fin (K0 L m)) : lookup L m ↑(selectedMask gh) = ↑(pairRank gh) + 1

The inverse-table word at every selected block pair has the promised rank.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.exists_selectedMask_of_lookup {L m a : ℕ} (h : lookup L m a ≠ 0) : ∃ (gh : Fin (K0 L m) × Fin (K0 L m)), ↑(selectedMask gh) = a

A nonzero inverse-table word belongs to one of the selected block pairs.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.lookup_blockPair {L m : ℕ} (gh : Fin (K0 L m) × Fin (K0 L m)) : (lookup L m ↑(selectedMask gh) - 1) / K0 L m = ↑gh.1 ∧ (lookup L m ↑(selectedMask gh) - 1) % K0 L m = ↑gh.2

Inverse-table division and remainder recover exactly the two block indices.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.lookup_block_lt {L m a : ℕ} (h : lookup L m a ≠ 0) (rightSide : Bool) : (if rightSide = true then (lookup L m a - 1) % K0 L m else (lookup L m a - 1) / K0 L m) < K0 L m

Both decoded block indices are in range whenever the inverse-table word is nonzero.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.card_selectedMask {L m : ℕ} (gh : Fin (K0 L m) × Fin (K0 L m)) : (maskSet (selectedMask gh)).card = m

Selected masks always have exactly the required cardinality.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.selectedMask_injective (L m : ℕ) : Function.Injective fun (gh : Fin (K0 L m) × Fin (K0 L m)) => maskSet (selectedMask gh)

Distinct block pairs receive distinct level sets.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.innerDigits : Fin 4 ≃ Fin 2 × Fin 2

The thin-dimension pair digit uses row-major order, as do the encoder's inner variables.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.MaskTable.layout {L m : ℕ} (hmL : m ≤ L) : Layout L m

Explicit base-three outer strings and base-four strings of index pairs, with the first K0² binary masks in increasing order as the shared block table.