Values and flat addresses of the native recursion

Main definitions

• PrunedQuery.partialValue: the requested accumulator after a prefix of the ten terms.

Main results

• PrunedQuery.slice_strided: flat strided leaf arrays agree with the existing sliceAt.
• PrunedQuery.abs_partialValue_le: every intermediate accumulator has an explicit bound.

These are identities and magnitude bounds for the controller invariant. They do not assume that a machine executes the recursion.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.leafIndex_cons {n : ℕ} (lam : MatrixMultiplication.Schonhage.Term) (v : MatrixMultiplication.Schonhage.Leaf n) : ↑(Encoding.leafIndex (Fin.cons lam v)) = ↑(Encoding.termDigits.symm lam) + 10 * ↑(Encoding.leafIndex v)

The existing leaf indexing has the same least-significant-first decomposition as queries.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.slice_strided {n : ℕ} (a : ℕ → ℤ) (p s : ℕ) (lam : MatrixMultiplication.Schonhage.Term) : MatrixMultiplication.Schonhage.sliceAt (fun (v : MatrixMultiplication.Schonhage.Leaf (n + 1)) => a (p + s * ↑(Encoding.leafIndex v))) lam = fun (v : MatrixMultiplication.Schonhage.Leaf n) => a (p + ↑(Encoding.termDigits.symm lam) * s + s * 10 * ↑(Encoding.leafIndex v))

The native prefix/stride update selects exactly the existing mathematical child slice.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.leafAddress_lt {n p s size : ℕ} (hp : p < s) (hs : s * 10 ^ n = size) (v : MatrixMultiplication.Schonhage.Leaf n) : p + s * ↑(Encoding.leafIndex v) < size

A frame's prefix and stride put every remaining leaf inside the original encoding array.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.partialValue {n : ℕ} (a b : MatrixMultiplication.Schonhage.Leaf (n + 1) → ℤ) (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) (w : MatrixMultiplication.Schonhage.OutStr (n + 1)) (k : ℕ) : ℤ

The mathematical value of a requested native accumulator after terms numbered below k. Unrequested directory cells are deliberately unspecified by the native interface.

@[simp]

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.partialValue_zero {n : ℕ} (a b : MatrixMultiplication.Schonhage.Leaf (n + 1) → ℤ) (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) (w : MatrixMultiplication.Schonhage.OutStr (n + 1)) : partialValue a b S w 0 = 0

Before the first child, the native accumulator is zero.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.partialValue_succ {n : ℕ} (a b : MatrixMultiplication.Schonhage.Leaf (n + 1) → ℤ) (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) (w : MatrixMultiplication.Schonhage.OutStr (n + 1)) (k : Fin 10) : partialValue a b S w (↑k + 1) = partialValue a b S w ↑k + if (Encoding.termDigits k).Contributes (w 0) then MatrixMultiplication.Schonhage.Pruned.childResult a b S (Encoding.termDigits k) (Fin.tail w) else 0

Processing the next term adds exactly its contributing child, or leaves the value unchanged.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.partialValue_ten {n : ℕ} (a b : MatrixMultiplication.Schonhage.Leaf (n + 1) → ℤ) (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) (w : MatrixMultiplication.Schonhage.OutStr (n + 1)) (hw : w ∈ S) : partialValue a b S w 10 = MatrixMultiplication.Schonhage.Pruned.result (n + 1) a b S w

After all ten terms, a requested accumulator is the existing pruned result.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.abs_childResult_le {n : ℕ} (a b : MatrixMultiplication.Schonhage.Leaf (n + 1) → ℤ) (A B : ℤ) (hA : ∀ (v : MatrixMultiplication.Schonhage.Leaf (n + 1)), |a v| ≤ A) (hB : ∀ (v : MatrixMultiplication.Schonhage.Leaf (n + 1)), |b v| ≤ B) (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) (lam : MatrixMultiplication.Schonhage.Term) (w : MatrixMultiplication.Schonhage.OutStr n) : |MatrixMultiplication.Schonhage.Pruned.childResult a b S lam w| ≤ 10 ^ n * (A * B)

Every child's mathematical result has the bound for its remaining depth, including a skipped empty child whose value is zero.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.abs_partialValue_le {n : ℕ} (a b : MatrixMultiplication.Schonhage.Leaf (n + 1) → ℤ) (A B : ℤ) (hA : ∀ (v : MatrixMultiplication.Schonhage.Leaf (n + 1)), |a v| ≤ A) (hB : ∀ (v : MatrixMultiplication.Schonhage.Leaf (n + 1)), |b v| ≤ B) (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) (w : MatrixMultiplication.Schonhage.OutStr (n + 1)) (k : ℕ) : |partialValue a b S w k| ≤ 10 ^ (n + 1) * (A * B)

The bound covers all partial sums, not only the final recursively specified output.