Native shared tensor encoding

The two fixed programs use unsigned addresses and counters, and sign-and-magnitude encoded integer entries. Address 1 holds the depth; the 7^L encoded entries begin at address 2. The ordinary State.init length header is at address 0. Output and scratch are consecutive blocks of 10^L cells immediately after the input. Each coordinate transform reads the previous stage and writes the other buffer. No initialization of unread scratch is needed. A final charged copy puts the result in the first buffer, also at depth zero.

The coordinate transform is a new iterative implementation of the linear forms in [AlmanWilliams2026, Section 2.4.1]. The coefficients and mathematical encoding are selectively adapted from Anthropic's formal-math revision 16a5ce41304fcdaea4e0be7c132e1c361dc26da5, Step and Recursion. The source's recursive machine and execution semantics are not used.

Main definitions

• Encoding.program: fixed native code for either coefficient table.
• Encoding.input: concrete input for State.init, including the depth header.
• Encoding.outputBase, Encoding.scratchBase: disjoint output and scratch blocks.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.leftAt (s : Fin 7) : MatrixMultiplication.Schonhage.LeftVar

Seven variable digits: the three outer variables, then the four inner variables.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.rightAt (s : Fin 7) : MatrixMultiplication.Schonhage.RightVar

Right-variable digits use the same order as the left-variable digits.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.termAt (t : Fin 10) : MatrixMultiplication.Schonhage.Term

Row-major order on the nine P terms, followed by P0.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.leftDigits : Fin 7 ≃ MatrixMultiplication.Schonhage.LeftVar

Executable flat address digits for the seven left variables. LeftVar.equiv instead exposes their mathematical sum carrier Fin 3 ⊕ (Fin 2 × Fin 2). This dictionary gives a single Fin 7 digit for each variable, for the native array layout.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.rightDigits : Fin 7 ≃ MatrixMultiplication.Schonhage.RightVar

Executable flat address digits for the seven right variables. RightVar.equiv instead exposes their mathematical sum carrier Fin 3 ⊕ (Fin 2 × Fin 2). This dictionary gives a single Fin 7 digit for each variable, in the same order as leftDigits.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.termDigits : Fin 10 ≃ MatrixMultiplication.Schonhage.Term

Executable flat address digits for all ten terms. Term.equiv instead exposes their mathematical carrier Option (Fin 3 × Fin 3). The native dictionary uses Fin 10, with row-major P i j at digit 3*i+j and P0 at digit 9.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.coefficients (rightSide : Bool) (t : Fin 10) (s : Fin 7) : ℤ

The left and right coefficient tables, with digits made explicit.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.coefficients_values (side : Bool) (t : Fin 10) (s : Fin 7) : coefficients side t s = 0 ∨ coefficients side t s = 1 ∨ coefficients side t s = -1

Every actual coefficient is zero, one or minus one.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.outputBase (L : ℕ) : ℕ

The input block ends where the output block begins.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.scratchBase (L : ℕ) : ℕ

The scratch block immediately follows the entire output block.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.input (L : ℕ) (a : Fin (7 ^ L) → ℤ) : List ℕ

Concrete input: depth header followed by the signed input entries in flat order. The caller encodes each integer with Signed.encode before passing the list to State.init. The native unsigned length header is installed by State.init itself.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.inputL {L : ℕ} (a : MatrixMultiplication.Schonhage.LeftStr L → ℤ) : List ℕ

The concrete left-array input, using Mathlib's base-seven string numbering.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.inputR {L : ℕ} (a : MatrixMultiplication.Schonhage.RightStr L → ℤ) : List ℕ

The concrete right-array input, in exactly the same flat memory layout.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.depth : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.inputSize : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.capacity : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.src : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.dst : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.output : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.scratch : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.stride : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.prefixes : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.stage : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.cell : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.block : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.term : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.suffix : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.address : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.accumulator : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.one : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.seven : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.ten : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.group : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.temporary : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.stageSize : Fin 32

All thirty-two registers are fixed independently of depth and width. Registers 0–8 are precisely the existing signed-arithmetic workspace.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.summand (s : Fin 7) (c : ℤ) : WordRAM.Code WordRAM.Basis.standard 32

One coefficient in {0, 1, -1} times one array entry. Zero coefficients cause no load. Nonzero coefficients use the proved native signed addition or subtraction block.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.sumCode : List (Fin 7 × ℤ) → WordRAM.Code WordRAM.Basis.standard 32

A finite unrolling of the seven coefficients. This recursion constructs code; it does not recurse on the input depth.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.form (side : Bool) (t : Fin 10) : WordRAM.Code WordRAM.Basis.standard 32

One linear form, including accumulator initialization.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.dispatch (side : Bool) : List (Fin 10) → WordRAM.Code WordRAM.Basis.standard 32

A fixed finite dispatch on the ten possible term digits.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.cellSetup : WordRAM.Code WordRAM.Basis.standard 32

Decode one flat output index into its mixed-radix coordinates and source group.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.cellFinish : WordRAM.Code WordRAM.Basis.standard 32

Store the computed entry and advance the flat index.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.cellBody (side : Bool) : WordRAM.Code WordRAM.Basis.standard 32

One output cell. The flat index is (prefix * 10 + term) * stride + suffix; its seven source addresses are (prefix * 7 + s) * stride + suffix.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.stageHead : WordRAM.Code WordRAM.Basis.standard 32

Divide the suffix stride and compute the next stage size.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.stageTail : WordRAM.Code WordRAM.Basis.standard 32

Alternate the two buffers and advance the prefix and stage counters.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.stageBody (side : Bool) : WordRAM.Code WordRAM.Basis.standard 32

Transform the next coordinate, then alternate the output buffers.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.setupHead : WordRAM.Code WordRAM.Basis.standard 32

Load the actual depth header and initialize the power counters.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.powerBody : WordRAM.Code WordRAM.Basis.standard 32

One multiplication by each radix and one counter increment.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.setupTail : WordRAM.Code WordRAM.Basis.standard 32

Compute the concrete buffer addresses from the powers and initialize the first stage.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.setup : WordRAM.Code WordRAM.Basis.standard 32

Read the depth and compute both powers in a charged native loop.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.copyRegisters : Fin 7 → Fin 32

Reuse the existing seven-register array copy inside the encoder's register file.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.copyRegisters_injective : Function.Injective copyRegisters

The seven copy registers are distinct.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.copyOut : WordRAM.Code WordRAM.Basis.standard 32

A charged copy into the fixed output block, permitting disjoint blocks in either order or identical source and destination.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.program (side : Bool) : WordRAM.Code WordRAM.Basis.standard 32

The complete fixed native encoder, excluding its final halt. The returned output register identifies the first output cell; the capacity register holds its length.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.program_readsWidth (side : Bool) : ¬(program side).ReadsWidth

The code performs no word-width queries.