Actual initialized-input clients for the shared encoders

Main results

• Encoding.exec_input: flat signed array, concrete depth header and actual State.init.
• Encoding.exec_left, Encoding.exec_right: all public tensor encodings, at every depth.

The two programs and their thirty-two registers are independent of depth and word width. Inputs are signed words encoded with WordRAM.Signed.encode; the depth and the machine's length header are ordinary unsigned words. All input and reachable data words fit the target width. Output and scratch are disjoint concrete blocks immediately after the input.

References

The encodings are from [AlmanWilliams2026, Section 2.4.1]; see Encoding for provenance.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.exec_input {w L : ℕ} (hw : 0 < w) (side : Bool) (a : Fin (7 ^ L) → ℤ) (A : ℤ) (hA : 0 ≤ A) (ha : ∀ (i : Fin (7 ^ L)), |a i| ≤ A) (hmag : ↑(7 ^ L) * A < 2 ^ (w - 1)) (haddr : WordRAM.Fits (w + 2) (addressBound L)) : WordRAM.InputFits (w + 2) (input L a) ∧ ∃ (y : WordRAM.Data 32), WordRAM.ExecWithin (w + 2) (program side) (WordRAM.State.init (input L a)).data y (timeBound L) ∧ WordRAM.Data.Bounded (w + 2) y ∧ (∀ p < 10 ^ L, y.mem (outputBase L + p) = WordRAM.Signed.encode (MatrixMultiplication.Schonhage.CoordinateTransform.value (MatrixMultiplication.Schonhage.CoordinateTransform.table (coefficients side)) L 0 (fun (i : ℕ) => (List.ofFn a).getD i 0) p 0)) ∧ (∀ (b : ℕ), ¬(outputBase L ≤ b ∧ b < scratchBase L + 10 ^ L) → y.mem b = (WordRAM.State.init (input L a)).data.mem b) ∧ y.regs output = outputBase L ∧ y.regs capacity = 10 ^ L

The complete native encoder starts from the ordinary State.init convention with a real depth header and encoded input words. It returns all flat shared-transform values, keeps the input and every outside cell, and leaves only target-sized words in memory and registers.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.exec_left {w L : ℕ} (hw : 0 < w) (a : MatrixMultiplication.Schonhage.LeftStr L → ℤ) (A : ℤ) (hA : 0 ≤ A) (ha : ∀ (u : MatrixMultiplication.Schonhage.LeftStr L), |a u| ≤ A) (hmag : ↑(7 ^ L) * A < 2 ^ (w - 1)) (haddr : WordRAM.Fits (w + 2) (addressBound L)) : WordRAM.InputFits (w + 2) (inputL a) ∧ ∃ (y : WordRAM.Data 32), WordRAM.ExecWithin (w + 2) (program false) (WordRAM.State.init (inputL a)).data y (timeBound L) ∧ WordRAM.Data.Bounded (w + 2) y ∧ (∀ (τ : MatrixMultiplication.Schonhage.Leaf L), y.mem (outputBase L + ↑(leafIndex τ)) = WordRAM.Signed.encode (MatrixMultiplication.Schonhage.encodingL a τ)) ∧ (∀ (b : ℕ), ¬(outputBase L ≤ b ∧ b < scratchBase L + 10 ^ L) → y.mem b = (WordRAM.State.init (inputL a)).data.mem b) ∧ y.regs output = outputBase L ∧ y.regs capacity = 10 ^ L

Complete left encoder on arbitrary signed arrays indexed by the original seven-symbol strings. Every one of the 10^L leaves receives the unchanged public encodingL value.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.exec_right {w L : ℕ} (hw : 0 < w) (a : MatrixMultiplication.Schonhage.RightStr L → ℤ) (A : ℤ) (hA : 0 ≤ A) (ha : ∀ (u : MatrixMultiplication.Schonhage.RightStr L), |a u| ≤ A) (hmag : ↑(7 ^ L) * A < 2 ^ (w - 1)) (haddr : WordRAM.Fits (w + 2) (addressBound L)) : WordRAM.InputFits (w + 2) (inputR a) ∧ ∃ (y : WordRAM.Data 32), WordRAM.ExecWithin (w + 2) (program true) (WordRAM.State.init (inputR a)).data y (timeBound L) ∧ WordRAM.Data.Bounded (w + 2) y ∧ (∀ (τ : MatrixMultiplication.Schonhage.Leaf L), y.mem (outputBase L + ↑(leafIndex τ)) = WordRAM.Signed.encode (MatrixMultiplication.Schonhage.encodingR a τ)) ∧ (∀ (b : ℕ), ¬(outputBase L ≤ b ∧ b < scratchBase L + 10 ^ L) → y.mem b = (WordRAM.State.init (inputR a)).data.mem b) ∧ y.regs output = outputBase L ∧ y.regs capacity = 10 ^ L

Complete right encoder on arbitrary signed arrays with the original encodingR API.