Numerical query codes for native pruned evaluation

The output variables use the existing term numbering through their private terms: the nine outer outputs have digits zero through eight and the inner output has digit nine. The first coordinate is the least significant digit, exactly as for the encoded leaf arrays.

Main definitions

• PrunedQuery.queryIndex: the flat code of an output string.
• PrunedQuery.childCodes: the child request set, computed by digit tests and division.

Main results

• PrunedQuery.queryIndex_privateLeaf: agreement with the existing leaf-array indexing.
• PrunedQuery.queryIndex_cons: the numerical first-digit decomposition.

References

The child-set definition is adapted from [AlmanWilliams2026, Section 2.4.2] and Anthropic's formal source at revision 16a5ce41304fcdaea4e0be7c132e1c361dc26da5, pinned source. These are finite coding identities, not native run claims.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.outputDigits : Fin 10 ≃ MatrixMultiplication.Schonhage.OutVar

Output digits follow their private terms in the existing encoder's numbering.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.queryIndex {L : ℕ} (w : MatrixMultiplication.Schonhage.OutStr L) : Fin (10 ^ L)

The least-significant-first flat code of an output string.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.queryAt {L : ℕ} (q : Fin (10 ^ L)) : MatrixMultiplication.Schonhage.OutStr L

Decode a supplied finite query code with the existing executable digit enumeration.

@[simp]

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.queryIndex_queryAt {L : ℕ} (q : Fin (10 ^ L)) : queryIndex (queryAt q) = q

Encoding a decoded query returns the actual supplied code.

@[simp]

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.queryAt_queryIndex {L : ℕ} (w : MatrixMultiplication.Schonhage.OutStr L) : queryAt (queryIndex w) = w

Decoding a query's code returns every output coordinate unchanged.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.requested {L : ℕ} (qs : List (Fin (10 ^ L))) : Finset (MatrixMultiplication.Schonhage.OutStr L)

The requested output set is computed from the ordinary initialized list of query codes. Repeated list entries are allowed and will be reported in their original order.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.image_queryIndex_requested {L : ℕ} (qs : List (Fin (10 ^ L))) : Finset.image (fun (w : MatrixMultiplication.Schonhage.OutStr L) => ↑(queryIndex w)) (requested qs) = Finset.image Fin.val qs.toFinset

The request set's numerical image is precisely the set of supplied numerical codes.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.queryAt_mem_requested {L : ℕ} {qs : List (Fin (10 ^ L))} {q : Fin (10 ^ L)} (hq : q ∈ qs) : queryAt q ∈ requested qs

Every supplied list entry is one of the requested mathematical outputs.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.queryIndex_privateLeaf {L : ℕ} (w : MatrixMultiplication.Schonhage.OutStr L) : queryIndex w = Encoding.leafIndex (MatrixMultiplication.Schonhage.privateLeaf w)

A query's code is the leaf-array address of its private leaf.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.queryIndex_bijective (L : ℕ) : Function.Bijective queryIndex

Every flat code denotes exactly one output string.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.card_image_queryIndex {L : ℕ} (S : Finset (MatrixMultiplication.Schonhage.OutStr L)) : (Finset.image (fun (w : MatrixMultiplication.Schonhage.OutStr L) => ↑(queryIndex w)) S).card = S.card

Replacing output strings by their numerical codes preserves a request-set cardinality.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.queryIndex_cons {L : ℕ} (z : MatrixMultiplication.Schonhage.OutVar) (w : MatrixMultiplication.Schonhage.OutStr L) : ↑(queryIndex (Fin.cons z w)) = ↑(outputDigits.symm z) + 10 * ↑(queryIndex w)

The first query digit is its output-variable digit; the suffix is shifted by one place.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.queryIndex_mod {L : ℕ} (w : MatrixMultiplication.Schonhage.OutStr (L + 1)) : ↑(queryIndex w) % 10 = ↑(outputDigits.symm (w 0))

Taking the first numerical digit recovers the first output variable.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.queryIndex_div {L : ℕ} (w : MatrixMultiplication.Schonhage.OutStr (L + 1)) : ↑(queryIndex w) / 10 = ↑(queryIndex (Fin.tail w))

Integer division discards the first output coordinate.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.contributes_iff_digit (t : Fin 10) (z : MatrixMultiplication.Schonhage.OutVar) : (Encoding.termDigits t).Contributes z ↔ ↑(outputDigits.symm z) = 9 ∨ ↑(outputDigits.symm z) = ↑t

A term contributes to the inner digit or to its own outer digit.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.childCodes (S : Finset ℕ) (term : ℕ) : Finset ℕ

Numerical child requests are selected by the actual digit tests, then shortened by division. The finite-set image removes repeated suffixes. Native code will implement that deduplication.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.childCodes_bounded {n : ℕ} {S : Finset ℕ} (term : ℕ) (hS : ∀ q ∈ S, q < 10 ^ (n + 1)) (q : ℕ) : q ∈ childCodes S term → q < 10 ^ n

Child suffixes stay within the smaller numerical query space.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.mem_childCodes {L : ℕ} (S : Finset (MatrixMultiplication.Schonhage.OutStr (L + 1))) (t : Fin 10) (w : MatrixMultiplication.Schonhage.OutStr L) : ↑(queryIndex w) ∈ childCodes (Finset.image (fun (v : MatrixMultiplication.Schonhage.OutStr (L + 1)) => ↑(queryIndex v)) S) ↑t ↔ w ∈ MatrixMultiplication.Schonhage.childSet S (Encoding.termDigits t)

The numerical child requests agree exactly with the existing finite pruning definition.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.childCodes_eq_image {L : ℕ} (S : Finset (MatrixMultiplication.Schonhage.OutStr (L + 1))) (t : Fin 10) : childCodes (Finset.image (fun (w : MatrixMultiplication.Schonhage.OutStr (L + 1)) => ↑(queryIndex w)) S) ↑t = Finset.image (fun (w : MatrixMultiplication.Schonhage.OutStr L) => ↑(queryIndex w)) (MatrixMultiplication.Schonhage.childSet S (Encoding.termDigits t))

The whole native child-set specification is the numerical image of the existing child set.