Splitting flat tensor digits into band indices

Outer digits 0,1,2 contribute to a base-three offset. Inner digits 3,4,5,6 contribute to a base-four offset and set the corresponding binary mask bit. All positions are least significant first, in the encoder's existing numbering.

Main definitions

• BandDigits.parts: the three indices computed by the native digit loop.
• BandDigits.sevenDigits: exactly L digits, retaining leading zeros.

Main results

• BandDigits.parts_bounds: component bounds derived from the original depth.
• BandDigits.parts_lists: the compressed digit-list interpretation of all three indices.

structure Cslib.Algorithms.MatrixMultiplication.Schonhage.BandDigits.Parts : Type

Binary level mask and the two compressed offsets.

• mask : ℕ

  Inner-level mask.

• outer : ℕ

  Base-three outer offset.

• inner : ℕ

  Base-four inner offset.

@[instance_reducible]

instance Cslib.Algorithms.MatrixMultiplication.Schonhage.BandDigits.instDecidableEqParts : DecidableEq Parts

def Cslib.Algorithms.MatrixMultiplication.Schonhage.BandDigits.instDecidableEqParts.decEq (x✝ x✝¹ : Parts) : Decidable (x✝ = x✝¹)

def Cslib.Algorithms.MatrixMultiplication.Schonhage.BandDigits.instReprParts.repr : Parts → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Algorithms.MatrixMultiplication.Schonhage.BandDigits.instReprParts : Repr Parts

def Cslib.Algorithms.MatrixMultiplication.Schonhage.BandDigits.parts : ℕ → ℕ → Parts

Remove one base-seven digit, recursively interpreting the remaining higher levels.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.BandDigits.parts_bounds (L a : ℕ) : (parts L a).mask < 2 ^ L ∧ (parts L a).outer < 3 ^ L ∧ (parts L a).inner < 4 ^ L

Component fits depend only on the input depth, even for an unbounded argument.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.BandDigits.sevenDigits : ℕ → ℕ → List ℕ

A fixed number of digits, so that zero digits at the end are retained.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.BandDigits.sevenDigits_eq_ofFn (L a : ℕ) : sevenDigits L a = List.ofFn fun (i : Fin L) => a / 7 ^ ↑i % 7

These are exactly the digits in Mathlib's finite-function numbering.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.BandDigits.parts_lists (L a : ℕ) : (parts L a).mask = Nat.ofDigits 2 (List.map (fun (d : ℕ) => if d < 3 then 0 else 1) (sevenDigits L a)) ∧ (parts L a).outer = Nat.ofDigits 3 (List.filter (fun (d : ℕ) => decide (d < 3)) (sevenDigits L a)) ∧ (parts L a).inner = Nat.ofDigits 4 (List.map (fun (d : ℕ) => d - 3) (List.filter (fun (d : ℕ) => decide ¬d < 3) (sevenDigits L a)))

The native indices are precisely the binary mask and the two compressed digit lists.