Wanted query codes and the existing output strings

Main results

• Wanted.pack_output_list: packing the inner mask and compressed outer digits recovers the existing pruned evaluator's output numbering, including repeated zero digits.
• Wanted.pack_outStrOfPos: the computed mask and the ordinary row/column offsets give exactly the original thin-product query, without a caller-supplied output string.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.outputDigits_outer (i j : Fin 3) : ↑(PrunedQuery.outputDigits.symm (MatrixMultiplication.Schonhage.OutVar.z i j)) = 3 * ↑i + ↑j

The pruned evaluator uses row-major digits for ordinary outer outputs.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.outputDigits_inner : ↑(PrunedQuery.outputDigits.symm MatrixMultiplication.Schonhage.OutVar.z0) = 9

Its inner output is the existing private term numbered nine.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.pack_output_list (zs : List MatrixMultiplication.Schonhage.OutVar) : MatrixMultiplication.Schonhage.QueryDigits.pack zs.length (Nat.ofDigits 2 (List.map (fun (z : MatrixMultiplication.Schonhage.OutVar) => if z.IsInner then 1 else 0) zs)) (Nat.ofDigits 3 (List.map (fun (z : MatrixMultiplication.Schonhage.OutVar) => ↑z.rowIndex) (List.filter (fun (z : MatrixMultiplication.Schonhage.OutVar) => decide ¬z.IsInner) zs))) (Nat.ofDigits 3 (List.map (fun (z : MatrixMultiplication.Schonhage.OutVar) => ↑z.colIndex) (List.filter (fun (z : MatrixMultiplication.Schonhage.OutVar) => decide ¬z.IsInner) zs))) = Nat.ofDigits 10 (List.map (fun (z : MatrixMultiplication.Schonhage.OutVar) => ↑(PrunedQuery.outputDigits.symm z)) zs)

The arithmetic recurrence reconstructs every output list from its inner flags and the two outer-coordinate lists. It does not need a supplied cardinality certificate.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.pack_queryIndex {L m : ℕ} (w : MatrixMultiplication.Schonhage.OutStr L) (h : (MatrixMultiplication.Schonhage.innerSetO w).card = m) : MatrixMultiplication.Schonhage.QueryDigits.pack L ↑(MatrixMultiplication.Schonhage.MaskTable.maskCode (MatrixMultiplication.Schonhage.innerSetO w)) ↑(finFunctionFinEquiv (MatrixMultiplication.Schonhage.rowO w h)) ↑(finFunctionFinEquiv (MatrixMultiplication.Schonhage.colO w h)) = ↑(PrunedQuery.queryIndex w)

A packed mask and the ordered outer coordinates recover every original output code.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.pack_outStrOfPos {L m : ℕ} (hm : m ≤ L) (I J : ℕ) : MatrixMultiplication.Schonhage.QueryDigits.pack L (↑(MatrixMultiplication.Schonhage.MaskTable.selectedMask (MatrixMultiplication.Schonhage.blockOf (MatrixMultiplication.Schonhage.MaskTable.layout hm) I, MatrixMultiplication.Schonhage.blockOf (MatrixMultiplication.Schonhage.MaskTable.layout hm) J))) (I % MatrixMultiplication.Schonhage.N0 L m) (J % MatrixMultiplication.Schonhage.N0 L m) = ↑(PrunedQuery.queryIndex (MatrixMultiplication.Schonhage.outStrOfPos (MatrixMultiplication.Schonhage.MaskTable.layout hm) I J))

The actual deterministic table mask and the original offsets compute precisely outStrOfPos, in the unchanged pruned evaluator's least-significant-first numbering.