Shared coordinate transforms in flat arrays

After j coordinates have been transformed, the array has 10^j * 7^k entries, where j + k = L. Its entry at (p, r) sums the input entries with suffix r, weighting their prefixes by the product of the selected coefficients. The next coordinate transform computes each new entry from seven entries of this shared array. It does not independently enumerate all input entries for every final leaf.

Main definitions

• CoordinateTransform.weight: product of coefficients along the transformed prefix.
• CoordinateTransform.value: prefix expansion at a mixed-radix array position.

Main results

• CoordinateTransform.value_step: the seven-to-ten shared coordinate update.
• CoordinateTransform.stageSize_le: every stage has at most 10^L entries.

References

An iterative implementation invariant for [AlmanWilliams2026, Section 2.4.1]. The coefficients are those of the existing encoding API, adapted from Anthropic, PBC's formal source at 16a5ce41304fcdaea4e0be7c132e1c361dc26da5. This module defines mathematical arrays and sums, not a separate machine or an instruction-counting semantics.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform.weight (c : ℕ → ℕ → ℤ) : ℕ → ℕ → ℕ → ℤ

Product of j coefficients, reading prefix digits from least significant to most significant. Values at noncanonical indices are harmless; clients use indices below the powers.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform.value (c : ℕ → ℕ → ℤ) (j k : ℕ) (a : ℕ → ℤ) (p r : ℕ) : ℤ

Value at transformed prefix p and original suffix r. The remaining suffix has k base-seven digits; the original input index is v * 7^k + r.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform.value_zero (c : ℕ → ℕ → ℤ) (k : ℕ) (a : ℕ → ℤ) (p r : ℕ) : value c 0 k a p r = a r

At the initial stage no coordinate is transformed, so the entry is the input itself.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform.value_step (c : ℕ → ℕ → ℤ) (j k : ℕ) (a : ℕ → ℤ) (p r : ℕ) {t : ℕ} (ht : t < 10) : value c (j + 1) k a (p * 10 + t) r = ∑ s ∈ Finset.range 7, c t s * value c j (k + 1) a p (s * 7 ^ k + r)

The next array entry uses seven already shared values. This is the exact algebraic invariant of the mixed-radix native loop.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform.abs_weight_le {c : ℕ → ℕ → ℤ} (hc : ∀ t < 10, ∀ s < 7, |c t s| ≤ 1) (j p v : ℕ) : |weight c j p v| ≤ 1

Each prefix product has absolute value at most one.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform.abs_value_le {c : ℕ → ℕ → ℤ} (hc : ∀ t < 10, ∀ s < 7, |c t s| ≤ 1) (j k p r : ℕ) {a : ℕ → ℤ} {A : ℤ} (ha : ∀ v < 7 ^ j, |a (v * 7 ^ k + r)| ≤ A) : |value c j k a p r| ≤ ↑(7 ^ j) * A

Intermediate transformed values are bounded from the original input values.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform.abs_value_le_of_input {c : ℕ → ℕ → ℤ} (hc : ∀ t < 10, ∀ s < 7, |c t s| ≤ 1) {L j k : ℕ} (hjk : j + k = L) (p r : ℕ) (hr : r < 7 ^ k) {a : ℕ → ℤ} {A : ℤ} (ha : ∀ i < 7 ^ L, |a i| ≤ A) : |value c j k a p r| ≤ ↑(7 ^ j) * A

Input bounds suffice for every shared intermediate value, including all depths and all prefixes. Only the original input segment is used in this estimate.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform.table (c : Fin 10 → Fin 7 → ℤ) (t s : ℕ) : ℤ

Digitwise coefficients as a total flat table. Only the first ten rows and seven columns are read by the transform.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform.weight_index (c : Fin 10 → Fin 7 → ℤ) {L : ℕ} (τ : Fin L → Fin 10) (u : Fin L → Fin 7) : weight (table c) L ↑(finFunctionFinEquiv τ) ↑(finFunctionFinEquiv u) = ∏ i : Fin L, c (τ i) (u i)

Flat prefix weights are exactly the product of the original coordinate coefficients. finFunctionFinEquiv supplies the existing Mathlib digit numbering, least significant first.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform.value_final (c : Fin 10 → Fin 7 → ℤ) (L : ℕ) (a : (Fin L → Fin 7) → ℤ) (arr : ℕ → ℤ) (harr : ∀ (u : Fin L → Fin 7), arr ↑(finFunctionFinEquiv u) = a u) (τ : Fin L → Fin 10) : value (table c) L 0 arr (↑(finFunctionFinEquiv τ)) 0 = ∑ u : Fin L → Fin 7, a u * ∏ i : Fin L, c (τ i) (u i)

At the final stage the flat transform is the tensor encoding sum on digit strings. The input array is supplied explicitly by its values at Mathlib's numbered string positions.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform.stageSize_le (j k : ℕ) : 10 ^ j * 7 ^ k ≤ 10 ^ (j + k)

The mixed-radix stage fits into a buffer of 10^(j+k) entries.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.CoordinateTransform.total_stageSize_le (L : ℕ) : ∑ j ∈ Finset.range L, 10 ^ (j + 1) * 7 ^ (L - (j + 1)) ≤ L * 10 ^ L

Even charging every one of the L stages at the maximum array size gives only L * 10^L cells. This is a combinatorial bound; native loop and arithmetic costs are separate.