Meaning of the native band indices

Main results

• BandPreparation.leftAt_isInner, BandPreparation.rightAt_isInner: the original encoder numberings classify the same inner positions as the native decoder.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.leftAt_isInner (d : Fin 7) : (Encoding.leftAt d).IsInner ↔ ¬↑d < 3

Digits three through six are exactly the inner left variables.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.rightAt_isInner (d : Fin 7) : (Encoding.rightAt d).IsInner ↔ ¬↑d < 3

The same four digits classify the inner right variables.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.leftAt_outer (d : Fin 7) (h : ↑d < 3) : ↑(Encoding.leftAt d).outerIndex = ↑d

An outer left digit is its ordinary base-three value.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.rightAt_outer (d : Fin 7) (h : ↑d < 3) : ↑(Encoding.rightAt d).outerIndex = ↑d

An outer right digit is its ordinary base-three value.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.leftAt_inner (d : Fin 7) (h : ¬↑d < 3) : ↑(finProdFinEquiv (Encoding.leftAt d).innerIndex) = ↑d - 3

The four inner left digits use the existing row-major pair numbering.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.rightAt_inner (d : Fin 7) (h : ¬↑d < 3) : ↑(finProdFinEquiv (Encoding.rightAt d).innerIndex) = ↑d - 3

The four inner right digits use the same pair numbering.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.outer_digits_left {L m : ℕ} (u : Fin L → Fin 7) (h : (MatrixMultiplication.Schonhage.innerSetL fun (ℓ : Fin L) => Encoding.leftAt (u ℓ)).card = m) : List.filter (fun (d : ℕ) => decide (d < 3)) (List.ofFn fun (ℓ : Fin L) => ↑(u ℓ)) = List.ofFn fun (k : Fin (L - m)) => ↑(MatrixMultiplication.Schonhage.outerPartL (fun (ℓ : Fin L) => Encoding.leftAt (u ℓ)) h k)

Base-three compression follows the increasing outer positions used by outerPartL.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.outer_digits_right {L m : ℕ} (u : Fin L → Fin 7) (h : (MatrixMultiplication.Schonhage.innerSetR fun (ℓ : Fin L) => Encoding.rightAt (u ℓ)).card = m) : List.filter (fun (d : ℕ) => decide (d < 3)) (List.ofFn fun (ℓ : Fin L) => ↑(u ℓ)) = List.ofFn fun (k : Fin (L - m)) => ↑(MatrixMultiplication.Schonhage.outerPartR (fun (ℓ : Fin L) => Encoding.rightAt (u ℓ)) h k)

Base-three compression follows the increasing outer positions used by outerPartR.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.inner_digits_left {L m : ℕ} (u : Fin L → Fin 7) (h : (MatrixMultiplication.Schonhage.innerSetL fun (ℓ : Fin L) => Encoding.leftAt (u ℓ)).card = m) : List.map (fun (d : ℕ) => d - 3) (List.filter (fun (d : ℕ) => decide ¬d < 3) (List.ofFn fun (ℓ : Fin L) => ↑(u ℓ))) = List.ofFn fun (k : Fin m) => ↑(finProdFinEquiv (MatrixMultiplication.Schonhage.innerPartL (fun (ℓ : Fin L) => Encoding.leftAt (u ℓ)) h k))

Base-four compression follows the increasing inner positions used by innerPartL.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.inner_digits_right {L m : ℕ} (u : Fin L → Fin 7) (h : (MatrixMultiplication.Schonhage.innerSetR fun (ℓ : Fin L) => Encoding.rightAt (u ℓ)).card = m) : List.map (fun (d : ℕ) => d - 3) (List.filter (fun (d : ℕ) => decide ¬d < 3) (List.ofFn fun (ℓ : Fin L) => ↑(u ℓ))) = List.ofFn fun (k : Fin m) => ↑(finProdFinEquiv (MatrixMultiplication.Schonhage.innerPartR (fun (ℓ : Fin L) => Encoding.rightAt (u ℓ)) h k))

The right inner index uses the identical four pair digits.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.parts_mask_left {L : ℕ} (a : Fin (7 ^ L)) : (MatrixMultiplication.Schonhage.BandDigits.parts L ↑a).mask = ↑(MatrixMultiplication.Schonhage.MaskTable.maskCode (MatrixMultiplication.Schonhage.innerSetL fun (ℓ : Fin L) => Encoding.leftAt (finFunctionFinEquiv.symm a ℓ)))

Native mask compression agrees with the exact inner level set of the original array.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.parts_mask_right {L : ℕ} (a : Fin (7 ^ L)) : (MatrixMultiplication.Schonhage.BandDigits.parts L ↑a).mask = ↑(MatrixMultiplication.Schonhage.MaskTable.maskCode (MatrixMultiplication.Schonhage.innerSetR fun (ℓ : Fin L) => Encoding.rightAt (finFunctionFinEquiv.symm a ℓ)))

The right mask is classified identically, without changing the encoder numbering.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.parts_outer_left {L m : ℕ} (a : Fin (7 ^ L)) (h : (MatrixMultiplication.Schonhage.innerSetL fun (ℓ : Fin L) => Encoding.leftAt (finFunctionFinEquiv.symm a ℓ)).card = m) : (MatrixMultiplication.Schonhage.BandDigits.parts L ↑a).outer = ↑(finFunctionFinEquiv (MatrixMultiplication.Schonhage.outerPartL (fun (ℓ : Fin L) => Encoding.leftAt (finFunctionFinEquiv.symm a ℓ)) h))

Native left outer offset, with the exact public mathematical string interface.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.parts_outer_right {L m : ℕ} (a : Fin (7 ^ L)) (h : (MatrixMultiplication.Schonhage.innerSetR fun (ℓ : Fin L) => Encoding.rightAt (finFunctionFinEquiv.symm a ℓ)).card = m) : (MatrixMultiplication.Schonhage.BandDigits.parts L ↑a).outer = ↑(finFunctionFinEquiv (MatrixMultiplication.Schonhage.outerPartR (fun (ℓ : Fin L) => Encoding.rightAt (finFunctionFinEquiv.symm a ℓ)) h))

Native right outer offset in the same least-significant-first convention.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.parts_inner_left {L m : ℕ} (a : Fin (7 ^ L)) (h : (MatrixMultiplication.Schonhage.innerSetL fun (ℓ : Fin L) => Encoding.leftAt (finFunctionFinEquiv.symm a ℓ)).card = m) : (MatrixMultiplication.Schonhage.BandDigits.parts L ↑a).inner = ↑(finFunctionFinEquiv fun (k : Fin m) => finProdFinEquiv (MatrixMultiplication.Schonhage.innerPartL (fun (ℓ : Fin L) => Encoding.leftAt (finFunctionFinEquiv.symm a ℓ)) h k))

Native left thin-dimension offset agrees with the row-major pair digits of Layout.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.parts_inner_right {L m : ℕ} (a : Fin (7 ^ L)) (h : (MatrixMultiplication.Schonhage.innerSetR fun (ℓ : Fin L) => Encoding.rightAt (finFunctionFinEquiv.symm a ℓ)).card = m) : (MatrixMultiplication.Schonhage.BandDigits.parts L ↑a).inner = ↑(finFunctionFinEquiv fun (k : Fin m) => finProdFinEquiv (MatrixMultiplication.Schonhage.innerPartR (fun (ℓ : Fin L) => Encoding.rightAt (finFunctionFinEquiv.symm a ℓ)) h k))

Native right thin-dimension offset uses the same Layout equivalence.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.bandValue (L m N β : ℕ) (rightSide : Bool) (matrix : ℕ → ℕ → ℤ) (a : ℕ) : ℤ

Numeric specification of one guarded band-array read. matrix r k denotes an original matrix cell (or the transposed indexing of the right matrix); the native implementation computes its actual row-major address and loads it.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.bandValue_left {L m N : ℕ} (hm : m ≤ L) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (matrix : ℕ → ℕ → ℤ) (hX : ∀ (i : Fin N) (k : Fin (MatrixMultiplication.Schonhage.D m)), matrix ↑i ↑k = X i k) (β : ℕ) (a : Fin (7 ^ L)) : bandValue L m N β false matrix ↑a = MatrixMultiplication.Schonhage.bandArrayL (MatrixMultiplication.Schonhage.MaskTable.layout hm) X β fun (ℓ : Fin L) => Encoding.leftAt (finFunctionFinEquiv.symm a ℓ)

The numeric left-band specification is the unchanged mathematical bandArrayL for the computed deterministic layout, including all unselected strings and padding.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.bandValue_right {L m N : ℕ} (hm : m ≤ L) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (matrix : ℕ → ℕ → ℤ) (hY : ∀ (i : Fin N) (k : Fin (MatrixMultiplication.Schonhage.D m)), matrix ↑i ↑k = Y k i) (β : ℕ) (a : Fin (7 ^ L)) : bandValue L m N β true matrix ↑a = MatrixMultiplication.Schonhage.bandArrayR (MatrixMultiplication.Schonhage.MaskTable.layout hm) Y β fun (ℓ : Fin L) => Encoding.rightAt (finFunctionFinEquiv.symm a ℓ)

The numeric right-band specification is the unchanged mathematical bandArrayR. Its natural row parameter refers to a column of the original right matrix.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.selected_parts_bounds {L m : ℕ} (a : Fin (7 ^ L)) (hz : MatrixMultiplication.Schonhage.MaskTable.lookup L m (MatrixMultiplication.Schonhage.BandDigits.parts L ↑a).mask ≠ 0) : (MatrixMultiplication.Schonhage.BandDigits.parts L ↑a).outer < MatrixMultiplication.Schonhage.N0 L m ∧ (MatrixMultiplication.Schonhage.BandDigits.parts L ↑a).inner < MatrixMultiplication.Schonhage.D m

A selected native mask ensures that its compressed offsets fit the actual matrix dimensions, rather than merely the coarser depth-based bounds.