Documentation

Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Meaning

Agreement of the flat tensor transform with the public encodings #

The digit numbering is supplied by Mathlib's finFunctionFinEquiv. The explicit alphabet numberings contain exactly the original seven variables and ten terms. The final mixed-radix transform is encodingL or encodingR for every depth, including zero.

Main results #

References #

The original encodings and coefficients are from [AlmanWilliams2026, Section 2.4.1], selectively adapted from Anthropic, PBC's formal source; see Encoding for the exact pin and paths.

source
def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.leafIndex {L : ℕ} (τ : MatrixMultiplication.Schonhage.Leaf L) :
Fin (10 ^ L)

The numbered output position of a term string.

Instances For
    source
    theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.value_final_left {L : ℕ} (a : MatrixMultiplication.Schonhage.LeftStr L → ℤ) (arr : ℕ → ℤ) (harr : ∀ (u : Fin L → Fin 7), arr ↑(finFunctionFinEquiv u) = a fun (i : Fin L) => leftAt (u i)) (τ : MatrixMultiplication.Schonhage.Leaf L) :
    MatrixMultiplication.Schonhage.CoordinateTransform.value (MatrixMultiplication.Schonhage.CoordinateTransform.table (coefficients false)) L 0 arr (↑(leafIndex τ)) 0 = MatrixMultiplication.Schonhage.encodingL a τ

    The flat shared left transform equals the existing encodingL on every leaf.

    source
    theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.value_final_right {L : ℕ} (a : MatrixMultiplication.Schonhage.RightStr L → ℤ) (arr : ℕ → ℤ) (harr : ∀ (u : Fin L → Fin 7), arr ↑(finFunctionFinEquiv u) = a fun (i : Fin L) => rightAt (u i)) (τ : MatrixMultiplication.Schonhage.Leaf L) :
    MatrixMultiplication.Schonhage.CoordinateTransform.value (MatrixMultiplication.Schonhage.CoordinateTransform.table (coefficients true)) L 0 arr (↑(leafIndex τ)) 0 = MatrixMultiplication.Schonhage.encodingR a τ

    The flat shared right transform equals the existing encodingR on every leaf.

    source
    theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.stageResult_value (side : Bool) (j k i : ℕ) (arr : ℕ → ℤ) :
    stageResult side (7 ^ k) (fun (i : ℕ) (a : Fin 7) => MatrixMultiplication.Schonhage.CoordinateTransform.value (MatrixMultiplication.Schonhage.CoordinateTransform.table (coefficients side)) j (k + 1) arr (i / (10 * 7 ^ k)) (↑a * 7 ^ k + i % 7 ^ k)) i = MatrixMultiplication.Schonhage.CoordinateTransform.value (MatrixMultiplication.Schonhage.CoordinateTransform.table (coefficients side)) (j + 1) k arr (i / 7 ^ k) (i % 7 ^ k)

    The native stage's row-wise specification is the next shared-prefix value. This includes the quotient/remainder decomposition of its actual flat loop counter.